diff --git a/src/tactic/ackr/ackermannize_tactic.cpp b/src/tactic/ackr/ackermannize_tactic.cpp index a1d8917df..6e95d564b 100644 --- a/src/tactic/ackr/ackermannize_tactic.cpp +++ b/src/tactic/ackr/ackermannize_tactic.cpp @@ -38,7 +38,7 @@ public: expr_ref_vector flas(m); const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); - scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas); + scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas, NULL); flas.reset(); // mk result goal_ref resg(alloc(goal, *g, true)); diff --git a/src/tactic/ackr/ackr.pyg b/src/tactic/ackr/ackr.pyg index d1ec8efe2..f2e244cfd 100644 --- a/src/tactic/ackr/ackr.pyg +++ b/src/tactic/ackr/ackr.pyg @@ -1,8 +1,7 @@ def_module_params('ackr', - description='solving UF via ackermannization (currently for QF_UFBV)', + description='solving UF via ackermannization', export=True, params=( ('eager', BOOL, True, 'eagerly instantiate all congruence rules'), - ('sat_backend', BOOL, False, 'use SAT rather than SMT'), )) diff --git a/src/tactic/ackr/ackr_helper.h b/src/tactic/ackr/ackr_helper.h new file mode 100644 index 000000000..60f9639a4 --- /dev/null +++ b/src/tactic/ackr/ackr_helper.h @@ -0,0 +1,43 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + ackr_helper.h + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: + --*/ +#ifndef ACKR_HELPER_H_6475 +#define ACKR_HELPER_H_6475 +#include"bv_decl_plugin.h" +class ackr_helper { + public: + ackr_helper(ast_manager& m) : m_bvutil(m) {} + inline bool should_ackermannize(app const * a) const { + if (a->get_family_id() == m_bvutil.get_family_id()) { + switch (a->get_decl_kind()) { + case OP_BSDIV0: + case OP_BUDIV0: + case OP_BSREM0: + case OP_BUREM0: + case OP_BSMOD0: + return true; + default: + return is_uninterp(a); + } + } + return (is_uninterp(a)); + } + + bv_util& bvutil() { return m_bvutil; } + private: + bv_util m_bvutil; +}; +#endif /* ACKR_HELPER_H_6475 */ diff --git a/src/tactic/ackr/lackr.cpp b/src/tactic/ackr/lackr.cpp index cb1d5e559..05c87bb58 100644 --- a/src/tactic/ackr/lackr.cpp +++ b/src/tactic/ackr/lackr.cpp @@ -22,20 +22,16 @@ #include"ackr_info.h" #include"for_each_expr.h" /////////////// -#include"inc_sat_solver.h" -#include"qfaufbv_tactic.h" -#include"qfbv_tactic.h" -#include"tactic2solver.h" -/////////////// #include"model_smt2_pp.h" /////////////// -lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas) +lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas, + solver * uffree_solver) : m_m(m) , m_p(p) , m_formulas(formulas) , m_abstr(m) - , m_sat(NULL) - , m_bvutil(m) + , m_sat(uffree_solver) + , m_ackr_helper(m) , m_simp(m) , m_ackrs(m) , m_st(st) @@ -52,7 +48,7 @@ lackr::~lackr() { } lbool lackr::operator() () { - setup_sat(); + SASSERT(m_sat); init(); const lbool rv = m_eager ? eager() : lazy(); if (rv == l_true) m_sat->get_model(m_model); @@ -91,7 +87,7 @@ bool lackr::ackr(app * const t1, app * const t2) { expr * const arg1 = t1->get_arg(i); expr * const arg2 = t2->get_arg(i); if (arg1 == arg2) continue; // quickly skip syntactically equal - if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) { + if (m_ackr_helper.bvutil().is_numeral(arg1) && m_ackr_helper.bvutil().is_numeral(arg2)) { // quickly abort if there are two distinct numerals SASSERT(arg1 != arg2); TRACE("lackr", tout << "never eq\n";); @@ -178,9 +174,8 @@ void lackr::abstract() { void lackr::add_term(app* a) { if (a->get_num_args() == 0) return; - if (!should_ackermannize(a)) return; + if (!m_ackr_helper.should_ackermannize(a)) return; func_decl* const fd = a->get_decl(); - SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a)); app_set* ts = 0; if (!m_fun2terms.find(fd, ts)) { ts = alloc(app_set); @@ -239,21 +234,6 @@ lbool lackr::lazy() { } } -void lackr::setup_sat() { - SASSERT(m_sat == NULL); - if (m_use_sat) { - tactic_ref t = mk_qfbv_tactic(m_m, m_p); - m_sat = mk_tactic2solver(m_m, t.get(), m_p); - } - else { - tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); - m_sat = mk_tactic2solver(m_m, t.get(), m_p); - } - SASSERT(m_sat != NULL); - m_sat->set_produce_models(true); -} - - // // Collect all uninterpreted terms, skipping 0-arity. // diff --git a/src/tactic/ackr/lackr.h b/src/tactic/ackr/lackr.h index 3258b9d6c..f684b4b6a 100644 --- a/src/tactic/ackr/lackr.h +++ b/src/tactic/ackr/lackr.h @@ -18,6 +18,7 @@ #define LACKR_H_15079 /////////////// #include"ackr_info.h" +#include"ackr_helper.h" #include"ackr_params.hpp" #include"th_rewriter.h" #include"cooperate.h" @@ -42,12 +43,12 @@ struct lackr_stats { **/ class lackr { public: - lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas); + lackr(ast_manager& m, params_ref p, lackr_stats& st, + expr_ref_vector& formulas, solver * uffree_solver); ~lackr(); void updt_params(params_ref const & _p) { ackr_params p(_p); m_eager = p.eager(); - m_use_sat = p.sat_backend(); } /** \brief @@ -87,18 +88,16 @@ class lackr { expr_ref_vector m_abstr; fun2terms_map m_fun2terms; ackr_info_ref m_info; - scoped_ptr m_sat; - bv_util m_bvutil; + solver* m_sat; + ackr_helper m_ackr_helper; th_rewriter m_simp; expr_ref_vector m_ackrs; model_ref m_model; bool m_eager; - bool m_use_sat; lackr_stats& m_st; bool m_is_init; void init(); - void setup_sat(); lbool eager(); lbool lazy(); @@ -122,24 +121,5 @@ class lackr { // Collect all uninterpreted terms, skipping 0-arity. // void collect_terms(); - - inline bool should_ackermannize(app const * a) const; }; - -inline bool lackr::should_ackermannize(app const * a) const { - if (a->get_family_id() == m_bvutil.get_family_id()) { - switch (a->get_decl_kind()) { - case OP_BSDIV0: - case OP_BUDIV0: - case OP_BSREM0: - case OP_BUREM0: - case OP_BSMOD0: - return true; - default: - return is_uninterp(a); - } - } - return (is_uninterp(a)); -} - #endif /* LACKR_H_15079 */ diff --git a/src/tactic/ackr/lackr_model_constructor.cpp b/src/tactic/ackr/lackr_model_constructor.cpp index 22eb4b40b..2a38a1a4e 100644 --- a/src/tactic/ackr/lackr_model_constructor.cpp +++ b/src/tactic/ackr/lackr_model_constructor.cpp @@ -34,6 +34,7 @@ struct lackr_model_constructor::imp { , m_b_rw(m) , m_bv_rw(m) , m_empty_model(m) + , m_ackr_helper(m) {} ~imp() { @@ -141,6 +142,7 @@ struct lackr_model_constructor::imp { values2val_t m_values2val; app2val_t m_app2val; ptr_vector m_stack; + ackr_helper m_ackr_helper; static inline val_info mk_val_info(expr* value, app* source_term) { val_info rv; @@ -227,7 +229,7 @@ struct lackr_model_constructor::imp { values[i] = val; } // handle functions - if (a->get_family_id() == null_family_id) { // handle uninterpreted + if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m); if (!make_value_uninterpreted_function(a, values, key.get(), result)) { return false; diff --git a/src/tactic/ackr/lackr_model_constructor.h b/src/tactic/ackr/lackr_model_constructor.h index 478efe97f..f74c3c90d 100644 --- a/src/tactic/ackr/lackr_model_constructor.h +++ b/src/tactic/ackr/lackr_model_constructor.h @@ -19,7 +19,9 @@ #define LACKR_MODEL_CONSTRUCTOR_H_626 #include"ast.h" #include"ackr_info.h" +#include"ackr_helper.h" #include"model.h" + class lackr_model_constructor { public: typedef std::pair app_pair; @@ -50,6 +52,7 @@ class lackr_model_constructor { conflict_list m_conflicts; ast_manager& m_m; const ackr_info_ref m_info; + unsigned m_ref_count; // reference counting }; diff --git a/src/tactic/ackr_tactics/ackr_tactics.pyg b/src/tactic/ackr_tactics/ackr_tactics.pyg new file mode 100644 index 000000000..8f391bc91 --- /dev/null +++ b/src/tactic/ackr_tactics/ackr_tactics.pyg @@ -0,0 +1,7 @@ +def_module_params('ackr_tactics', + description='tactics based on solving UF-theories via ackermannization (see also ackr module)', + export=True, + params=( + ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + )) + diff --git a/src/tactic/ackr/qfufbv_ackr_tactic.cpp b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp similarity index 76% rename from src/tactic/ackr/qfufbv_ackr_tactic.cpp rename to src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp index 28a801ce1..4eb3792ff 100644 --- a/src/tactic/ackr/qfufbv_ackr_tactic.cpp +++ b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp @@ -28,14 +28,22 @@ Revision History: #include"model_smt2_pp.h" #include"cooperate.h" #include"lackr.h" -#include"ackr_params.hpp" +#include"ackr_tactics_params.hpp" #include"ackr_model_converter.h" +/////////////// +#include"inc_sat_solver.h" +#include"qfaufbv_tactic.h" +#include"qfbv_tactic.h" +#include"tactic2solver.h" +/////////////// + class qfufbv_ackr_tactic : public tactic { public: qfufbv_ackr_tactic(ast_manager& m, params_ref const& p) : m_m(m) , m_p(p) + , m_use_sat(false) {} virtual ~qfufbv_ackr_tactic() { } @@ -47,12 +55,13 @@ public: expr_dependency_ref & core) { mc = 0; ast_manager& m(g->m()); - TRACE("lackr", g->display(tout << "goal:\n");); + TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n");); // running implementation expr_ref_vector flas(m); const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); - scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas); + scoped_ptr uffree_solver = setup_sat(); + scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get()); const lbool o = imp->operator()(); flas.reset(); // report result @@ -66,6 +75,11 @@ public: } } + void updt_params(params_ref const & _p) { + ackr_tactics_params p(_p); + m_use_sat = p.sat_backend(); + } + virtual void collect_statistics(statistics & st) const { ackr_params p(m_p); if (!p.eager()) st.update("lackr-its", m_st.m_it); @@ -83,6 +97,24 @@ private: ast_manager& m_m; params_ref m_p; lackr_stats m_st; + bool m_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); + } + else { + tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); + sat = mk_tactic2solver(m_m, t.get(), m_p); + } + SASSERT(sat != NULL); + sat->set_produce_models(true); + return sat; + } + + }; tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/ackr/qfufbv_ackr_tactic.h b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h similarity index 85% rename from src/tactic/ackr/qfufbv_ackr_tactic.h rename to src/tactic/ackr_tactics/qfufbv_ackr_tactic.h index bf7d42bc2..699500be6 100644 --- a/src/tactic/ackr/qfufbv_ackr_tactic.h +++ b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h @@ -14,8 +14,8 @@ Mikolas Janota Revision History: --*/ -#ifndef _QFUFBF_ACKR_TACTIC_H_ -#define _QFUFBF_ACKR_TACTIC_H_ +#ifndef _QFUFBV_ACKR_TACTIC_H_ +#define _QFUFBV_ACKR_TACTIC_H_ #include"tactical.h" tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p); diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 4e017e9e6..4ebcd8b50 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -28,6 +28,7 @@ Notes: #include"bv_size_reduction_tactic.h" #include"aig_tactic.h" #include"sat_tactic.h" +#include"ackermannize_tactic.h" #define MEMLIMIT 300 @@ -66,7 +67,9 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { // We should decide later, if we keep it or not. // using_params(mk_simplify_tactic(m), hoist_p), - mk_max_bv_sharing_tactic(m)); + mk_max_bv_sharing_tactic(m), + mk_ackermannize_tactic(m,p) + ); } static tactic * main_p(tactic* t) { @@ -98,7 +101,6 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti big_aig_p.set_bool("aig_per_assertion", false); tactic* preamble_st = mk_qfbv_preamble(m, p); - tactic * st = main_p(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function // symbols. In this case, we should not use