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

Fix bug in smt_model_finder, it was producing the incorrect instantiation set.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-13 19:02:48 -07:00
parent 21f69c2b3a
commit 39b9da7118
1 changed files with 17 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/smt/smt_model_finder.cpp
View file

@ -1924,7 +1924,8 @@ namespace smt {
m_mutil.mk_add(t1, t2, r); m_mutil.mk_add(t1, t2, r);
} }
bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const { bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) const {
inv = false; // true if invert the sign
TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";); TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
if (is_var(lhs) && is_ground(rhs)) { if (is_var(lhs) && is_ground(rhs)) {
v = to_var(lhs); v = to_var(lhs);
@ -1939,7 +1940,6 @@ namespace smt {
return true; return true;
} }
else { else {
bool inv = false; // true if invert the sign
expr_ref tmp(m_manager); expr_ref tmp(m_manager);
if (is_var_plus_ground(lhs, inv, v, tmp) && is_ground(rhs)) { if (is_var_plus_ground(lhs, inv, v, tmp) && is_ground(rhs)) {
if (inv) if (inv)
@ -1959,6 +1959,11 @@ namespace smt {
return false; return false;
} }
bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) const {
bool inv;
return is_var_and_ground(lhs, rhs, v, t, inv);
}
bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const { bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) const {
if (!is_app(n)) if (!is_app(n))
return false; return false;
@ -2011,22 +2016,28 @@ namespace smt {
if (sign) { if (sign) {
bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t); bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t);
CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
<< mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";); << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
tout << "sign: " << sign << "\n";);
return r; return r;
} }
else { else {
if (is_le_ge(atom)) { if (is_le_ge(atom)) {
expr_ref tmp(m_manager); expr_ref tmp(m_manager);
if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp)) { bool le = is_le(atom);
bool inv = false;
if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp, inv)) {
if (inv)
le = !le;
sort * s = m_manager.get_sort(tmp); sort * s = m_manager.get_sort(tmp);
expr_ref one(m_manager); expr_ref one(m_manager);
one = mk_one(s); one = mk_one(s);
if (is_le(atom)) if (le)
mk_add(tmp, one, t); mk_add(tmp, one, t);
else else
mk_sub(tmp, one, t); mk_sub(tmp, one, t);
TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n" TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
<< mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";); << mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
tout << "sign: " << sign << "\n";);
return true; return true;
} }
} }