mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
c388d99c35
commit
ed49c1eae3
|
@ -141,6 +141,7 @@ namespace sat {
|
|||
m_participated.reset();
|
||||
m_canceled.reset();
|
||||
m_reasoned.reset();
|
||||
m_case_split_queue.reset();
|
||||
m_simplifier.reset_todos();
|
||||
m_qhead = 0;
|
||||
m_trail.reset();
|
||||
|
@ -3541,7 +3542,7 @@ namespace sat {
|
|||
else {
|
||||
set_eliminated(v, true);
|
||||
if (!is_external(v) || true) {
|
||||
m_free_vars.push_back(v);
|
||||
m_free_vars.push_back(v);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -3556,6 +3557,7 @@ namespace sat {
|
|||
bool_var v = m_free_vars[i];
|
||||
cleanup_watch(literal(v, false));
|
||||
cleanup_watch(literal(v, true));
|
||||
|
||||
}
|
||||
TRACE("sat",
|
||||
tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
|
||||
|
@ -3574,10 +3576,10 @@ namespace sat {
|
|||
m_free_vars[j++] = w;
|
||||
m_free_vars.shrink(j);
|
||||
|
||||
for (bool_var i = v; i < m_justification.size(); ++i) {
|
||||
m_case_split_queue.del_var_eh(i);
|
||||
m_probing.reset_cache(literal(i, true));
|
||||
m_probing.reset_cache(literal(i, false));
|
||||
for (bool_var w = m_justification.size(); w-- > v;) {
|
||||
m_case_split_queue.del_var_eh(w);
|
||||
m_probing.reset_cache(literal(w, true));
|
||||
m_probing.reset_cache(literal(w, false));
|
||||
}
|
||||
m_watches.shrink(2*v);
|
||||
m_assignment.shrink(2*v);
|
||||
|
@ -3600,6 +3602,7 @@ namespace sat {
|
|||
void solver::pop(unsigned num_scopes) {
|
||||
if (num_scopes == 0)
|
||||
return;
|
||||
unsigned free_vars_head = m_free_vars.size();
|
||||
if (m_ext) {
|
||||
pop_vars(num_scopes);
|
||||
m_ext->pop(num_scopes);
|
||||
|
@ -3609,6 +3612,8 @@ namespace sat {
|
|||
scope & s = m_scopes[new_lvl];
|
||||
m_inconsistent = false; // TBD: use model seems to make this redundant: s.m_inconsistent;
|
||||
unassign_vars(s.m_trail_lim, new_lvl);
|
||||
for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
|
||||
m_case_split_queue.del_var_eh(m_free_vars[i]);
|
||||
m_scope_lvl -= num_scopes;
|
||||
reinit_clauses(s.m_clauses_to_reinit_lim);
|
||||
m_scopes.shrink(new_lvl);
|
||||
|
|
|
@ -1057,7 +1057,7 @@ private:
|
|||
CTRACE("sat", !m.is_true(tmp),
|
||||
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
|
||||
model_smt2_pp(tout, m, *(mdl.get()), 0););
|
||||
if (!m.is_true(tmp)) {
|
||||
if (m.is_false(tmp)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n");
|
||||
IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n");
|
||||
all_true = false;
|
||||
|
|
|
@ -8,7 +8,7 @@ Module Name:
|
|||
Abstract:
|
||||
|
||||
E-matching quantifier instantiation plugin
|
||||
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-01-24
|
||||
|
@ -374,6 +374,7 @@ namespace q {
|
|||
clause* cl = alloc(clause, m, m_clauses.size());
|
||||
cl->m_literal = ctx.mk_literal(_q);
|
||||
quantifier_ref q(_q, m);
|
||||
q = m_qs.flatten(q);
|
||||
if (is_exists(q)) {
|
||||
cl->m_literal.neg();
|
||||
expr_ref body(mk_not(m, q->get_expr()), m);
|
||||
|
|
|
@ -157,6 +157,7 @@ namespace q {
|
|||
expr* t = todo.back();
|
||||
SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
|
||||
if (is_ground(t)) {
|
||||
m_mark.mark(t);
|
||||
m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
|
||||
SASSERT(m_eval[t->get_id()]);
|
||||
todo.pop_back();
|
||||
|
|
Loading…
Reference in a new issue