From cbed3bfde4bb2b42902d4c862b476aec7e3aa636 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jan 2022 11:08:03 +0100 Subject: [PATCH 1/3] fi: match_non_zero_linear --- src/math/polysat/forbidden_intervals.cpp | 55 +++++++++++++++++++++--- src/math/polysat/forbidden_intervals.h | 5 +++ 2 files changed, 53 insertions(+), 7 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 9586b820d..63b97ed5b 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -55,14 +55,7 @@ namespace polysat { _backtrack.released = true; - - // a*v <= 0, a odd - if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi)) - return true; - // v > q - // 2^k*a*v + b > 0 - // TODO: is !ok2 required? if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi)) return true; @@ -77,6 +70,14 @@ namespace polysat { SASSERT(b1.is_val()); SASSERT(b2.is_val()); + // a*v <= 0, a odd + if (match_zero(c, a1, b1, e1, a2, b2, e2, fi)) + return true; + + // a*v + b > 0, a odd + if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi)) + return true; + if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi)) @@ -271,6 +272,10 @@ namespace polysat { /** * a*v <= 0, a odd * forbidden interval for v is [1,0[ + * + * TODO: extend to + * 2^k*a*v <= 0, a odd + * (using periodic intervals?) */ bool forbidden_intervals::match_zero( signed_constraint const& c, @@ -294,6 +299,42 @@ namespace polysat { return false; } + /** + * a*v + b > 0, a odd + * + * TODO: extend to + * 2^k*a*v + b > 0, a odd + * (using periodic intervals?) + */ + bool forbidden_intervals::match_non_zero_linear( + signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi) { + if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) { + // a*v + b > 0 + // <=> a*v + b != 0 + // <=> v + a^-1 * b != 0 + // <=> v != - a^-1 * b + auto& m = e1.manager(); + rational const& mod_value = m.two_to_N(); + rational a1_inv; + VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv)); + rational lo_val(mod(-b1.val() * a1_inv, mod_value)); + auto lo = -e1 * a1_inv; + rational hi_val(mod(lo_val + 1, mod_value)); + auto hi = lo + 1; + fi.coeff = 1; + fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val); + if (b1 != e1) + fi.side_cond.push_back(s.eq(b1, e1)); + if (b2 != e2) + fi.side_cond.push_back(s.eq(b2, e2)); + return true; + } + return false; + } + /** * v > q * forbidden interval for v is [0,1[ diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 4b8dc2d3e..2d88216d3 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -57,6 +57,11 @@ namespace polysat { rational const & a2, pdd const& b2, pdd const& e2, fi_record& fi); + bool match_non_zero_linear(signed_constraint const& c, + rational const & a1, pdd const& b1, pdd const& e1, + rational const & a2, pdd const& b2, pdd const& e2, + fi_record& fi); + bool match_non_zero(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, fi_record& fi); From 645f190e35e1b1cff19140403a7ab1a3e31a80a4 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jan 2022 11:44:01 +0100 Subject: [PATCH 2/3] 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}}); From d7548f6867eb74bdebd34af0ddd8e6b7f9551ab7 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jan 2022 11:50:49 +0100 Subject: [PATCH 3/3] Now we can have a working binary add_eq/add_diseq --- src/math/polysat/solver.h | 47 ++++++++++++++++++++++----------------- src/test/polysat.cpp | 8 +++---- 2 files changed, 31 insertions(+), 24 deletions(-) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 87a4f2ec6..c23445560 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -310,6 +310,7 @@ namespace polysat { signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); } signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); } signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); } + signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); } signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); } signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); } @@ -325,27 +326,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, 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_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); } + void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_eq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } + void add_diseq(pdd const& p, dependency dep = null_dependency) { assign_eh(diseq(p), dep); } + void add_diseq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); } + void add_diseq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); } + void add_diseq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(diseq(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, 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, 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); } + 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. diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 7b5082bbf..0d79452d4 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); + s.add_diseq(idx, 0); 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); - s.add_eq(c); // add c to prevent simplification by leading coefficient + s.add_eq(a, 0); + s.add_eq(c, 0); // 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}});