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

reset pdd manager for output parameters

Browse source
This commit is contained in:
Jakob Rath 2023-10-23 15:37:08 +02:00
parent a797220484
commit 45bd052b3e
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -434,6 +434,7 @@ namespace polysat {
* Match [x] x <= y * Match [x] x <= y
*/ */
bool saturation::is_x_l_Y(pvar x, inequality const& i, pdd& y) { bool saturation::is_x_l_Y(pvar x, inequality const& i, pdd& y) {
y.reset(i.rhs().manager());
y = i.rhs(); y = i.rhs();
return is_g_v(x, i); return is_g_v(x, i);
} }
@ -442,6 +443,7 @@ namespace polysat {
* Match [x] y <= x * Match [x] y <= x
*/ */
bool saturation::is_Y_l_x(pvar x, inequality const& i, pdd& y) { bool saturation::is_Y_l_x(pvar x, inequality const& i, pdd& y) {
y.reset(i.lhs().manager());
y = i.lhs(); y = i.lhs();
return is_l_v(x, i); return is_l_v(x, i);
} }
@ -450,6 +452,7 @@ namespace polysat {
* Match [x] y <= a*x * Match [x] y <= a*x
*/ */
bool saturation::is_Y_l_Ax(pvar x, inequality const& i, pdd& a, pdd& y) { bool saturation::is_Y_l_Ax(pvar x, inequality const& i, pdd& a, pdd& y) {
y.reset(i.lhs().manager());
y = i.lhs(); y = i.lhs();
return is_xY(x, i.rhs(), a); return is_xY(x, i.rhs(), a);
} }
@ -462,6 +465,7 @@ namespace polysat {
* Match [x] a*x <= y * Match [x] a*x <= y
*/ */
bool saturation::is_Ax_l_Y(pvar x, inequality const& i, pdd& a, pdd& y) { bool saturation::is_Ax_l_Y(pvar x, inequality const& i, pdd& a, pdd& y) {
y.reset(i.rhs().manager());
y = i.rhs(); y = i.rhs();
return is_xY(x, i.lhs(), a); return is_xY(x, i.lhs(), a);
} }
@ -474,6 +478,7 @@ namespace polysat {
* Match [x] a*x + b <= y * Match [x] a*x + b <= y
*/ */
bool saturation::is_AxB_l_Y(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) { bool saturation::is_AxB_l_Y(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) {
y.reset(i.rhs().manager());
y = i.rhs(); y = i.rhs();
return i.lhs().degree(x) == 1 && (i.lhs().factor(x, 1, a, b), true); return i.lhs().degree(x) == 1 && (i.lhs().factor(x, 1, a, b), true);
} }
@ -484,6 +489,7 @@ namespace polysat {
bool saturation::is_Y_l_AxB(pvar x, inequality const& i, pdd& y, pdd& a, pdd& b) { bool saturation::is_Y_l_AxB(pvar x, inequality const& i, pdd& y, pdd& a, pdd& b) {
y.reset(i.lhs().manager());
y = i.lhs(); y = i.lhs();
return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true); return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true);
} }
@ -497,6 +503,7 @@ namespace polysat {
* Match [x] a*x + b <= y, val(y) = 0 * Match [x] a*x + b <= y, val(y) = 0
*/ */
bool saturation::is_AxB_eq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) { bool saturation::is_AxB_eq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) {
y.reset(i.rhs().manager());
y = i.rhs(); y = i.rhs();
rational y_val; rational y_val;
if (!s.try_eval(y, y_val) || y_val != 0) if (!s.try_eval(y, y_val) || y_val != 0)
@ -511,12 +518,15 @@ namespace polysat {
bool saturation::is_AxB_diseq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) { bool saturation::is_AxB_diseq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) {
if (!i.is_strict()) if (!i.is_strict())
return false; return false;
y.reset(i.lhs().manager());
y = i.lhs(); y = i.lhs();
if (i.rhs().is_val() && i.rhs().val() == 1) if (i.rhs().is_val() && i.rhs().val() == 1)
return false; return false;
rational y_val; rational y_val;
if (!s.try_eval(y, y_val) || y_val != 0) if (!s.try_eval(y, y_val) || y_val != 0)
return false; return false;
a.reset(i.rhs().manager());
b.reset(i.rhs().manager());
return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true); return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true);
} }