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

removing unit clauses and dependency manager, use minisat approach by tracking assumption literals directly also in clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-20 15:10:03 -07:00
parent bb5ff8db24
commit 8ee54c665a
12 changed files with 60 additions and 179 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -23,6 +23,7 @@ namespace polysat {
m_value.push_back(l_undef);
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_watch.push_back({});
@ -37,6 +38,7 @@ namespace polysat {
SASSERT_EQ(m_value[2*var+1], l_undef);
SASSERT_EQ(m_reason[var], nullptr);
SASSERT_EQ(m_lemma[var], nullptr);
SASSERT_EQ(m_deps[var], null_dependency);
}
m_free_vars.mk_var_eh(var);
return var;
@ -50,6 +52,7 @@ namespace polysat {
m_level[var] = UINT_MAX;
m_reason[var] = nullptr;
m_lemma[var] = nullptr;
m_deps[var] = null_dependency;
m_watch[lit.index()].reset();
m_watch[(~lit).index()].reset();
m_free_vars.del_var_eh(var);
@ -57,13 +60,14 @@ namespace polysat {
// m_unused.push_back(var);
}
void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma) {
void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep) {
SASSERT(!is_assigned(lit));
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_deps[lit.var()] = dep;
m_free_vars.del_var_eh(lit.var());
}
@ -74,6 +78,7 @@ namespace polysat {
m_level[lit.var()] = UINT_MAX;
m_reason[lit.var()] = nullptr;
m_lemma[lit.var()] = nullptr;
m_deps[lit.var()] = null_dependency;
m_free_vars.unassign_var_eh(lit.var());
}

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

@ -21,12 +21,13 @@ namespace polysat {
class bool_var_manager {
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)
svector<unsigned> m_level; // level of assignment (indexed by variable)
unsigned_vector m_level; // level of assignment (indexed by variable)
unsigned_vector m_deps; // dependencies of external asserts
unsigned_vector m_activity; //
svector<clause*> m_reason; // propagation reason, NULL for decisions (indexed by variable)
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
svector<clause*> m_lemma;
ptr_vector<clause> m_lemma;
var_queue m_free_vars; // free Boolean variables
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
@ -68,7 +69,7 @@ namespace polysat {
void dec_activity(sat::literal lit) { m_activity[lit.var()] /= 2; }
/// Set the given literal to true
void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma);
void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep = null_dependency);
void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const;

16
src/math/polysat/clause.cpp
View file

@ -17,15 +17,15 @@ Author:
namespace polysat {
clause_ref clause::from_unit(unsigned lvl, signed_constraint c, p_dependency_ref d) {
clause_ref clause::from_unit(signed_constraint c) {
SASSERT(c->has_bvar());
sat::literal_vector lits;
lits.push_back(c.blit());
return clause::from_literals(lvl, std::move(d), std::move(lits));
return clause::from_literals(std::move(lits));
}
clause_ref clause::from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals) {
return alloc(clause, lvl, std::move(d), std::move(literals));
clause_ref clause::from_literals(sat::literal_vector literals) {
return alloc(clause, std::move(literals));
}
bool clause::is_always_false(solver& s) const {
@ -51,14 +51,6 @@ namespace polysat {
out << " \\/ ";
out << lit;
}
if (m_dep) {
ptr_vector<p_dependency> todo;
todo.push_back(m_dep.get());
vector<unsigned, false> vs;
poly_dep_manager::linearize_todo(todo, vs);
out << " deps ...";
// out << "| " << vs;
}
return out;
}

12
src/math/polysat/clause.h
View file

@ -33,9 +33,7 @@ namespace polysat {
friend class constraint_manager;
unsigned m_ref_count = 0; // TODO: remove refcount once we confirm it's not needed anymore
unsigned m_level;
pvar m_justified_var = null_var; // The variable that was restricted by learning this lemma.
p_dependency_ref m_dep;
bool m_redundant = false;
sat::literal_vector m_literals;
@ -49,8 +47,8 @@ namespace polysat {
}
*/
clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals):
m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)) {
clause(sat::literal_vector literals):
m_literals(std::move(literals)) {
SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
}
@ -58,11 +56,9 @@ namespace polysat {
void inc_ref() { m_ref_count++; }
void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
static clause_ref from_unit(unsigned lvl, signed_constraint c, p_dependency_ref d);
static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals);
static clause_ref from_unit(signed_constraint c);
static clause_ref from_literals(sat::literal_vector literals);
p_dependency* dep() const { return m_dep; }
unsigned level() const { return m_level; }
pvar justified_var() const { return m_justified_var; }
void set_justified_var(pvar v) { SASSERT(m_justified_var == null_var); m_justified_var = v; }

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

@ -23,26 +23,20 @@ namespace polysat {
static_assert(std::is_move_constructible_v<clause_builder>);
clause_builder::clause_builder(solver& s):
m_solver(&s), m_dep(nullptr, s.m_dm)
m_solver(&s)
{}
void clause_builder::reset() {
m_literals.reset();
m_level = 0;
m_dep = nullptr;
SASSERT(empty());
}
clause_ref clause_builder::build() {
clause_ref cl = clause::from_literals(m_level, std::move(m_dep), std::move(m_literals));
m_level = 0;
clause_ref cl = clause::from_literals(std::move(m_literals));
SASSERT(empty());
return cl;
}
void clause_builder::add_dependency(p_dependency* d) {
m_dep = m_solver->m_dm.mk_join(m_dep, d);
}
void clause_builder::push(sat::literal lit) {
push(m_solver->m_constraints.lookup(lit));
@ -53,8 +47,6 @@ namespace polysat {
SASSERT(c->has_bvar());
SASSERT(!c.is_always_true()); // clause would be a tautology
if (c->unit_clause()) {
add_dependency(c->unit_dep());
m_level = std::max(m_level, c->unit_clause()->level());
return;
}
m_literals.push_back(c.blit());

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

@ -26,8 +26,6 @@ namespace polysat {
class clause_builder {
solver* m_solver;
sat::literal_vector m_literals;
p_dependency_ref m_dep;
unsigned m_level = 0;
public:
clause_builder(solver& s);
@ -36,21 +34,17 @@ namespace polysat {
clause_builder& operator=(clause_builder const& s) = delete;
clause_builder& operator=(clause_builder&& s) = default;
bool empty() const { return m_literals.empty() && m_dep == nullptr && m_level == 0; }
bool empty() const { return m_literals.empty(); }
void reset();
unsigned level() const { return m_level; }
/// Build the clause. This will reset the clause builder so it can be reused.
clause_ref build();
void add_dependency(p_dependency* d);
void push(sat::literal lit);
void push(signed_constraint c);
void push(inequality const& i) {
push(i.as_signed_constraint());
}
void push(inequality const& i) { push(i.as_signed_constraint()); }
/// Push a new constraint. Allocates a boolean variable for the constraint, if necessary.
void push_new(signed_constraint c);

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

@ -56,39 +56,12 @@ namespace polysat {
}
void constraint_manager::store(clause* cl, solver& s) {
while (m_clauses.size() <= cl->level())
while (m_clauses.size() <= s.base_level())
m_clauses.push_back({});
m_clauses[cl->level()].push_back(cl);
m_clauses[s.base_level()].push_back(cl);
watch(*cl, s);
}
void constraint_manager::register_external(signed_constraint c) {
SASSERT(c);
SASSERT(!c->is_external());
if (c->unit_dep() && c->unit_dep()->is_leaf()) {
unsigned const dep = c->unit_dep()->leaf_value();
SASSERT(!m_external_constraints.contains(dep));
m_external_constraints.insert(dep, c.get());
}
c->set_external(c.is_negative());
++m_num_external;
}
void constraint_manager::unregister_external(constraint* c) {
if (c->unit_dep() && c->unit_dep()->is_leaf())
m_external_constraints.remove(c->unit_dep()->leaf_value());
c->unset_external();
--m_num_external;
}
signed_constraint constraint_manager::lookup_external(unsigned dep) const {
constraint* c = m_external_constraints.get(dep, nullptr);
if (c)
return {c, !c->external_sign()};
else
return {};
}
// Release constraints at the given level and above.
void constraint_manager::release_level(unsigned lvl) {
for (unsigned l = m_clauses.size(); l-- > lvl; ) {
@ -292,14 +265,14 @@ namespace polysat {
void constraint::set_unit_clause(clause *cl) {
// can be seen as a cache... store the lowest-level unit clause for this constraint.
if (!cl || !m_unit_clause || m_unit_clause->level() > cl->level())
if (!cl || !m_unit_clause)
m_unit_clause = cl;
}
unsigned constraint::level(solver& s) const {
if (s.m_bvars.value(sat::literal(bvar())) != l_undef)
return s.m_bvars.level(bvar());
unsigned level = 0;
unsigned level = s.base_level();
for (auto v : vars())
if (s.is_assigned(v))
level = std::max(level, s.get_level(v));

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

@ -77,11 +77,6 @@ namespace polysat {
void store(clause* cl, solver& s);
/// Register a unit clause with an external dependency.
void register_external(signed_constraint c);
void unregister_external(constraint* c);
signed_constraint lookup_external(unsigned dep) const;
/// Release clauses at the given level and above.
void release_level(unsigned lvl);
@ -185,7 +180,6 @@ namespace polysat {
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl);
p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
void set_external(bool sign) { m_external_sign = to_lbool(sign); }
void unset_external() { m_external_sign = l_undef; }

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

@ -37,7 +37,6 @@ namespace polysat {
solver::solver(reslimit& lim):
m_lim(lim),
m_viable(*this),
m_dm(m_value_manager, m_alloc),
m_linear_solver(*this),
m_conflict(*this),
m_bvars(),
@ -110,53 +109,31 @@ namespace polysat {
m_free_pvars.del_var_eh(v);
}
void solver::ext_constraint(signed_constraint c, unsigned dep, bool activate) {
VERIFY(at_base_level());
void solver::assign_eh(signed_constraint c, unsigned dep) {
SASSERT(at_base_level());
SASSERT(c);
SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later.
if (is_conflict())
return; // no need to do anything if we already have a conflict at base level
m_constraints.ensure_bvar(c.get());
clause_ref unit = clause::from_unit(m_level, c, mk_dep_ref(dep));
clause_ref unit = clause::from_unit(c);
m_constraints.store(unit.get(), *this);
c->set_unit_clause(unit.get());
if (dep != null_dependency && !c->is_external()) {
m_constraints.register_external(c);
m_trail.push_back(trail_instr_t::ext_constraint_i);
m_ext_constraint_trail.push_back(c.get());
}
LOG("New constraint: " << c);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c.get());
#endif
if (activate)
assert_ext_constraint(c);
(void) dep; // dependencies go into justification
assign_bool(m_level, c.blit(), c->unit_clause(), nullptr);
#if 0
// just add them as axioms, tracked by dependencies
literal lit = c.blit();
m_bvars.assign(lit, m_level, nullptr, nullptr, dep);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
#endif
}
void solver::assign_eh(unsigned dep, bool is_true) {
VERIFY(at_base_level());
if (is_conflict())
return; // no need to do anything if we already have a conflict at base level
signed_constraint c = m_constraints.lookup_external(dep);
if (!c) {
LOG("WARN: there is no constraint for dependency " << dep);
return;
}
assert_ext_constraint(is_true ? c : ~c);
}
void solver::assert_ext_constraint(signed_constraint c) {
SASSERT(at_base_level());
SASSERT(!is_conflict());
SASSERT(c->unit_clause());
if (c.bvalue(*this) == l_false)
m_conflict.set(~c); // we already added ~c => conflict
else if (c.is_always_false())
m_conflict.set(c);
else
assign_bool(m_level, c.blit(), c->unit_clause(), nullptr);
}
bool solver::can_propagate() {
return m_qhead < m_search.size() && !is_conflict();
@ -319,12 +296,6 @@ namespace polysat {
m_cjust_trail.pop_back();
break;
}
case trail_instr_t::ext_constraint_i: {
constraint* c = m_ext_constraint_trail.back();
m_constraints.unregister_external(c);
m_ext_constraint_trail.pop_back();
break;
}
default:
UNREACHABLE();
}
@ -699,7 +670,7 @@ namespace polysat {
}
unsigned solver::level(clause const& cl) {
unsigned lvl = 0;
unsigned lvl = base_level();
for (auto lit : cl) {
auto c = lit2cnstr(lit);
if (m_bvars.is_false(lit) || c.is_currently_false(*this))

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

@ -69,9 +69,6 @@ namespace polysat {
params_ref m_params;
viable m_viable; // viable sets per variable
scoped_ptr_vector<dd::pdd_manager> m_pdd;
dep_value_manager m_value_manager;
small_object_allocator m_alloc;
poly_dep_manager m_dm;
linear_solver m_linear_solver;
conflict m_conflict;
bool_var_manager m_bvars; // Map boolean variables to constraints
@ -105,7 +102,6 @@ namespace polysat {
svector<trail_instr_t> m_trail;
unsigned_vector m_qhead_trail;
unsigned_vector m_cjust_trail;
ptr_vector<constraint> m_ext_constraint_trail;
unsigned_vector m_base_levels; // External clients can push/pop scope.
@ -183,9 +179,6 @@ namespace polysat {
void narrow(pvar v);
void linear_propagate();
p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
p_dependency_ref mk_dep_ref(unsigned dep) { return p_dependency_ref(mk_dep(dep), m_dm); }
/// Evaluate term under the current assignment.
bool try_eval(pdd const& p, rational& out_value) const;
@ -204,20 +197,9 @@ namespace polysat {
void backjump(unsigned new_level);
void add_lemma(clause& lemma);
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); }
signed_constraint eq(pdd const& p, pdd const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
signed_constraint ult(pdd const& p, pdd const& q) { return m_constraints.ult(p, q); }
signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
void ext_constraint(signed_constraint c, unsigned dep, bool activate);
void assert_constraint(signed_constraint c, unsigned dep);
static void insert_constraint(signed_constraints& cs, signed_constraint c);
void assert_ext_constraint(signed_constraint c);
bool inc() { return m_lim.inc(); }
@ -277,24 +259,25 @@ namespace polysat {
unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
/**
* Create polynomial constraints (but do not activate them).
* Each constraint is tracked by a dependency.
*/
void new_eq(pdd const& p, unsigned dep) { ext_constraint(eq(p), dep, false); }
void new_diseq(pdd const& p, unsigned dep) { ext_constraint(diseq(p), dep, false); }
void new_ule(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(ule(p, q), dep, false); }
void new_ult(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(ult(p, q), dep, false); }
void new_sle(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(sle(p, q), dep, false); }
void new_slt(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(slt(p, q), dep, false); }
/** Create constraints */
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); }
signed_constraint eq(pdd const& p, pdd const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
signed_constraint ult(pdd const& p, pdd const& q) { return m_constraints.ult(p, q); }
signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
/** Create and activate polynomial constraints. */
void add_eq(pdd const& p, unsigned dep = null_dependency) { ext_constraint(eq(p), dep, true); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { ext_constraint(diseq(p), dep, true); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(ule(p, q), dep, true); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(ult(p, q), dep, true); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(sle(p, q), dep, true); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(slt(p, q), dep, true); }
void add_eq(pdd const& p, unsigned dep = null_dependency) { assign_eh(eq(p), dep); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { assign_eh(diseq(p), dep); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ule(p, q), dep); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(ult(p, q), dep); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(sle(p, q), dep); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(slt(p, q), dep); }
void add_ule(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
void add_ule(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
@ -309,7 +292,7 @@ namespace polysat {
* Activate the constraint corresponding to the given boolean variable.
* Note: to deactivate, use push/pop.
*/
void assign_eh(unsigned dep, bool is_true);
void assign_eh(signed_constraint c, unsigned dep);
/**
* main state transitions.

3
src/math/polysat/trail.h
View file

@ -23,8 +23,7 @@ namespace polysat {
viable_i,
assign_i,
just_i,
assign_bool_i,
ext_constraint_i
assign_bool_i
};

19
src/math/polysat/types.h
View file

@ -11,7 +11,6 @@ Author:
--*/
#pragma once
#include "util/dependency.h"
#include "util/trail.h"
#include "util/lbool.h"
#include "util/map.h"
@ -34,22 +33,4 @@ namespace polysat {
const unsigned null_dependency = UINT_MAX;
const pvar null_var = UINT_MAX;
struct dep_value_manager {
void inc_ref(unsigned) {}
void dec_ref(unsigned) {}
};
struct dep_config {
typedef dep_value_manager value_manager;
typedef unsigned value;
typedef small_object_allocator allocator;
static const bool ref_count = false;
};
typedef dependency_manager<dep_config> poly_dep_manager;
typedef poly_dep_manager::dependency p_dependency;
typedef obj_ref<p_dependency, poly_dep_manager> p_dependency_ref;
typedef ref_vector<p_dependency, poly_dep_manager> p_dependency_refv;
}