mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Store only literals in the conflict state

Browse source
This commit is contained in:
Jakob Rath 2022-04-11 15:00:06 +02:00
parent fde78f99c3
commit 63031548cb
10 changed files with 73 additions and 145 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -77,8 +77,6 @@ namespace polysat {
void clause_builder::push_new(signed_constraint c) {
if (c.is_always_false()) // filter out trivial constraints such as "4 < 2" (may come in from forbidden intervals)
return;
if (!c->has_bvar())
m_solver->m_constraints.ensure_bvar(c.get());
push(c);
}
}

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

@ -60,10 +60,16 @@ namespace polysat {
return out;
}
bool conflict::empty() const {
return m_literals.empty()
&& m_vars.empty()
&& m_bail_vars.empty()
&& m_conflict_var == null_var;
}
void conflict::reset() {
for (auto c : *this)
unset_mark(c);
m_constraints.reset();
m_literals.reset();
m_vars.reset();
m_bail_vars.reset();
@ -135,19 +141,15 @@ namespace polysat {
void conflict::insert(signed_constraint c) {
if (c.is_always_true())
return;
if (c->is_marked())
if (is_marked(c))
return;
LOG("inserting: " << c);
SASSERT(!c->vars().empty());
set_mark(c);
if (c->has_bvar())
insert_literal(c.blit());
else
m_constraints.push_back(c);
m_literals.insert(c.blit().index());
}
void conflict::propagate(signed_constraint c) {
cm().ensure_bvar(c.get());
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
@ -175,13 +177,11 @@ namespace polysat {
* Ensure that c is assigned and justified
*/
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
keep(c);
// keep(c);
clause_builder c_lemma(s);
for (auto premise : premises) {
LOG_H3("premise: " << premise);
keep(premise);
SASSERT(premise->has_bvar());
// keep(premise);
SASSERT(premise.bvalue(s) != l_false);
c_lemma.push(~premise.blit());
}
@ -194,12 +194,8 @@ namespace polysat {
}
void conflict::remove(signed_constraint c) {
SASSERT(!c->has_bvar() || std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
unset_mark(c);
if (c->has_bvar())
remove_literal(c.blit());
else
m_constraints.erase(c);
m_literals.remove(c.blit().index());
}
void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
@ -207,12 +203,12 @@ namespace polysat {
insert(c_new, c_new_premises);
}
bool conflict::contains(signed_constraint c) const {
return m_literals.contains(c.blit().index());
}
bool conflict::contains(signed_constraint c) {
if (c->has_bvar())
return m_literals.contains(c.blit().index());
else
return m_constraints.contains(c);
bool conflict::contains(sat::literal lit) const {
return m_literals.contains(lit.index());
}
void conflict::set_bailout() {
@ -228,14 +224,12 @@ namespace polysat {
SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
SASSERT(contains_literal(lit));
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains_literal(~lit));
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove_literal(lit);
unset_mark(s.lit2cnstr(lit));
remove(s.lit2cnstr(lit));
for (sat::literal lit2 : cl)
if (lit2 != lit)
insert(s.lit2cnstr(~lit2));
@ -247,9 +241,8 @@ namespace polysat {
SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
SASSERT(contains_literal(lit));
SASSERT(!contains_literal(~lit));
SASSERT(contains(lit));
SASSERT(!contains(~lit));
signed_constraint c = s.lit2cnstr(lit);
bool has_decision = false;
@ -260,35 +253,19 @@ namespace polysat {
if (!has_decision) {
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v))
if (s.is_assigned(v)) {
// TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that?
SASSERT(s.get_level(v) <= lvl);
m_vars.insert(v);
}
}
}
/**
* If the constraint c is a temporary constraint derived by core saturation,
* insert it (and recursively, its premises) into \Gamma
*/
void conflict::keep(signed_constraint c) {
if (c->has_bvar())
return;
LOG_H3("keeping: " << c);
remove(c);
cm().ensure_bvar(c.get());
insert(c);
}
clause_builder conflict::build_lemma() {
// SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
LOG_H3("Build lemma from core");
LOG("core: " << *this);
clause_builder lemma(s);
while (!m_constraints.empty())
keep(m_constraints.back());
for (auto c : *this)
minimize_vars(c);
@ -297,7 +274,6 @@ namespace polysat {
for (unsigned v : m_vars) {
auto eq = s.eq(s.var(v), s.get_value(v));
cm().ensure_bvar(eq.get());
if (eq.bvalue(s) == l_undef)
s.assign_eval(eq.blit());
lemma.push(~eq);
@ -410,50 +386,27 @@ namespace polysat {
}
void conflict::set_mark(signed_constraint c) {
if (c->is_marked())
return;
c->set_mark();
if (c->has_bvar())
set_bmark(c->bvar());
}
/**
* unset marking on the constraint, but keep variable dependencies.
*/
void conflict::unset_mark(signed_constraint c) {
if (!c->is_marked())
return;
c->unset_mark();
if (c->has_bvar())
unset_bmark(c->bvar());
}
void conflict::set_bmark(sat::bool_var b) {
sat::bool_var b = c->bvar();
if (b >= m_bvar2mark.size())
m_bvar2mark.resize(b + 1);
SASSERT(!m_bvar2mark[b]);
m_bvar2mark[b] = true;
}
void conflict::unset_bmark(sat::bool_var b) {
/**
* unset marking on the constraint, but keep variable dependencies.
*/
void conflict::unset_mark(signed_constraint c) {
sat::bool_var b = c->bvar();
SASSERT(m_bvar2mark[b]);
m_bvar2mark[b] = false;
}
bool conflict::is_bmarked(sat::bool_var b) const {
bool conflict::is_marked(signed_constraint c) const {
return is_marked(c->bvar());
}
bool conflict::is_marked(sat::bool_var b) const {
return m_bvar2mark.get(b, false);
}
bool conflict::contains_literal(sat::literal lit) const {
return m_literals.contains(lit.to_uint());
}
void conflict::insert_literal(sat::literal lit) {
m_literals.insert(lit.to_uint());
}
void conflict::remove_literal(sat::literal lit) {
m_literals.remove(lit.to_uint());
}
}

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

@ -85,7 +85,7 @@ namespace polysat {
/** Conflict state, represented as core (~negation of clause). */
class conflict {
solver& s;
signed_constraints m_constraints; // new constraints used as premises
// signed_constraints m_constraints; // new constraints used as premises
indexed_uint_set m_literals; // set of boolean literals in the conflict
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
@ -95,16 +95,9 @@ namespace polysat {
pvar m_conflict_var = null_var;
bool_vector m_bvar2mark; // mark of Boolean variables
void set_bmark(sat::bool_var b);
void unset_bmark(sat::bool_var b);
void set_mark(signed_constraint c);
void unset_mark(signed_constraint c);
void unset_bmark(signed_constraint c);
bool contains_literal(sat::literal lit) const;
void insert_literal(sat::literal lit);
void remove_literal(sat::literal lit);
void minimize_vars(signed_constraint c);
@ -126,14 +119,12 @@ namespace polysat {
void set_bailout();
bool empty() const {
return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;
}
bool empty() const;
void reset();
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool is_bmarked(sat::bool_var b) const;
bool is_marked(signed_constraint c) const;
bool is_marked(sat::bool_var b) const;
/** conflict because the constraint c is false under current variable assignment */
void set(signed_constraint c);
@ -149,9 +140,8 @@ namespace polysat {
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
void keep(signed_constraint c);
bool contains(signed_constraint c);
bool contains(signed_constraint c) const;
bool contains(sat::literal lit) const;
/** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals.
@ -187,23 +177,20 @@ namespace polysat {
class conflict_iterator {
friend class conflict;
using it1_t = signed_constraints::const_iterator;
using it2_t = indexed_uint_set::iterator;
using inner_t = indexed_uint_set::iterator;
constraint_manager* m_cm;
it1_t m_it1;
it1_t m_end1;
it2_t m_it2;
inner_t m_inner;
conflict_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) {}
conflict_iterator(constraint_manager& cm, inner_t inner):
m_cm(&cm), m_inner(inner) {}
static conflict_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.begin(), cs.end(), lits.begin()};
static conflict_iterator begin(constraint_manager& cm, indexed_uint_set const& lits) {
return {cm, lits.begin()};
}
static conflict_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.end(), cs.end(), lits.end()};
static conflict_iterator end(constraint_manager& cm, indexed_uint_set const& lits) {
return {cm, lits.end()};
}
public:
@ -214,28 +201,22 @@ namespace polysat {
using iterator_category = std::input_iterator_tag;
conflict_iterator& operator++() {
if (m_it1 != m_end1)
++m_it1;
else
++m_it2;
++m_inner;
return *this;
}
signed_constraint operator*() const {
if (m_it1 != m_end1)
return *m_it1;
else
return m_cm->lookup(sat::to_literal(*m_it2));
return m_cm->lookup(sat::to_literal(*m_inner));
}
bool operator==(conflict_iterator const& other) const {
return m_it1 == other.m_it1 && m_it2 == other.m_it2;
return m_inner == other.m_inner;
}
bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
};
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_constraints, m_literals); }
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_constraints, m_literals); }
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
}

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

@ -151,6 +151,8 @@ namespace polysat {
return c2;
}
else {
SASSERT(!c1->has_bvar());
ensure_bvar(c1);
m_constraint_table.insert(c1);
store(c1);
return c1;

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

@ -74,14 +74,13 @@ namespace polysat {
void register_clause(clause* cl, solver& s);
void ensure_bvar(constraint* c);
void erase_bvar(constraint* c);
public:
constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
~constraint_manager();
void ensure_bvar(constraint* c);
void erase_bvar(constraint* c);
// sat::literal get_or_assign_blit(signed_constraint& c);
void store(clause* cl, solver& s, bool value_propagate);
/// Release clauses at the given level and above.
@ -146,11 +145,9 @@ namespace polysat {
friend class smul_fl_constraint;
friend class op_constraint;
// constraint_manager* m_manager;
ckind_t m_kind;
unsigned_vector m_vars;
lbool m_external_sign = l_undef;
bool m_is_marked = false;
bool m_is_active = false;
/** The boolean variable associated to this constraint, if any.
* If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
@ -159,7 +156,6 @@ namespace polysat {
sat::bool_var m_bvar = sat::null_bool_var;
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
public:
virtual ~constraint() {}
@ -199,7 +195,7 @@ namespace polysat {
unsigned var(unsigned idx) const { return m_vars[idx]; }
bool contains_var(pvar v) const { return m_vars.contains(v); }
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { return m_bvar; }
sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
std::string bvar2string() const;
unsigned level(solver& s) const;
@ -208,10 +204,6 @@ namespace polysat {
bool is_external() const { return m_external_sign != l_undef; }
bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
void set_mark() { m_is_marked = true; }
void unset_mark() { m_is_marked = false; }
bool is_marked() const { return m_is_marked; }
bool is_active() const { return m_is_active; }
void set_active(bool f) { m_is_active = f; }

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

@ -61,8 +61,6 @@ namespace polysat {
signed_constraint c = resolve1(v, c1, c2);
if (!c)
continue;
if (!c->has_bvar())
s.m_constraints.ensure_bvar(c.get());
switch (c.bvalue(s)) {
case l_false:

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

@ -50,7 +50,6 @@ namespace polysat {
void search_state::push_assignment(pvar p, rational const& r) {
m_items.push_back(search_item::assignment(p));
m_assignment.push_back({p, r});
auto& m = s.var2pdd(p);
unsigned sz = s.size(p);
pdd& s = assignment(sz);
m_subst_trail.push_back(s);

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

@ -48,6 +48,8 @@ namespace polysat {
return false;
}
void simplify::operator()() {}
void simplify::operator()() {
(void)s; // silence warning
}
}

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

@ -186,7 +186,6 @@ namespace polysat {
SASSERT(c);
if (is_conflict())
return; // no need to do anything if we already have a conflict at base level
m_constraints.ensure_bvar(c.get());
sat::literal lit = c.blit();
LOG("New constraint: " << c);
switch (m_bvars.value(lit)) {
@ -624,7 +623,7 @@ namespace polysat {
SASSERT(item.is_boolean());
sat::literal const lit = item.lit();
sat::bool_var const var = lit.var();
if (!m_conflict.is_bmarked(var))
if (!m_conflict.is_marked(var))
continue;
LOG_H2("Working on " << search_item_pp(m_search, item));
@ -639,8 +638,10 @@ namespace polysat {
}
else if (m_bvars.is_bool_propagation(var))
m_conflict.resolve(lit, *m_bvars.reason(lit));
else
else {
SASSERT(m_bvars.is_value_propagation(var));
m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
}
}
}
// here we build conflict clause if it has free variables.
@ -938,7 +939,6 @@ namespace polysat {
signed_constraint c = cs[i];
if (c.is_always_false())
continue;
m_constraints.ensure_bvar(c.get());
cb.push(c);
}
clause_ref clause = cb.build();
@ -1114,7 +1114,7 @@ namespace polysat {
pdd solver::subst(assignment_t const& sub, pdd const& p) const {
unsigned sz = p.manager().power_of_2();
pdd s = p.manager().mk_val(1);
for (auto const [var, val] : sub)
for (auto const& [var, val] : sub)
if (size(var) == sz)
s = p.manager().subst_add(s, var, val);
return p.subst_val(s);

3
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -17,6 +17,7 @@ Author:
--*/
#include "math/polysat/univariate/univariate_solver.h"
#include "math/polysat/log.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "solver/solver.h"
#include "util/util.h"
@ -54,7 +55,9 @@ namespace polysat {
~univariate_bitblast_solver() override = default;
void push() override {
// LOG("univariate push...");
s->push();
// LOG("univariate push done");
}
void pop(unsigned n) override {