mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

work on ashr

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-15 14:30:13 -08:00
parent 78f64cda1c
commit a315c7c47a
3 changed files with 30 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/constraints.h
View file

@ -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)); }

39
src/sat/smt/polysat/op_constraint.cpp
View file

@ -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();
}

1
src/sat/smt/polysat/op_constraint.h
View file

@ -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 {}