mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-13 16:49:45 +02:00
commit 9e6fd7cb70
9 changed files with 107 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

57
src/math/polysat/conflict_core.cpp
View file

@ -50,12 +50,12 @@ namespace polysat {
std::ostream& conflict_core::display(std::ostream& out) const {
char const* sep = "";
for (auto c : m_constraints)
for (auto c : *this)
out << sep << c, sep = " ; ";
if (!m_vars.empty())
out << " vars";
for (auto v : m_vars)
out << " " << v;
out << " v" << v;
return out;
}
@ -136,14 +136,29 @@ namespace polysat {
}
void conflict_core::remove_var(pvar v) {
LOG("Removing v" << v << " from core");
unsigned j = 0;
for (unsigned i = 0; i < m_constraints.size(); ++i)
if (m_constraints[i]->contains_var(v))
unset_mark(m_constraints[i]);
else
m_constraints[j++] = m_constraints[i];
m_constraints[j++] = m_constraints[i];
m_constraints.shrink(j);
indexed_uint_set literals_copy = m_literals; // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
for (unsigned lit_idx : literals_copy) {
signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
if (c->contains_var(v)) {
unset_mark(c);
m_literals.remove(lit_idx);
}
}
m_vars.remove(v);
}
void conflict_core::set_bailout() {
SASSERT(!is_bailout());
m_bailout = true;
s().m_stats.m_num_bailouts++;
}
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
@ -152,9 +167,10 @@ namespace polysat {
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
SASSERT(var != sat::null_bool_var);
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));
bool core_has_neg = contains_literal(~sat::literal(var));
DEBUG_CODE({
bool core_has_pos = std::count_if(begin(), end(), [var](auto c){ return c.blit() == sat::literal(var); }) > 0;
bool core_has_neg = std::count_if(begin(), end(), [var](auto c){ return c.blit() == ~sat::literal(var); }) > 0;
bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 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
@ -162,14 +178,10 @@ namespace polysat {
SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
});
int j = 0;
for (auto c : m_constraints) {
if (c->bvar() != var)
m_constraints[j++] = c;
else
unset_mark(c);
}
m_constraints.shrink(j);
if (core_has_pos)
remove_literal(sat::literal(var));
if (core_has_neg)
remove_literal(~sat::literal(var));
for (sat::literal lit : cl)
if (lit.var() != var)
@ -179,9 +191,9 @@ namespace polysat {
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
void conflict_core::keep(signed_constraint c) {
if (!c->has_bvar()) {
m_constraints.erase(c);
remove(c);
cm().ensure_bvar(c.get());
insert_literal(c.blit());
insert(c);
}
LOG_H3("keeping: " << c);
// NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
@ -194,6 +206,7 @@ namespace polysat {
for (auto premise : premises) {
keep(premise);
SASSERT(premise->has_bvar());
SASSERT(s().m_bvars.value(premise.blit()) == l_true); // otherwise the propagation doesn't make sense
c_lemma.push(~premise.blit());
active_level = std::max(active_level, s().m_bvars.level(premise.blit()));
}
@ -210,11 +223,13 @@ namespace polysat {
clause_builder lemma(s());
for (auto c : m_constraints) {
if (!c->has_bvar())
keep(c);
lemma.push(~c);
SASSERT(!c->has_bvar());
keep(c);
}
for (auto c : *this)
lemma.push(~c);
for (unsigned v : m_vars) {
if (!is_pmarked(v))
continue;
@ -355,6 +370,10 @@ namespace polysat {
return m_bvar2mark.get(b, false);
}
bool conflict_core::contains_literal(sat::literal lit) const {
return m_literals.contains(lit.to_uint());
}
void conflict_core::insert_literal(sat::literal lit) {
m_literals.insert(lit.to_uint());
}

7
src/math/polysat/conflict_core.h
View file

@ -45,6 +45,7 @@ namespace polysat {
void set_mark(signed_constraint c);
void unset_mark(signed_constraint c);
bool contains_literal(sat::literal lit) const;
void insert_literal(sat::literal lit);
void remove_literal(sat::literal lit);
@ -68,7 +69,7 @@ namespace polysat {
pvar conflict_var() const { return m_conflict_var; }
bool is_bailout() const { return m_bailout; }
void set_bailout() { SASSERT(!is_bailout()); m_bailout = true; s().m_stats.m_num_bailouts++; }
void set_bailout();
bool empty() const {
return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;
@ -135,11 +136,11 @@ namespace polysat {
conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {}
static conflict_core_iterator begin(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) {
static conflict_core_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.begin(), cs.end(), lits.begin()};
}
static conflict_core_iterator end(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) {
static conflict_core_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.end(), cs.end(), lits.end()};
}

8
src/math/polysat/explain.cpp
View file

@ -47,8 +47,7 @@ namespace polysat {
// c2 ... constraint that is currently false
// Try to replace it with a new false constraint (derived from superposition with a true constraint)
signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) {
for (auto it1 = core.begin(); it1 != core.end(); ++it1) {
signed_constraint c1 = *it1;
for (auto c1 : core) {
if (!is_positive_equality_over(v, c1))
continue;
if (!c1.is_currently_true(s()))
@ -69,14 +68,13 @@ namespace polysat {
// TODO(later): check superposition into disequality again (see notes)
// true = done, false = abort, undef = continue
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
for (auto it2 = core.begin(); it2 != core.end(); ++it2) {
signed_constraint c2 = *it2;
for (auto c2 : core) {
if (!is_positive_equality_over(v, c2))
continue;
if (!c2.is_currently_false(s()))
continue;
// TODO: can try multiple replacements at once; then the it2 loop needs to be done only once... (requires some reorganization for storing the premises)
// TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
signed_constraint c = find_replacement(c2, v, core);
if (!c)
continue;

79
src/math/polysat/saturation.cpp
View file

@ -55,25 +55,26 @@ namespace polysat {
/**
* Propagate c. It is added to reason and core all other literals in reason are false in current stack.
* The lemmas outlines in the rules are valid and therefore c is implied.
* The lemmas outlined in the rules are valid and therefore c is implied.
*/
bool inf_saturate::propagate(conflict_core& core, inequality const& crit, signed_constraint& c, clause_builder& reason) {
if (crit.as_signed_constraint().is_currently_false(s()) && c.is_currently_true(s()))
bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
bool crit1_false = crit1.as_signed_constraint().is_currently_false(s());
bool crit2_false = crit2.as_signed_constraint().is_currently_false(s());
if ((crit1_false || crit2_false) && c.is_currently_true(s())) // TODO: check filter
return false;
for (auto d : new_constraints)
core.insert(d);
core.insert(c);
reason.push(c);
s().propagate_bool(c.blit(), reason.build().get());
core.remove(crit.as_signed_constraint()); // needs to be after propagation so we know it is propagated
return true;
}
bool inf_saturate::propagate(conflict_core& core, inequality const& crit, bool is_strict, pdd const& lhs, pdd const& rhs, clause_builder& reason) {
bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints) {
signed_constraint c = ineq(is_strict, lhs, rhs);
return propagate(core, crit, c, reason);
return propagate(core, crit1, crit2, c, new_constraints);
}
/// Add premises for Ω*(x, y)
void inf_saturate::push_omega_bisect(clause_builder& reason, pdd const& x, rational x_max, pdd const& y, rational y_max) {
void inf_saturate::push_omega_bisect(vector<signed_constraint>& new_constraints, pdd const& x, rational x_max, pdd const& y, rational y_max) {
rational x_val, y_val;
auto& pddm = x.manager();
unsigned bit_size = pddm.power_of_2();
@ -125,13 +126,13 @@ namespace polysat {
// where we add explicit equality propagations from the current assignment.
auto c1 = s().ule(x, pddm.mk_val(x_lo));
auto c2 = s().ule(y, pddm.mk_val(y_lo));
reason.push(~c1);
reason.push(~c2);
new_constraints.insert(c1);
new_constraints.insert(c2);
}
// determine worst case upper bounds for x, y
// then extract premises for a non-worst-case bound.
void inf_saturate::push_omega(clause_builder& reason, pdd const& x, pdd const& y) {
void inf_saturate::push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y) {
auto& pddm = x.manager();
unsigned bit_size = pddm.power_of_2();
rational bound = rational::power_of_two(bit_size);
@ -144,12 +145,12 @@ namespace polysat {
y_max = s().m_viable.max_viable(y.var());
if (x_max * y_max >= bound)
push_omega_bisect(reason, x, x_max, y, y_max);
push_omega_bisect(new_constraints, x, x_max, y, y_max);
else {
for (auto c : s().m_cjust[y.var()])
reason.push(~c);
new_constraints.insert(c);
for (auto c : s().m_cjust[x.var()])
reason.push(~c);
new_constraints.insert(c);
}
}
@ -258,12 +259,11 @@ namespace polysat {
if (!c.is_strict && s().get_value(v).is_zero())
return false;
clause_builder reason(s());
vector<signed_constraint> new_constraints;
if (!c.is_strict)
reason.push(s().eq(x));
reason.push(~c.as_signed_constraint());
push_omega(reason, x, y);
return propagate(core, c, c.is_strict, y, z, reason);
new_constraints.push_back(~s().eq(x));
push_omega(new_constraints, x, y);
return propagate(core, c, c, c.is_strict, y, z, new_constraints);
}
/// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x
@ -278,12 +278,12 @@ namespace polysat {
pdd const& z_prime = le_y.lhs;
clause_builder reason(s());
reason.push(~le_y.as_signed_constraint());
reason.push(~yx_l_zx.as_signed_constraint());
push_omega(reason, x, y);
vector<signed_constraint> new_constraints;
new_constraints.push_back(le_y.as_signed_constraint());
new_constraints.push_back(yx_l_zx.as_signed_constraint());
push_omega(new_constraints, x, y);
// z'x <= zx
return propagate(core, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, reason);
return propagate(core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, new_constraints);
}
bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& c) {
@ -326,11 +326,11 @@ namespace polysat {
pdd z = x_l_z.rhs;
if (!is_non_overflow(a, z))
return false;
clause_builder reason(s());
reason.push(~x_l_z.as_signed_constraint());
reason.push(~y_l_ax.as_signed_constraint());
push_omega(reason, a, z);
return propagate(core, y_l_ax, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, reason);
vector<signed_constraint> new_constraints;
new_constraints.push_back(x_l_z.as_signed_constraint());
new_constraints.push_back(y_l_ax.as_signed_constraint());
push_omega(new_constraints, a, z);
return propagate(core, x_l_z, y_l_ax, x_l_z.is_strict || y_l_ax.is_strict, y, a * z, new_constraints);
}
@ -351,19 +351,18 @@ namespace polysat {
return false;
}
bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& c, inequality const& d, pdd const& x, pdd const& y) {
SASSERT(is_g_v(z, c));
SASSERT(verify_YX_l_zX(z, d, x, y));
pdd const& y_prime = c.rhs;
bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
SASSERT(is_g_v(z, z_l_y));
SASSERT(verify_YX_l_zX(z, yx_l_zx, x, y));
pdd const& y_prime = z_l_y.rhs;
if (!is_non_overflow(x, y_prime))
return false;
clause_builder reason(s());
reason.push(~c.as_signed_constraint());
reason.push(~d.as_signed_constraint());
push_omega(reason, x, y_prime);
vector<signed_constraint> new_constraints;
new_constraints.push_back(z_l_y.as_signed_constraint());
new_constraints.push_back(yx_l_zx.as_signed_constraint());
push_omega(new_constraints, x, y_prime);
// yx <= y'x
return propagate(core, d, c.is_strict || d.is_strict, y * x, y_prime * x, reason);
return propagate(core, z_l_y, yx_l_zx, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x, new_constraints);
}
}

8
src/math/polysat/saturation.h
View file

@ -37,11 +37,11 @@ namespace polysat {
class inf_saturate : public inference_engine {
bool find_upper_bound(pvar x, signed_constraint& c, rational& bound);
void push_omega(clause_builder& reason, pdd const& x, pdd const& y);
void push_omega_bisect(clause_builder& reason, pdd const& x, rational x_max, pdd const& y, rational y_max);
void push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y);
void push_omega_bisect(vector<signed_constraint>& new_constraints, pdd const& x, rational x_max, pdd const& y, rational y_max);
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
bool propagate(conflict_core& core, inequality const& crit, signed_constraint& c, clause_builder& reason);
bool propagate(conflict_core& core, inequality const& crit, bool strict, pdd const& lhs, pdd const& rhs, clause_builder& reason);
bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints);
bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints);
bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);

4
src/math/polysat/search_state.cpp
View file

@ -19,9 +19,9 @@ namespace polysat {
std::ostream& search_item::display(std::ostream& out) const {
switch (kind()) {
case search_item_k::assignment:
return out << "assignment(v" << var() << ")";
return out << "v" << var() << "=?";
case search_item_k::boolean:
return out << "boolean(" << lit() << ")";
return out << lit();
}
UNREACHABLE();
return out;

10
src/math/polysat/search_state.h
View file

@ -92,7 +92,7 @@ namespace polysat {
void init() {
first = m_search->size();
current = first - 1;
current = first; // we start one before the beginning
}
void try_push_block() {
@ -104,7 +104,8 @@ namespace polysat {
void pop_block() {
current = m_index_stack.back().current;
first = m_index_stack.back().first;
// We don't restore 'first', otherwise 'next()' will immediately push a new block again.
// Instead, the current block is merged with the popped one.
m_index_stack.pop_back();
}
@ -116,7 +117,6 @@ namespace polysat {
search_iterator(search_state& search):
m_search(&search) {
init();
current++; // we start one before the beginning, then it also works for empty m_search
}
search_item const& operator*() const {
@ -124,7 +124,9 @@ namespace polysat {
}
bool next() {
#if 0 // If you want to resolve over constraints that have been added during conflict resolution, enable this.
try_push_block();
#endif
if (current > last()) {
--current;
return true;
@ -134,7 +136,7 @@ namespace polysat {
if (m_index_stack.empty())
return false;
pop_block();
return true;
return next();
}
}
};

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

@ -210,14 +210,14 @@ namespace polysat {
}
void solver::propagate(sat::literal lit) {
LOG_H2("Propagate boolean literal " << lit);
LOG_H2("Propagate bool " << lit);
signed_constraint c = m_constraints.lookup(lit);
SASSERT(c);
activate_constraint(c);
}
void solver::propagate(pvar v) {
LOG_H2("Propagate pvar " << v);
LOG_H2("Propagate v" << v);
auto& wlist = m_watch[v];
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
@ -453,6 +453,7 @@ namespace polysat {
search_iterator search_it(m_search);
while (search_it.next()) {
LOG("search state: " << m_search);
LOG("Conflict: " << m_conflict);
auto const& item = *search_it;
LOG_H2("Working on " << item);
@ -479,7 +480,7 @@ namespace polysat {
sat::bool_var const var = lit.var();
if (!m_conflict.is_bmarked(var))
continue;
if (m_bvars.level(var) <= base_level())
if (m_bvars.level(var) <= base_level()) // TODO: this doesn't work with out-of-level-order iteration.
break;
if (m_bvars.is_decision(var)) {
revert_bool_decision(lit);
@ -600,17 +601,8 @@ namespace polysat {
m_viable.add_non_viable(v, val);
learn_lemma(v, std::move(lemma));
if (is_conflict()) {
LOG_H1("Conflict during revert_decision/learn_lemma!");
return;
}
narrow(v);
if (m_justification[v].is_unassigned()) {
m_free_vars.del_var_eh(v);
decide(v);
}
if (!is_conflict())
narrow(v);
}
bool solver::is_decision(search_item const& item) const {
@ -814,8 +806,8 @@ namespace polysat {
for (auto* cl : m_redundant_clauses) {
out << "\t" << *cl << "\n";
for (auto lit : *cl) {
auto c = m_constraints.lookup(lit.var());
out << "\t\t" << lit.var() << ": " << *c << "\n";
auto c = m_constraints.lookup(lit);
out << "\t\t" << lit << ": " << c << "\n";
}
}
return out;

7
src/math/polysat/ule_constraint.cpp
View file

@ -50,14 +50,13 @@ namespace polysat {
// p <= 0, e.g., p == 0
if (q.is_zero() && p.is_unilinear()) {
// a*x + b == 0
pvar v = q.var();
pvar v = p.var();
s.push_cjust(v, { this, is_positive });
rational a = q.hi().val();
rational b = q.lo().val();
rational a = p.hi().val();
rational b = p.lo().val();
s.m_viable.intersect_eq(a, v, b, is_positive);
rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, { this, is_positive });