mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Use mul_ovfl constraint directly instead of approximating it with bounds

Browse source
This commit is contained in:
Jakob Rath 2022-06-29 14:28:59 +02:00
parent 69a28a7740
commit c78007fd1a
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -181,9 +181,11 @@ namespace polysat {
return x.manager().max_value(); return x.manager().max_value();
} }
void inf_saturate::push_omega(pdd const& x, pdd const& y) {
m_new_constraints.insert(~s.mul_ovfl(x, y));
/*
// determine worst case upper bounds for x, y // determine worst case upper bounds for x, y
// then extract premises for a non-worst-case bound. // then extract premises for a non-worst-case bound.
void inf_saturate::push_omega(pdd const& x, pdd const& y) {
auto& pddm = x.manager(); auto& pddm = x.manager();
rational x_max = max_value(x); rational x_max = max_value(x);
rational y_max = max_value(y); rational y_max = max_value(y);
@ -198,6 +200,7 @@ namespace polysat {
for (auto const& c : s.m_viable.get_constraints(x.var())) for (auto const& c : s.m_viable.get_constraints(x.var()))
m_new_constraints.insert(c); m_new_constraints.insert(c);
} }
*/
} }
/* /*