From 2f8465552cd05e7f8fd66885c01f40bf9f9b8094 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Thu, 18 Feb 2016 17:08:54 +0000 Subject: [PATCH 1/4] additional logging --- src/ackermannization/ackermannize_bv_tactic.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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()); } From a2140085d6197716fe69d94ed78ce5c5715fa8e2 Mon Sep 17 00:00:00 2001 From: mikolas Date: Fri, 26 Feb 2016 13:02:59 +0000 Subject: [PATCH 2/4] In lazy ackermannization, collect all conflicting terms in one iteration. --- .../lackr_model_constructor.cpp | 35 ++++++++++++------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 09034fa36..3ff7d2c10 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -60,15 +60,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; } @@ -144,6 +146,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 +155,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 +182,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; } From ae9f369574e6a94d0d008a38c8205160fe5b3f8b Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Fri, 26 Feb 2016 14:48:00 +0000 Subject: [PATCH 3/4] Fix in lackr_model_constructor. --- src/ackermannization/lackr_model_constructor.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 3ff7d2c10..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(); @@ -136,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; }; @@ -221,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'; ); From 419e2c4899a55ea8e698a00cd6abff5638de7032 Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 29 Feb 2016 11:39:52 +0000 Subject: [PATCH 4/4] Inc sat for ackr. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 12 ++++++++++-- src/tactic/smtlogics/qfufbv_tactic_params.pyg | 1 + 2 files changed, 11 insertions(+), 2 deletions(-) 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'), ))