From d7548f6867eb74bdebd34af0ddd8e6b7f9551ab7 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 26 Jan 2022 11:50:49 +0100 Subject: [PATCH] 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}});