mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

merge changes from master

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-10-05 07:50:13 -07:00
parent 45c0ed126e
commit b61f4ac51f
4 changed files with 29 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_lra.cpp
View file

@ -2115,6 +2115,9 @@ public:
flush_bound_axioms();
// disabled in master:
propagate_nla();
if (ctx().inconsistent())
return true;
if (!can_propagate_core())
return false;
@ -2212,6 +2215,9 @@ public:
}
void propagate_bounds_with_lp_solver() {
if (!should_propagate())
return;
m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);
@ -3546,7 +3552,6 @@ public:
if (r == l_true) {
nctx.display_asserted_formulas(std::cout);
std::cout.flush();
std::cout.flush();
}
return l_true != r;
}

7
src/smt/theory_user_propagator.cpp
View file

@ -62,8 +62,7 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
if (is_attached_to_var(n))
return;
theory_var v = mk_var(n);
m_var2expr.reserve(v + 1);
m_var2expr[v] = term;
@ -146,7 +145,7 @@ final_check_status theory_user_propagator::final_check_eh() {
return FC_DONE;
force_push();
unsigned sz1 = m_prop.size();
unsigned sz2 = m_expr2var.size();
unsigned sz2 = get_num_vars();
try {
m_final_eh(m_user_context, this);
}
@ -157,7 +156,7 @@ final_check_status theory_user_propagator::final_check_eh() {
propagate();
CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n");
// check if it became inconsistent or something new was propagated/registered
bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
bool done = (sz1 == m_prop.size()) && (sz2 == get_num_vars()) && !ctx.inconsistent();
return done ? FC_DONE : FC_CONTINUE;
}