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

extra px < qx axioms

Browse source
This commit is contained in:
Jakob Rath 2024-05-13 22:46:49 +02:00
parent d28441bd8f
commit 1292fb2adb
3 changed files with 43 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/polysat/inequality.h
View file

@ -100,13 +100,14 @@ namespace polysat {
bool verify_YX_l_zX(pvar z, pdd const& x, pdd const& y) const;
// c := xY <= xZ
bool is_xY_l_xZ(pvar x, pdd& y, pdd& z) const { return is_xY(x, lhs(), y) && is_xY(x, rhs(), z); }
bool is_xY_l_xZ(pvar x, pdd& y, pdd& z) const { return is_xY_2(x, lhs(), y) && is_xY_2(x, rhs(), z); }
/**
* Match xy = x * Y
*/
/// Match xy = x * Y s.t. Y is free of x
static bool is_xY(pvar x, pdd const& xy, pdd& y) { return xy.degree(x) == 1 && xy.factor(x, 1, y); }
/// Match xy = x * Y
static bool is_xY_2(pvar x, pdd const& xy, pdd& y) { return xy.factor(x, 1, y); }
/**
* Rewrite to one of six equivalent forms:
*
@ -165,7 +166,7 @@ namespace polysat {
r.d -= d;
return r;
}
};
};
inline std::ostream& operator<<(std::ostream& out, bilinear const& b) {
return out << b.a << "*x*y + " << b.b << "*x + " << b.c << "*y + " << b.d;

46
src/sat/smt/polysat/saturation.cpp
View file

@ -118,22 +118,48 @@ namespace polysat {
/**
* Implement the inferences
* [x] yx < zx ==> Ω*(x,y) \/ y < z
* [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0
* [x] px < qx ==> p != q
* [x] px < qx ==> Ω*(p,x) \/ p < q
* [x] px < qx ==> Ω*(-q,x) \/ p < q
* [x] px < qx ==> Ω*(q,-x) \/ p > q \/ p = 0
* [x] px < qx ==> Ω*(-p,-x) \/ p > q \/ p = 0
*
* [x] px <= qx ==> Ω*(p,x) \/ p <= q \/ x = 0
* [x] px <= qx ==> Ω*(-q,x) \/ p <= q \/ x = 0 \/ q = 0
* [x] px <= qx ==> Ω*(q,-x) \/ p >= q \/ x = 0 \/ p = 0
* [x] px <= qx ==> Ω*(-p,-x) \/ p >= q \/ x = 0 \/ p = 0
*/
void saturation::try_ugt_x(pvar v, inequality const& i) {
pdd x = c.var(v);
pdd y = x;
pdd z = x;
pdd p = x;
pdd q = x;
auto const& d = i.dep();
if (!i.is_xY_l_xZ(v, y, z))
if (!i.is_xY_l_xZ(v, p, q))
return;
auto ovfl = C.umul_ovfl(x, y);
if (i.is_strict())
add_clause("[x] yx < zx ==> Ω*(x,y) \\/ y < z", { i.dep(), ovfl, C.ult(y, z)}, true);
else
add_clause("[x] yx <= zx ==> Ω*(x,y) \\/ y <= z \\/ x = 0", { i.dep(), ovfl, C.eq(x), C.ule(y, z) }, true);
if (i.is_strict()) {
if (!c.inconsistent())
add_clause("[x] px < qx ==> p != q", { d, C.diseq(p, q) });
if (!c.inconsistent())
add_clause("[x] px < qx ==> Ω*(p,x) \\/ p < q", { d, C.umul_ovfl(p, x), C.ult(p, q) });
if (!c.inconsistent())
add_clause("[x] px < qx ==> Ω*(-q,x) \\/ p < q", { d, C.umul_ovfl(-q, x), C.ult(p, q) });
if (!c.inconsistent())
add_clause("[x] px < qx ==> Ω*(q,-x) \\/ p > q \\/ p = 0", { d, C.umul_ovfl(q, -x), C.ugt(p, q), C.eq(p) });
if (!c.inconsistent())
add_clause("[x] px < qx ==> Ω*(-p,-x) \\/ p > q \\/ p = 0", { d, C.umul_ovfl(-p, -x), C.ugt(p, q), C.eq(p) });
}
else {
if (!c.inconsistent())
add_clause("[x] px <= qx ==> Ω*(p,x) \\/ p <= q \\/ x = 0", { d, C.umul_ovfl(p, x), C.eq(x), C.ule(p, q) });
if (!c.inconsistent())
add_clause("[x] px <= qx ==> Ω*(-q,x) \\/ p <= q \\/ x = 0 \\/ q = 0", { d, C.umul_ovfl(-q, x), C.eq(x), C.eq(q), C.ule(p, q) });
if (!c.inconsistent())
add_clause("[x] px <= qx ==> Ω*(q,-x) \\/ p >= q \\/ x = 0 \\/ p = 0", { d, C.umul_ovfl(q, -x), C.eq(x), C.eq(p), C.uge(p, q) });
if (!c.inconsistent())
add_clause("[x] px <= qx ==> Ω*(-p,-x) \\/ p >= q \\/ x = 0 \\/ p = 0", { d, C.umul_ovfl(-p, -x), C.eq(x), C.eq(p), C.uge(p, q) });
}
}
/**

2
src/sat/smt/polysat/saturation.h
View file

@ -29,7 +29,7 @@ namespace polysat {
core& c;
constraints& C;
void add_clause(char const* name, clause const& cs, bool is_redundant);
void add_clause(char const* name, clause const& cs, bool is_redundant = true);
struct constraint_filter {
core& c;