From 3e960eadd2b14f1da9b89927e6dd17cf77eea063 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Aug 2017 12:14:19 +0100 Subject: [PATCH] (Re-)added option to disable lemma deletion in the smt_context. --- src/smt/params/smt_params.h | 31 +- src/smt/smt_context.cpp | 556 ++++++++++++++++++------------------ 2 files changed, 295 insertions(+), 292 deletions(-) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 4539ebe58..b01499c04 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -31,7 +31,7 @@ Revision History: #include "smt/params/preprocessor_params.h" #include "cmd_context/context_params.h" -enum phase_selection { +enum phase_selection { PS_ALWAYS_FALSE, PS_ALWAYS_TRUE, PS_CACHING, @@ -52,7 +52,8 @@ enum restart_strategy { enum lemma_gc_strategy { LGC_FIXED, LGC_GEOMETRIC, - LGC_AT_RESTART + LGC_AT_RESTART, + LGC_NONE }; enum initial_activity { @@ -71,11 +72,11 @@ enum case_split_strategy { CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity }; -struct smt_params : public preprocessor_params, - public dyn_ack_params, - public qi_params, - public theory_arith_params, - public theory_array_params, +struct smt_params : public preprocessor_params, + public dyn_ack_params, + public qi_params, + public theory_arith_params, + public theory_array_params, public theory_bv_params, public theory_str_params, public theory_pb_params, @@ -153,12 +154,12 @@ struct smt_params : public preprocessor_params, unsigned m_lemma_gc_initial; double m_lemma_gc_factor; unsigned m_new_old_ratio; //!< the ratio of new and old clauses. - unsigned m_new_clause_activity; + unsigned m_new_clause_activity; unsigned m_old_clause_activity; unsigned m_new_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. unsigned m_old_clause_relevancy; //!< Max. number of unassigned literals to be considered relevant. double m_inv_clause_decay; //!< clause activity decay - + // ----------------------------------- // // SMT-LIB (debug) pretty printer @@ -166,7 +167,7 @@ struct smt_params : public preprocessor_params, // ----------------------------------- bool m_smtlib_dump_lemmas; symbol m_logic; - + // ----------------------------------- // // Statistics for Profiling @@ -179,10 +180,10 @@ struct smt_params : public preprocessor_params, // ----------------------------------- // - // Model generation + // Model generation // // ----------------------------------- - bool m_model; + bool m_model; bool m_model_compact; bool m_model_on_timeout; bool m_model_on_final_check; @@ -213,7 +214,7 @@ struct smt_params : public preprocessor_params, unsigned m_timeout; unsigned m_rlimit; bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. - bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. + bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_dump_goal_as_smt; bool m_auto_config; @@ -237,7 +238,7 @@ struct smt_params : public preprocessor_params, m_display_proof(false), m_display_dot_proof(false), m_display_unsat_core(false), - m_check_proof(false), + m_check_proof(false), m_eq_propagation(true), m_binary_clause_opt(true), m_relevancy_lvl(2), @@ -279,7 +280,7 @@ struct smt_params : public preprocessor_params, m_new_old_ratio(16), m_new_clause_activity(10), m_old_clause_activity(500), - m_new_clause_relevancy(45), + m_new_clause_relevancy(45), m_old_clause_relevancy(6), m_inv_clause_decay(1), m_smtlib_dump_lemmas(false), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index daa408161..b966b8380 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -95,7 +95,7 @@ namespace smt { if (!relevancy()) m_fparams.m_relevancy_lemma = false; - + m_model_generator->set_context(this); } @@ -106,29 +106,29 @@ namespace smt { ast_manager& src_m = src_ctx.get_manager(); expr_ref dst_f(dst_m); - SASSERT(lit != false_literal && lit != true_literal); - bool_var v = b2v.get(lit.var(), null_bool_var); - if (v == null_bool_var) { - expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0); - SASSERT(e); - dst_f = tr(e); + SASSERT(lit != false_literal && lit != true_literal); + bool_var v = b2v.get(lit.var(), null_bool_var); + if (v == null_bool_var) { + expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0); + SASSERT(e); + dst_f = tr(e); v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id()); - if (v != null_bool_var) { - } + if (v != null_bool_var) { + } else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) || - src_m.is_iff(e) || src_m.is_ite(e)) { - v = dst_ctx.mk_bool_var(dst_f); - } - else { - dst_ctx.internalize_formula(dst_f, false); - v = dst_ctx.get_bool_var(dst_f); - } - b2v.setx(lit.var(), v, null_bool_var); - } - return literal(v, lit.sign()); + src_m.is_iff(e) || src_m.is_ite(e)) { + v = dst_ctx.mk_bool_var(dst_f); + } + else { + dst_ctx.internalize_formula(dst_f, false); + v = dst_ctx.get_bool_var(dst_f); + } + b2v.setx(lit.var(), v, null_bool_var); + } + return literal(v, lit.sign()); } - bool context::get_cancel_flag() { + bool context::get_cancel_flag() { return !m_manager.limit().inc(); } @@ -137,12 +137,12 @@ namespace smt { ast_manager& dst_m = dst_ctx.get_manager(); ast_manager& src_m = src_ctx.get_manager(); src_ctx.pop_to_base_lvl(); - + if (src_ctx.m_base_lvl > 0) { throw default_exception("Cloning contexts within a user-scope is not allowed"); } SASSERT(src_ctx.m_base_lvl == 0); - + ast_translation tr(src_m, dst_m, false); dst_ctx.set_logic(src_ctx.m_setup.get_logic()); @@ -151,7 +151,7 @@ namespace smt { asserted_formulas& src_af = src_ctx.m_asserted_formulas; asserted_formulas& dst_af = dst_ctx.m_asserted_formulas; - // Copy asserted formulas. + // Copy asserted formulas. for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) { expr_ref fml(dst_m); proof_ref pr(dst_m); @@ -160,7 +160,7 @@ namespace smt { if (pr_src) { pr = tr(pr_src); } - dst_af.assert_expr(fml, pr); + dst_af.assert_expr(fml, pr); } if (!src_ctx.m_setup.already_configured()) { @@ -191,7 +191,7 @@ namespace smt { lits.push_back(lit); } dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0); - } + } vector::const_iterator it = src_ctx.m_watches.begin(); vector::const_iterator end = src_ctx.m_watches.end(); literal ls[2]; @@ -207,12 +207,12 @@ namespace smt { ls[0] = TRANSLATE(neg_l1); ls[1] = TRANSLATE(l2); dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0); - } + } } } #endif - - TRACE("smt_context", + + TRACE("smt_context", src_ctx.display(tout); dst_ctx.display(tout);); } @@ -227,7 +227,7 @@ namespace smt { // copy missing simplifier_plugins // remark: some simplifier_plugins are automatically created by the asserted_formulas class. simplifier & src_s = src.get_simplifier(); - simplifier & dst_s = dst.get_simplifier(); + simplifier & dst_s = dst.get_simplifier(); ptr_vector::const_iterator it1 = src_s.begin_plugins(); ptr_vector::const_iterator end1 = src_s.end_plugins(); for (; it1 != end1; ++it1) { @@ -248,9 +248,9 @@ namespace smt { context * context::mk_fresh(symbol const * l, smt_params * p) { context * new_ctx = alloc(context, m_manager, p == 0 ? m_fparams : *p); new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l); - copy_plugins(*this, *new_ctx); + copy_plugins(*this, *new_ctx); return new_ctx; - } + } void context::init() { app * t = m_manager.mk_true(); @@ -299,9 +299,9 @@ namespace smt { d.set_justification(j); } - + void context::assign_core(literal l, b_justification j, bool decision) { - TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; + TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " "; display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n"; display(tout, j);); m_assigned_literals.push_back(l); @@ -319,7 +319,7 @@ namespace smt { d.m_phase = !l.sign(); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); - TRACE("relevancy", + TRACE("relevancy", tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";); if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l))) m_atom_propagation_queue.push_back(l); @@ -331,12 +331,12 @@ namespace smt { // a unit is asserted at search level. Mark it as relevant. // this addresses bug... where a literal becomes fixed to true (false) // as a conflict gets assigned misses relevancy (and quantifier instantiation). - // + // if (false && !decision && relevancy() && at_search_level() && !is_relevant_core(l)) { mark_as_relevant(l); } } - + bool context::bcp() { SASSERT(!inconsistent()); while (m_qhead < m_assigned_literals.size()) { @@ -385,17 +385,17 @@ namespace smt { cls->set_literal(0, cls->get_literal(1)); cls->set_literal(1, not_l); } - + SASSERT(cls->get_literal(1) == not_l); - - literal first_lit = cls->get_literal(0); + + literal first_lit = cls->get_literal(0); lbool first_lit_val = get_assignment(first_lit); - - if (first_lit_val == l_true) { - *it2 = *it; // clause is already satisfied, keep it + + if (first_lit_val == l_true) { + *it2 = *it; // clause is already satisfied, keep it it2++; } - else { + else { literal * it3 = cls->begin_literals() + 2; literal * end3 = cls->end_literals(); for(; it3 != end3; ++it3) { @@ -408,7 +408,7 @@ namespace smt { goto found_watch; } } - // did not find watch... + // did not find watch... if (first_lit_val == l_false) { // CONFLICT // copy remaining watches @@ -427,8 +427,8 @@ namespace smt { // PROPAGATION SASSERT(first_lit_val == l_undef); SASSERT(get_assignment(first_lit) == l_undef); - SASSERT(is_unit_clause(cls)); - *it2 = *it; + SASSERT(is_unit_clause(cls)); + *it2 = *it; it2++; // keep clause m_stats.m_num_propagations++; // It is safe to call assign_core instead of assign because first_lit is unassigned @@ -440,13 +440,13 @@ namespace smt { //if (!(m_manager.is_eq(e) && m_manager.get_sort(to_app(e)->get_arg(0))->get_family_id() == m_manager.get_family_id("array"))) mark_as_relevant(e); } - } - found_watch:; - } + } + found_watch:; + } } - SASSERT(it2 <= end); + SASSERT(it2 <= end); w.set_end_clause(it2); - } + } return true; } @@ -473,7 +473,7 @@ namespace smt { theory * t = get_theory(th); if (t->get_enode(lhs)->is_interpreted() && t->get_enode(rhs)->is_interpreted()) return; - TRACE("add_diseq", + TRACE("add_diseq", tout << "#" << t->get_enode(lhs)->get_owner_id() << " != " << "#" << t->get_enode(rhs)->get_owner_id() << "\n";); @@ -490,7 +490,7 @@ namespace smt { m_n1(n1), m_r2_num_parents(r2_num_parents) { } - + virtual void undo(context & ctx) { ctx.undo_add_eq(m_r1, m_n1, m_r2_num_parents); } @@ -506,27 +506,27 @@ namespace smt { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n"; tout << "kind: " << js.get_kind() << "\n";); - + m_stats.m_num_add_eq++; enode * r1 = n1->get_root(); enode * r2 = n2->get_root(); - + if (r1 == r2) { TRACE("add_eq", tout << "redundant constraint.\n";); return; } - + if (r1->is_interpreted() && r2->is_interpreted()) { TRACE("add_eq", tout << "interpreted roots conflict.\n";); set_conflict(mk_justification(eq_conflict_justification(n1, n2, js))); return; } - + // Swap r1 and r2: // 1. if the "equivalence" class of r1 is bigger than the equivalence class of r2 // OR // 2. r1 is interpreted but r2 is not. - // + // // The second condition is used to enforce the invariant that if a class contain // an interepreted enode then the root is also interpreted. if ((r1->get_class_size() > r2->get_class_size() && !r2->is_interpreted()) || r1->is_interpreted()) { @@ -534,10 +534,10 @@ namespace smt { std::swap(n1, n2); std::swap(r1, r2); } - - TRACE("add_eq", tout << "merging: #" << r1->get_owner_id() << " #" << r2->get_owner_id() << + + TRACE("add_eq", tout << "merging: #" << r1->get_owner_id() << " #" << r2->get_owner_id() << " n1: #" << n1->get_owner_id() << "\n";); - + // It is necessary to propagate relevancy to other elements of // the equivalence class. This is nessary to enforce the invariant // in the field m_parent of the enode class. @@ -554,13 +554,13 @@ namespace smt { else if (is_relevant(r2)) { // && !m_manager.is_eq(r2->get_owner())) { // !is_eq HACK mark_as_relevant(r1); } - + push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); - + m_qmanager->add_eq_eh(r1, r2); - + merge_theory_vars(n2, n1, js); - + // 'Proof' tree // n1 -> ... -> r1 // n2 -> ... -> r2 @@ -571,8 +571,8 @@ namespace smt { SASSERT(r1->trans_reaches(n1)); // --------------- // r1 -> .. -> n1 -> n2 -> ... -> r2 - - + + #if 0 { static unsigned counter = 0; @@ -584,35 +584,35 @@ namespace smt { num_bad_adds++; } if (num_adds % 100000 == 0) { - verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " " + verbose_stream() << "[add-eq]: " << num_bad_adds << " " << num_adds << " " << static_cast(num_bad_adds)/static_cast(num_adds) << "\n"; } } #endif - - + + remove_parents_from_cg_table(r1); - + enode * curr = r1; do { curr->m_root = r2; curr = curr->m_next; } while(curr != r1); - + SASSERT(r1->get_root() == r2); - + reinsert_parents_into_cg_table(r1, r2, n1, n2, js); - + if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); - + // Merge "equivalence" classes std::swap(r1->m_next, r2->m_next); - + // Update "equivalence" class size r2->m_class_size += r1->m_class_size; - + CASSERT("add_eq", check_invariant()); } catch (...) { @@ -642,12 +642,12 @@ namespace smt { num_eqs++; num_parents++; if (num_parents % 100000 == 0) { - verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " " + verbose_stream() << "[remove-cg] " << num_eqs << " " << num_parents << " " << static_cast(num_eqs)/static_cast(num_parents) << "\n"; } } #endif - SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || + SASSERT(parent->is_marked() || !parent->is_cgc_enabled() || (!parent->is_true_eq() && parent->is_cgr() == m_cg_table.contains_ptr(parent)) || (parent->is_true_eq() && !m_cg_table.contains_ptr(parent))); if (!parent->is_marked() && parent->is_cgr() && !parent->is_true_eq()) { @@ -667,12 +667,12 @@ namespace smt { cg_table at remove_parents_from_cg_table. Some of these parents will become congruent to other enodes, and a new equality will be propagated. Moreover, this method is also used for doing equality propagation. - + The parents of r1 that remain as congruence roots are copied to the r2->m_parents. The n1, n2, js arguments are used to implement dynamic ackermanization. - js is a justification for n1 and n2 being equal, and the equality n1 = n2 is + js is a justification for n1 and n2 being equal, and the equality n1 = n2 is the one that implied r1 = r2. */ void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) { @@ -737,7 +737,7 @@ namespace smt { the following sequence starting at n and ending at n->get_root. - N1 = n + N1 = n N_{i+1} = N_i->m_trans.m_target and, there is an k such that N_k = n->get_root() @@ -768,12 +768,12 @@ namespace smt { This method is used to improve the quality of the conflict clauses produced by the logical context. - + Consider the following example: - Consider the following sequence of equalities: n1 = n2 = n3 = n4 = n5 = n6 - + - Now, assume that n1 is the root of the equivalence class after each merge. So, the 'proof' branch will have the following shape: @@ -782,12 +782,12 @@ namespace smt { - Assuming that all nodes are attached to theory variable, then the following sequence of equalities is sent to the theory if the method get_closest_var is not used: - + n1 = n2, n1 = n3, n1 = n4, n1 = n5, n1 = n6 - This sequence is bad, and bad justifications may be produced by theory. For example, assume the following arithmetic constraint - + n5 < n6 For the arithmetic module, the best justification will be: @@ -798,7 +798,7 @@ namespace smt { When the method get_closest_var is used in the communication with theories, the logical context will send the natural sequence of equalities to the theories: - + n1 = n2 = n3 = n4 = n5 = n6 */ theory_var context::get_closest_var(enode * n, theory_id th_id) { @@ -816,7 +816,7 @@ namespace smt { /** \brief Merge the theory variables of n2->get_root() and n1->get_root(), the result is stored in n2->get_root(). New th_var equalities are propagated to the theories. - + \remark In most cases, an enode is attached to at most one theory var. */ void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) { @@ -826,7 +826,7 @@ namespace smt { TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_owner()->get_id() << " #" << n2->get_owner()->get_id() << "\n";); return; } - + theory_id from_th = null_theory_id; if (js.get_kind() == eq_justification::JUSTIFICATION) @@ -839,8 +839,8 @@ namespace smt { // verbose_stream() << "[merge_theory_vars] t2: " << t2 << ", t1: " << t1 << "\n"; theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var(); theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var(); - TRACE("merge_theory_vars", - tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() + TRACE("merge_theory_vars", + tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() << ", t2: " << t2 << ", t1: " << t1 << "\n";); if (v2 != null_theory_var && v1 != null_theory_var) { if (t1 == t2) { @@ -867,7 +867,7 @@ namespace smt { } else { // r1 and/or r2 have more than one theory variable. - TRACE("merge_theory_vars", + TRACE("merge_theory_vars", tout << "#" << r1->get_owner_id() << " == #" << r2->get_owner_id() << "\n";); @@ -889,7 +889,7 @@ namespace smt { } l2 = l2->get_next(); } - + theory_var_list * l1 = r1->get_th_var_list(); while (l1) { theory_id t1 = l1->get_th_id(); @@ -905,7 +905,7 @@ namespace smt { } } } - + /** \brief Propabate the boolean assignment when two equivalence classes are merged. */ @@ -959,7 +959,7 @@ namespace smt { bool_var v2 = enode2bool_var(target); lbool val2 = get_assignment(v2); if (val2 != val) { - if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0) + if (val2 != l_undef && congruent(source, target) && source->get_num_args() > 0) m_dyn_ack_manager.cg_conflict_eh(source->get_owner(), target->get_owner()); assign(literal(v2, sign), mk_justification(mp_iff_justification(source, target))); } @@ -986,7 +986,7 @@ namespace smt { enode * parent = *it; if (parent->is_cgc_enabled()) { TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); - CTRACE("add_eq", !parent->is_cgr(), + CTRACE("add_eq", !parent->is_cgr(), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; for (unsigned i = 0; i < r2->m_parents.size(); i++) { @@ -1017,10 +1017,10 @@ namespace smt { TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";); if (parent->is_cgc_enabled()) { enode * cg = parent->m_cg; - if (!parent->is_true_eq() && + if (!parent->is_true_eq() && (parent == cg || // parent was root of the congruence class before and after the merge !congruent(parent, cg) // parent was root of the congruence class before but not after the merge - )) { + )) { TRACE("add_eq_parents", tout << "trying to reinsert\n";); m_cg_table.insert(parent); parent->m_cg = parent; @@ -1057,17 +1057,17 @@ namespace smt { // n2 -> ... -> r2 SASSERT(n1->trans_reaches(r1)); SASSERT(r1->m_trans.m_target == 0); - + CASSERT("add_eq", check_invariant()); } /** - \brief Auxiliary method for undo_add_eq. + \brief Auxiliary method for undo_add_eq. It restores the theory variables of a given root enode. This method deletes any theory variable v2 of r2 (for a theory t2) whenever: - get_theory(t2)->get_enode(v2)->get_root() != r2 + get_theory(t2)->get_enode(v2)->get_root() != r2 That is, v2 is not equivalent to r2 anymore. */ @@ -1078,7 +1078,7 @@ namespace smt { while (l2) { theory_var v2 = l2->get_th_var(); theory_id t2 = l2->get_th_id(); - + if (get_theory(t2)->get_enode(v2)->get_root() != r2) { SASSERT(get_theory(t2)->get_enode(v2)->get_root() == r1); l2 = l2->get_next(); @@ -1122,7 +1122,7 @@ namespace smt { #ifdef Z3DEBUG push_trail(push_back_trail(m_diseq_vector)); m_diseq_vector.push_back(enode_pair(n1, n2)); -#endif +#endif if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); @@ -1166,7 +1166,7 @@ namespace smt { } return true; } - + /** \brief Return true if n1 and n2 are known to be disequal in the logical context. @@ -1215,7 +1215,7 @@ namespace smt { if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false && ((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) || (parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) { - TRACE("is_diseq_bug", tout << "parent: #" << parent->get_owner_id() << ", parent->root: #" << + TRACE("is_diseq_bug", tout << "parent: #" << parent->get_owner_id() << ", parent->root: #" << parent->get_root()->get_owner_id() << " assignment(parent): " << get_assignment(enode2bool_var(parent)) << " args: #" << parent->get_arg(0)->get_owner_id() << " #" << parent->get_arg(1)->get_owner_id() << "\n";); return true; @@ -1274,7 +1274,7 @@ namespace smt { enode * arg2 = p2->get_arg(j)->get_root(); if (arg1 == arg2) continue; - if ((arg1 == r1 || arg1 == r2) && + if ((arg1 == r1 || arg1 == r2) && (arg2 == r1 || arg2 == r2)) continue; break; @@ -1353,8 +1353,8 @@ namespace smt { expr * arg = r->get_owner()->get_arg(i); SASSERT(e_internalized(arg)); enode * _arg = get_enode(arg); - CTRACE("eq_to_bug", args[i]->get_root() != _arg->get_root(), - tout << "#" << args[i]->get_owner_id() << " #" << args[i]->get_root()->get_owner_id() + CTRACE("eq_to_bug", args[i]->get_root() != _arg->get_root(), + tout << "#" << args[i]->get_owner_id() << " #" << args[i]->get_root()->get_owner_id() << " #" << _arg->get_owner_id() << " #" << _arg->get_root()->get_owner_id() << "\n"; tout << "#" << r->get_owner_id() << "\n"; display(tout);); @@ -1367,8 +1367,8 @@ namespace smt { } /** - \brief Process the equality propagation queue. - + \brief Process the equality propagation queue. + \remark The method assign_eq adds a new entry on this queue. */ bool context::propagate_eqs() { @@ -1385,7 +1385,7 @@ namespace smt { std::cout << counter1 << " " << counter2 << "\n"; #endif add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification); - if (inconsistent()) + if (inconsistent()) return false; } m_eq_propagation_queue.reset(); @@ -1403,7 +1403,7 @@ namespace smt { bool_var v = l.var(); bool_var_data & d = get_bdata(v); lbool val = get_assignment(v); - TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() + TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() << " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";); SASSERT(val != l_undef); if (d.is_enode()) @@ -1435,7 +1435,7 @@ namespace smt { // Remark: when RELEVANCY_LEMMA is true, a quantifier can be asserted to false and marked as relevant. // This happens when a quantifier is part of a lemma (conflict-clause), and this conflict clause // becomes an unit-clause and the remaining literal is the negation of a quantifier. - CTRACE("assign_quantifier_bug", get_assignment(v) != l_true, + CTRACE("assign_quantifier_bug", get_assignment(v) != l_true, tout << "#" << bool_var2expr(v)->get_id() << " val: " << get_assignment(v) << "\n"; tout << mk_pp(bool_var2expr(v), m_manager) << "\n"; display(tout);); @@ -1562,7 +1562,7 @@ namespace smt { /** \brief Return the truth assignment for an expression that is attached to a boolean variable. - + \pre The expression must be attached to a boolean variable. */ inline lbool context::get_assignment_core(expr * n) const { @@ -1582,7 +1582,7 @@ namespace smt { lbool context::get_assignment(expr * n) const { if (m_manager.is_false(n)) return l_false; - if (m_manager.is_not(n)) + if (m_manager.is_not(n)) return ~get_assignment_core(to_app(n)->get_arg(0)); return get_assignment_core(n); } @@ -1621,14 +1621,14 @@ namespace smt { */ void context::get_assignments(expr_ref_vector& assignments) { literal_vector::const_iterator it = m_assigned_literals.begin(); - literal_vector::const_iterator end = m_assigned_literals.end(); + literal_vector::const_iterator end = m_assigned_literals.end(); for (; it != end; ++it) { expr_ref e(m_manager); literal2expr(*it, e); assignments.push_back(e); } } - + void context::relevant_eh(expr * n) { if (b_internalized(n)) { bool_var v = get_bool_var(n); @@ -1646,7 +1646,7 @@ namespace smt { #ifndef SMTCOMP m_case_split_queue->relevant_eh(n); #endif - + if (is_app(n)) { if (e_internalized(n)) { SASSERT(relevancy()); @@ -1663,15 +1663,15 @@ namespace smt { propagated_th = th; // <<< mark that relevancy_eh was already invoked for theory th. } } - + if (e_internalized(n)) { - enode * e = get_enode(n); + enode * e = get_enode(n); theory_var_list * l = e->get_th_var_list(); while (l) { theory_id th_id = l->get_th_id(); theory * th = get_theory(th_id); // I don't want to invoke relevant_eh twice for the same n. - if (th != propagated_th) + if (th != propagated_th) th->relevant_eh(to_app(n)); l = l->get_next(); } @@ -1749,7 +1749,7 @@ namespace smt { } bool context::can_propagate() const { - return + return m_qhead != m_assigned_literals.size() || m_relevancy_propagator->can_propagate() || !m_atom_propagation_queue.empty() || @@ -1776,7 +1776,7 @@ namespace smt { } SASSERT(!inconsistent()); propagate_relevancy(qhead); - if (inconsistent()) + if (inconsistent()) return false; if (!propagate_atoms()) return false; @@ -1784,7 +1784,7 @@ namespace smt { return false; propagate_th_eqs(); propagate_th_diseqs(); - if (inconsistent()) + if (inconsistent()) return false; if (!propagate_theories()) return false; @@ -1820,11 +1820,11 @@ namespace smt { return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings); } - bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, + bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation, ptr_vector & used_enodes) { return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes); } - + void context::rescale_bool_var_activity() { TRACE("case_split", tout << "rescale\n";); svector::iterator it = m_activity.begin(); @@ -1851,15 +1851,15 @@ namespace smt { static unsigned counter = 0; counter++; if (counter % 100 == 0) { - TRACE("activity_profile", + TRACE("activity_profile", for (unsigned i=0; i m_lit_occs[(~l).index()].size(); + is_pos = m_lit_occs[l.index()].size() > m_lit_occs[(~l).index()].size(); break; } default: @@ -1972,7 +1972,7 @@ namespace smt { m_fingerprints.push_scope(); m_case_split_queue->push_scope(); m_asserted_formulas.push_scope(); - + ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); for (; it != end; ++it) @@ -1989,7 +1989,7 @@ namespace smt { /** \brief Remove watch literal idx from the given clause. - + \pre idx must be 0 or 1. */ void context::remove_watch_literal(clause * cls, unsigned idx) { @@ -2015,13 +2015,13 @@ namespace smt { } /** - \brief Delete the given clause. - + \brief Delete the given clause. + \pre Clause is not in the reinit stack. */ void context::del_clause(clause * cls) { SASSERT(m_flushing || !cls->in_reinit_stack()); - if (!cls->deleted()) + if (!cls->deleted()) remove_cls_occs(cls); cls->deallocate(m_manager); m_stats.m_num_del_clause++; @@ -2067,7 +2067,7 @@ namespace smt { d.set_null_justification(); m_case_split_queue->unassign_var_eh(v); } - + m_assigned_literals.shrink(old_lim); m_qhead = old_lim; SASSERT(m_qhead == m_assigned_literals.size()); @@ -2137,8 +2137,8 @@ namespace smt { /** \brief When a clause is reinitialized (see reinit_clauses) enodes and literals may need to be recreated. When an enode is recreated, I want to use the same generation - number it had before being deleted. Otherwise the generation will be 0, and will affect - the loop prevetion heuristics used to control quantifier instantiation. + number it had before being deleted. Otherwise the generation will be 0, and will affect + the loop prevetion heuristics used to control quantifier instantiation. Thus, I cache the generation number of enodes that will be deleted during backtracking and recreated by reinit_clauses. */ @@ -2184,11 +2184,11 @@ namespace smt { for(unsigned i = 0; i < num_lits; i++) { bool_var v = lits[i].var(); unsigned ilvl = get_intern_level(v); - if (ilvl > new_scope_lvl) + if (ilvl > new_scope_lvl) cache_generation(bool_var2expr(v), new_scope_lvl); } } - + /** \brief See cache_generation(unsigned new_scope_lvl) */ @@ -2223,7 +2223,7 @@ namespace smt { } } } - + /** \brief See cache_generation(unsigned new_scope_lvl) */ @@ -2235,7 +2235,7 @@ namespace smt { /** \brief Reinitialize learned clauses (lemmas) that contain boolean variables that were deleted during backtracking. - + \remark num_bool_vars contains the number of boolean variables alive after backtracking. So, a clause contains a dead variable if it contains a literal l where l.var() >= num_bool_vars. @@ -2290,20 +2290,20 @@ namespace smt { } } } - + unsigned ilvl = 0; (void)ilvl; for (unsigned j = 0; j < num; j++) { expr * atom = cls->get_atom(j); bool sign = cls->get_atom_sign(j); - // Atom can be (NOT foo). This can happen, for example, when + // Atom can be (NOT foo). This can happen, for example, when // the NOT-application is a child of an uninterpreted function symbol. // So, when reinternalizing the NOT-atom I should set the gate_ctx to false, // and force expression to be reinternalized. // Otherwise I set gate_ctx to true bool gate_ctx = !m_manager.is_not(atom); internalize(atom, gate_ctx); - SASSERT(b_internalized(atom)); + SASSERT(b_internalized(atom)); bool_var v = get_bool_var(atom); DEBUG_CODE({ if (get_intern_level(v) > ilvl) @@ -2322,7 +2322,7 @@ namespace smt { if (lit_occs_enabled()) add_lit_occs(cls); - + literal l1 = cls->get_literal(0); literal l2 = cls->get_literal(1); @@ -2330,9 +2330,9 @@ namespace smt { set_conflict(b_justification(cls)); else if (get_assignment(l2) == l_false) assign(l1, b_justification(cls)); - + TRACE("reinit_clauses", tout << "reinit clause:\n"; display_clause_detail(tout, cls); tout << "\n"; - tout << "activity: " << cls->get_activity() << ", num_bool_vars: " << num_bool_vars << ", scope_lvl: " + tout << "activity: " << cls->get_activity() << ", num_bool_vars: " << num_bool_vars << ", scope_lvl: " << m_scope_lvl << "\n";); keep = true; } @@ -2349,8 +2349,8 @@ namespace smt { keep = true; } } - - // SASSERT(!(cls->get_num_literals() == 3 && + + // SASSERT(!(cls->get_num_literals() == 3 && // (cls->get_literal(0).index() == 624 || cls->get_literal(0).index() == 103 || cls->get_literal(0).index() == 629) && // (cls->get_literal(1).index() == 624 || cls->get_literal(1).index() == 103 || cls->get_literal(1).index() == 629) && // (cls->get_literal(2).index() == 624 || cls->get_literal(2).index() == 103 || cls->get_literal(2).index() == 629))); @@ -2398,7 +2398,7 @@ namespace smt { of boolean variables before reinitializing clauses. This value is useful because it can be used to detect which boolean variables were deleted. - + \warning This method will not invoke reset_cache_generation. */ unsigned context::pop_scope_core(unsigned num_scopes) { @@ -2406,25 +2406,25 @@ namespace smt { try { if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; - + TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";); TRACE("pop_scope_detail", display(tout);); SASSERT(num_scopes > 0); SASSERT(num_scopes <= m_scope_lvl); SASSERT(m_scopes.size() == m_scope_lvl); - + unsigned new_lvl = m_scope_lvl - num_scopes; - + cache_generation(new_lvl); m_qmanager->pop(num_scopes); m_case_split_queue->pop_scope(num_scopes); - + TRACE("pop_scope", tout << "backtracking: " << num_scopes << ", new_lvl: " << new_lvl << "\n";); scope & s = m_scopes[new_lvl]; TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); - + unsigned units_to_reassert_lim = s.m_units_to_reassert_lim; - + if (new_lvl < m_base_lvl) { base_scope & bs = m_base_scopes[new_lvl]; del_clauses(m_lemmas, bs.m_lemmas_lim); @@ -2441,35 +2441,35 @@ namespace smt { m_not_l = null_literal; } del_clauses(m_aux_clauses, s.m_aux_clauses_lim); - + m_relevancy_propagator->pop(num_scopes); - + m_fingerprints.pop_scope(num_scopes); unassign_vars(s.m_assigned_literals_lim); undo_trail_stack(s.m_trail_stack_lim); - + for (theory* th : m_theory_set) { th->pop_scope_eh(num_scopes); } - + del_justifications(m_justifications, s.m_justifications_lim); - + m_asserted_formulas.pop_scope(num_scopes); - + m_eq_propagation_queue.reset(); m_th_eq_propagation_queue.reset(); m_th_diseq_propagation_queue.reset(); m_atom_propagation_queue.reset(); - + m_region.pop_scope(num_scopes); m_scopes.shrink(new_lvl); - + m_scope_lvl = new_lvl; if (new_lvl < m_base_lvl) { m_base_lvl = new_lvl; m_search_lvl = new_lvl; // Remark: not really necessary } - + unsigned num_bool_vars = get_num_bool_vars(); // any variable >= num_bool_vars was deleted during backtracking. reinit_clauses(num_scopes, num_bool_vars); @@ -2516,32 +2516,32 @@ namespace smt { bool context::simplify_clause(clause * cls) { SASSERT(m_scope_lvl == m_base_lvl); unsigned s = cls->get_num_literals(); - if (get_assignment(cls->get_literal(0)) == l_true || + if (get_assignment(cls->get_literal(0)) == l_true || get_assignment(cls->get_literal(1)) == l_true) { // clause is already satisfied. - return true; + return true; } - + literal_buffer simp_lits; unsigned i = 2; - unsigned j = i; - for(; i < s; i++) { + unsigned j = i; + for(; i < s; i++) { literal l = cls->get_literal(i); switch(get_assignment(l)) { - case l_false: - if (m_manager.proofs_enabled()) + case l_false: + if (m_manager.proofs_enabled()) simp_lits.push_back(~l); - if (lit_occs_enabled()) + if (lit_occs_enabled()) m_lit_occs[l.index()].erase(cls); break; - case l_undef: + case l_undef: cls->set_literal(j, l); j++; break; - case l_true: + case l_true: return true; - } + } } if (j < s) { @@ -2554,15 +2554,15 @@ namespace smt { justification * js = cls->get_justification(); justification * new_js = 0; if (js->in_region()) - new_js = mk_justification(unit_resolution_justification(m_region, - js, + new_js = mk_justification(unit_resolution_justification(m_region, + js, simp_lits.size(), simp_lits.c_ptr())); else new_js = alloc(unit_resolution_justification, js, simp_lits.size(), simp_lits.c_ptr()); cls->set_justification(new_js); } - return false; + return false; } /** @@ -2598,7 +2598,7 @@ namespace smt { SASSERT(m_search_lvl == m_base_lvl); literal_buffer simp_lits; unsigned num_lits = cls->get_num_literals(); - for(unsigned i = 0; i < num_lits; i++) { + for(unsigned i = 0; i < num_lits; i++) { if (i != idx) { literal l = cls->get_literal(i); SASSERT(l != l0); @@ -2610,13 +2610,13 @@ namespace smt { if (!cls_js || cls_js->in_region()) { // If cls_js is 0 or is allocated in a region, then // we can allocate the new justification in a region too. - js = mk_justification(unit_resolution_justification(m_region, + js = mk_justification(unit_resolution_justification(m_region, cls_js, simp_lits.size(), - simp_lits.c_ptr())); + simp_lits.c_ptr())); } else { - js = alloc(unit_resolution_justification, cls_js, simp_lits.size(), simp_lits.c_ptr()); + js = alloc(unit_resolution_justification, cls_js, simp_lits.size(), simp_lits.c_ptr()); // js took ownership of the justification object. cls->set_justification(0); m_justifications.push_back(js); @@ -2648,7 +2648,7 @@ namespace smt { // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed. if (m_scope_lvl > m_base_lvl) return; - + unsigned sz = m_assigned_literals.size(); SASSERT(m_simp_qhead <= sz); @@ -2678,7 +2678,7 @@ namespace smt { // a variable during propagation. // m_simp_counter = 0; - // the field m_simp_qhead is used to check whether there are + // the field m_simp_qhead is used to check whether there are // new assigned literals at the base level. m_simp_qhead = m_assigned_literals.size(); @@ -2709,13 +2709,15 @@ namespace smt { \brief Delete low activity lemmas */ inline void context::del_inactive_lemmas() { - if (m_fparams.m_lemma_gc_half) + if (m_fparams.m_lemma_gc_strategy == LGC_NONE) + return; + else if (m_fparams.m_lemma_gc_half) del_inactive_lemmas1(); else del_inactive_lemmas2(); m_num_conflicts_since_lemma_gc = 0; - if (m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC) + if (m_fparams.m_lemma_gc_strategy == LGC_GEOMETRIC) m_lemma_gc_threshold = static_cast(m_lemma_gc_threshold * m_fparams.m_lemma_gc_factor); } @@ -2737,12 +2739,12 @@ namespace smt { unsigned i = start_del_at; unsigned j = i; unsigned num_del_cls = 0; - TRACE("del_inactive_lemmas", tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at + TRACE("del_inactive_lemmas", tout << "sz: " << sz << ", start_at: " << start_at << ", end_at: " << end_at << ", start_del_at: " << start_del_at << "\n";); for (; i < end_at; i++) { clause * cls = m_lemmas[i]; if (can_delete(cls)) { - TRACE("del_inactive_lemmas", tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " << + TRACE("del_inactive_lemmas", tout << "deleting: "; display_clause(tout, cls); tout << ", activity: " << cls->get_activity() << "\n";); del_clause(cls); num_del_cls++; @@ -2763,7 +2765,7 @@ namespace smt { m_lemmas[j] = cls; j++; } - } + } m_lemmas.shrink(j); if (m_fparams.m_clause_decay > 1) { // rescale activity @@ -2805,7 +2807,7 @@ namespace smt { } // A clause is deleted if it has low activity and the number of unknowns is greater than a threshold. // The activity threshold depends on how old the clause is. - unsigned act_threshold = m_fparams.m_old_clause_activity - + unsigned act_threshold = m_fparams.m_old_clause_activity - (m_fparams.m_old_clause_activity - m_fparams.m_new_clause_activity) * ((i - start_at) / real_sz); if (cls->get_activity() < act_threshold) { unsigned rel_threshold = (i >= new_first_idx ? m_fparams.m_new_clause_relevancy : m_fparams.m_old_clause_relevancy); @@ -2843,10 +2845,10 @@ namespace smt { return false; } - void context::register_plugin(simplifier_plugin * s) { + void context::register_plugin(simplifier_plugin * s) { SASSERT(!already_internalized()); SASSERT(m_scope_lvl == 0); - m_asserted_formulas.register_simplifier_plugin(s); + m_asserted_formulas.register_simplifier_plugin(s); } #ifdef Z3DEBUG @@ -2873,7 +2875,7 @@ namespace smt { } #endif - void context::register_plugin(theory * th) { + void context::register_plugin(theory * th) { if (m_theories.get_plugin(th->get_family_id()) != 0) { dealloc(th); return; // context already has a theory for the given family id. @@ -2881,7 +2883,7 @@ namespace smt { SASSERT(std::find(m_theory_set.begin(), m_theory_set.end(), th) == m_theory_set.end()); SASSERT(!already_internalized_theory(th)); th->init(this); - m_theories.register_plugin(th); + m_theories.register_plugin(th); m_theory_set.push_back(th); { #ifdef Z3DEBUG @@ -2933,18 +2935,18 @@ namespace smt { ptr_vector::iterator it = m_theory_set.begin(); ptr_vector::iterator end = m_theory_set.end(); for (; it != end; ++it) - (*it)->flush_eh(); + (*it)->flush_eh(); undo_trail_stack(0); m_qmanager = 0; del_clauses(m_aux_clauses, 0); del_clauses(m_lemmas, 0); del_justifications(m_justifications, 0); - if (m_is_diseq_tmp) { + if (m_is_diseq_tmp) { m_is_diseq_tmp->del_eh(m_manager, false); - m_manager.dec_ref(m_is_diseq_tmp->get_owner()); + m_manager.dec_ref(m_is_diseq_tmp->get_owner()); enode::del_dummy(m_is_diseq_tmp); - m_is_diseq_tmp = 0; - } + m_is_diseq_tmp = 0; + } std::for_each(m_almost_cg_tables.begin(), m_almost_cg_tables.end(), delete_proc()); } @@ -3042,7 +3044,7 @@ namespace smt { // not counting any literals that get assigned by this method // this relies on bcp() to give us its old m_qhead and therefore // bcp() should always be called before this method - + unsigned assigned_literal_end = m_assigned_literals.size(); for (; qhead < assigned_literal_end; ++qhead) { literal l = m_assigned_literals[qhead]; @@ -3129,7 +3131,7 @@ namespace smt { return true; if (m.is_not(assumption, arg) && is_uninterp_const(arg)) return true; - if (!is_app(assumption)) + if (!is_app(assumption)) return false; if (to_app(assumption)->get_num_args() == 0) return true; @@ -3146,7 +3148,7 @@ namespace smt { SASSERT(assumptions[i]); if (!is_valid_assumption(m_manager, assumptions[i])) { warning_msg("an assumption must be a propositional variable or the negation of one"); - return false; + return false; } } return true; @@ -3158,11 +3160,11 @@ namespace smt { m_unsat_core.reset(); if (num_assumptions > 0) { // We must give a chance to the theories to propagate before we create a new scope... - propagate(); + propagate(); // Internal backtracking scopes (created with push_scope()) must only be created when we are // in a consistent context. if (inconsistent()) - return; + return; if (get_cancel_flag()) return; push_scope(); @@ -3270,9 +3272,9 @@ namespace smt { /** \brief Setup the logical context based on the current set of asserted formulas and execute the check command. - + \remark A logical context can only be configured at scope level 0, - and before internalizing any formulas. + and before internalizing any formulas. */ lbool context::setup_and_check(bool reset_cancel) { if (!check_preamble(reset_cancel)) @@ -3371,7 +3373,7 @@ namespace smt { expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions); if (!already_did_theory_assumptions) { - add_theory_assumptions(all_assumptions); + add_theory_assumptions(all_assumptions); } unsigned num_assumptions = all_assumptions.size(); @@ -3484,7 +3486,7 @@ namespace smt { lbool context::search() { -#ifndef _EXTERNAL_RELEASE +#ifndef _EXTERNAL_RELEASE if (m_fparams.m_abort_after_preproc) { exit(1); } @@ -3507,16 +3509,16 @@ namespace smt { status = bounded_search(); TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";); - TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); + TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); tout << ", num_assigned: " << m_assigned_literals.size() << "\n";); - + if (!restart(status, curr_lvl)) { break; } } - + TRACE("search_lite", tout << "status: " << status << "\n";); - TRACE("guessed_literals", + TRACE("guessed_literals", expr_ref_vector guessed_lits(m_manager); get_guessed_literals(guessed_lits); unsigned sz = guessed_lits.size(); @@ -3547,7 +3549,7 @@ namespace smt { // possible outcomes DONE l_true, DONE l_undef, CONTINUE quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value()); if (cmr == quantifier_manager::SAT) { - // done + // done status = l_true; return false; } @@ -3562,7 +3564,7 @@ namespace smt { inc_limits(); if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) { SASSERT(!inconsistent()); - IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations + IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations << " :decisions " << m_stats.m_num_decisions << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold; if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) { @@ -3582,9 +3584,9 @@ namespace smt { ptr_vector::iterator end = m_theory_set.end(); for (; it != end && !inconsistent(); ++it) (*it)->restart_eh(); - TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); + TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); if (!inconsistent()) { - m_qmanager->restart_eh(); + m_qmanager->restart_eh(); } if (inconsistent()) { VERIFY(!resolve_conflict()); @@ -3600,7 +3602,7 @@ namespace smt { status = l_undef; return true; } - + void context::tick(unsigned & counter) const { counter++; if (counter > m_fparams.m_tick) { @@ -3617,7 +3619,7 @@ namespace smt { lbool context::bounded_search() { unsigned counter = 0; - + TRACE("bounded_search", tout << "starting bounded search...\n";); while (true) { @@ -3636,14 +3638,14 @@ namespace smt { return l_false; SASSERT(m_scope_lvl >= m_base_lvl); - + if (!inconsistent()) { if (resource_limits_exceeded()) return l_undef; if (get_cancel_flag()) return l_undef; - + if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) { TRACE("search_bug", tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";); return l_undef; // restart @@ -3664,7 +3666,7 @@ namespace smt { m_dyn_ack_manager.propagate_eh(); CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses)); } - + if (resource_limits_exceeded() && !inconsistent()) { return l_undef; } @@ -3674,7 +3676,7 @@ namespace smt { if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses) simplify_clauses(); - + if (!decide()) { final_check_status fcs = final_check(); TRACE("final_check_result", tout << "fcs: " << fcs << " last_search_failure: " << m_last_search_failure << "\n";); @@ -3697,11 +3699,11 @@ namespace smt { bool context::resource_limits_exceeded() { if (m_searching) { - // Some of the flags only make sense to check when searching. + // Some of the flags only make sense to check when searching. // For example, the timer is only started in init_search(). if (m_last_search_failure != OK) return true; - + if (m_timer.ms_timeout(m_fparams.m_timeout)) { m_last_search_failure = TIMEOUT; return true; @@ -3715,12 +3717,12 @@ namespace smt { } } } - + if (get_cancel_flag()) { m_last_search_failure = CANCELED; return true; } - + if (memory::above_high_watermark()) { m_last_search_failure = MEMOUT; return true; @@ -3771,15 +3773,15 @@ namespace smt { ok = m_qmanager->final_check_eh(true); TRACE("final_check_step", tout << "quantifier ok: " << ok << " " << "inconsistent " << inconsistent() << "\n";); } - + m_final_check_idx = (m_final_check_idx + 1) % range; // IF_VERBOSE(1000, verbose_stream() << "final check status: " << ok << "\n";); - + switch (ok) { - case FC_DONE: + case FC_DONE: break; case FC_GIVEUP: - result = FC_GIVEUP; + result = FC_GIVEUP; break; case FC_CONTINUE: return FC_CONTINUE; @@ -3844,23 +3846,23 @@ namespace smt { unsigned new_lvl = m_conflict_resolution->get_new_scope_lvl(); unsigned num_lits = m_conflict_resolution->get_lemma_num_literals(); literal * lits = m_conflict_resolution->get_lemma_literals(); - + SASSERT(num_lits > 0); unsigned conflict_lvl = get_assign_level(lits[0]); SASSERT(conflict_lvl <= m_scope_lvl); - // When num_lits == 1, then the default behavior is to go + // When num_lits == 1, then the default behavior is to go // to base-level. If the problem has quantifiers, it may be // too expensive to do that, since all instances will need to // be recreated. If that is the case, I store the assertions in // a special vector and keep reasserting whenever I backtrack. // Moreover, I backtrack only one level. - bool delay_forced_restart = + bool delay_forced_restart = m_fparams.m_delay_units && - internalized_quantifiers() && - num_lits == 1 && - conflict_lvl > m_search_lvl + 1 && - !m_manager.proofs_enabled() && + internalized_quantifiers() && + num_lits == 1 && + conflict_lvl > m_search_lvl + 1 && + !m_manager.proofs_enabled() && m_units_to_reassert.size() < m_fparams.m_delay_units_threshold; if (delay_forced_restart) { new_lvl = conflict_lvl - 1; @@ -3868,20 +3870,20 @@ namespace smt { // Some of the literals/enodes of the conflict clause will be destroyed during // backtracking, and will need to be recreated. However, I want to keep - // the generation number for enodes that are going to be recreated. See + // the generation number for enodes that are going to be recreated. See // comment in cache_generation(unsigned). if (m_conflict_resolution->get_lemma_intern_lvl() > new_lvl) cache_generation(num_lits, lits, new_lvl); SASSERT(new_lvl < m_scope_lvl); - TRACE("resolve_conflict_bug", + TRACE("resolve_conflict_bug", tout << "m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n"; tout << "num_lits: " << num_lits << "\n"; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; tout << l << " "; - display_literal(tout, l); - tout << ", ilvl: " << get_intern_level(l.var()) << "\n" + display_literal(tout, l); + tout << ", ilvl: " << get_intern_level(l.var()) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n"; }); @@ -3891,7 +3893,7 @@ namespace smt { m_manager.trace_stream() << "\n"; } -#ifdef Z3DEBUG +#ifdef Z3DEBUG expr_ref_vector expr_lits(m_manager); svector expr_signs; for (unsigned i = 0; i < num_lits; i++) { @@ -3906,7 +3908,7 @@ namespace smt { pr = m_conflict_resolution->get_lemma_proof(); // check_proof(pr); TRACE("context_proof", tout << mk_ll_pp(pr, m_manager);); - TRACE("context_proof_hack", + TRACE("context_proof_hack", static ast_mark visited; ast_ll_pp(tout, m_manager, pr, visited);); } @@ -3948,15 +3950,15 @@ namespace smt { if (relevancy()) restore_relevancy(num_lits, lits); // Resetting the cache manually because I did not invoke pop_scope, but pop_scope_core reset_cache_generation(); - TRACE("resolve_conflict_bug", - tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << + TRACE("resolve_conflict_bug", + tout << "AFTER m_scope_lvl: " << m_scope_lvl << ", new_lvl: " << new_lvl << ", lemma_intern_lvl: " << m_conflict_resolution->get_lemma_intern_lvl() << "\n"; tout << "num_lits: " << num_lits << "\n"; for (unsigned i = 0; i < num_lits; i++) { literal l = lits[i]; tout << l << " "; - display_literal(tout, l); - tout << ", ilvl: " << get_intern_level(l.var()) << "\n" + display_literal(tout, l); + tout << ", ilvl: " << get_intern_level(l.var()) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n"; }); #ifdef Z3DEBUG @@ -3980,7 +3982,7 @@ namespace smt { } #if 0 { - static unsigned counter = 0; + static unsigned counter = 0; static uint64 total = 0; static unsigned max = 0; counter++; @@ -4006,13 +4008,13 @@ namespace smt { m_units_to_reassert_sign.push_back(unit_sign); TRACE("reassert_units", tout << "asserting #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";); } - + m_conflict_resolution->release_lemma_atoms(); - TRACE("context_lemma", tout << "new lemma: "; + TRACE("context_lemma", tout << "new lemma: "; literal_vector v(num_lits, lits); std::sort(v.begin(), v.end()); for (unsigned i = 0; i < num_lits; i++) { - display_literal(tout, v[i]); + display_literal(tout, v[i]); tout << "\n"; v[i].display(tout, m_manager, m_bool_var2expr.c_ptr()); tout << "\n\n"; @@ -4028,7 +4030,7 @@ namespace smt { } return false; } - + /* \brief we record and restore relevancy information for literals in conflict clauses. A literal may have been marked relevant within the scope that gets popped during @@ -4064,11 +4066,11 @@ namespace smt { if (!checker.check(fml)) { warning_msg("Boogie generated formula that can require multiple '@' labels in a counter-example"); break; - } + } } } } - + SASSERT(!inconsistent()); unsigned sz = m_b_internalized_stack.size(); for (unsigned i = 0; i < sz; i++) { @@ -4079,7 +4081,7 @@ namespace smt { } } } - + /** \brief Collect relevant literals that may be used to block the current assignment. If at_lbls is true, then only labels that contains '@' are considered. (This is a hack for Boogie). @@ -4192,7 +4194,7 @@ namespace smt { } bool r = false; if (!b_internalized(eq)) { - // I do not invoke internalize(eq, true), because I want to + // I do not invoke internalize(eq, true), because I want to // mark the try_true_first flag before invoking theory::internalize_eq_eh. // Reason: Theories like arithmetic should be able to know if the try_true_first flag is // marked or not. They use this information to also mark auxiliary atoms such as: @@ -4254,13 +4256,13 @@ namespace smt { if (m_qmanager->is_shared(n)) { return true; } - - // the variabe is shared if the equivalence class of n + + // the variabe is shared if the equivalence class of n // contains a parent application. - + theory_var_list * l = n->get_th_var_list(); theory_id th_id = l->get_th_id(); - + enode_vector::const_iterator it = n->begin_parents(); enode_vector::const_iterator end = n->end_parents(); for (; it != end; ++it) { @@ -4271,12 +4273,12 @@ namespace smt { return true; } } - + // Some theories implement families of theories. Examples: // Arrays and Tuples. For example, array theory is a // parametric theory, that is, it implements several theories: // (array int int), (array int (array int int)), ... - // + // // Example: // // a : (array int int) @@ -4323,18 +4325,18 @@ namespace smt { if (fcs == FC_DONE) { mk_proto_model(l_true); m_model = m_proto_model->mk_model(); - add_rec_funs_to_model(); + add_rec_funs_to_model(); } - + return fcs == FC_DONE; } void context::mk_proto_model(lbool r) { - TRACE("get_model", - display(tout); + TRACE("get_model", + display(tout); display_normalized_enodes(tout); display_enodes_lbls(tout); - m_fingerprints.display(tout); + m_fingerprints.display(tout); ); failure fl = get_last_search_failure(); if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) { @@ -4351,7 +4353,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); - } + } else { } @@ -4363,19 +4365,19 @@ namespace smt { return m_unsat_proof; } - void context::get_model(model_ref & m) const { + void context::get_model(model_ref & m) const { if (inconsistent()) m = 0; else - m = const_cast(m_model.get()); + m = const_cast(m_model.get()); } void context::get_proto_model(proto_model_ref & m) const { m = const_cast(m_proto_model.get()); } - failure context::get_last_search_failure() const { - return m_last_search_failure; + failure context::get_last_search_failure() const { + return m_last_search_failure; } void context::add_rec_funs_to_model() { @@ -4394,7 +4396,7 @@ namespace smt { func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity()); fi->set_else(body); - m_model->register_decl(f, fi); + m_model->register_decl(f, fi); } } }