mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix sle

Browse source
This commit is contained in:
Jakob Rath 2024-05-13 15:14:49 +02:00
parent 94955e3fae
commit fb5a40a6fd
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -153,14 +153,13 @@ namespace polysat {
signed_constraint slt(int p, pdd const& q) { return slt(rational(p), q); }
signed_constraint slt(unsigned p, pdd const& q) { return slt(rational(p), q); }
signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); }
signed_constraint sgt(pdd const& p, int q) { return slt(q, p); }
signed_constraint sgt(pdd const& p, unsigned q) { return slt(q, p); }
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, pdd const& q) { return sle(q, p); }
signed_constraint sge(pdd const& p, int q) { return sge(p, p.manager().mk_val(q)); }
signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); }