From 09b3d99db17698b59ef9bb30f6d218cc9ea65cd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 31 Dec 2023 17:09:49 -0800 Subject: [PATCH] tidy Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/op_constraint.cpp | 18 ++++-------------- src/sat/smt/polysat/umul_ovfl_constraint.cpp | 4 ++-- 2 files changed, 6 insertions(+), 16 deletions(-) diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index bfab8da95..4123ada2a 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -9,14 +9,6 @@ Author: Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09 -Notes: - -Additional possible functionality on constraints: - -- bit-wise assignments - narrow based on bit assignment, not entire word assignment. -- integration with congruence tables -- integration with conflict resolution - --*/ #include "util/log.h" @@ -428,12 +420,10 @@ namespace polysat { unsigned k = qv.val().get_unsigned(); // q = k -> r[i+k] = p[i] for 0 <= i < N - k for (unsigned i = 0; i < N - k; ++i) { - if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) { - c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true); - } - if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) { - c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true); - } + if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) + c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true); + else if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) + c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true); } } else { diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.cpp b/src/sat/smt/polysat/umul_ovfl_constraint.cpp index 619b820f4..e7991952f 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.cpp +++ b/src/sat/smt/polysat/umul_ovfl_constraint.cpp @@ -138,7 +138,7 @@ namespace polysat { SASSERT(p_bound * q_bound >= M); SASSERT(p_bound * (q_bound - 1) < M); // LOG("p_bound: " << p.manager().mk_val(p_bound)); - c.add_axiom("~Ovfl(p, q) & p <= p_bound ==> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, false); + c.add_axiom("~Ovfl(p, q) & p <= p_bound -> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, true); } else { // Find lowest bound for p such that q_bound is still correct. @@ -148,7 +148,7 @@ namespace polysat { SASSERT(p_bound * q_bound >= M); SASSERT(p_bound * (q_bound - 1) < M); // LOG("p_bound: " << p.manager().mk_val(p_bound)); - c.add_axiom("~Ovfl(p, q) & p >= p_bound ==> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, false); + c.add_axiom("~Ovfl(p, q) & p >= p_bound -> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, true); } return true; }