mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Change old solver::propagate method

Browse source
This commit is contained in:
Jakob Rath 2022-10-04 17:09:09 +02:00
parent a0fe568561
commit dc9373dcbd
3 changed files with 66 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,7 +25,7 @@ Author:
namespace polysat { namespace polysat {
solver::solver(reslimit& lim): solver::solver(reslimit& lim):
m_lim(lim), m_lim(lim),
m_viable(*this), m_viable(*this),
m_viable_fallback(*this), m_viable_fallback(*this),
@ -54,13 +54,13 @@ namespace polysat {
} }
bool solver::should_search() { bool solver::should_search() {
return return
m_lim.inc() && m_lim.inc() &&
(m_stats.m_num_conflicts < get_config().m_max_conflicts) && (m_stats.m_num_conflicts < get_config().m_max_conflicts) &&
(m_stats.m_num_decisions < get_config().m_max_decisions); (m_stats.m_num_decisions < get_config().m_max_decisions);
} }
lbool solver::check_sat() { lbool solver::check_sat() {
LOG("Starting"); LOG("Starting");
while (should_search()) { while (should_search()) {
m_stats.m_num_iterations++; m_stats.m_num_iterations++;
@ -99,7 +99,7 @@ namespace polysat {
dd::pdd_manager& solver::var2pdd(pvar v) { dd::pdd_manager& solver::var2pdd(pvar v) {
return sz2pdd(size(v)); return sz2pdd(size(v));
} }
unsigned solver::add_var(unsigned sz) { unsigned solver::add_var(unsigned sz) {
pvar v = m_value.size(); pvar v = m_value.size();
m_value.push_back(rational::zero()); m_value.push_back(rational::zero());
@ -240,7 +240,7 @@ namespace polysat {
m_linear_solver.new_constraint(*c.get()); m_linear_solver.new_constraint(*c.get());
#endif #endif
} }
bool solver::can_propagate() { bool solver::can_propagate() {
return m_qhead < m_search.size() && !is_conflict(); return m_qhead < m_search.size() && !is_conflict();
@ -453,22 +453,6 @@ namespace polysat {
} }
} }
// TODO: get rid of this or at least rename it
void solver::propagate(pvar v, rational const& val, signed_constraint c) {
// this looks weird... mixing propagation and conflict with c? also, the conflict should not be c but the whole of viable+c.
LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
if (m_viable.is_viable(v, val)) {
m_free_pvars.del_var_eh(v);
assign_core(v, val, justification::propagation(m_level));
}
else {
UNREACHABLE();
// set_conflict(c);
}
}
void solver::push_level() { void solver::push_level() {
++m_level; ++m_level;
m_trail.push_back(trail_instr_t::inc_level_i); m_trail.push_back(trail_instr_t::inc_level_i);
@ -477,8 +461,6 @@ namespace polysat {
#endif #endif
} }
void solver::pop_levels(unsigned num_levels) { void solver::pop_levels(unsigned num_levels) {
if (num_levels == 0) if (num_levels == 0)
return; return;
@ -550,8 +532,8 @@ namespace polysat {
if (active_level <= target_level) if (active_level <= target_level)
replay.push_back(lit); replay.push_back(lit);
else else
m_bvars.unassign(lit); m_bvars.unassign(lit);
m_search.pop(); m_search.pop();
break; break;
} }
@ -650,13 +632,33 @@ namespace polysat {
return; return;
case dd::find_t::singleton: case dd::find_t::singleton:
// NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search
// NOTE 2: probably not true anymore; viable::intersect should trigger all propagations now
DEBUG_CODE( UNREACHABLE(); );
j = justification::propagation(m_level); j = justification::propagation(m_level);
break; break;
case dd::find_t::multiple: case dd::find_t::multiple:
j = justification::decision(m_level + 1); j = justification::decision(m_level + 1);
break; break;
} }
// Verify the value we're trying to assign assign_verify(v, val, j);
}
void solver::assign_propagate(pvar v, rational const& val) {
LOG("Propagation: " << assignment_pp(*this, v, val));
SASSERT(!is_assigned(v));
SASSERT(m_viable.is_viable(v, val));
m_free_pvars.del_var_eh(v);
// NOTE: we do not have to check the univariate solver here.
// Since we propagate, this means at most the single value 'val' is viable.
// If it is not actually viable, the propagation loop will find out and enter the conflict state.
// (However, if we do check here, we might find the conflict earlier. Might be worth a try.)
assign_core(v, val, justification::propagation(m_level));
}
/// Verify the value we're trying to assign against the univariate solver
void solver::assign_verify(pvar v, rational val, justification j) {
SASSERT(j.is_decision() || j.is_propagation());
// First, check evaluation of the currently-univariate constraints
// TODO: we should add a better way to test constraints under assignments, without modifying the solver state. // TODO: we should add a better way to test constraints under assignments, without modifying the solver state.
m_value[v] = val; m_value[v] = val;
m_search.push_assignment(v, val); m_search.push_assignment(v, val);
@ -672,8 +674,7 @@ namespace polysat {
case dd::find_t::singleton: case dd::find_t::singleton:
case dd::find_t::multiple: case dd::find_t::multiple:
LOG("Fallback solver: " << assignment_pp(*this, v, val)); LOG("Fallback solver: " << assignment_pp(*this, v, val));
// NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives. SASSERT(!j.is_propagation()); // all excluded values are true negatives, so if j.is_propagation() the univariate solver must return unsat
SASSERT(!j.is_propagation());
j = justification::decision(m_level + 1); j = justification::decision(m_level + 1);
break; break;
case dd::find_t::empty: case dd::find_t::empty:
@ -686,12 +687,12 @@ namespace polysat {
if (j.is_decision()) if (j.is_decision())
push_level(); push_level();
assign_core(v, val, j); assign_core(v, val, j);
} }
void solver::assign_core(pvar v, rational const& val, justification const& j) { void solver::assign_core(pvar v, rational const& val, justification const& j) {
if (j.is_decision()) if (j.is_decision())
++m_stats.m_num_decisions; ++m_stats.m_num_decisions;
else else
++m_stats.m_num_propagations; ++m_stats.m_num_propagations;
LOG(assignment_pp(*this, v, val) << " by " << j); LOG(assignment_pp(*this, v, val) << " by " << j);
SASSERT(m_viable.is_viable(v, val)); SASSERT(m_viable.is_viable(v, val));
@ -702,7 +703,7 @@ namespace polysat {
m_value[v] = val; m_value[v] = val;
m_search.push_assignment(v, val); m_search.push_assignment(v, val);
m_trail.push_back(trail_instr_t::assign_i); m_trail.push_back(trail_instr_t::assign_i);
m_justification[v] = j; m_justification[v] = j;
// Decision should satisfy all univariate constraints. // Decision should satisfy all univariate constraints.
// Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated. // Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated.
// TODO: on the other hand, checking constraints here would have us discover some conflicts earlier. // TODO: on the other hand, checking constraints here would have us discover some conflicts earlier.
@ -820,10 +821,10 @@ namespace polysat {
/** /**
* Variable activity accounting. * Variable activity accounting.
* As a placeholder we increment activity * As a placeholder we increment activity
* 1. when a variable assignment is used in a conflict. * 1. when a variable assignment is used in a conflict.
* 2. when a variable propagation is resolved against. * 2. when a variable propagation is resolved against.
* The hypothesis that this is useful should be tested against a * The hypothesis that this is useful should be tested against a
* broader suite of benchmarks and tested with micro-benchmarks. * broader suite of benchmarks and tested with micro-benchmarks.
* It should be tested in conjunction with restarts. * It should be tested in conjunction with restarts.
*/ */
@ -846,7 +847,7 @@ namespace polysat {
} }
m_activity_inc >>= 14; m_activity_inc >>= 14;
} }
void solver::report_unsat() { void solver::report_unsat() {
backjump(base_level()); backjump(base_level());
SASSERT(!m_conflict.empty()); SASSERT(!m_conflict.empty());
@ -889,13 +890,13 @@ namespace polysat {
/** /**
* Revert a decision that caused a conflict. * Revert a decision that caused a conflict.
* Variable v was assigned by a decision at position i in the search stack. * Variable v was assigned by a decision at position i in the search stack.
* *
* C & v = val is conflict. * C & v = val is conflict.
* *
* C => v != val * C => v != val
* *
* l1 \/ l2 \/ ... \/ lk \/ v != val * l1 \/ l2 \/ ... \/ lk \/ v != val
* *
*/ */
void solver::revert_decision(pvar v) { void solver::revert_decision(pvar v) {
rational val = m_value[v]; rational val = m_value[v];
@ -990,7 +991,7 @@ namespace polysat {
m_search.push_boolean(lit); m_search.push_boolean(lit);
} }
/** /**
* Activate constraint immediately * Activate constraint immediately
* Activation and de-activation of constraints follows the scope controlled by push/pop. * Activation and de-activation of constraints follows the scope controlled by push/pop.
* constraints activated within the linear solver are de-activated when the linear * constraints activated within the linear solver are de-activated when the linear
@ -1067,7 +1068,7 @@ namespace polysat {
void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) { void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
signed_constraint cs[2] = { c1, c2 }; signed_constraint cs[2] = { c1, c2 };
add_clause(2, cs, is_redundant); add_clause(2, cs, is_redundant);
} }
void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) { void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) {
@ -1099,7 +1100,7 @@ namespace polysat {
bool solver::at_base_level() const { bool solver::at_base_level() const {
return m_level == base_level(); return m_level == base_level();
} }
unsigned solver::base_level() const { unsigned solver::base_level() const {
return m_base_levels.empty() ? 0 : m_base_levels.back(); return m_base_levels.empty() ? 0 : m_base_levels.back();
} }
@ -1118,7 +1119,7 @@ namespace polysat {
pvar v = item.var(); pvar v = item.var();
auto const& j = m_justification[v]; auto const& j = m_justification[v];
out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level() << " "; out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level() << " ";
if (j.is_propagation()) if (j.is_propagation())
for (auto const& c : m_viable.get_constraints(v)) for (auto const& c : m_viable.get_constraints(v))
out << c << " "; out << c << " ";
out << "\n"; out << "\n";
@ -1138,8 +1139,8 @@ namespace polysat {
for (auto const& cls : m_constraints.clauses()) { for (auto const& cls : m_constraints.clauses()) {
for (auto const& cl : cls) { for (auto const& cl : cls) {
out << "\t" << *cl << "\n"; out << "\t" << *cl << "\n";
for (auto lit : *cl) for (auto lit : *cl)
out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n"; out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n";
} }
} }
return out; return out;
@ -1190,7 +1191,7 @@ namespace polysat {
rational const& p = rational::power_of_two(s.size(var)); rational const& p = rational::power_of_two(s.size(var));
if (val > mod(-val, p)) if (val > mod(-val, p))
out << -mod(-val, p); out << -mod(-val, p);
else else
out << val; out << val;
return out; return out;
} }
@ -1281,8 +1282,8 @@ namespace polysat {
return true; return true;
bool ok = true; bool ok = true;
for (sat::bool_var v = m_bvars.size(); v-- > 0; ) { for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
sat::literal lit(v); sat::literal lit(v);
auto c = lit2cnstr(lit); auto c = lit2cnstr(lit);
if (!all_of(c->vars(), [this](auto w) { return is_assigned(w); })) if (!all_of(c->vars(), [this](auto w) { return is_assigned(w); }))
continue; continue;
ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this); ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this);

25
src/math/polysat/solver.h
View file

@ -84,9 +84,9 @@ namespace polysat {
friend class assignment_pp; friend class assignment_pp;
friend class assignments_pp; friend class assignments_pp;
friend class ex_polynomial_superposition; friend class ex_polynomial_superposition;
friend class inf_saturate; friend class inf_saturate;
friend class constraint_manager; friend class constraint_manager;
friend class scoped_solverv; friend class scoped_solverv;
friend class test_polysat; friend class test_polysat;
friend class test_fi; friend class test_fi;
friend struct inf_resolve_with_assignment; friend struct inf_resolve_with_assignment;
@ -119,7 +119,7 @@ namespace polysat {
bool m_propagating = false; // set to true during propagation bool m_propagating = false; // set to true during propagation
#endif #endif
unsigned_vector m_activity; unsigned_vector m_activity;
vector<pdd> m_vars; vector<pdd> m_vars;
unsigned_vector m_size; // store size of variables (bit width) unsigned_vector m_size; // store size of variables (bit width)
@ -137,9 +137,9 @@ namespace polysat {
ptr_vector<clause> m_lemmas; ///< the non-asserting lemmas ptr_vector<clause> m_lemmas; ///< the non-asserting lemmas
unsigned m_lemmas_qhead = 0; unsigned m_lemmas_qhead = 0;
unsigned_vector m_base_levels; // External clients can push/pop scope. unsigned_vector m_base_levels; // External clients can push/pop scope.
void push_qhead() { void push_qhead() {
m_trail.push_back(trail_instr_t::qhead_i); m_trail.push_back(trail_instr_t::qhead_i);
m_qhead_trail.push_back(m_qhead); m_qhead_trail.push_back(m_qhead);
} }
@ -172,6 +172,8 @@ namespace polysat {
void deactivate_constraint(signed_constraint c); void deactivate_constraint(signed_constraint c);
unsigned level(sat::literal lit, clause const& cl); unsigned level(sat::literal lit, clause const& cl);
void assign_propagate(pvar v, rational const& val);
void assign_verify(pvar v, rational val, justification j);
void assign_core(pvar v, rational const& val, justification const& j); void assign_core(pvar v, rational const& val, justification const& j);
bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); } bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
bool is_decision(pvar v) const { return m_justification[v].is_decision(); } bool is_decision(pvar v) const { return m_justification[v].is_decision(); }
@ -181,7 +183,6 @@ namespace polysat {
void propagate(sat::literal lit); void propagate(sat::literal lit);
void propagate(pvar v); void propagate(pvar v);
bool propagate(pvar v, constraint* c); bool propagate(pvar v, constraint* c);
void propagate(pvar v, rational const& val, signed_constraint c);
bool propagate(sat::literal lit, clause& cl); bool propagate(sat::literal lit, clause& cl);
void add_pwatch(constraint* c); void add_pwatch(constraint* c);
void add_pwatch(constraint* c, pvar v); void add_pwatch(constraint* c, pvar v);
@ -237,7 +238,7 @@ namespace polysat {
bool wlist_invariant(); bool wlist_invariant();
bool assignment_invariant(); bool assignment_invariant();
bool verify_sat(); bool verify_sat();
bool can_propagate(); bool can_propagate();
void propagate(); void propagate();
@ -279,7 +280,7 @@ namespace polysat {
bool try_eval(pdd const& p, rational& out_value) const; bool try_eval(pdd const& p, rational& out_value) const;
/** /**
* Add variable with bit-size. * Add variable with bit-size.
*/ */
pvar add_var(unsigned sz); pvar add_var(unsigned sz);
@ -290,9 +291,9 @@ namespace polysat {
/** /**
* Create terms for unsigned quot-rem * Create terms for unsigned quot-rem
* *
* Return tuple (quot, rem) * Return tuple (quot, rem)
* *
* The following properties are enforced: * The following properties are enforced:
* b*quot + rem = a * b*quot + rem = a
* ~ovfl(b*quot) * ~ovfl(b*quot)
@ -343,7 +344,7 @@ namespace polysat {
/** /**
* Apply current substitution to p. * Apply current substitution to p.
*/ */
pdd subst(pdd const& p) const; pdd subst(pdd const& p) const;
/** Create constraints */ /** Create constraints */
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); } signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
@ -423,7 +424,7 @@ namespace polysat {
*/ */
void push(); void push();
void pop(unsigned num_scopes = 1); void pop(unsigned num_scopes = 1);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
void collect_statistics(statistics& st) const; void collect_statistics(statistics& st) const;

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

@ -130,7 +130,7 @@ namespace polysat {
rational val; rational val;
switch (find_viable(v, val)) { switch (find_viable(v, val)) {
case dd::find_t::singleton: case dd::find_t::singleton:
s.propagate(v, val, sc); // TBD why is sc used as justification? It should be all of viable s.assign_propagate(v, val);
prop = true; prop = true;
break; break;
case dd::find_t::empty: case dd::find_t::empty: