From d0b03a15269fb20b173ca110ad5c1d8735ec5c5d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 14:30:13 -0800 Subject: [PATCH] work on ashr Signed-off-by: Nikolaj Bjorner --- src/sat/smt/polysat/constraints.h | 4 +++ src/sat/smt/polysat/op_constraint.cpp | 39 +++++++++++++++++---------- src/sat/smt/polysat/op_constraint.h | 1 + 3 files changed, 30 insertions(+), 14 deletions(-) diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 47c9beb49..fa2b62c11 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -119,6 +119,7 @@ namespace polysat { signed_constraint uge(pdd const& p, pdd const& q) { return ule(q, p); } signed_constraint uge(pdd const& p, rational const& q) { return ule(q, p); } + signed_constraint uge(pdd const& p, int q) { return ule(q, p); } signed_constraint ult(pdd const& p, rational const& q) { return ult(p, p.manager().mk_val(q)); } signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); } @@ -141,6 +142,9 @@ namespace polysat { signed_constraint sgt(int p, pdd const& q) { return slt(q, p); } signed_constraint sgt(unsigned p, pdd const& q) { return slt(q, p); } + signed_constraint sge(pdd const& p, pdd const& q) { return ~slt(q, p); } + signed_constraint sge(pdd const& p, int q) { return ~slt(q, p); } + signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); } signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); } signed_constraint umul_ovfl(pdd const& p, int q) { return umul_ovfl(p, rational(q)); } diff --git a/src/sat/smt/polysat/op_constraint.cpp b/src/sat/smt/polysat/op_constraint.cpp index 175d3a145..666d950a9 100644 --- a/src/sat/smt/polysat/op_constraint.cpp +++ b/src/sat/smt/polysat/op_constraint.cpp @@ -203,6 +203,9 @@ namespace polysat { case code::and_op: activate_and(c, dep); break; + case code::ashr_op: + activate_ashr(c, dep); + break; default: break; } @@ -309,6 +312,28 @@ namespace polysat { } } + void op_constraint::activate_ashr(core& c, dependency const& d) { + // + // if q = k & p >= 0 -> r*2^k + + // if q = k & p < 0 -> (p / 2^k) - 1 + 2^{N-k} + // + + auto& m = p.manager(); + auto const pv = c.subst(p); + auto const qv = c.subst(q); + auto const rv = c.subst(r); + unsigned const N = m.power_of_2(); + + auto& C = c.cs(); + c.add_clause("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, true); + c.add_clause("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, true); + c.add_clause("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, true); + for (unsigned k = 0; k < N; ++k) { +// c.add_clause("q = k & p >= 0 -> p << q = p / 2^k", {~C.eq(q, k), ~C.sge(p, 0), ... }, true); +// c.add_clause("q = k & p < 0 -> p << q = (p / 2^k) -1 + 2^{N-k}", {~C.eq(q, k), ~C.slt(p, 0), ... }, true); + } + } + void op_constraint::activate_and(core& c, dependency const& d) { auto x = p, y = q; @@ -336,21 +361,7 @@ namespace polysat { } void op_constraint::propagate_ashr(core& c, dependency const& dep) { - // - // ashr(x, y) - // if q >= N & p < 0 -> -1 - // if q >= N & p >= 0 -> 0 - // if q = k & p >= 0 -> p / 2^k - // if q = k & p < 0 -> (p / 2^k) - 1 + 2^{N-k} - // - auto& m = p.manager(); - auto const pv = c.subst(p); - auto const qv = c.subst(q); - auto const rv = c.subst(r); - unsigned const N = m.power_of_2(); - - NOT_IMPLEMENTED_YET(); } diff --git a/src/sat/smt/polysat/op_constraint.h b/src/sat/smt/polysat/op_constraint.h index c5400fbab..4b44b3009 100644 --- a/src/sat/smt/polysat/op_constraint.h +++ b/src/sat/smt/polysat/op_constraint.h @@ -68,6 +68,7 @@ namespace polysat { std::ostream& display(std::ostream& out, char const* eq) const; void activate_and(core& s, dependency const& d); + void activate_ashr(core& s, dependency const& d); public: ~op_constraint() override {}