mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-15 14:11:28 +00:00
Code Activity

take into account integer coefficients

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-31 16:07:37 -07:00
parent e91e432496
commit 4c0c199e32
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/nla_grobner.cpp
View file

@ -250,6 +250,8 @@ namespace nla {
// z < 0 & x < 0 => -x <= -z
bool grobner::propagate_quotients(dd::solver::equation const& eq) {
dd::pdd const& p = eq.poly();
dd::pdd_eval eval;
eval.var2val() = [&](unsigned j) { return val(j); };
if (p.is_linear())
return false;
if (p.is_val())
@ -260,15 +262,17 @@ namespace nla {
for (auto v : p.free_vars())
if (!c().var_is_int(v))
return false;
if (eval(p) == 0)
return false;
tracked_uint_set nl_vars;
rational d(1);
for (auto const& m : p) {
d = lcm(d, denominator(m.coeff));
if (m.vars.size() == 1)
continue;
for (auto j : m.vars)
nl_vars.insert(j);
}
dd::pdd_eval eval;
eval.var2val() = [&](unsigned j) { return val(j); };
for (auto v : nl_vars) {
auto& m = p.manager();
@ -276,9 +280,16 @@ namespace nla {
p.factor(v, 1, lc, r);
if (!r.is_linear())
continue;
if (d != 1) {
lc *= d;
r *= d;
}
auto v_value = val(v);
auto r_value = eval(r);
auto lc_value = eval(lc);
SASSERT(v_value.is_int());
SASSERT(r_value.is_int());
SASSERT(lc_value.is_int());
if (r_value == 0) {
if (v_value == 0)
continue;

3
src/smt/theory_lra.cpp
View file

@ -1660,9 +1660,6 @@ public:
return FC_CONTINUE;
}
if (st == FC_GIVEUP)
IF_VERBOSE(0, display(verbose_stream()));
if (!int_undef && !check_bv_terms())
return FC_CONTINUE;