diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 08986d96b..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') @@ -70,10 +71,10 @@ def init_project_def(): add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality') add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') - add_lib('smtlogic_tactics', ['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('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', ['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') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') diff --git a/src/ackermannization/ackermannization_params.pyg b/src/ackermannization/ackermannization_params.pyg new file mode 100644 index 000000000..fe7ac7b63 --- /dev/null +++ b/src/ackermannization/ackermannization_params.pyg @@ -0,0 +1,7 @@ +def_module_params('ackermannization', + description='solving UF via ackermannization', + export=True, + params=( + ('eager', BOOL, True, 'eagerly instantiate all congruence rules'), + )) + diff --git a/src/ackermannization/ackermannize_bv_model_converter.cpp b/src/ackermannization/ackermannize_bv_model_converter.cpp new file mode 100644 index 000000000..d47735a56 --- /dev/null +++ b/src/ackermannization/ackermannize_bv_model_converter.cpp @@ -0,0 +1,22 @@ +/*++ + 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/ackermannization/ackermannize_bv_model_converter.h b/src/ackermannization/ackermannize_bv_model_converter.h new file mode 100644 index 000000000..e51792bad --- /dev/null +++ b/src/ackermannization/ackermannize_bv_model_converter.h @@ -0,0 +1,25 @@ + /*++ + 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/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp new file mode 100644 index 000000000..310269fec --- /dev/null +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -0,0 +1,97 @@ +/*++ +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"model_smt2_pp.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/ackermannization/ackermannize_bv_tactic.h b/src/ackermannization/ackermannize_bv_tactic.h new file mode 100644 index 000000000..3e3d5636c --- /dev/null +++ b/src/ackermannization/ackermannize_bv_tactic.h @@ -0,0 +1,28 @@ +/*++ +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/ackermannization/ackermannize_bv_tactic_params.pyg b/src/ackermannization/ackermannize_bv_tactic_params.pyg new file mode 100644 index 000000000..bd17dcaff --- /dev/null +++ b/src/ackermannization/ackermannize_bv_tactic_params.pyg @@ -0,0 +1,8 @@ +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/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp new file mode 100644 index 000000000..5cb8e9448 --- /dev/null +++ b/src/ackermannization/ackr_bound_probe.cpp @@ -0,0 +1,77 @@ +/*++ + 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/ackermannization/ackr_bound_probe.h b/src/ackermannization/ackr_bound_probe.h new file mode 100644 index 000000000..6c0a66605 --- /dev/null +++ b/src/ackermannization/ackr_bound_probe.h @@ -0,0 +1,29 @@ + /*++ + 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/ackermannization/ackr_helper.cpp b/src/ackermannization/ackr_helper.cpp new file mode 100644 index 000000000..803fc3c54 --- /dev/null +++ b/src/ackermannization/ackr_helper.cpp @@ -0,0 +1,29 @@ +/*++ + 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/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h new file mode 100644 index 000000000..5c572907e --- /dev/null +++ b/src/ackermannization/ackr_helper.h @@ -0,0 +1,69 @@ + /*++ + 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/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h new file mode 100644 index 000000000..703f1f3d5 --- /dev/null +++ b/src/ackermannization/ackr_info.h @@ -0,0 +1,109 @@ +/*++ +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/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp new file mode 100644 index 000000000..7967cdb63 --- /dev/null +++ b/src/ackermannization/ackr_model_converter.cpp @@ -0,0 +1,153 @@ +/*++ +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/ackermannization/ackr_model_converter.h b/src/ackermannization/ackr_model_converter.h new file mode 100644 index 000000000..2c1f0c78c --- /dev/null +++ b/src/ackermannization/ackr_model_converter.h @@ -0,0 +1,25 @@ +/*++ +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/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp new file mode 100644 index 000000000..cc98545de --- /dev/null +++ b/src/ackermannization/lackr.cpp @@ -0,0 +1,290 @@ +/*++ + Copyright (c) 2015 Microsoft Corporation + + Module Name: + + lackr.cpp + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: +--*/ + +#include"lackr.h" +#include"ackermannization_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); +} + +void lackr::updt_params(params_ref const & _p) { + ackermannization_params p(_p); + m_eager = p.eager(); +} + +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/ackermannization/lackr.h b/src/ackermannization/lackr.h new file mode 100644 index 000000000..cdac6b3e4 --- /dev/null +++ b/src/ackermannization/lackr.h @@ -0,0 +1,123 @@ + /*++ + 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"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); + + /** \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/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp new file mode 100644 index 000000000..09034fa36 --- /dev/null +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -0,0 +1,376 @@ +/*++ + 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)); + 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(); + return true; + } + + 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(); + if (s_fid == m_bv_rw.get_fid()) + m_bv_rw.mk_eq_core(values.get(0), values.get(1), result); + } else { + m_b_rw.mk_app_core(fd, num, values.c_ptr(), result); + } + } else { + if (fid == m_bv_rw.get_fid()) { + 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/ackermannization/lackr_model_constructor.h b/src/ackermannization/lackr_model_constructor.h new file mode 100644 index 000000000..71c9c0710 --- /dev/null +++ b/src/ackermannization/lackr_model_constructor.h @@ -0,0 +1,61 @@ + /*++ + 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; + ast_manager & m_m; + enum {CHECKED, CONFLICT, UNKNOWN} m_state; + conflict_list m_conflicts; + 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/ackermannization/lackr_model_converter_lazy.cpp b/src/ackermannization/lackr_model_converter_lazy.cpp new file mode 100644 index 000000000..5a0d1c4be --- /dev/null +++ b/src/ackermannization/lackr_model_converter_lazy.cpp @@ -0,0 +1,59 @@ +/*++ + 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/ackermannization/lackr_model_converter_lazy.h b/src/ackermannization/lackr_model_converter_lazy.h new file mode 100644 index 000000000..c9b3eac80 --- /dev/null +++ b/src/ackermannization/lackr_model_converter_lazy.h @@ -0,0 +1,25 @@ + /*++ + 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/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 81bf2136b..1c5da3829 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -187,8 +187,8 @@ public: tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); tref->set_logic(ctx.get_logic()); ast_manager & m = ctx.m(); - unsigned timeout = p.get_uint("timeout", UINT_MAX); - unsigned rlimit = p.get_uint("rlimit", 0); + unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); + unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout);); diff --git a/src/muz/README b/src/muz/README index c7d5a9665..3cebe98f6 100644 --- a/src/muz/README +++ b/src/muz/README @@ -9,4 +9,4 @@ solving Datalog programs. - clp - Dart/Symbolic execution-based solver - tab - Tabulation based solver - bmc - Bounded model checking based solver -- fp - main exported routines \ No newline at end of file +- fp - main exported routines diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 2e142cb13..e7327e7a9 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -481,8 +481,6 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) { class is_qfbv_eq_probe : public probe { public: virtual result operator()(goal const & g) { - bv_rewriter rw(g.m()); - if (!rw.hi_div0()) return false; bv1_blaster_tactic t(g.m()); return t.is_target(g); diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h index 608a831e0..336911bf7 100644 --- a/src/tactic/bv/bvarray2uf_tactic.h +++ b/src/tactic/bv/bvarray2uf_tactic.h @@ -30,4 +30,4 @@ tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref */ -#endif \ No newline at end of file +#endif diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 534fb6e1c..854543f24 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -107,4 +107,4 @@ protected: model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv); -#endif \ No newline at end of file +#endif diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp index dd27691d3..a12d2c90d 100644 --- a/src/tactic/probe.cpp +++ b/src/tactic/probe.cpp @@ -285,9 +285,16 @@ struct is_non_qfbv_predicate { throw found(); family_id fid = n->get_family_id(); if (fid == m.get_basic_family_id()) - return; - if (fid == u.get_family_id()) - return; + return; + if (fid == u.get_family_id()) { + if (n->get_decl_kind() == OP_BSDIV0 || + n->get_decl_kind() == OP_BUDIV0 || + n->get_decl_kind() == OP_BSREM0 || + n->get_decl_kind() == OP_BUREM0 || + n->get_decl_kind() == OP_BSMOD0) + throw found(); + return; + } if (is_uninterp_const(n)) return; throw found(); @@ -301,11 +308,10 @@ public: } }; + class is_qfbv_probe : public probe { public: virtual result operator()(goal const & g) { - bv_rewriter rw(g.m()); - if (!rw.hi_div0()) return false; return !test(g); } }; @@ -356,6 +362,46 @@ probe * mk_is_qfaufbv_probe() { return alloc(is_qfaufbv_probe); } + +struct is_non_qfufbv_predicate { + struct found {}; + ast_manager & m; + bv_util m_bv_util; + + is_non_qfufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + if (!m.is_bool(n) && !m_bv_util.is_bv(n)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == m_bv_util.get_family_id()) + return; + if (is_uninterp(n)) + return; + + throw found(); + } +}; + +class is_qfufbv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qfufbv_probe() { + return alloc(is_qfufbv_probe); +} + + + class num_consts_probe : public probe { bool m_bool; // If true, track only boolean constants. Otherwise, track only non boolean constants. char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family. diff --git a/src/tactic/probe.h b/src/tactic/probe.h index 56269094e..a5bc5c0a3 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -112,6 +112,7 @@ probe * mk_div(probe * p1, probe * p2); probe * mk_is_propositional_probe(); probe * mk_is_qfbv_probe(); probe * mk_is_qfaufbv_probe(); +probe * mk_is_qfufbv_probe(); /* ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()") diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 4e017e9e6..cd446852e 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_bv_tactic.h" #define MEMLIMIT 300 @@ -46,7 +47,6 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som - params_ref hoist_p; hoist_p.set_bool("hoist_mul", true); hoist_p.set_bool("som", false); @@ -66,7 +66,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_bv_tactic(m,p) + ); } static tactic * main_p(tactic* t) { @@ -98,14 +100,14 @@ 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 - cond(mk_is_qfbv_probe(), - cond(mk_is_qfbv_eq_probe(), - and_then(mk_bv1_blaster_tactic(m), - using_params(smt, solver_p)), + // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively, + // the UFs can be eliminated by eager ackermannization in the preamble. + cond(mk_is_qfbv_eq_probe(), + and_then(mk_bv1_blaster_tactic(m), + using_params(smt, solver_p)), + cond(mk_is_qfbv_probe(), and_then(mk_bit_blaster_tactic(m), when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), and_then(using_params(and_then(mk_simplify_tactic(m), @@ -115,8 +117,8 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti mk_aig_tactic(), using_params(mk_aig_tactic(), big_aig_p))))), - sat)), - smt))); + sat), + smt)))); st->updt_params(p); return st; diff --git a/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp b/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp new file mode 100644 index 000000000..4d20631b1 --- /dev/null +++ b/src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp @@ -0,0 +1,22 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + qfufbv_ackr_model_converter.cpp + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: +--*/ +#include"qfufbv_ackr_model_converter.h" +#include"ackr_model_converter.h" + +model_converter * mk_qfufbv_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) { + return mk_ackr_model_converter(m, info, abstr_model); +} diff --git a/src/tactic/smtlogics/qfufbv_ackr_model_converter.h b/src/tactic/smtlogics/qfufbv_ackr_model_converter.h new file mode 100644 index 000000000..a361a78e0 --- /dev/null +++ b/src/tactic/smtlogics/qfufbv_ackr_model_converter.h @@ -0,0 +1,25 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + qfufbv_ackr_model_converter.h + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: + --*/ +#ifndef QFUFBV_ACKR_MODEL_CONVERTER_H_ +#define QFUFBV_ACKR_MODEL_CONVERTER_H_ + +#include"model_converter.h" +#include"ackr_info.h" + +model_converter * mk_qfufbv_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); + +#endif /* QFUFBV_ACKR_MODEL_CONVERTER_H_ */ diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 816d69b1f..f943b68c9 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -12,6 +12,7 @@ Abstract: Author: Leonardo (leonardo) 2012-02-27 + Mikolas Janota Notes: @@ -26,27 +27,163 @@ Notes: #include"bv_size_reduction_tactic.h" #include"reduce_args_tactic.h" #include"qfbv_tactic.h" +#include"qfufbv_tactic_params.hpp" +/////////////// +#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" +#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() { } + + 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("qfufbv_ackr", *g); + fail_if_unsat_core_generation("qfufbv_ackr", g); + fail_if_proof_generation("qfufbv_ackr", g); + + 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 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 + goal_ref resg(alloc(goal, *g, true)); + if (o == l_false) resg->assert_expr(m.mk_false()); + if (o != l_undef) result.push_back(resg.get()); + // report model + if (g->models_enabled() && (o == l_true)) { + model_ref abstr_model = imp->get_model(); + mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model); + } + } + + void updt_params(params_ref const & _p) { + qfufbv_tactic_params p(_p); + m_use_sat = p.sat_backend(); + } + + virtual void collect_statistics(statistics & st) const { + 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); + } + + virtual void reset_statistics() { m_st.reset(); } + + virtual void cleanup() { } + + virtual tactic* translate(ast_manager& m) { + return alloc(qfufbv_ackr_tactic, m, m_p); + } +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_preamble1(ast_manager & m, params_ref const & p) { + params_ref simp2_p = p; + simp2_p.set_bool("pull_cheap_ite", true); + simp2_p.set_bool("push_ite_bv", false); + simp2_p.set_bool("local_ctx", true); + simp2_p.set_uint("local_ctx_limit", 10000000); + + simp2_p.set_bool("ite_extra_rules", true); + simp2_p.set_bool("mul2concat", true); + + params_ref ctx_simp_p; + ctx_simp_p.set_uint("max_depth", 32); + ctx_simp_p.set_uint("max_steps", 5000000); + + return and_then( + mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p), + mk_solve_eqs_tactic(m), + mk_elim_uncnstr_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), + mk_max_bv_sharing_tactic(m), + using_params(mk_simplify_tactic(m), simp2_p) + ); +} + +tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { + params_ref main_p; + main_p.set_bool("elim_and", true); + main_p.set_bool("blast_distinct", true); + + return and_then(mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + mk_solve_eqs_tactic(m), + mk_elim_uncnstr_tactic(m), + if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), + if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), + mk_max_bv_sharing_tactic(m) + ); +} tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; main_p.set_bool("elim_and", true); main_p.set_bool("blast_distinct", true); - tactic * preamble_st = and_then(mk_simplify_tactic(m), - mk_propagate_values_tactic(m), - mk_solve_eqs_tactic(m), - mk_elim_uncnstr_tactic(m), - if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))), - if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), - mk_max_bv_sharing_tactic(m) - ); + 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())), - main_p); + cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic())), + main_p); st->updt_params(p); return st; } + +tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { + tactic * const preamble_t = mk_qfufbv_preamble1(m, 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())); +} diff --git a/src/tactic/smtlogics/qfufbv_tactic.h b/src/tactic/smtlogics/qfufbv_tactic.h index ceb125517..1f1431d70 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.h +++ b/src/tactic/smtlogics/qfufbv_tactic.h @@ -25,8 +25,11 @@ class tactic; tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p); + /* ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)") + ADD_TACTIC("qfufbv_ackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_qfufbv_ackr_tactic(m, p)") */ #endif diff --git a/src/tactic/smtlogics/qfufbv_tactic_params.pyg b/src/tactic/smtlogics/qfufbv_tactic_params.pyg new file mode 100644 index 000000000..6c4bd5b8e --- /dev/null +++ b/src/tactic/smtlogics/qfufbv_tactic_params.pyg @@ -0,0 +1,8 @@ +def_module_params('ackermannization', + description='tactics based on solving UF-theories via ackermannization (see also ackr module)', + class_name='qfufbv_tactic_params', + export=True, + params=( + ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + )) +