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

Treat eval'd literals as propagations (not as decisions)

Browse source
This commit is contained in:
Jakob Rath 2022-01-21 15:55:05 +01:00
parent 8765dc16a5
commit c4c9c84aeb
7 changed files with 92 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/math/polysat/boolean.cpp
View file

@ -24,8 +24,8 @@ namespace polysat {
m_value.push_back(l_undef);
m_level.push_back(UINT_MAX);
m_deps.push_back(null_dependency);
m_reason.push_back(nullptr);
m_lemma.push_back(nullptr);
m_kind.push_back(kind_t::unassigned);
m_clause.push_back(nullptr);
m_watch.push_back({});
m_watch.push_back({});
m_activity.push_back(0);
@ -36,8 +36,8 @@ namespace polysat {
SASSERT_EQ(m_level[var], UINT_MAX);
SASSERT_EQ(m_value[2*var], l_undef);
SASSERT_EQ(m_value[2*var+1], l_undef);
SASSERT_EQ(m_reason[var], nullptr);
SASSERT_EQ(m_lemma[var], nullptr);
SASSERT_EQ(m_kind[var], kind_t::unassigned);
SASSERT_EQ(m_clause[var], nullptr);
SASSERT_EQ(m_deps[var], null_dependency);
}
m_free_vars.mk_var_eh(var);
@ -50,8 +50,8 @@ namespace polysat {
m_value[lit.index()] = l_undef;
m_value[(~lit).index()] = l_undef;
m_level[var] = UINT_MAX;
m_reason[var] = nullptr;
m_lemma[var] = nullptr;
m_kind[var] = kind_t::unassigned;
m_clause[var] = nullptr;
m_deps[var] = null_dependency;
m_watch[lit.index()].reset();
m_watch[(~lit).index()].reset();
@ -62,31 +62,36 @@ namespace polysat {
void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
assign(lit, lvl, &reason, nullptr, null_dependency);
assign(kind_t::propagation, lit, lvl, &reason);
SASSERT(is_propagation(lit));
}
void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause* lemma) {
void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause& lemma) {
LOG("Decide literal " << lit << " @ " << lvl);
assign(lit, lvl, nullptr, lemma);
assign(kind_t::decision, lit, lvl, &lemma);
SASSERT(is_decision(lit));
}
void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
LOG("Eval literal " << lit << " @ " << lvl);
assign(lit, lvl, nullptr, nullptr);
assign(kind_t::propagation, lit, lvl, nullptr);
SASSERT(is_propagation(lit));
}
void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) {
LOG("Asserted " << lit << " @ " << lvl);
assign(lit, lvl, nullptr, nullptr, dep);
assign(kind_t::decision, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit));
}
void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep) {
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep) {
SASSERT(!is_assigned(lit));
SASSERT(k != kind_t::unassigned);
m_value[lit.index()] = l_true;
m_value[(~lit).index()] = l_false;
m_level[lit.var()] = lvl;
m_reason[lit.var()] = reason;
m_lemma[lit.var()] = lemma;
m_kind[lit.var()] = k;
m_clause[lit.var()] = reason;
m_deps[lit.var()] = dep;
m_free_vars.del_var_eh(lit.var());
}
@ -96,8 +101,8 @@ namespace polysat {
m_value[lit.index()] = l_undef;
m_value[(~lit).index()] = l_undef;
m_level[lit.var()] = UINT_MAX;
m_reason[lit.var()] = nullptr;
m_lemma[lit.var()] = nullptr;
m_kind[lit.var()] = kind_t::unassigned;
m_clause[lit.var()] = nullptr;
m_deps[lit.var()] = null_dependency;
m_free_vars.unassign_var_eh(lit.var());
}

41
src/math/polysat/boolean.h
View file

@ -19,20 +19,28 @@ namespace polysat {
class clause;
class bool_var_manager {
enum class kind_t {
unassigned,
propagation,
decision,
};
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
svector<lbool> m_value; // current value (indexed by literal)
unsigned_vector m_level; // level of assignment (indexed by variable)
unsigned_vector m_deps; // dependencies of external asserts
unsigned_vector m_activity; //
ptr_vector<clause> m_reason; // propagation reason, NULL for decisions and external asserts (indexed by variable)
// For enumerative backtracking we store the lemma we're handling with a certain decision
ptr_vector<clause> m_lemma;
unsigned_vector m_activity; //
svector<kind_t> m_kind; // decision or propagation?
// Clause associated with the assignment (indexed by variable):
// - for propagations: the reason (or NULL for eval'd literals)
// - for decisions: the lemma (or NULL for externally asserted literals)
ptr_vector<clause> m_clause;
var_queue m_free_vars; // free Boolean variables
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep = null_dependency);
void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep = null_dependency);
public:
@ -46,19 +54,21 @@ namespace polysat {
bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; }
bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
bool is_decision(sat::bool_var var) const { return is_assigned(var) && !reason(var); }
bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; }
bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
bool is_propagation(sat::bool_var var) const { return is_assigned(var) && reason(var); }
bool is_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::propagation; }
bool is_propagation(sat::literal lit) const { return is_propagation(lit.var()); }
lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
lbool value(sat::literal lit) const { return m_value[lit.index()]; }
bool is_true(sat::literal lit) const { return value(lit) == l_true; }
bool is_false(sat::literal lit) const { return value(lit) == l_false; }
unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; }
clause* reason(sat::literal lit) const { return reason(lit.var()); }
unsigned dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; }
ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
unsigned_vector& activity() { return m_activity; }
@ -71,12 +81,21 @@ namespace polysat {
/// Set the given literal to true
void propagate(sat::literal lit, unsigned lvl, clause& reason);
void decide(sat::literal lit, unsigned lvl, clause* lemma);
void decide(sat::literal lit, unsigned lvl, clause& lemma);
void eval(sat::literal lit, unsigned lvl);
void asserted(sat::literal lit, unsigned lvl, unsigned dep);
void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const;
friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
switch (k) {
case kind_t::unassigned: return out << "unassigned"; break;
case kind_t::propagation: return out << "propagation"; break;
case kind_t::decision: return out << "decision"; break;
default: UNREACHABLE();
}
}
};
inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); }

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

@ -194,7 +194,7 @@ namespace polysat {
s.m_stats.m_num_bailouts++;
}
void conflict::resolve(constraint_manager const& m, sat::literal lit, clause const& cl) {
void conflict::resolve(sat::literal lit, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
// clause: x \/ u \/ v
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
@ -208,10 +208,28 @@ namespace polysat {
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove_literal(lit);
unset_mark(m.lookup(lit));
unset_mark(s.lit2cnstr(lit));
for (sat::literal lit2 : cl)
if (lit2 != lit)
insert(m.lookup(~lit2));
insert(s.lit2cnstr(~lit2));
}
void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
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));
remove_literal(lit);
signed_constraint c = s.lit2cnstr(lit);
unset_mark(c);
for (pvar v : c->vars())
if (s.is_assigned(v) && s.get_level(v) <= lvl)
m_vars.insert(v); // TODO: check this
}
/**

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

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

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

@ -250,14 +250,12 @@ namespace polysat {
DEBUG_CODE(m_locked_wlist = v;);
auto& wlist = m_pwatch[v];
unsigned i = 0, j = 0, sz = wlist.size();
LOG("wlist old: " << wlist);
for (; i < sz && !is_conflict(); ++i)
if (!wlist[i].propagate(*this, v))
wlist[j++] = wlist[i];
for (; i < sz; ++i)
wlist[j++] = wlist[i];
wlist.shrink(j);
LOG("wlist new: " << wlist);
DEBUG_CODE(m_locked_wlist = std::nullopt;);
}
@ -578,10 +576,13 @@ namespace polysat {
* NOTE: boolean resolution should work normally even in bailout mode.
*/
void solver::resolve_bool(sat::literal lit) {
SASSERT(m_bvars.is_propagation(lit.var()));
clause const& other = *m_bvars.reason(lit.var());
LOG_H3("resolve_bool: " << lit << " " << other);
m_conflict.resolve(m_constraints, lit, other);
SASSERT(m_bvars.is_propagation(lit));
clause const* other = m_bvars.reason(lit);
LOG_H3("resolve_bool: " << lit << " " << show_deref(other));
if (other)
m_conflict.resolve(lit, *other);
else
m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
}
void solver::report_unsat() {
@ -664,7 +665,7 @@ namespace polysat {
break;
default:
push_level();
assign_decision(choice, &lemma);
assign_decision(choice, lemma);
break;
}
}
@ -740,14 +741,16 @@ namespace polysat {
// The lemma where 'lit' comes from.
// Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned
// We only revert decisions that come from lemmas, so lemma must not be NULL here.
// (Externally asserted literals are at a base level, so we would return UNSAT instead of reverting.)
SASSERT(lemma);
backjump(m_bvars.level(var) - 1);
// reason should force ~lit after propagation
add_clause(*reason);
if (lemma) // TODO: can (should) this ever be NULL?
enqueue_decision_on_lemma(*lemma);
enqueue_decision_on_lemma(*lemma);
}
unsigned solver::level(sat::literal lit0, clause const& cl) {
@ -768,7 +771,7 @@ namespace polysat {
m_search.push_boolean(lit);
}
void solver::assign_decision(sat::literal lit, clause* lemma) {
void solver::assign_decision(sat::literal lit, clause& lemma) {
m_bvars.decide(lit, m_level, lemma);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);

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

@ -152,7 +152,7 @@ namespace polysat {
void pop_levels(unsigned num_levels);
void assign_propagate(sat::literal lit, clause& reason);
void assign_decision(sat::literal lit, clause* lemma);
void assign_decision(sat::literal lit, clause& lemma);
void assign_eval(sat::literal lit);
void activate_constraint(signed_constraint c);
void deactivate_constraint(signed_constraint c);

4
src/test/polysat.cpp
View file

@ -1310,9 +1310,6 @@ void tst_polysat() {
test_fi::randomized();
return;
test_polysat::test_ineq_axiom1(32, 2); // crashes
return;
// looks like a fishy conflict lemma?
test_polysat::test_monot_bounds();
return;
@ -1433,6 +1430,7 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
VERIFY(parse_smt2_commands(ctx, is));
ptr_vector<expr> fmls = ctx.assertions();
polysat::scoped_solver s("polysat");
s.set_max_conflicts(1000);
g_solver = &s;
polysat::internalize(m, s, fmls);
std::cout << "checking\n";