mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

umul

Browse source
This commit is contained in:
Jakob Rath 2022-07-21 11:57:27 +02:00
parent 8d871bf8b5
commit d4592f2abf
5 changed files with 32 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/saturation.cpp
View file

@ -183,7 +183,7 @@ namespace polysat {
} }
void inf_saturate::push_omega(pdd const& x, pdd const& y) { void inf_saturate::push_omega(pdd const& x, pdd const& y) {
m_new_constraints.insert(~s.mul_ovfl(x, y)); m_new_constraints.insert(~s.umul_ovfl(x, y));
/* /*
// determine worst case upper bounds for x, y // determine worst case upper bounds for x, y
// then extract premises for a non-worst-case bound. // then extract premises for a non-worst-case bound.

16
src/math/polysat/smul_fl_constraint.cpp
View file

@ -80,13 +80,13 @@ namespace polysat {
s.add_clause(~sc, s.ule(2, q()), false); s.add_clause(~sc, s.ule(2, q()), false);
s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(q(), 0), false); s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(q(), 0), false);
s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p(), 0), false); s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p(), 0), false);
s.add_clause(~sc, ~s.sgt(p(), 0), s.slt(p()*q(), 0), s.mul_ovfl(p(), q()), false); s.add_clause(~sc, ~s.sgt(p(), 0), s.slt(p()*q(), 0), s.umul_ovfl(p(), q()), false);
s.add_clause(~sc, s.sgt(p(), 0), s.slt(p()*q(), 0), s.mul_ovfl(-p(), -q()), false); s.add_clause(~sc, s.sgt(p(), 0), s.slt(p()*q(), 0), s.umul_ovfl(-p(), -q()), false);
} }
else { else {
s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.mul_ovfl(p(), q()), false); s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.umul_ovfl(p(), q()), false);
s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.slt(p()*q(), 0), false); s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), ~s.slt(p()*q(), 0), false);
s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.mul_ovfl(-p(), -q()), false); s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.umul_ovfl(-p(), -q()), false);
s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.slt((-p())*(-q()), 0), false); s.add_clause(~sc, ~s.slt(p(), 0), ~s.slt(q(), 0), ~s.slt((-p())*(-q()), 0), false);
} }
} }
@ -96,13 +96,13 @@ namespace polysat {
s.add_clause(~sc, s.ule(2, q()), false); s.add_clause(~sc, s.ule(2, q()), false);
s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), false); s.add_clause(~sc, ~s.sgt(p(), 0), ~s.sgt(q(), 0), false);
s.add_clause(~sc, s.sgt(q(), 0), s.sgt(p(), 0), false); s.add_clause(~sc, s.sgt(q(), 0), s.sgt(p(), 0), false);
s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(p(), -q()), false); s.add_clause(~sc, ~s.sgt(p(), 0), s.sgt(p()*q(), 0), s.umul_ovfl(p(), -q()), false);
s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p()*q(), 0), s.mul_ovfl(-p(), q()), false); s.add_clause(~sc, ~s.sgt(q(), 0), s.sgt(p()*q(), 0), s.umul_ovfl(-p(), q()), false);
} }
else { else {
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.mul_ovfl(p(), -q()), false); s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.umul_ovfl(p(), -q()), false);
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false); s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false);
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.mul_ovfl(-p(), q()), false); s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.umul_ovfl(-p(), q()), false);
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false); s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
} }
} }

2
src/math/polysat/solver.cpp
View file

@ -150,7 +150,7 @@ namespace polysat {
// b ≠ 0 ==> r < b // b ≠ 0 ==> r < b
// b = 0 ==> q = -1 // b = 0 ==> q = -1
add_eq(a, b * q + r); add_eq(a, b * q + r);
add_noovfl(b, q); add_umul_noovfl(b, q);
add_ule(r, b*q+r); add_ule(r, b*q+r);
auto c_eq = eq(b); auto c_eq = eq(b);

42
src/math/polysat/solver.h
View file

@ -264,6 +264,18 @@ namespace polysat {
*/ */
void unsat_core(dependency_vector& deps); void unsat_core(dependency_vector& deps);
/**
* Return value / level of v in the current model (only meaningful if check_sat() returned l_true).
*/
rational get_value(pvar v) const { SASSERT(is_assigned(v)); return m_value[v]; }
unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
/**
* Evaluate term under the current assignment.
*/
bool try_eval(pdd const& p, rational& out_value) const;
/** /**
* Add variable with bit-size. * Add variable with bit-size.
*/ */
@ -301,25 +313,11 @@ namespace polysat {
*/ */
pdd value(rational const& v, unsigned sz); pdd value(rational const& v, unsigned sz);
/**
* Return value / level of v in the current model (only meaningful if check_sat() returned l_true).
*/
rational get_value(pvar v) const { SASSERT(is_assigned(v)); return m_value[v]; }
unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
/**
* Evaluate term under the current assignment.
*/
bool try_eval(pdd const& p, rational& out_value) const;
/** /**
* Apply current substitution to p. * Apply current substitution to p.
*/ */
pdd subst(pdd const& p) const; pdd subst(pdd const& p) const;
/** Create constraints */ /** Create constraints */
signed_constraint eq(pdd const& p) { return m_constraints.eq(p); } signed_constraint eq(pdd const& p) { return m_constraints.eq(p); }
signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); } signed_constraint diseq(pdd const& p) { return ~m_constraints.eq(p); }
@ -346,8 +344,8 @@ namespace polysat {
signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); } signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); }
signed_constraint sgt(pdd const& p, int n) { return slt(n, p); } signed_constraint sgt(pdd const& p, int n) { return slt(n, p); }
signed_constraint sgt(int n, pdd const& p) { return slt(p, n); } signed_constraint sgt(int n, pdd const& p) { return slt(p, n); }
signed_constraint mul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); } signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.mul_ovfl(p, q); }
signed_constraint mul_ovfl(rational const& p, pdd const& q) { return mul_ovfl(q.manager().mk_val(p), q); } signed_constraint umul_ovfl(rational const& p, pdd const& q) { return umul_ovfl(q.manager().mk_val(p), q); }
signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); } signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); }
signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); } signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
@ -365,8 +363,8 @@ namespace polysat {
void add_ult(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(ult(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_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_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_umul_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(~umul_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_umul_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(umul_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(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(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
@ -376,10 +374,10 @@ namespace polysat {
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(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(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_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_umul_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency) { add_umul_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_umul_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency) { add_umul_noovfl(q, p, dep); }
void add_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency) { add_noovfl(p, rational(q), dep); } void add_umul_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency) { add_umul_noovfl(p, rational(q), dep); }
void add_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); } void add_umul_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency) { add_umul_noovfl(q, p, dep); }
/** /**
* Activate the constraint corresponding to the given boolean variable. * Activate the constraint corresponding to the given boolean variable.

2
src/sat/smt/bv_polysat.cpp
View file

@ -58,7 +58,7 @@ namespace bv {
case OP_UGT: polysat_le<false, false, true>(a); break; case OP_UGT: polysat_le<false, false, true>(a); break;
case OP_SGT: polysat_le<true, false, true>(a); break; case OP_SGT: polysat_le<true, false, true>(a); break;
case OP_BUMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.mul_ovfl(p, q); }); break; case OP_BUMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.umul_ovfl(p, q); }); break;
case OP_BSMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break; case OP_BSMUL_NO_OVFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_ovfl(p, q); }); break;
case OP_BSMUL_NO_UDFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break; case OP_BSMUL_NO_UDFL: mk_binaryc(a, [&](pdd const& p, pdd const& q) { return m_polysat.smul_udfl(p, q); }); break;