Fixed: when assume_consistent, Solver::Assign() must not test [].
The semantics within G modalities is that the set of literals in the grounded clause plus the transitive closure of literals occurring in clauses in UP^-(s) is consistent. In the extreme case where UP^-(s) contains [], this means only the literals in the clause are checked. This particular extreme case is somewhat counterintuitive because the trivial answer is 'no', but it simplifies the definition.
Loading
Please register or sign in to comment