From 645f190e35e1b1cff19140403a7ab1a3e31a80a4 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jan 2022 11:44:01 +0100 Subject: [PATCH] Add wrapper for external dependencies to prevent accidental conversions --- src/math/polysat/boolean.cpp | 4 ++-- src/math/polysat/boolean.h | 8 +++---- src/math/polysat/solver.cpp | 4 ++-- src/math/polysat/solver.h | 44 ++++++++++++++++++------------------ src/math/polysat/types.h | 26 ++++++++++++++++++--- src/test/polysat.cpp | 8 +++---- 6 files changed, 57 insertions(+), 37 deletions(-) diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 253be8fad..7a9e46a09 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -78,13 +78,13 @@ namespace polysat { 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); assign(kind_t::decision, lit, lvl, nullptr, dep); 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(k != kind_t::unassigned); m_value[lit.index()] = l_true; diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index 7cb7de457..2ef826779 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -29,7 +29,7 @@ namespace polysat { svector m_unused; // previously deleted variables that can be reused by new_var(); svector 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 + dependency_vector m_deps; // dependencies of external asserts unsigned_vector m_activity; // svector m_kind; // decision or propagation? // Clause associated with the assignment (indexed by variable): @@ -40,7 +40,7 @@ namespace polysat { var_queue m_free_vars; // free Boolean variables vector> 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: @@ -66,7 +66,7 @@ namespace polysat { 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::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]; } @@ -83,7 +83,7 @@ namespace polysat { void propagate(sat::literal lit, unsigned lvl, clause& reason); 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 asserted(sat::literal lit, unsigned lvl, dependency dep); void unassign(sat::literal lit); std::ostream& display(std::ostream& out) const; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index e3d351d64..f30786215 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -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(c); if (is_conflict()) @@ -592,7 +592,7 @@ namespace polysat { SASSERT(!m_conflict.empty()); } - void solver::unsat_core(unsigned_vector& deps) { + void solver::unsat_core(dependency_vector& deps) { deps.reset(); for (auto c : m_conflict) { auto d = m_bvars.dep(c.blit()); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 1d676ca22..87a4f2ec6 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -255,7 +255,7 @@ namespace polysat { /** * retrieve unsat core dependencies */ - void unsat_core(unsigned_vector& deps); + void unsat_core(dependency_vector& deps); /** * 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); } /** Create and activate polynomial constraints. */ - 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_noovfl(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, unsigned dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); } + void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(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, dependency dep = null_dependency) { assign_eh(ule(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, dependency dep = null_dependency) { assign_eh(sle(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, dependency 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(rational const& p, pdd const& q, unsigned 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(unsigned p, pdd const& q, unsigned 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(rational const& p, pdd const& q, unsigned 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(unsigned p, pdd const& q, unsigned 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(rational const& p, pdd const& q, unsigned 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(unsigned p, pdd const& q, unsigned dep = null_dependency) { add_noovfl(q, p, 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, dependency dep = null_dependency) { add_ule(q.manager().mk_val(p), 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, dependency dep = null_dependency) { add_ule(rational(p), 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, dependency dep = null_dependency) { add_ult(q.manager().mk_val(p), 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, dependency dep = null_dependency) { add_ult(rational(p), 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, dependency dep = null_dependency) { add_noovfl(q, p, 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, dependency dep = null_dependency) { add_noovfl(q, p, dep); } /** * Activate the constraint corresponding to the given boolean variable. * 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. diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 0a5cd24b4..e3c08434d 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -28,9 +28,29 @@ namespace polysat { typedef dd::pdd pdd; typedef dd::bdd bdd; typedef dd::bddv bddv; - typedef unsigned pvar; - const unsigned null_dependency = UINT_MAX; - const pvar null_var = UINT_MAX; + typedef unsigned pvar; + 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_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; + } } diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 0d79452d4..7b5082bbf 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1014,11 +1014,11 @@ public: auto idx = s.var(s.add_var(bw)); auto second = 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_noovfl(q, idx); s.add_ult(first, second); - s.add_diseq(idx, 0); + s.add_diseq(idx); s.add_ule(second - first, q); s.add_noovfl(second - first, idx); s.check(); @@ -1074,8 +1074,8 @@ public: auto a = s.var(s.add_var(256)); auto b = s.var(s.add_var(256)); auto c = s.var(s.add_var(256)); - s.add_eq(a, 0); - s.add_eq(c, 0); // add c to prevent simplification by leading coefficient + s.add_eq(a); + s.add_eq(c); // add c to prevent simplification by leading coefficient s.add_eq(4*a - 123456789*b + c); s.check(); s.expect_sat({{a, 0}, {b, 0}});