diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 82cdc04d0..a22d34209 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -36,6 +36,7 @@ def init_project_def(): add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') add_lib('aig_tactic', ['tactic'], 'tactic/aig') add_lib('solver', ['model', 'tactic']) + add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization') add_lib('interp', ['solver']) add_lib('cmd_context', ['solver', 'rewriter', 'interp']) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') @@ -52,7 +53,6 @@ def init_project_def(): add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa']) - add_lib('ackr', ['smt'], 'tactic/ackr') add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('smt_tactic', ['smt'], 'smt/tactic') @@ -73,7 +73,7 @@ def init_project_def(): add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver') - add_lib('smtlogic_tactics', ['ackr', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') + add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') diff --git a/src/ackermannization/ackermannization.pyg b/src/ackermannization/ackermannization.pyg deleted file mode 100644 index fe7ac7b63..000000000 --- a/src/ackermannization/ackermannization.pyg +++ /dev/null @@ -1,7 +0,0 @@ -def_module_params('ackermannization', - description='solving UF via ackermannization', - export=True, - params=( - ('eager', BOOL, True, 'eagerly instantiate all congruence rules'), - )) - diff --git a/src/tactic/ackr/ackermannize_bv_model_converter.cpp b/src/tactic/ackr/ackermannize_bv_model_converter.cpp deleted file mode 100644 index d47735a56..000000000 --- a/src/tactic/ackr/ackermannize_bv_model_converter.cpp +++ /dev/null @@ -1,22 +0,0 @@ -/*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackermannize_bv_model_converter.cpp - - Abstract: - - - Author: - - Mikolas Janota (MikolasJanota) - - Revision History: ---*/ -#include"ackr_model_converter.h" -#include"ackermannize_bv_model_converter.h" - -model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info) { - return mk_ackr_model_converter(m, info); -} diff --git a/src/tactic/ackr/ackermannize_bv_model_converter.h b/src/tactic/ackr/ackermannize_bv_model_converter.h deleted file mode 100644 index e51792bad..000000000 --- a/src/tactic/ackr/ackermannize_bv_model_converter.h +++ /dev/null @@ -1,25 +0,0 @@ - /*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackermannize_bv_model_converter.h - - Abstract: - - - Author: - - Mikolas Janota (MikolasJanota) - - Revision History: - --*/ -#ifndef ACKERMANNIZE_BV_MODEL_CONVERTER_H_ -#define ACKERMANNIZE_BV_MODEL_CONVERTER_H_ - -#include"model_converter.h" -#include"ackr_info.h" - -model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info); - -#endif /* ACKERMANNIZE_BV_MODEL_CONVERTER_H_ */ diff --git a/src/tactic/ackr/ackermannize_bv_tactic.cpp b/src/tactic/ackr/ackermannize_bv_tactic.cpp deleted file mode 100644 index 30547d7fc..000000000 --- a/src/tactic/ackr/ackermannize_bv_tactic.cpp +++ /dev/null @@ -1,99 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - -ackermannize_bv_tactic.cpp - -Abstract: - -Author: - -Mikolas Janota - -Revision History: ---*/ -#include"ackermannize_bv_tactic.h" -#include"tactical.h" -#include"lackr.h" -#include"ackr_params.hpp" -#include"model_smt2_pp.h" -#include"ackr_bound_probe.h" -#include"ackermannize_bv_tactic_params.hpp" -#include"ackermannize_bv_model_converter.h" - - -class ackermannize_bv_tactic : public tactic { -public: - ackermannize_bv_tactic(ast_manager& m, params_ref const& p) - : m_m(m) - , m_p(p) - {} - - virtual ~ackermannize_bv_tactic() { } - - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - mc = 0; - ast_manager& m(g->m()); - tactic_report report("ackermannize", *g); - fail_if_unsat_core_generation("ackermannize", g); - fail_if_proof_generation("ackermannize", g); - - 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, NULL); - flas.reset(); - // mk result - goal_ref resg(alloc(goal, *g, true)); - const bool success = imp->mk_ackermann(resg, m_lemma_limit); - if (!success) { // Just pass on the input unchanged - result.reset(); - result.push_back(g.get()); - mc = 0; - pc = 0; - core = 0; - return; - } - result.push_back(resg.get()); - // report model - if (g->models_enabled()) { - mc = mk_ackermannize_bv_model_converter(m, imp->get_info()); - } - - resg->inc_depth(); - TRACE("ackermannize", resg->display(tout);); - SASSERT(resg->is_well_sorted()); - } - - - void updt_params(params_ref const & _p) { - ackermannize_bv_tactic_params p(_p); - m_lemma_limit = p.div0_ackermann_limit(); - } - - virtual void collect_statistics(statistics & st) const { - st.update("ackr-constraints", m_st.m_ackrs_sz); - } - - virtual void reset_statistics() { m_st.reset(); } - - virtual void cleanup() { } - - virtual tactic* translate(ast_manager& m) { - return alloc(ackermannize_bv_tactic, m, m_p); - } -private: - ast_manager& m_m; - params_ref m_p; - lackr_stats m_st; - double m_lemma_limit; -}; - -tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p) { - return alloc(ackermannize_bv_tactic, m, p); -} diff --git a/src/tactic/ackr/ackermannize_bv_tactic.h b/src/tactic/ackr/ackermannize_bv_tactic.h deleted file mode 100644 index 3e3d5636c..000000000 --- a/src/tactic/ackr/ackermannize_bv_tactic.h +++ /dev/null @@ -1,28 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - -ackermannize_bv_tactic.h - -Abstract: - -Author: - -Mikolas Janota - -Revision History: ---*/ - -#ifndef _ACKERMANNIZE_TACTIC_H_ -#define _ACKERMANNIZE_TACTIC_H_ -#include"tactical.h" - -tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p); - -/* - ADD_TACTIC("ackermannize_bv", "A tactic for performing full Ackermannization on bv instances.", "mk_ackermannize_bv_tactic(m, p)") -*/ - -#endif - diff --git a/src/tactic/ackr/ackermannize_bv_tactic_params.pyg b/src/tactic/ackr/ackermannize_bv_tactic_params.pyg deleted file mode 100644 index bd17dcaff..000000000 --- a/src/tactic/ackr/ackermannize_bv_tactic_params.pyg +++ /dev/null @@ -1,8 +0,0 @@ -def_module_params(module_name='rewriter', - class_name='ackermannize_bv_tactic_params', - export=True, - params=( - ("div0_ackermann_limit", UINT, 1000, "a bound for number of congruence Ackermann lemmas for div0 modelling"), - ) - ) - diff --git a/src/tactic/ackr/ackr.pyg b/src/tactic/ackr/ackr.pyg deleted file mode 100644 index f2e244cfd..000000000 --- a/src/tactic/ackr/ackr.pyg +++ /dev/null @@ -1,7 +0,0 @@ -def_module_params('ackr', - description='solving UF via ackermannization', - export=True, - params=( - ('eager', BOOL, True, 'eagerly instantiate all congruence rules'), - )) - diff --git a/src/tactic/ackr/ackr_bound_probe.cpp b/src/tactic/ackr/ackr_bound_probe.cpp deleted file mode 100644 index 5cb8e9448..000000000 --- a/src/tactic/ackr/ackr_bound_probe.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackr_bound_probe.cpp - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: ---*/ -#include"ackr_helper.h" -#include"ackr_bound_probe.h" -#include"ast_smt2_pp.h" - -/* - For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2". - The probe then sums up these for all functions. - This upper bound might be crude because some congruence lemmas trivially simplify to true. -*/ -class ackr_bound_probe : public probe { - struct proc { - typedef ackr_helper::fun2terms_map fun2terms_map; - typedef ackr_helper::app_set app_set; - ast_manager& m_m; - fun2terms_map m_fun2terms; // a map from functions to occurrences - ackr_helper m_ackr_helper; - - proc(ast_manager & m) : m_m(m), m_ackr_helper(m) { } - - ~proc() { - fun2terms_map::iterator it = m_fun2terms.begin(); - const fun2terms_map::iterator end = m_fun2terms.end(); - for (; it != end; ++it) dealloc(it->get_value()); - } - - void operator()(quantifier *) {} - void operator()(var *) {} - void operator()(app * a) { - if (a->get_num_args() == 0) return; - if (!m_ackr_helper.should_ackermannize(a)) return; - func_decl* const fd = a->get_decl(); - app_set* ts = 0; - if (!m_fun2terms.find(fd, ts)) { - ts = alloc(app_set); - m_fun2terms.insert(fd, ts); - } - ts->insert(a); - } - }; - -public: - ackr_bound_probe() {} - - virtual result operator()(goal const & g) { - proc p(g.m()); - unsigned sz = g.size(); - expr_fast_mark1 visited; - for (unsigned i = 0; i < sz; i++) { - for_each_expr_core(p, visited, g.form(i)); - } - const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms); - TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;); - return result(total); - } - - inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); } -}; - -probe * mk_ackr_bound_probe() { - return alloc(ackr_bound_probe); -} diff --git a/src/tactic/ackr/ackr_bound_probe.h b/src/tactic/ackr/ackr_bound_probe.h deleted file mode 100644 index 6c0a66605..000000000 --- a/src/tactic/ackr/ackr_bound_probe.h +++ /dev/null @@ -1,29 +0,0 @@ - /*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackr_bound_probe.h - - Abstract: - - A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate. - - Author: - - Mikolas Janota - - Revision History: - --*/ -#ifndef ACKR_BOUND_PROBE_H_ -#define ACKR_BOUND_PROBE_H_ - -#include"probe.h" - -probe * mk_ackr_bound_probe(); - -/* - ADD_PROBE("ackr-bound-probe", "A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.", "mk_ackr_bound_probe()") -*/ - -#endif /* ACKR_BOUND_PROBE_H_ */ diff --git a/src/tactic/ackr/ackr_helper.cpp b/src/tactic/ackr/ackr_helper.cpp deleted file mode 100644 index 803fc3c54..000000000 --- a/src/tactic/ackr/ackr_helper.cpp +++ /dev/null @@ -1,29 +0,0 @@ -/*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackr_helper.cpp - - Abstract: - - - Author: - - Mikolas Janota (MikolasJanota) - - Revision History: ---*/ -#include"ackr_helper.h" - -double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) { - fun2terms_map::iterator it = occurrences.begin(); - const fun2terms_map::iterator end = occurrences.end(); - double total = 0; - for (; it != end; ++it) { - const unsigned fsz = it->m_value->size(); - const double n2 = n_choose_2_chk(fsz); - total += n2; - } - return total; -} diff --git a/src/tactic/ackr/ackr_helper.h b/src/tactic/ackr/ackr_helper.h deleted file mode 100644 index 5c572907e..000000000 --- a/src/tactic/ackr/ackr_helper.h +++ /dev/null @@ -1,69 +0,0 @@ - /*++ - Copyright (c) 2016 Microsoft Corporation - - Module Name: - - ackr_helper.h - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: - --*/ -#ifndef ACKR_HELPER_H_ -#define ACKR_HELPER_H_ - -#include"bv_decl_plugin.h" - -class ackr_helper { - public: - typedef obj_hashtable app_set; - typedef obj_map fun2terms_map; - - ackr_helper(ast_manager& m) : m_bvutil(m) {} - - /** - \brief Determines if a given function should be Ackermannized. - - This includes all uninterpreted functions but also "special" functions, e.g. OP_BSMOD0, - which are not marked as uninterpreted but effectively are. - */ - 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)); - } - - inline bv_util& bvutil() { return m_bvutil; } - - /** - \brief Calculates an upper bound for congruence lemmas given a map of function of occurrences. - */ - static double calculate_lemma_bound(fun2terms_map& occurrences); - - /** \brief Calculate n choose 2. **/ - inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); } - - /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/ - inline static double n_choose_2_chk(unsigned n) { - SASSERT(std::numeric_limits().max() & 32); - return n & (1 << 16) ? std::numeric_limits().infinity() : n_choose_2(n); - } - private: - bv_util m_bvutil; -}; -#endif /* ACKR_HELPER_H_6475 */ diff --git a/src/tactic/ackr/ackr_info.h b/src/tactic/ackr/ackr_info.h deleted file mode 100644 index 703f1f3d5..000000000 --- a/src/tactic/ackr/ackr_info.h +++ /dev/null @@ -1,109 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - -ackr_info.h - -Abstract: - -Author: - -Mikolas Janota - -Revision History: ---*/ -#ifndef ACKR_INFO_H_ -#define ACKR_INFO_H_ - -#include"obj_hashtable.h" -#include"ast.h" -#include"ref.h" -#include"expr_replacer.h" - -/** \brief - Information about how a formula is being converted into - a formula without uninterpreted function symbols via ackermannization. - - The intended use is that new terms are added via set_abstr. - Once all terms are abstracted, call seal. - The function abstract may only be called when sealed. - - The class enables reference counting. -**/ -class ackr_info { - public: - ackr_info(ast_manager& m) - : m_m(m) - , m_consts(m) - , m_er(mk_default_expr_replacer(m)) - , m_subst(m_m) - , m_ref_count(0) - , m_sealed(false) - {} - - virtual ~ackr_info() { - m_consts.reset(); - } - - inline void set_abstr(app* term, app* c) { - SASSERT(!m_sealed); - SASSERT(c); - m_t2c.insert(term,c); - m_c2t.insert(c->get_decl(),term); - m_subst.insert(term, c); - m_consts.push_back(c); - } - - inline void abstract(expr * e, expr_ref& res) { - SASSERT(m_sealed); - (*m_er)(e, res); - } - - inline app* find_term(func_decl* c) const { - app * rv = 0; - m_c2t.find(c,rv); - return rv; - } - - inline app* get_abstr(app* term) const { - app * const rv = m_t2c.find(term); - SASSERT(rv); - return rv; - } - - inline void seal() { - m_sealed=true; - m_er->set_substitution(&m_subst); - } - - // - // Reference counting - // - void inc_ref() { ++m_ref_count; } - void dec_ref() { - --m_ref_count; - if (m_ref_count == 0) { - dealloc(this); - } - } - private: - typedef obj_map t2ct; - typedef obj_map c2tt; - ast_manager& m_m; - - t2ct m_t2c; // terms to constants - c2tt m_c2t; // constants to terms (inversion of m_t2c) - expr_ref_vector m_consts; // the constants introduced during abstraction - - // replacer and substitution used to compute abstractions - scoped_ptr m_er; - expr_substitution m_subst; - - unsigned m_ref_count; // reference counting - bool m_sealed; // debugging -}; - -typedef ref ackr_info_ref; - -#endif /* ACKR_INFO_H_ */ diff --git a/src/tactic/ackr/ackr_model_converter.cpp b/src/tactic/ackr/ackr_model_converter.cpp deleted file mode 100644 index 7967cdb63..000000000 --- a/src/tactic/ackr/ackr_model_converter.cpp +++ /dev/null @@ -1,153 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - -ackr_model_converter.cpp - -Abstract: - -Author: - -Mikolas Janota - -Revision History: ---*/ -#include"ackr_model_converter.h" -#include"model_evaluator.h" -#include"ast_smt2_pp.h" -#include"ackr_info.h" - - -class ackr_model_converter : public model_converter { -public: - ackr_model_converter(ast_manager & m, - const ackr_info_ref& info, - model_ref& abstr_model) - : m(m) - , info(info) - , abstr_model(abstr_model) - , fixed_model(true) - { } - - ackr_model_converter(ast_manager & m, - const ackr_info_ref& info) - : m(m) - , info(info) - , fixed_model(false) - { } - - virtual ~ackr_model_converter() { } - - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); - SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())); - model_ref& old_model = fixed_model ? abstr_model : md; - SASSERT(old_model.get()); - model * new_model = alloc(model, m); - convert(old_model.get(), new_model); - md = new_model; - } - - virtual void operator()(model_ref & md) { operator()(md, 0); } - - //void display(std::ostream & out); - - virtual model_converter * translate(ast_translation & translator) {NOT_IMPLEMENTED_YET();} -protected: - ast_manager& m; - const ackr_info_ref info; - model_ref abstr_model; - bool fixed_model; - void convert(model * source, model * destination); - void add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations); - void convert_sorts(model * source, model * destination); - void convert_constants(model * source, model * destination); -}; - -void ackr_model_converter::convert(model * source, model * destination) { - //SASSERT(source->get_num_functions() == 0); - for (unsigned i = 0; i < source->get_num_functions(); i++) { - func_decl * const fd = source->get_function(i); - func_interp * const fi = source->get_func_interp(fd); - destination->register_decl(fd, fi); - } - convert_constants(source,destination); - convert_sorts(source,destination); -} - -void ackr_model_converter::convert_constants(model * source, model * destination) { - TRACE("ackr_model", tout << "converting constants\n";); - obj_map interpretations; - model_evaluator evaluator(*source); - for (unsigned i = 0; i < source->get_num_constants(); i++) { - func_decl * const c = source->get_constant(i); - app * const term = info->find_term(c); - expr * value = source->get_const_interp(c); - if(!term) { - destination->register_decl(c, value); - } else { - add_entry(evaluator, term, value, interpretations); - } - } - - obj_map::iterator e = interpretations.end(); - for (obj_map::iterator i = interpretations.begin(); - i!=e; ++i) { - func_decl* const fd = i->m_key; - func_interp* const fi = i->get_value(); - fi->set_else(m.get_some_value(fd->get_range())); - destination->register_decl(fd, fi); - } -} - -void ackr_model_converter::add_entry(model_evaluator & evaluator, - app* term, expr* value, - obj_map& interpretations) { - TRACE("ackr_model", tout << "add_entry" - << mk_ismt2_pp(term, m, 2) - << "->" - << mk_ismt2_pp(value, m, 2) << "\n"; - ); - - func_interp* fi = 0; - func_decl * const declaration = term->get_decl(); - const unsigned sz = declaration->get_arity(); - SASSERT(sz == term->get_num_args()); - if (!interpretations.find(declaration, fi)) { - fi = alloc(func_interp,m,sz); - interpretations.insert(declaration, fi); - } - expr_ref_vector args(m); - for (unsigned gi = 0; gi < sz; ++gi) { - expr * const arg = term->get_arg(gi); - expr_ref aarg(m); - info->abstract(arg, aarg); - expr_ref arg_value(m); - evaluator(aarg,arg_value); - args.push_back(arg_value); - } - if (fi->get_entry(args.c_ptr()) == 0) { - fi->insert_new_entry(args.c_ptr(), value); - } else { - TRACE("ackr_model", tout << "entry already present\n";); - } -} - -void ackr_model_converter::convert_sorts(model * source, model * destination) { - for (unsigned i = 0; i < source->get_num_uninterpreted_sorts(); i++) { - sort * const s = source->get_uninterpreted_sort(i); - ptr_vector u = source->get_universe(s); - destination->register_usort(s, u.size(), u.c_ptr()); - } -} - -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) { - return alloc(ackr_model_converter, m, info); -} - -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) { - return alloc(ackr_model_converter, m, info, abstr_model); -} diff --git a/src/tactic/ackr/ackr_model_converter.h b/src/tactic/ackr/ackr_model_converter.h deleted file mode 100644 index 2c1f0c78c..000000000 --- a/src/tactic/ackr/ackr_model_converter.h +++ /dev/null @@ -1,25 +0,0 @@ -/*++ -Copyright (c) 2015 Microsoft Corporation - -Module Name: - -ackr_model_converter.h - -Abstract: - -Author: - -Mikolas Janota - -Revision History: ---*/ -#ifndef ACKR_MODEL_CONVERTER_H_ -#define ACKR_MODEL_CONVERTER_H_ - -#include"model_converter.h" -#include"ackr_info.h" - -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); -model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info); - -#endif /* LACKR_MODEL_CONVERTER_H_ */ diff --git a/src/tactic/ackr/lackr.cpp b/src/tactic/ackr/lackr.cpp deleted file mode 100644 index 0a526f7ec..000000000 --- a/src/tactic/ackr/lackr.cpp +++ /dev/null @@ -1,285 +0,0 @@ -/*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - lackr.cpp - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: ---*/ - -#include"lackr.h" -#include"ackr_params.hpp" -#include"tactic.h" -#include"lackr_model_constructor.h" -#include"ackr_info.h" -#include"for_each_expr.h" -#include"model_smt2_pp.h" - -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(uffree_solver) - , m_ackr_helper(m) - , m_simp(m) - , m_ackrs(m) - , m_st(st) - , m_is_init(false) -{ - updt_params(p); -} - -lackr::~lackr() { - const fun2terms_map::iterator e = m_fun2terms.end(); - for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) { - dealloc(i->get_value()); - } -} - -lbool lackr::operator() () { - SASSERT(m_sat); - init(); - const lbool rv = m_eager ? eager() : lazy(); - if (rv == l_true) m_sat->get_model(m_model); - CTRACE("lackr", rv == l_true, - model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; ); - return rv; -} - -bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) { - if (lemmas_upper_bound <= 0) return false; - init(); - if (lemmas_upper_bound != std::numeric_limits::infinity()) { - const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms); - if (lemmas_bound > lemmas_upper_bound) return false; - } - eager_enc(); - for (unsigned i = 0; i < m_abstr.size(); ++i) g->assert_expr(m_abstr.get(i)); - for (unsigned i = 0; i < m_ackrs.size(); ++i) g->assert_expr(m_ackrs.get(i)); - return true; -} - -void lackr::init() { - SASSERT(!m_is_init); - m_is_init = true; - params_ref simp_p(m_p); - m_simp.updt_params(simp_p); - m_info = alloc(ackr_info, m_m); - collect_terms(); - abstract(); -} - -// -// Introduce ackermann lemma for the two given terms. -// -bool lackr::ackr(app * const t1, app * const t2) { - TRACE("lackr", tout << "ackr " - << mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";); - const unsigned sz = t1->get_num_args(); - SASSERT(t2->get_num_args() == sz); - expr_ref_vector eqs(m_m); - for (unsigned i = 0; i < sz; ++i) { - expr * const arg1 = t1->get_arg(i); - expr * const arg2 = t2->get_arg(i); - if (arg1 == arg2) continue; // quickly skip syntactically equal - 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";); - return false; - } - eqs.push_back(m_m.mk_eq(arg1, arg2)); - } - app * const a1 = m_info->get_abstr(t1); - app * const a2 = m_info->get_abstr(t2); - SASSERT(a1 && a2); - TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";); - TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";); - expr_ref lhs(m_m.mk_and(eqs.size(), eqs.c_ptr()), m_m); - TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";); - expr_ref rhs(m_m.mk_eq(a1, a2),m_m); - TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";); - expr_ref cg(m_m.mk_implies(lhs, rhs), m_m); - TRACE("lackr", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";); - expr_ref cga(m_m); - m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications - m_simp(cga); - TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";); - if (m_m.is_true(cga)) return false; - m_st.m_ackrs_sz++; - m_ackrs.push_back(cga); - return true; -} - -// -// Introduce the ackermann lemma for each pair of terms. -// -void lackr::eager_enc() { - TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;); - const fun2terms_map::iterator e = m_fun2terms.end(); - for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) { - checkpoint(); - func_decl* const fd = i->m_key; - app_set * const ts = i->get_value(); - const app_set::iterator r = ts->end(); - for (app_set::iterator j = ts->begin(); j != r; ++j) { - app_set::iterator k = j; - ++k; - for (; k != r; ++k) { - app * const t1 = *j; - app * const t2 = *k; - SASSERT(t1->get_decl() == fd); - SASSERT(t2->get_decl() == fd); - if (t1 == t2) continue; - ackr(t1,t2); - } - } - } -} - - -void lackr::abstract() { - const fun2terms_map::iterator e = m_fun2terms.end(); - for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) { - func_decl* const fd = i->m_key; - app_set * const ts = i->get_value(); - sort* const s = fd->get_range(); - const app_set::iterator r = ts->end(); - for (app_set::iterator j = ts->begin(); j != r; ++j) { - app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s); - app * const t = *j; - SASSERT(t->get_decl() == fd); - m_info->set_abstr(t, fc); - TRACE("lackr", tout << "abstr term " - << mk_ismt2_pp(t, m_m, 2) - << " -> " - << mk_ismt2_pp(fc, m_m, 2) - << "\n";); - } - } - m_info->seal(); - // perform abstraction of the formulas - const unsigned sz = m_formulas.size(); - for (unsigned i = 0; i < sz; ++i) { - expr_ref a(m_m); - m_info->abstract(m_formulas.get(i), a); - m_abstr.push_back(a); - } -} - -void lackr::add_term(app* a) { - if (a->get_num_args() == 0) return; - if (!m_ackr_helper.should_ackermannize(a)) return; - func_decl* const fd = a->get_decl(); - app_set* ts = 0; - if (!m_fun2terms.find(fd, ts)) { - ts = alloc(app_set); - m_fun2terms.insert(fd, ts); - } - TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";); - ts->insert(a); -} - -void lackr::push_abstraction() { - const unsigned sz = m_abstr.size(); - for (unsigned i = 0; i < sz; ++i) { - m_sat->assert_expr(m_abstr.get(i)); - } -} - -lbool lackr::eager() { - push_abstraction(); - TRACE("lackr", tout << "run sat 0\n"; ); - const lbool rv0 = m_sat->check_sat(0, 0); - if (rv0 == l_false) return l_false; - eager_enc(); - expr_ref all(m_m); - all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr()); - m_simp(all); - m_sat->assert_expr(all); - TRACE("lackr", tout << "run sat all\n"; ); - return m_sat->check_sat(0, 0); -} - -lbool lackr::lazy() { - lackr_model_constructor mc(m_m, m_info); - push_abstraction(); - unsigned ackr_head = 0; - while (1) { - m_st.m_it++; - checkpoint(); - TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";); - const lbool r = m_sat->check_sat(0, 0); - if (r == l_undef) return l_undef; // give up - if (r == l_false) return l_false; // abstraction unsat - // reconstruct model - model_ref am; - m_sat->get_model(am); - const bool mc_res = mc.check(am); - if (mc_res) return l_true; // model okay - // refine abstraction - const lackr_model_constructor::conflict_list conflicts = mc.get_conflicts(); - for (lackr_model_constructor::conflict_list::const_iterator i = conflicts.begin(); - i != conflicts.end(); ++i) { - ackr(i->first, i->second); - } - while (ackr_head < m_ackrs.size()) { - m_sat->assert_expr(m_ackrs.get(ackr_head++)); - } - } -} - -// -// Collect all uninterpreted terms, skipping 0-arity. -// -void lackr::collect_terms() { - ptr_vector stack; - expr * curr; - expr_mark visited; - for(unsigned i = 0; i < m_formulas.size(); ++i) { - stack.push_back(m_formulas.get(i)); - TRACE("lackr", tout << "infla: " <get_kind()) { - case AST_VAR: - visited.mark(curr, true); - stack.pop_back(); - break; - case AST_APP: - { - app * const a = to_app(curr); - if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) { - visited.mark(curr, true); - stack.pop_back(); - add_term(a); - } - } - break; - case AST_QUANTIFIER: - UNREACHABLE(); - break; - default: - UNREACHABLE(); - return; - } - } - visited.reset(); -} diff --git a/src/tactic/ackr/lackr.h b/src/tactic/ackr/lackr.h deleted file mode 100644 index e6612a578..000000000 --- a/src/tactic/ackr/lackr.h +++ /dev/null @@ -1,127 +0,0 @@ - /*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - lackr.h - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: - --*/ -#ifndef LACKR_H_ -#define LACKR_H_ - -#include"ackr_info.h" -#include"ackr_helper.h" -#include"ackr_params.hpp" -#include"th_rewriter.h" -#include"cooperate.h" -#include"bv_decl_plugin.h" -#include"lbool.h" -#include"model.h" -#include"solver.h" -#include"util.h" -#include"tactic_exception.h" -#include"goal.h" - -struct lackr_stats { - lackr_stats() : m_it(0), m_ackrs_sz(0) {} - void reset() { m_it = m_ackrs_sz = 0; } - unsigned m_it; // number of lazy iterations - unsigned m_ackrs_sz; // number of congruence constraints -}; - -/** \brief - A class to encode or directly solve problems with uninterpreted functions via ackermannization. - Currently, solving is supported only for QF_UFBV. -**/ -class lackr { - public: - 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(); - } - - /** \brief - * Solve the formula that the class was initialized with. - **/ - lbool operator() (); - - - /** \brief - Converts function occurrences to constants and encodes all congruence ackermann lemmas. - - This procedure guarantees a equisatisfiability with the input formula and it has a worst-case quadratic blowup. - Before ackermannization an upper bound on congruence lemmas is computed and tested against \p lemmas_upper_bound. - If this bound is exceeded, the function returns false, it returns true otherwise. - **/ - bool mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound); - - // - // getters - // - inline ackr_info_ref get_info() { return m_info; } - inline model_ref get_model() { return m_model; } - - // - // timeout mechanism - // - void checkpoint() { - if (m_m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); - } - cooperate("lackr"); - } - private: - typedef ackr_helper::fun2terms_map fun2terms_map; - typedef ackr_helper::app_set app_set; - ast_manager& m_m; - params_ref m_p; - expr_ref_vector m_formulas; - expr_ref_vector m_abstr; - fun2terms_map m_fun2terms; - ackr_info_ref m_info; - solver* m_sat; - ackr_helper m_ackr_helper; - th_rewriter m_simp; - expr_ref_vector m_ackrs; - model_ref m_model; - bool m_eager; - lackr_stats& m_st; - bool m_is_init; - - void init(); - lbool eager(); - lbool lazy(); - - // - // Introduce congruence ackermann lemma for the two given terms. - // - bool ackr(app * const t1, app * const t2); - - // - // Introduce the ackermann lemma for each pair of terms. - // - void eager_enc(); - - void abstract(); - - void push_abstraction(); - - void add_term(app* a); - - // - // Collect all uninterpreted terms, skipping 0-arity. - // - void collect_terms(); -}; -#endif /* LACKR_H_ */ diff --git a/src/tactic/ackr/lackr_model_constructor.cpp b/src/tactic/ackr/lackr_model_constructor.cpp deleted file mode 100644 index f9eded93b..000000000 --- a/src/tactic/ackr/lackr_model_constructor.cpp +++ /dev/null @@ -1,377 +0,0 @@ -/*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - model_constructor.cpp - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: ---*/ -#include"lackr_model_constructor.h" -#include"model_evaluator.h" -#include"ast_smt2_pp.h" -#include"ackr_info.h" -#include"for_each_expr.h" -#include"bv_rewriter.h" -#include"bool_rewriter.h" -struct lackr_model_constructor::imp { - public: - imp(ast_manager& m, - ackr_info_ref info, - model_ref& abstr_model, - conflict_list& conflicts) - : m_m(m) - , m_info(info) - , m_abstr_model(abstr_model) - , m_conflicts(conflicts) - , m_b_rw(m) - , m_bv_rw(m) - , m_empty_model(m) - , m_ackr_helper(m) - {} - - ~imp() { - { - values2val_t::iterator i = m_values2val.begin(); - const values2val_t::iterator e = m_values2val.end(); - for (; i != e; ++i) { - m_m.dec_ref(i->m_key); - m_m.dec_ref(i->m_value.value); - m_m.dec_ref(i->m_value.source_term); - } - } - { - app2val_t::iterator i = m_app2val.begin(); - const app2val_t::iterator e = m_app2val.end(); - for (; i != e; ++i) { - m_m.dec_ref(i->m_value); - m_m.dec_ref(i->m_key); - } - } - } - - // - // Returns true iff model was successfully constructed. - // - bool check() { - 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)); - } - return run(); - } - - - void make_model(model_ref& destination) { - { - for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) { - sort * const s = m_abstr_model->get_uninterpreted_sort(i); - ptr_vector u = m_abstr_model->get_universe(s); - destination->register_usort(s, u.size(), u.c_ptr()); - } - } - for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) { - func_decl * const fd = m_abstr_model->get_function(i); - func_interp * const fi = m_abstr_model->get_func_interp(fd); - destination->register_decl(fd, fi); - } - - { - const app2val_t::iterator e = m_app2val.end(); - app2val_t::iterator i = m_app2val.end(); - for (; i != e; ++i) { - app * a = i->m_key; - if (a->get_num_args()) continue; - destination->register_decl(a->get_decl(), i->m_value); - } - } - - obj_map interpretations; - { - const values2val_t::iterator e = m_values2val.end(); - values2val_t::iterator i = m_values2val.end(); - for (; i != e; ++i) add_entry(i->m_key, i->m_value.value, interpretations); - } - - { - obj_map::iterator ie = interpretations.end(); - obj_map::iterator ii = interpretations.begin(); - for (; ii != ie; ++ii) { - func_decl* const fd = ii->m_key; - func_interp* const fi = ii->get_value(); - fi->set_else(m_m.get_some_value(fd->get_range())); - destination->register_decl(fd, fi); - } - } - } - - void add_entry(app* term, expr* value, - obj_map& interpretations) { - func_interp* fi = 0; - func_decl * const declaration = term->get_decl(); - const unsigned sz = declaration->get_arity(); - SASSERT(sz == term->get_num_args()); - if (!interpretations.find(declaration, fi)) { - fi = alloc(func_interp, m_m, sz); - interpretations.insert(declaration, fi); - } - fi->insert_new_entry(term->get_args(), value); - } - private: - ast_manager& m_m; - ackr_info_ref m_info; - model_ref& m_abstr_model; - conflict_list& m_conflicts; - bool_rewriter m_b_rw; - bv_rewriter m_bv_rw; - scoped_ptr m_evaluator; - model m_empty_model; - private: - struct val_info { expr * value; app * source_term; }; - typedef obj_map app2val_t; - typedef obj_map values2val_t; - 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; - rv.value = value; - rv.source_term = source_term; - 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; - expr * curr; - while (!m_stack.empty()) { - curr = m_stack.back(); - if (visited.is_marked(curr)) { - m_stack.pop_back(); - continue; - } - - switch (curr->get_kind()) { - case AST_VAR: - UNREACHABLE(); - 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); - m_stack.pop_back(); - if (!mk_value(a)) return false; - } - } - break; - case AST_QUANTIFIER: - UNREACHABLE(); - return false; - default: - UNREACHABLE(); - return false; - } - } - return true; - } - - inline bool is_val(expr * e) { return m_m.is_value(e); } - - inline bool eval_cached(app * a, expr *& val) { - if (is_val(a)) { val = a; return true; } - return m_app2val.find(a, val); - } - - bool evaluate(app * const a, expr_ref& result) { - SASSERT(!is_val(a)); - const unsigned num = a->get_num_args(); - if (num == 0) { // handle constants - make_value_constant(a, result); - return true; - } - // evaluate arguments - expr_ref_vector values(m_m); - values.reserve(num); - expr * const * args = a->get_args(); - 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); ); - TRACE("model_constructor", tout << - "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2) - << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; ); - SASSERT(b); - values[i] = val; - } - // handle functions - 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; - } - } - else { // handle interpreted - make_value_interpreted_function(a, values, result); - } - return true; - } - - // - // Check and record the value for a given term, given that all arguments are already checked. - // - bool mk_value(app * a) { - if (is_val(a)) return true; // skip numerals - TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";); - SASSERT(!m_app2val.contains(a)); - const unsigned num = a->get_num_args(); - expr_ref result(m_m); - if (!evaluate(a, result)) return false; - SASSERT(is_val(result)); - TRACE("model_constructor", - tout << "map term(\n" << mk_ismt2_pp(a, m_m, 2) << "\n->" - << mk_ismt2_pp(result.get(), m_m, 2)<< ")\n"; ); - CTRACE("model_constructor", - !is_val(result.get()), - tout << "eval fail\n" << mk_ismt2_pp(a, m_m, 2) << mk_ismt2_pp(result, m_m, 2) << "\n"; - ); - SASSERT(is_val(result.get())); - m_app2val.insert(a, result.get()); // memoize - m_m.inc_ref(a); - m_m.inc_ref(result.get()); - return true; - } - - // Constants from the abstract model are directly mapped to the concrete one. - void make_value_constant(app * const a, expr_ref& result) { - SASSERT(a->get_num_args() == 0); - func_decl * const fd = a->get_decl(); - expr * val = m_abstr_model->get_const_interp(fd); - if (val == 0) { // TODO: avoid model completetion? - sort * s = fd->get_range(); - val = m_abstr_model->get_some_value(s); - } - result = val; - } - - bool make_value_uninterpreted_function(app* a, - expr_ref_vector& values, - app* key, - expr_ref& result) { - // get ackermann constant - app * const ac = m_info->get_abstr(a); - func_decl * const a_fd = a->get_decl(); - SASSERT(ac->get_num_args() == 0); - SASSERT(a_fd->get_range() == ac->get_decl()->get_range()); - expr_ref value(m_m); - value = m_abstr_model->get_const_interp(ac->get_decl()); - // get ackermann constant's interpretation - if (value.get() == 0) { // TODO: avoid model completion? - sort * s = a_fd->get_range(); - value = m_abstr_model->get_some_value(s); - } - // check congruence - val_info vi; - if(m_values2val.find(key,vi)) { // already is mapped to a value - SASSERT(vi.source_term); - const bool ok = vi.value == value; - if (!ok) { - TRACE("model_constructor", - tout << "already mapped by(\n" << mk_ismt2_pp(vi.source_term, m_m, 2) << "\n->" - << mk_ismt2_pp(vi.value, m_m, 2) << ")\n"; ); - m_conflicts.push_back(std::make_pair(a, vi.source_term)); - } - result = vi.value; - return ok; - } else { // new value - result = value; - vi.value = value; - vi.source_term = a; - m_values2val.insert(key,vi); - m_m.inc_ref(vi.source_term); - m_m.inc_ref(vi.value); - m_m.inc_ref(key); - return true; - } - UNREACHABLE(); - } - - void make_value_interpreted_function(app* a, - expr_ref_vector& values, - expr_ref& result) { - const unsigned num = values.size(); - func_decl * const fd = a->get_decl(); - const family_id fid = fd->get_family_id(); - expr_ref term(m_m); - term = m_m.mk_app(a->get_decl(), num, values.c_ptr()); - m_evaluator->operator() (term, result); - TRACE("model_constructor", - tout << "eval(\n" << mk_ismt2_pp(term.get(), m_m, 2) << "\n->" - << mk_ismt2_pp(result.get(), m_m, 2) << ")\n"; ); - return; - if (fid == m_b_rw.get_fid()) { - decl_kind k = fd->get_decl_kind(); - if (k == OP_EQ) { - // theory dispatch for = - SASSERT(num == 2); - family_id s_fid = m_m.get_sort(values.get(0))->get_family_id(); - br_status st = BR_FAILED; - if (s_fid == m_bv_rw.get_fid()) - st = m_bv_rw.mk_eq_core(values.get(0), values.get(1), result); - } else { - br_status st = m_b_rw.mk_app_core(fd, num, values.c_ptr(), result); - } - } else { - br_status st = BR_FAILED; - if (fid == m_bv_rw.get_fid()) { - st = m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result); - } - else { - UNREACHABLE(); - } - } - } -}; - -lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref info) - : m_imp(0) - , m_m(m) - , m_state(UNKNOWN) - , m_info(info) - , m_ref_count(0) -{} - -lackr_model_constructor::~lackr_model_constructor() { - if (m_imp) dealloc(m_imp); -} - -bool lackr_model_constructor::check(model_ref& abstr_model) { - m_conflicts.reset(); - if (m_imp) { - dealloc(m_imp); - m_imp = 0; - } - m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts); - const bool rv = m_imp->check(); - m_state = rv ? CHECKED : CONFLICT; - return rv; -} - -void lackr_model_constructor::make_model(model_ref& model) { - SASSERT(m_state == CHECKED); - m_imp->make_model(model); -} diff --git a/src/tactic/ackr/lackr_model_constructor.h b/src/tactic/ackr/lackr_model_constructor.h deleted file mode 100644 index ce9edba26..000000000 --- a/src/tactic/ackr/lackr_model_constructor.h +++ /dev/null @@ -1,61 +0,0 @@ - /*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - model_constructor.h - - Abstract: - Given a propositional abstraction, attempt to construct a model. - - - Author: - - Mikolas Janota - - Revision History: - --*/ -#ifndef LACKR_MODEL_CONSTRUCTOR_H_ -#define LACKR_MODEL_CONSTRUCTOR_H_ - -#include"ast.h" -#include"ackr_info.h" -#include"ackr_helper.h" -#include"model.h" - -class lackr_model_constructor { - public: - typedef std::pair app_pair; - typedef vector conflict_list; - lackr_model_constructor(ast_manager& m, ackr_info_ref info); - ~lackr_model_constructor(); - bool check(model_ref& abstr_model); - const conflict_list& get_conflicts() { - SASSERT(m_state == CONFLICT); - return m_conflicts; - } - void make_model(model_ref& model); - - // - // Reference counting - // - void inc_ref() { ++m_ref_count; } - void dec_ref() { - --m_ref_count; - if (m_ref_count == 0) { - dealloc(this); - } - } - private: - struct imp; - imp * m_imp; - enum {CHECKED, CONFLICT, UNKNOWN} m_state; - conflict_list m_conflicts; - ast_manager& m_m; - const ackr_info_ref m_info; - - unsigned m_ref_count; // reference counting -}; - -typedef ref lackr_model_constructor_ref; -#endif /* MODEL_CONSTRUCTOR_H_ */ diff --git a/src/tactic/ackr/lackr_model_converter_lazy.cpp b/src/tactic/ackr/lackr_model_converter_lazy.cpp deleted file mode 100644 index 30dba8a04..000000000 --- a/src/tactic/ackr/lackr_model_converter_lazy.cpp +++ /dev/null @@ -1,60 +0,0 @@ -/*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - lackr_model_converter_lazy.cpp - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: ---*/ -#include"lackr_model_converter_lazy.h" -#include"model_evaluator.h" -#include"ast_smt2_pp.h" -#include"ackr_info.h" -#include"lackr_model_constructor.h" - - -class lackr_model_converter_lazy : public model_converter { -public: - lackr_model_converter_lazy(ast_manager & m, - const lackr_model_constructor_ref& lmc) - : m(m) - , model_constructor(lmc) - { } - - virtual ~lackr_model_converter_lazy() { } - - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); - SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions())); - SASSERT(model_constructor.get()); - model * new_model = alloc(model, m); - md = new_model; - model_constructor->make_model(md); - } - - virtual void operator()(model_ref & md) { - operator()(md, 0); - } - - //void display(std::ostream & out); - - virtual model_converter * translate(ast_translation & translator) { - NOT_IMPLEMENTED_YET(); - } -protected: - ast_manager& m; - const lackr_model_constructor_ref model_constructor; -}; - -model_converter * mk_lackr_model_converter_lazy(ast_manager & m, - const lackr_model_constructor_ref& model_constructor) { - return alloc(lackr_model_converter_lazy, m, model_constructor); -} diff --git a/src/tactic/ackr/lackr_model_converter_lazy.h b/src/tactic/ackr/lackr_model_converter_lazy.h deleted file mode 100644 index c9b3eac80..000000000 --- a/src/tactic/ackr/lackr_model_converter_lazy.h +++ /dev/null @@ -1,25 +0,0 @@ - /*++ - Copyright (c) 2015 Microsoft Corporation - - Module Name: - - lackr_model_converter_lazy.h - - Abstract: - - - Author: - - Mikolas Janota - - Revision History: - --*/ -#ifndef LACKR_MODEL_CONVERTER_LAZY_H_ -#define LACKR_MODEL_CONVERTER_LAZY_H_ - -#include"model_converter.h" -#include"ackr_info.h" - -model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); - -#endif /* LACKR_MODEL_CONVERTER_LAZY_H_ */ diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 526d72faa..c3ebb4f48 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -32,6 +32,7 @@ Notes: #include"model_smt2_pp.h" #include"cooperate.h" #include"lackr.h" +#include"ackermannization_params.hpp" #include"qfufbv_ackr_model_converter.h" /////////////// #include"inc_sat_solver.h" @@ -87,7 +88,7 @@ public: } virtual void collect_statistics(statistics & st) const { - ackr_params p(m_p); + ackermannization_params p(m_p); if (!p.eager()) st.update("lackr-its", m_st.m_it); st.update("ackr-constraints", m_st.m_ackrs_sz); } @@ -172,9 +173,7 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { tactic * const preamble_st = mk_qfufbv_preamble(m, p); tactic * st = using_params(and_then(preamble_st, - cond(mk_is_qfbv_probe(), - mk_qfbv_tactic(m), - mk_smt_tactic())), + cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic())), main_p); st->updt_params(p); @@ -187,4 +186,4 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p); return and_then(preamble_t, cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic())); -} \ No newline at end of file +}