mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

debugging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 17:09:36 -08:00
parent 0a5b03194c
commit db18c7206a
2 changed files with 18 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/forbidden_intervals.cpp
View file

@ -407,7 +407,6 @@ namespace polysat {
fi.side_cond.push_back(s.eq(b1, e1)); fi.side_cond.push_back(s.eq(b1, e1));
if (b2 != e2) if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2)); fi.side_cond.push_back(s.eq(b2, e2));
IF_VERBOSE(0, verbose_stream() << fi.interval << " " << fi.side_cond << "\n");
return true; return true;
} }
return false; return false;

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

@ -39,6 +39,10 @@ namespace polysat {
if (c.is_currently_true(s)) if (c.is_currently_true(s))
continue; continue;
auto i = inequality::from_ule(c); auto i = inequality::from_ule(c);
#if 0
if (try_mul_bounds(v, core, i))
return true;
#endif
if (try_ugt_x(v, core, i)) if (try_ugt_x(v, core, i))
return true; return true;
if (try_ugt_y(v, core, i)) if (try_ugt_y(v, core, i))
@ -192,10 +196,10 @@ namespace polysat {
*/ */
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 = i.rhs(); y = i.rhs();
if (!y.is_val() || y.val() != 0) rational y_val;
if (!s.try_eval(y, y_val) || y_val != 0)
return false; return false;
pdd aa = a, bb = b; 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, aa, bb), aa == a && bb == b);
} }
bool saturation::verify_AxB_eq_0(pvar x, inequality const& i, pdd const& a, pdd const& b, pdd const& y) { bool saturation::verify_AxB_eq_0(pvar x, inequality const& i, pdd const& a, pdd const& b, pdd const& y) {
@ -453,13 +457,17 @@ namespace polysat {
if (!is_AxB_eq_0(x, axb_l_y, a, b, y)) if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
return false; return false;
IF_VERBOSE(0, verbose_stream() << " mul bounds " << x << " " << axb_l_y.as_signed_constraint() << "\n");
if (!is_forced_eq(b, 0)) if (!is_forced_eq(b, 0))
return false; return false;
#if 0
// we could also use x.val(), a.val() if they exist and enforce bounds
if (s.try_eval(a, a_val) && s.try_eval(X, x_val) && a_val*x_val != 0) {
#if 1
// we could also use x.val(), a.val() if they exist and enforce bounds
rational a_val, x_val;
if (s.try_eval(a, a_val) && s.try_eval(X, x_val) && a_val*x_val != 0) {
IF_VERBOSE(0, verbose_stream() << " mul bounds " << axb_l_y.as_signed_constraint() << "\n");
} }
#endif #endif
@ -489,6 +497,10 @@ namespace polysat {
return false; return false;
if (!is_forced_diseq(a, 0, a_eq_0)) if (!is_forced_diseq(a, 0, a_eq_0))
return false; return false;
IF_VERBOSE(0, verbose_stream() << " mul bounds " << axb_l_y.as_signed_constraint() << "\n");
return false;
m_lemma.reset(); m_lemma.reset();
m_lemma.insert(~s.eq(b)); m_lemma.insert(~s.eq(b));
m_lemma.insert(~s.eq(y)); m_lemma.insert(~s.eq(y));