mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

added bounds (#81)

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-04 09:22:36 -07:00 • committed by Lev Nachmanson
parent 420895f303
commit 0d9aff9834
1 changed files with 26 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_lra.cpp
View file

@ -1969,6 +1969,27 @@ public:
visitor.display_asserts(out, fmls, true); visitor.display_asserts(out, fmls, true);
out << "(check-sat)\n"; out << "(check-sat)\n";
} }
bool all_variables_have_bounds() {
if (!m_has_int) {
return true;
}
unsigned nv = th.get_num_vars();
bool added_bound = false;
for (unsigned v = 0; v < nv; ++v) {
lp::constraint_index ci;
rational bound;
lp::var_index vi = m_theory_var2var_index[v];
if (!has_upper_bound(vi, ci, bound) && !has_lower_bound(vi, ci, bound)) {
lp::lar_term term;
term.add_coeff_var(rational::one(), vi);
app_ref b = mk_bound(term, rational::zero(), false);
TRACE("arith", tout << "added bound " << b << "\n";);
added_bound = true;
}
}
return !added_bound;
}
lbool check_lia() { lbool check_lia() {
if (m.canceled()) { if (m.canceled()) {
@ -1980,6 +2001,11 @@ public:
if (!check_idiv_bounds()) { if (!check_idiv_bounds()) {
return l_false; return l_false;
} }
lp::lar_term term;
lp::mpq k;
lp::explanation ex; // TBD, this should be streamlined accross different explanations
bool upper;
m_explanation.reset(); m_explanation.reset();
switch (m_lia->check()) { switch (m_lia->check()) {
case lp::lia_move::sat: case lp::lia_move::sat: