diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 123b496a1..f9c48c2bd 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -38,6 +38,7 @@ public: tactic_report report("ackermannize", *g); fail_if_unsat_core_generation("ackermannize", g); fail_if_proof_generation("ackermannize", g); + TRACE("ackermannize", g->display(tout << "in\n");); expr_ref_vector flas(m); const unsigned sz = g->size(); @@ -48,6 +49,7 @@ public: goal_ref resg(alloc(goal, *g, true)); const bool success = lackr.mk_ackermann(resg, m_lemma_limit); if (!success) { // Just pass on the input unchanged + TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;); result.reset(); result.push_back(g.get()); mc = 0; @@ -62,7 +64,7 @@ public: } resg->inc_depth(); - TRACE("ackermannize", resg->display(tout);); + TRACE("ackermannize", resg->display(tout << "out\n");); SASSERT(resg->is_well_sorted()); } diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 09034fa36..8e99fe2a2 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -34,11 +34,13 @@ struct lackr_model_constructor::imp { , m_conflicts(conflicts) , m_b_rw(m) , m_bv_rw(m) + , m_evaluator(NULL) , m_empty_model(m) , m_ackr_helper(m) {} ~imp() { + if (m_evaluator) dealloc(m_evaluator); { values2val_t::iterator i = m_values2val.begin(); const values2val_t::iterator e = m_values2val.end(); @@ -60,15 +62,17 @@ struct lackr_model_constructor::imp { // // Returns true iff model was successfully constructed. + // Conflicts are saved as a side effect. // bool check() { + bool retv = true; for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) { func_decl * const c = m_abstr_model->get_constant(i); - app * const term = m_info->find_term(c); - if (term) m_stack.push_back(term); - else m_stack.push_back(m_m.mk_const(c)); + app * const _term = m_info->find_term(c); + expr * const term = _term ? _term : m_m.mk_const(c); + if (!check_term(term)) retv = false; } - return run(); + return retv; } @@ -134,7 +138,7 @@ struct lackr_model_constructor::imp { conflict_list& m_conflicts; bool_rewriter m_b_rw; bv_rewriter m_bv_rw; - scoped_ptr m_evaluator; + model_evaluator * m_evaluator; model m_empty_model; private: struct val_info { expr * value; app * source_term; }; @@ -144,6 +148,7 @@ struct lackr_model_constructor::imp { app2val_t m_app2val; ptr_vector m_stack; ackr_helper m_ackr_helper; + expr_mark m_visited; static inline val_info mk_val_info(expr* value, app* source_term) { val_info rv; @@ -152,17 +157,23 @@ struct lackr_model_constructor::imp { return rv; } - // + // Performs congruence check on a given term. + bool check_term(expr * term) { + m_stack.push_back(term); + const bool rv = _check_stack(); + m_stack.reset(); + return rv; + } + // Performs congruence check on terms on the stack. - // (Currently stops upon the first failure). - // Returns true if and only if congruence check succeeded. - bool run() { - m_evaluator = alloc(model_evaluator, m_empty_model); - expr_mark visited; + // Stops upon the first failure. + // Returns true if and only if all congruence checks succeeded. + bool _check_stack() { + if (m_evaluator == NULL) m_evaluator = alloc(model_evaluator, m_empty_model); expr * curr; while (!m_stack.empty()) { curr = m_stack.back(); - if (visited.is_marked(curr)) { + if (m_visited.is_marked(curr)) { m_stack.pop_back(); continue; } @@ -173,8 +184,8 @@ struct lackr_model_constructor::imp { return false; case AST_APP: { app * a = to_app(curr); - if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) { - visited.mark(a, true); + if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) { + m_visited.mark(a, true); m_stack.pop_back(); if (!mk_value(a)) return false; } @@ -212,7 +223,11 @@ struct lackr_model_constructor::imp { for (unsigned i = 0; i < num; ++i) { expr * val; const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app? - CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); ); + CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; ); + if (!b) { + // bailing out because args eval failed previously + return false; + } TRACE("model_constructor", tout << "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2) << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; ); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 421a76cc7..3ee97308a 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -47,6 +47,7 @@ public: : m_m(m) , m_p(p) , m_use_sat(false) + , m_inc_use_sat(false) {} virtual ~qfufbv_ackr_tactic() { } @@ -85,6 +86,7 @@ public: void updt_params(params_ref const & _p) { qfufbv_tactic_params p(_p); m_use_sat = p.sat_backend(); + m_inc_use_sat = p.inc_sat_backend(); } virtual void collect_statistics(statistics & st) const { @@ -105,12 +107,18 @@ private: params_ref m_p; lackr_stats m_st; bool m_use_sat; + bool m_inc_use_sat; solver* setup_sat() { solver * sat(NULL); if (m_use_sat) { - tactic_ref t = mk_qfbv_tactic(m_m, m_p); - sat = mk_tactic2solver(m_m, t.get(), m_p); + if (m_inc_use_sat) { + sat = mk_inc_sat_solver(m_m, m_p); + } + else { + tactic_ref t = mk_qfbv_tactic(m_m, m_p); + sat = mk_tactic2solver(m_m, t.get(), m_p); + } } else { tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); diff --git a/src/tactic/smtlogics/qfufbv_tactic_params.pyg b/src/tactic/smtlogics/qfufbv_tactic_params.pyg index 6c4bd5b8e..b7640538d 100644 --- a/src/tactic/smtlogics/qfufbv_tactic_params.pyg +++ b/src/tactic/smtlogics/qfufbv_tactic_params.pyg @@ -4,5 +4,6 @@ def_module_params('ackermannization', export=True, params=( ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + ('inc_sat_backend', BOOL, False, 'use incremental SAT'), ))