mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

bound vars

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-09-07 22:00:25 -07:00
parent 1e11b62bc6
commit 211210338a
1 changed files with 31 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_lra.cpp
View file

@ -154,6 +154,7 @@ class theory_lra::imp {
ast_manager& m; ast_manager& m;
theory_arith_params& m_arith_params; theory_arith_params& m_arith_params;
arith_util a; arith_util a;
bool m_has_int;
arith_eq_adapter m_arith_eq_adapter; arith_eq_adapter m_arith_eq_adapter;
vector<rational> m_columns; vector<rational> m_columns;
@ -624,6 +625,7 @@ class theory_lra::imp {
} }
if (result == UINT_MAX) { if (result == UINT_MAX) {
result = m_solver->add_var(v, is_int(v)); result = m_solver->add_var(v, is_int(v));
m_has_int |= is_int(v);
m_theory_var2var_index.setx(v, result, UINT_MAX); m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v); m_var_trail.push_back(v);
@ -798,6 +800,7 @@ public:
th(th), m(m), th(th), m(m),
m_arith_params(ap), m_arith_params(ap),
a(m), a(m),
m_has_int(false),
m_arith_eq_adapter(th, ap, a), m_arith_eq_adapter(th, ap, a),
m_internalize_head(0), m_internalize_head(0),
m_not_handled(0), m_not_handled(0),
@ -1414,15 +1417,40 @@ public:
return atom; return atom;
} }
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_monomial(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()) {
TRACE("arith", tout << "canceled\n";); TRACE("arith", tout << "canceled\n";);
return l_undef; return l_undef;
} }
if (!all_variables_have_bounds()) {
return l_false;
}
lp::lar_term term; lp::lar_term term;
lp::mpq k; lp::mpq k;
lp::explanation ex; // TBD, this should be streamlined accross different explanations lp::explanation ex; // TBD, this should be streamlined accross different explanations
bool upper; bool upper;
std::cout << ".";
switch(m_lia->check(term, k, ex, upper)) { switch(m_lia->check(term, k, ex, upper)) {
case lp::lia_move::sat: case lp::lia_move::sat:
return l_true; return l_true;
@ -2918,7 +2946,9 @@ public:
for (auto const& kv : coeffs) { for (auto const& kv : coeffs) {
g = gcd(g, kv.m_value); g = gcd(g, kv.m_value);
} }
if (!g.is_one() && !g.is_zero()) { if (g.is_zero())
return rational::one();
if (!g.is_one()) {
for (auto& kv : coeffs) { for (auto& kv : coeffs) {
kv.m_value /= g; kv.m_value /= g;
} }