mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

simplify Boolean resolve

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-22 05:37:46 -07:00
parent ad267ce294
commit 2d78bc9282
3 changed files with 15 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/math/polysat/conflict.cpp
View file

@ -163,34 +163,26 @@ namespace polysat {
s().m_stats.m_num_bailouts++; s().m_stats.m_num_bailouts++;
} }
void conflict::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) { void conflict::resolve(constraint_manager const& m, sat::literal lit, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
// clause: x \/ u \/ v // clause: x \/ u \/ v
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v // resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
SASSERT(var != sat::null_bool_var); SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); })); SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
bool core_has_pos = contains_literal(sat::literal(var)); SASSERT(contains_literal(lit));
bool core_has_neg = contains_literal(~sat::literal(var)); SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
DEBUG_CODE({ SASSERT(!contains_literal(~lit));
bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0; SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0;
SASSERT(!core_has_pos || !core_has_neg); // otherwise core is tautology
SASSERT(!clause_has_pos || !clause_has_neg); // otherwise clause is tautology
SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
});
sat::literal var_lit(var); remove_literal(lit);
if (core_has_pos)
remove_literal(var_lit);
if (core_has_neg)
remove_literal(~var_lit);
unset_mark(m.lookup(var_lit)); unset_mark(m.lookup(lit));
for (sat::literal lit : cl) for (sat::literal lit2 : cl)
if (lit.var() != var) if (lit2 != lit)
insert(m.lookup(~lit)); insert(m.lookup(~lit2));
} }
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */ /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */

2
src/math/polysat/conflict.h
View file

@ -96,7 +96,7 @@ namespace polysat {
/** Perform boolean resolution with the clause upon variable 'var'. /** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals. * Precondition: core/clause contain complementary 'var'-literals.
*/ */
void resolve(constraint_manager const& m, sat::bool_var var, clause const& cl); void resolve(constraint_manager const& m, sat::literal lit, clause const& cl);
/** Perform value resolution by applying various inference rules. /** Perform value resolution by applying various inference rules.
* Returns true if it was possible to eliminate the variable 'v'. * Returns true if it was possible to eliminate the variable 'v'.

2
src/math/polysat/solver.cpp
View file

@ -486,7 +486,7 @@ namespace polysat {
// NOTE: boolean resolution should work normally even in bailout mode. // NOTE: boolean resolution should work normally even in bailout mode.
clause other = *m_bvars.reason(var); clause other = *m_bvars.reason(var);
LOG_H3("resolve_bool: " << lit << " " << other); LOG_H3("resolve_bool: " << lit << " " << other);
m_conflict.resolve(m_constraints, var, other); m_conflict.resolve(m_constraints, lit, other);
} }
void solver::report_unsat() { void solver::report_unsat() {