diff --git a/scripts/mk_project.py b/scripts/mk_project.py index eb7218d4b..12e8fea3c 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -76,10 +76,11 @@ def init_project_def(): 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') + add_lib('ackr', ['smt', 'smtlogic_tactics', 'sat_solver'], 'ackr') API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h'] add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) - add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') + add_exe('shell', ['api', 'sat', 'extra_cmds','opt','ackr'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False) _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', reexports=['api'], diff --git a/src/ackr/ackr.pyg b/src/ackr/ackr.pyg new file mode 100644 index 000000000..4b3d6f5f7 --- /dev/null +++ b/src/ackr/ackr.pyg @@ -0,0 +1,8 @@ +def_module_params('ackr', + description='solving UF via ackermannization (currently for QF_AUFBV)', + export=True, + params=( + ('eager', BOOL, True, 'eagerly instantiate all congruence rules'), + ('sat_backend', BOOL, False, 'use SAT rather than SMT'), + )) + diff --git a/src/ackr/ackr_info.h b/src/ackr/ackr_info.h new file mode 100644 index 000000000..6d2b596fe --- /dev/null +++ b/src/ackr/ackr_info.h @@ -0,0 +1,106 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + +ackr_info.h + +Abstract: + +Author: + +Mikolas Janota + +Revision History: +--*/ +#ifndef ACKR_INFO_H_12278 +#define ACKR_INFO_H_12278 +#include"obj_hashtable.h" +#include"ast.h" +#include"ref.h" +#include"expr_replacer.h" + +// +// Information about how a formula was extracted into +// a formula without uninterpreted function symbols. +// +// The intended use is that new terms are added via set_abstr. +// Once all terms are abstracted, call seal. +// 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; + + bool m_sealed; // debugging + unsigned m_ref_count; // reference counting +}; + +typedef ref ackr_info_ref; +#endif /* ACKR_INFO_H_12278 */ diff --git a/src/ackr/lackr.cpp b/src/ackr/lackr.cpp new file mode 100644 index 000000000..99e5cf0b5 --- /dev/null +++ b/src/ackr/lackr.cpp @@ -0,0 +1,337 @@ +/*++ + 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"array_decl_plugin.h" +#include"simplifier_plugin.h" +#include"basic_simplifier_plugin.h" +#include"array_simplifier_params.h" +#include"array_simplifier_plugin.h" +#include"bv_simplifier_plugin.h" +#include"bool_rewriter.h" +/////////////// +#include"th_rewriter.h" +/////////////// +#include"cooperate.h" +/////////////// +#include"model_smt2_pp.h" +/////////////// + +struct simp_wrap { + inline void operator() (expr * s, expr_ref & r) { + proof_ref dummy(m); + simp(s, r, dummy); + } + simp_wrap(ast_manager& m) + : m(m) + , simp(m) + , bsp(m) + , bvsp(m, bsp, bv_par) + , asp(m, bsp, simp, ar_par) + { + params_ref p; + p.set_bool("local_ctx", true); + p.set_uint("local_ctx_limit", 10000000); + p.set_bool("ite_extra_rules", true); + bsp.get_rewriter().updt_params(p); + + simp.register_plugin(&bsp); + simp.register_plugin(&bvsp); + } + + ~simp_wrap() { + simp.release_plugins(); + } + + ast_manager& m; + simplifier simp; + basic_simplifier_plugin bsp; + bv_simplifier_params bv_par; + bv_simplifier_plugin bvsp; + array_simplifier_params ar_par; + array_simplifier_plugin asp; +}; + + +lackr::lackr(ast_manager& m, params_ref p, expr_ref _f) + : m_m(m) + , m_p(p) + , m_fla(m) + , m_abstr(m) + , m_sat(0) + , m_bvutil(m) + , m_simp(m) + , m_ackrs(m) + , m_cancel(0) +{ + m_fla = _f; + 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() () { + setup_sat(); + const bool ok = init(); + if (!ok) return l_undef; + TRACE("lackr", tout << "sat goal\n"; m_sat->display(tout);); + const lbool rv = m_eager ? eager() : lazy(); + if (rv == l_true) m_sat->get_model(m_model); + TRACE("lackr", tout << "sat:" << rv << '\n'; ); + CTRACE("lackr", rv == l_true, + model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; ); + return rv; +} + + +bool lackr::init() { + params_ref simp_p(m_p); + m_simp.updt_params(simp_p); + m_info = alloc(ackr_info, m_m); + bool iok = collect_terms() && abstract(); + if (!iok) return false; + return true; +} + +// +// 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(); + expr_ref_vector eqs(m_m); + for (unsigned gi = 0; gi < sz; ++gi) { + expr * const arg1 = t1->get_arg(gi); + expr * const arg2 = t2->get_arg(gi); + if (arg1 == arg2) continue; + if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) { + SASSERT(arg1 != arg2); + TRACE("lackr", tout << "never eq\n";); + return true; + } + 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); + SASSERT(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); + m_simp(cga); + TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";); + if (!m_m.is_true(cga)) m_ackrs.push_back(cga); + return true; +} + +// +// Introduce the ackermann lemma for each pair of terms. +// +bool lackr::eager_enc() { + 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; + if (!ackr(t1,t2)) return false; + } + } + } + return true; +} + +bool 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(); + m_info->abstract(m_fla.get(), m_abstr); + TRACE("lackr", tout << "abs(\n" << mk_ismt2_pp(m_abstr.get(), m_m, 2) << ")\n";); + return true; +} + +void lackr::add_term(app* a) { + //TRACE("lackr", tout << "inspecting term(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";); + if (a->get_num_args() == 0) return; + func_decl* const fd = a->get_decl(); + if (!is_uninterp(a)) return; + SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a)); + app_set* ts = 0; + if (!m_fun2terms.find(fd, ts)) { + ts = alloc(app_set); + m_fun2terms.insert(fd, ts); + } + TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";); + ts->insert(a); +} + + +lbool lackr::eager() { + if (!eager_enc()) return l_undef; + m_sat->assert_expr(m_abstr); + TRACE("lackr", tout << "run sat 0\n"; ); + if (m_sat->check_sat(0, 0) == l_false) + return l_false; + checkpoint(); + expr_ref all(m_m); + all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr()); + m_simp(all); + TRACE("lackr", tout << "run sat\n"; ); + m_sat->assert_expr(all); + return m_sat->check_sat(0, 0); +} + + +lbool lackr::lazy() { + lackr_model_constructor mc(m_m, m_info); + m_sat->assert_expr(m_abstr); + unsigned ackr_head = 0; + unsigned it = 0; + while (1) { + checkpoint(); + //std::cout << "it: " << ++it << "\n"; + TRACE("lackr", tout << "lazy check\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++)); + } + } +} + +void lackr::setup_sat() { + if (m_use_sat) { + //std::cout << "; qfbv sat\n"; + tactic_ref t = mk_qfbv_tactic(m_m, m_p); + m_sat = mk_tactic2solver(m_m, t.get(), m_p); + } + else { + //std::cout << "; smt sat\n"; + tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); + m_sat = mk_tactic2solver(m_m, t.get(), m_p); + } + SASSERT(m_sat); + m_sat->set_produce_models(true); +} + + +// +// Collect all uninterpreted terms. +// +bool lackr::collect_terms() { + ptr_vector stack; + expr * curr; + expr_mark visited; + stack.push_back(m_fla.get()); + while (!stack.empty()) { + curr = stack.back(); + if (visited.is_marked(curr)) { + stack.pop_back(); + continue; + } + + switch (curr->get_kind()) { + case AST_VAR: + visited.mark(curr, true); + stack.pop_back(); + break; + + case AST_APP: + if (for_each_expr_args(stack, visited, + to_app(curr)->get_num_args(), to_app(curr)->get_args())) { + visited.mark(curr, true); + stack.pop_back(); + add_term(to_app(curr)); + } + break; + case AST_QUANTIFIER: + if (visited.is_marked(to_quantifier(curr)->get_expr())) { + visited.mark(curr, true); + stack.pop_back(); + } + else { + stack.push_back(to_quantifier(curr)->get_expr()); + } + break; + default: + UNREACHABLE(); + return false; + } + } + visited.reset(); + return true; +} diff --git a/src/ackr/lackr.h b/src/ackr/lackr.h new file mode 100644 index 000000000..2f685a001 --- /dev/null +++ b/src/ackr/lackr.h @@ -0,0 +1,106 @@ + /*++ + Copyright (c) 2015 Microsoft Corporation + + Module Name: + + lackr.h + + Abstract: + + + Author: + + Mikolas Janota + + Revision History: + --*/ +#ifndef LACKR_H_15079 +#define LACKR_H_15079 +/////////////// +#include"inc_sat_solver.h" +#include"qfaufbv_tactic.h" +#include"qfbv_tactic.h" +#include"tactic2solver.h" +#include"ackr_info.h" +#include"ackr_params.hpp" +#include"tactic_exception.h" +#include"th_rewriter.h" +#include"bv_decl_plugin.h" +#include"cooperate.h" + +class lackr { + public: + lackr(ast_manager& m, params_ref p, expr_ref _f); + lbool operator() (); + ~lackr(); + inline ackr_info_ref get_info() { return m_info; } + inline model_ref get_model() { return m_model; } + + void updt_params(params_ref const & _p) { + ackr_params p(_p); + m_eager = p.eager(); + m_use_sat = p.sat_backend(); + } + + // + // timeout mechanisms + // + + void checkpoint() { + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + cooperate("lackr"); + } + + //virtual void set_cancel(bool f) { + // //#pragma omp critical (lackr_cancel) + // { + // m_cancel = f; + // if (m_sat == NULL) return; + // if (f) m_sat->cancel(); + // else m_sat->reset_cancel(); + // } + //} + private: + typedef obj_hashtable app_set; + typedef obj_map fun2terms_map; + ast_manager& m_m; + params_ref m_p; + expr_ref m_fla; + expr_ref m_abstr; + fun2terms_map m_fun2terms; + ackr_info_ref m_info; + scoped_ptr m_sat; + bv_util m_bvutil; + th_rewriter m_simp; + expr_ref_vector m_ackrs; + model_ref m_model; + volatile bool m_cancel; + bool m_eager; + bool m_use_sat; + + bool init(); + void setup_sat(); + lbool eager(); + lbool lazy(); + + // + // Introduce ackermann lemma for the two given terms. + // + bool ackr(app * const t1, app * const t2); + + // + // Introduce the ackermann lemma for each pair of terms. + // + bool eager_enc(); + + bool abstract(); + + void add_term(app* a); + + // + // Collect all uninterpreted terms. + // + bool collect_terms(); +}; +#endif /* LACKR_H_15079 */ diff --git a/src/ackr/lackr_model_constructor.cpp b/src/ackr/lackr_model_constructor.cpp new file mode 100644 index 000000000..5f0060ad5 --- /dev/null +++ b/src/ackr/lackr_model_constructor.cpp @@ -0,0 +1,313 @@ +/*++ + 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, + vector>& 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) + {} + + ~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(); + } + private: + ast_manager& m_m; + ackr_info_ref m_info; + model_ref& m_abstr_model; + vector>& 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; + + 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) { + if (!is_app(e)) return false; + return is_val(to_app(e)); + } + + inline bool is_val(app * a) { + const family_id fid = a->get_decl()->get_family_id(); + const bool rv = fid != null_family_id && a->get_num_args() == 0; + SASSERT(rv == (m_bv_rw.is_numeral(a) || m_m.is_true(a) || m_m.is_false(a))); + return rv; + } + + 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 (a->get_family_id() == null_family_id) { // 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(m) + , state(UNKNOWN) + , info(info) +{} + +bool lackr_model_constructor::check(model_ref& abstr_model) { + conflicts.reset(); + lackr_model_constructor::imp i(m, info, abstr_model, conflicts); + const bool rv = i.check(); + state = rv ? CHECKED : CONFLICT; + return rv; +} \ No newline at end of file diff --git a/src/ackr/lackr_model_constructor.h b/src/ackr/lackr_model_constructor.h new file mode 100644 index 000000000..5b2385c2c --- /dev/null +++ b/src/ackr/lackr_model_constructor.h @@ -0,0 +1,40 @@ + /*++ + 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_626 +#define LACKR_MODEL_CONSTRUCTOR_H_626 +#include"ast.h" +#include"ackr_info.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); + bool check(model_ref& abstr_model); + const conflict_list& get_conflicts() { + SASSERT(state == CONFLICT); + return conflicts; + } + private: + struct imp; + enum {CHECKED, CONFLICT, UNKNOWN} state; + conflict_list conflicts; + ast_manager& m; + const ackr_info_ref info; +}; +#endif /* MODEL_CONSTRUCTOR_H_626 */ diff --git a/src/ackr/lackr_model_converter.cpp b/src/ackr/lackr_model_converter.cpp new file mode 100644 index 000000000..05db4e789 --- /dev/null +++ b/src/ackr/lackr_model_converter.cpp @@ -0,0 +1,138 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + +lackr_model_converter.cpp + +Abstract: + +Author: + +Mikolas Janota + +Revision History: +--*/ +#include"lackr_model_converter.h" +#include"model_evaluator.h" +#include"ast_smt2_pp.h" +#include"ackr_info.h" + + +class lackr_model_converter : public model_converter { +public: + lackr_model_converter(ast_manager & m, + const ackr_info_ref& info, + model_ref& abstr_model) + : m(m) + , info(info) + , abstr_model(abstr_model) + { } + + virtual ~lackr_model_converter() { } + + 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(abstr_model.get()); + model * new_model = alloc(model, m); + convert(abstr_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; + 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 lackr_model_converter::convert(model * source, model * destination) { + SASSERT(source->get_num_functions() == 0); + convert_constants(source,destination); + convert_sorts(source,destination); +} + +void lackr_model_converter::convert_constants(model * source, model * destination) { + TRACE("lackr_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 lackr_model_converter::add_entry(model_evaluator & evaluator, + app* term, expr* value, + obj_map& interpretations) { + TRACE("lackr_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("lackr_model", tout << "entry already present\n";); + } +} + +void lackr_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_lackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) { + return alloc(lackr_model_converter, m, info, abstr_model); +} diff --git a/src/ackr/lackr_model_converter.h b/src/ackr/lackr_model_converter.h new file mode 100644 index 000000000..ec59d7572 --- /dev/null +++ b/src/ackr/lackr_model_converter.h @@ -0,0 +1,22 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + +lackr_model_converter.h + +Abstract: + +Author: + +Mikolas Janota + +Revision History: +--*/ +#ifndef LACKR_MODEL_CONVERTER_H_5814 +#define LACKR_MODEL_CONVERTER_H_5814 +#include"model_converter.h" +#include"ackr_info.h" + +model_converter * mk_lackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model); +#endif /* LACKR_MODEL_CONVERTER_H_5814 */ diff --git a/src/ackr/lackr_tactic.cpp b/src/ackr/lackr_tactic.cpp new file mode 100644 index 000000000..c5368940b --- /dev/null +++ b/src/ackr/lackr_tactic.cpp @@ -0,0 +1,136 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + +lackr_tactic.cpp + +Abstract: + +Author: + +Mikolas Janota + +Revision History: +--*/ +#include"tactical.h" +/////////////// +#include"solve_eqs_tactic.h" +#include"simplify_tactic.h" +#include"propagate_values_tactic.h" +#include"bit_blaster_tactic.h" +#include"elim_uncnstr_tactic.h" +#include"max_bv_sharing_tactic.h" +#include"bv_size_reduction_tactic.h" +#include"ctx_simplify_tactic.h" +#include"nnf_tactic.h" +/////////////// +#include"model_smt2_pp.h" +#include"cooperate.h" +#include"lackr.h" +#include"lackr_model_converter.h" + +class lackr_tactic : public tactic { +public: + lackr_tactic(ast_manager& m, params_ref const& p) + : m_m(m) + , m_p(p) + , m_imp(0) + {} + + virtual ~lackr_tactic() { + if (m_imp) dealloc(m_imp); + } + + 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()); + TRACE("lackr", g->display(tout << "Goal:\n");); + // conflate all assertions into one conjunction + ptr_vector flas; + g->get_formulas(flas); + expr_ref f(m); + f = m.mk_and(flas.size(), flas.c_ptr()); + // running implementation + m_imp = alloc(lackr, m, m_p, f); + const lbool o = m_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 = m_imp->get_model(); + mc = mk_lackr_model_converter(m, m_imp->get_info(), abstr_model); + } + // clenup + lackr * d = m_imp; + #pragma omp critical (lackr) + { + m_imp = 0; + } + dealloc(d); + } + + virtual void cleanup() { } + + virtual tactic* translate(ast_manager& m) { + return alloc(lackr_tactic, m, m_p); + } + + // Currently tactics are not cancelable. + //virtual void set_cancel(bool f) { + // if (m_imp) m_imp->set_cancel(f); + //} +private: + ast_manager& m_m; + params_ref m_p; + lackr* m_imp; +}; + +tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p) { + //return and_then(mk_nnf_tactic(m_m, m_p), alloc(lackr_tactic, m_m, m_p)); + //return alloc(lackr_tactic, m_m, m_p); + //params_ref main_p; + //main_p.set_bool("elim_and", true); + //main_p.set_bool("sort_store", true); + //main_p.set_bool("expand_select_store", true); + //main_p.set_bool("expand_store_eq", true); + + params_ref simp2_p = p; + simp2_p.set_bool("som", true); + 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("blast_eq_value", true); + //simp2_p.set_bool("bv_sort_ac", true); + + params_ref ctx_simp_p; + ctx_simp_p.set_uint("max_depth", 32); + ctx_simp_p.set_uint("max_steps", 5000000); + + tactic * const preamble_t = 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), + //mk_macro_finder_tactic(m, p), + using_params(mk_simplify_tactic(m), simp2_p) + //mk_nnf_tactic(m_m, m_p) + ); + + return and_then( + preamble_t, + alloc(lackr_tactic, m, p)); +} diff --git a/src/ackr/lackr_tactic.h b/src/ackr/lackr_tactic.h new file mode 100644 index 000000000..792fa2072 --- /dev/null +++ b/src/ackr/lackr_tactic.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + +lackr_tactic.h + +Abstract: + +Author: + +Mikolas Janota + +Revision History: +--*/ + +#ifndef _LACKR_TACTIC_H_ +#define _LACKR_TACTIC_H_ +#include"tactical.h" + +tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p); + +/* +ADD_TACTIC("lackr", "lackr.", "mk_lackr_tactic(m, p)") +*/ + +#endif +