mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

add value-propagate flag to patch regression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-23 12:09:49 +01:00
parent 93410ccd81
commit cd11b70864
4 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -162,7 +162,7 @@ namespace polysat {
c_lemma.push(c.blit()); c_lemma.push(c.blit());
clause_ref lemma = c_lemma.build(); clause_ref lemma = c_lemma.build();
SASSERT(lemma); SASSERT(lemma);
cm().store(lemma.get(), s); cm().store(lemma.get(), s, false);
if (c.bvalue(s) == l_undef) if (c.bvalue(s) == l_undef)
s.assign_propagate(c.blit(), *lemma); s.assign_propagate(c.blit(), *lemma);
} }

13
src/math/polysat/constraint.cpp
View file

@ -57,11 +57,16 @@ namespace polysat {
m_constraints.push_back(c); m_constraints.push_back(c);
} }
void constraint_manager::store(clause* cl, solver& s) {
void constraint_manager::register_clause(clause* cl, solver& s) {
while (m_clauses.size() <= s.base_level()) while (m_clauses.size() <= s.base_level())
m_clauses.push_back({}); m_clauses.push_back({});
m_clauses[s.base_level()].push_back(cl); m_clauses[s.base_level()].push_back(cl);
watch(*cl, s); }
void constraint_manager::store(clause* cl, solver& s, bool value_propagate) {
register_clause(cl, s);
watch(*cl, s, value_propagate);
} }
// Release constraints at the given level and above. // Release constraints at the given level and above.
@ -79,7 +84,7 @@ namespace polysat {
// if clause is unsat then assign arbitrary // if clause is unsat then assign arbitrary
// solver handles unsat clauses by creating a conflict. // solver handles unsat clauses by creating a conflict.
// solver also can propagate, but need to check that it does indeed. // solver also can propagate, but need to check that it does indeed.
void constraint_manager::watch(clause& cl, solver& s) { void constraint_manager::watch(clause& cl, solver& s, bool value_propagate) {
if (cl.empty()) if (cl.empty())
return; return;
@ -88,7 +93,7 @@ namespace polysat {
if (m_bvars.is_false(cl[i])) if (m_bvars.is_false(cl[i]))
continue; continue;
signed_constraint sc = s.lit2cnstr(cl[i]); signed_constraint sc = s.lit2cnstr(cl[i]);
if (sc.is_currently_false(s)) { if (value_propagate && sc.is_currently_false(s)) {
if (m_bvars.is_true(cl[i])) { if (m_bvars.is_true(cl[i])) {
s.set_conflict(sc); s.set_conflict(sc);
return; return;

6
src/math/polysat/constraint.h
View file

@ -67,9 +67,11 @@ namespace polysat {
void gc_constraints(solver& s); void gc_constraints(solver& s);
void gc_clauses(solver& s); void gc_clauses(solver& s);
void watch(clause& cl, solver& s); void watch(clause& cl, solver& s, bool value_propagate);
void unwatch(clause& cl); void unwatch(clause& cl);
void register_clause(clause* cl, solver& s);
public: public:
constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
~constraint_manager(); ~constraint_manager();
@ -78,7 +80,7 @@ namespace polysat {
void erase_bvar(constraint* c); void erase_bvar(constraint* c);
// sat::literal get_or_assign_blit(signed_constraint& c); // sat::literal get_or_assign_blit(signed_constraint& c);
void store(clause* cl, solver& s); void store(clause* cl, solver& s, bool value_propagate);
/// Release clauses at the given level and above. /// Release clauses at the given level and above.
void release_level(unsigned lvl); void release_level(unsigned lvl);

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

@ -838,7 +838,7 @@ namespace polysat {
// SASSERT(m_bvars.value(lit) != l_true); // SASSERT(m_bvars.value(lit) != l_true);
} }
SASSERT(!clause.empty()); SASSERT(!clause.empty());
m_constraints.store(&clause, *this); m_constraints.store(&clause, *this, true);
} }
void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) { void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) {