mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

Add wrapper for external dependencies to prevent accidental conversions

Browse source
This commit is contained in:
Jakob Rath 2022-01-26 11:44:01 +01:00
parent cbed3bfde4
commit 645f190e35
6 changed files with 57 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -78,13 +78,13 @@ namespace polysat {
SASSERT(is_propagation(lit)); SASSERT(is_propagation(lit));
} }
void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) { void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) {
LOG("Asserted " << lit << " @ " << lvl); LOG("Asserted " << lit << " @ " << lvl);
assign(kind_t::decision, lit, lvl, nullptr, dep); assign(kind_t::decision, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit)); SASSERT(is_decision(lit));
} }
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep) { void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {
SASSERT(!is_assigned(lit)); SASSERT(!is_assigned(lit));
SASSERT(k != kind_t::unassigned); SASSERT(k != kind_t::unassigned);
m_value[lit.index()] = l_true; m_value[lit.index()] = l_true;

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

@ -29,7 +29,7 @@ namespace polysat {
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var(); 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<lbool> m_value; // current value (indexed by literal)
unsigned_vector 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 dependency_vector m_deps; // dependencies of external asserts
unsigned_vector m_activity; // unsigned_vector m_activity; //
svector<kind_t> m_kind; // decision or propagation? svector<kind_t> m_kind; // decision or propagation?
// Clause associated with the assignment (indexed by variable): // Clause associated with the assignment (indexed by variable):
@ -40,7 +40,7 @@ namespace polysat {
var_queue m_free_vars; // free Boolean variables var_queue m_free_vars; // free Boolean variables
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep = null_dependency); void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency);
public: public:
@ -66,7 +66,7 @@ namespace polysat {
unsigned level(sat::literal lit) const { return level(lit.var()); } unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; } 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()); } 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()]; } dependency 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_clause[var]; } clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; }
@ -83,7 +83,7 @@ namespace polysat {
void propagate(sat::literal lit, unsigned lvl, clause& reason); 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 eval(sat::literal lit, unsigned lvl);
void asserted(sat::literal lit, unsigned lvl, unsigned dep); void asserted(sat::literal lit, unsigned lvl, dependency dep);
void unassign(sat::literal lit); void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;

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

@ -164,7 +164,7 @@ namespace polysat {
} }
void solver::assign_eh(signed_constraint c, unsigned dep) { void solver::assign_eh(signed_constraint c, dependency dep) {
SASSERT(at_base_level()); SASSERT(at_base_level());
SASSERT(c); SASSERT(c);
if (is_conflict()) if (is_conflict())
@ -592,7 +592,7 @@ namespace polysat {
SASSERT(!m_conflict.empty()); SASSERT(!m_conflict.empty());
} }
void solver::unsat_core(unsigned_vector& deps) { void solver::unsat_core(dependency_vector& deps) {
deps.reset(); deps.reset();
for (auto c : m_conflict) { for (auto c : m_conflict) {
auto d = m_bvars.dep(c.blit()); auto d = m_bvars.dep(c.blit());

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

@ -255,7 +255,7 @@ namespace polysat {
/** /**
* retrieve unsat core dependencies * retrieve unsat core dependencies
*/ */
void unsat_core(unsigned_vector& deps); void unsat_core(dependency_vector& deps);
/** /**
* Add variable with bit-size. * Add variable with bit-size.
@ -325,33 +325,33 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
/** Create and activate polynomial constraints. */ /** Create and activate polynomial constraints. */
void add_eq(pdd const& p, unsigned dep = null_dependency) { assign_eh(eq(p), dep); } void add_eq(pdd const& p, dependency 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_diseq(pdd const& p, dependency 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_ule(pdd const& p, pdd const& q, dependency 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_ult(pdd const& p, pdd const& q, dependency 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_sle(pdd const& p, pdd const& q, dependency 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_slt(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(slt(p, q), dep); }
void add_noovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); } void add_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
void add_ovfl(pdd const& p, pdd const& q, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } void add_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(mul_ovfl(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(pdd const& p, rational const& q, dependency 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); } void add_ule(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
void add_ule(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ule(p, rational(q), dep); } void add_ule(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ule(p, rational(q), dep); }
void add_ule(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ule(rational(p), q, dep); } void add_ule(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ule(rational(p), q, dep); }
void add_ult(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); } void add_ult(pdd const& p, rational const& q, dependency dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); }
void add_ult(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); } void add_ult(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
void add_ult(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_ult(p, rational(q), dep); } void add_ult(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ult(p, rational(q), dep); }
void add_ult(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_ult(rational(p), q, dep); } void add_ult(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ult(rational(p), q, dep); }
void add_noovfl(pdd const& p, rational const& q, unsigned dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); } void add_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
void add_noovfl(rational const& p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } void add_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); }
void add_noovfl(pdd const& p, unsigned q, unsigned dep = null_dependency) { add_noovfl(p, rational(q), dep); } void add_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency) { add_noovfl(p, rational(q), dep); }
void add_noovfl(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, dep); } void add_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); }
/** /**
* Activate the constraint corresponding to the given boolean variable. * Activate the constraint corresponding to the given boolean variable.
* Note: to deactivate, use push/pop. * Note: to deactivate, use push/pop.
*/ */
void assign_eh(signed_constraint c, unsigned dep); void assign_eh(signed_constraint c, dependency dep);
/** /**
* main state transitions. * main state transitions.

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

@ -28,9 +28,29 @@ namespace polysat {
typedef dd::pdd pdd; typedef dd::pdd pdd;
typedef dd::bdd bdd; typedef dd::bdd bdd;
typedef dd::bddv bddv; typedef dd::bddv bddv;
typedef unsigned pvar;
const unsigned null_dependency = UINT_MAX; typedef unsigned pvar;
const pvar null_var = UINT_MAX; inline const pvar null_var = UINT_MAX;
class dependency {
unsigned m_val;
public:
explicit dependency(unsigned val): m_val(val) {}
unsigned val() const { return m_val; }
bool is_null() const { return m_val == UINT_MAX; }
unsigned hash() const { return val(); }
};
inline const dependency null_dependency = dependency(UINT_MAX);
typedef svector<dependency> dependency_vector;
inline bool operator<(dependency const& d1, dependency const& d2) { return d1.val() < d2.val(); }
inline bool operator==(dependency const& d1, dependency const& d2) { return d1.val() == d2.val(); }
inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); }
inline std::ostream& operator<<(std::ostream& out, dependency const& d) {
out << "dep(" << d.val() << ")";
return out;
}
} }

8
src/test/polysat.cpp
View file

@ -1014,11 +1014,11 @@ public:
auto idx = s.var(s.add_var(bw)); auto idx = s.var(s.add_var(bw));
auto second = s.var(s.add_var(bw)); auto second = s.var(s.add_var(bw));
auto first = s.var(s.add_var(bw)); auto first = s.var(s.add_var(bw));
s.add_eq(q*idx + r, UINT_MAX); s.add_eq(q*idx + r - UINT_MAX);
s.add_ult(r, idx); s.add_ult(r, idx);
s.add_noovfl(q, idx); s.add_noovfl(q, idx);
s.add_ult(first, second); s.add_ult(first, second);
s.add_diseq(idx, 0); s.add_diseq(idx);
s.add_ule(second - first, q); s.add_ule(second - first, q);
s.add_noovfl(second - first, idx); s.add_noovfl(second - first, idx);
s.check(); s.check();
@ -1074,8 +1074,8 @@ public:
auto a = s.var(s.add_var(256)); auto a = s.var(s.add_var(256));
auto b = s.var(s.add_var(256)); auto b = s.var(s.add_var(256));
auto c = s.var(s.add_var(256)); auto c = s.var(s.add_var(256));
s.add_eq(a, 0); s.add_eq(a);
s.add_eq(c, 0); // add c to prevent simplification by leading coefficient s.add_eq(c); // add c to prevent simplification by leading coefficient
s.add_eq(4*a - 123456789*b + c); s.add_eq(4*a - 123456789*b + c);
s.check(); s.check();
s.expect_sat({{a, 0}, {b, 0}}); s.expect_sat({{a, 0}, {b, 0}});