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

deal with non-termination in new arithmetic solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-27 16:15:36 -07:00
parent f6c9ead10c
commit 52d16a11f9
3 changed files with 19 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/arith_axioms.cpp
View file

@ -386,12 +386,12 @@ namespace arith {
ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs)); ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
} }
void solver::mk_diseq_axiom(euf::th_eq const& e) { void solver::mk_diseq_axiom(theory_var v1, theory_var v2) {
if (is_bool(e.v1())) if (is_bool(v1))
return; return;
force_push(); force_push();
expr* e1 = var2expr(e.v1()); expr* e1 = var2expr(v1);
expr* e2 = var2expr(e.v2()); expr* e2 = var2expr(v2);
if (e1->get_id() > e2->get_id()) if (e1->get_id() > e2->get_id())
std::swap(e1, e2); std::swap(e1, e2);
if (m.are_distinct(e1, e2)) if (m.are_distinct(e1, e2))

17
src/sat/smt/arith_solver.cpp
View file

@ -896,6 +896,9 @@ namespace arith {
} }
bool solver::assume_eqs() { bool solver::assume_eqs() {
if (delayed_assume_eqs())
return true;
TRACE("arith", display(tout);); TRACE("arith", display(tout););
random_update(); random_update();
m_model_eqs.reset(); m_model_eqs.reset();
@ -944,8 +947,15 @@ namespace arith {
continue; continue;
literal eq = eq_internalize(n1, n2); literal eq = eq_internalize(n1, n2);
ctx.mark_relevant(eq); ctx.mark_relevant(eq);
if (s().value(eq) != l_true) switch (s().value(eq)) {
case l_true:
break;
case l_undef:
return true; return true;
case l_false:
mk_diseq_axiom(v1, v2);
return true;
}
} }
return false; return false;
} }
@ -1025,6 +1035,7 @@ namespace arith {
} }
if (!check_delayed_eqs()) if (!check_delayed_eqs())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
if (ctx.get_config().m_arith_ignore_int && int_undef) if (ctx.get_config().m_arith_ignore_int && int_undef)
return sat::check_result::CR_GIVEUP; return sat::check_result::CR_GIVEUP;
if (m_not_handled != nullptr) { if (m_not_handled != nullptr) {
@ -1106,7 +1117,7 @@ namespace arith {
if (p.second) if (p.second)
new_eq_eh(e); new_eq_eh(e);
else if (is_eq(e.v1(), e.v2())) { else if (is_eq(e.v1(), e.v2())) {
mk_diseq_axiom(e); mk_diseq_axiom(e.v1(), e.v2());
found_diseq = true; found_diseq = true;
break; break;
} }
@ -1467,8 +1478,6 @@ namespace arith {
add_lemmas(); add_lemmas();
break; break;
case l_true: case l_true:
if (assume_eqs())
return l_false;
break; break;
case l_undef: case l_undef:
break; break;

2
src/sat/smt/arith_solver.h
View file

@ -355,7 +355,7 @@ namespace arith {
literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const; literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const;
void assert_bound(bool is_true, api_bound& b); void assert_bound(bool is_true, api_bound& b);
void mk_eq_axiom(bool is_eq, euf::th_eq const& eq); void mk_eq_axiom(bool is_eq, euf::th_eq const& eq);
void mk_diseq_axiom(euf::th_eq const& eq); void mk_diseq_axiom(theory_var v1, theory_var v2);
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r); void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound); api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true); lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);