From 0fd61eee1f5c295b4d42bbeaed43e5a4e13e2560 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Thu, 17 Dec 2015 13:25:56 +0000 Subject: [PATCH] Cleanup in lackr. --- src/ackr/lackr.cpp | 147 ++++++++++---------------------------- src/ackr/lackr.h | 44 ++++-------- src/ackr/lackr_tactic.cpp | 26 ++----- 3 files changed, 56 insertions(+), 161 deletions(-) diff --git a/src/ackr/lackr.cpp b/src/ackr/lackr.cpp index 6081633c1..aa99f347e 100644 --- a/src/ackr/lackr.cpp +++ b/src/ackr/lackr.cpp @@ -22,57 +22,13 @@ #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"inc_sat_solver.h" +#include"qfaufbv_tactic.h" +#include"qfbv_tactic.h" +#include"tactic2solver.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, lackr_stats& st, expr_ref _f) : m_m(m) , m_p(p) @@ -81,8 +37,7 @@ lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref _f) , m_sat(0) , m_bvutil(m) , m_simp(m) - , m_ackrs(m) - , m_cancel(0) + , m_ackrs(m) , m_st(st) { m_fla = _f; @@ -96,30 +51,22 @@ lackr::~lackr() { } } - - lbool lackr::operator() () { setup_sat(); - const bool ok = init(); - if (!ok) return l_undef; - TRACE("lackr", tout << "sat goal\n"; m_sat->display(tout);); + init(); const lbool rv = m_eager ? eager() : lazy(); - std::cout << "res: " << rv << "\n"; 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() { +void 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; + collect_terms(); + abstract(); } // @@ -127,10 +74,9 @@ bool lackr::init() { // 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";); + << 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 gi = 0; gi < sz; ++gi) { expr * const arg1 = t1->get_arg(gi); @@ -139,14 +85,13 @@ bool lackr::ackr(app * const t1, app * const t2) { if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) { SASSERT(arg1 != arg2); TRACE("lackr", tout << "never eq\n";); - return true; + 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); - SASSERT(a2); + 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); @@ -156,10 +101,10 @@ bool lackr::ackr(app * const t1, app * const t2) { 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_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 true; + if (m_m.is_true(cga)) return false; m_st.m_ackrs_sz++; m_ackrs.push_back(cga); return true; @@ -168,12 +113,12 @@ bool lackr::ackr(app * const t1, app * const t2) { // // Introduce the ackermann lemma for each pair of terms. // -bool lackr::eager_enc() { +void 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(); + 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; @@ -184,14 +129,13 @@ bool lackr::eager_enc() { SASSERT(t1->get_decl() == fd); SASSERT(t2->get_decl() == fd); if (t1 == t2) continue; - if (!ackr(t1,t2)) return false; + ackr(t1,t2); } } } - return true; } -bool lackr::abstract() { +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; @@ -212,12 +156,10 @@ bool lackr::abstract() { } 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; + TRACE("lackr", tout << "abs(\n" << mk_ismt2_pp(m_abstr.get(), m_m, 2) << ")\n";); } 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; @@ -235,25 +177,17 @@ void lackr::add_term(app* a) { lbool lackr::eager() { m_sat->assert_expr(m_abstr); TRACE("lackr", tout << "run sat 0\n"; ); - std::cout << "++sat call\n"; const lbool rv0 = m_sat->check_sat(0, 0); - std::cout << "--sat call\n"; if (rv0 == l_false) return l_false; - checkpoint(); - if (!eager_enc()) return l_undef; - checkpoint(); + eager_enc(); 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_simp(all); m_sat->assert_expr(all); - std::cout << "++sat call\n"; - const lbool rv = m_sat->check_sat(0, 0); - std::cout << "--sat call\n"; - return rv; + 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); m_sat->assert_expr(m_abstr); @@ -284,12 +218,10 @@ lbool lackr::lazy() { void lackr::setup_sat() { if (m_use_sat) { - //tactic_ref t = mk_qfbv_tactic(m_m, m_p); - //m_sat = mk_tactic2solver(m_m, t.get(), m_p); - m_sat = mk_inc_sat_solver(m_m, m_p); + 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); } @@ -299,9 +231,9 @@ void lackr::setup_sat() { // -// Collect all uninterpreted terms. +// Collect all uninterpreted terms, skipping 0-arity. // -bool lackr::collect_terms() { +void lackr::collect_terms() { ptr_vector stack; expr * curr; expr_mark visited; @@ -318,30 +250,23 @@ bool lackr::collect_terms() { 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())) { + { + 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(to_app(curr)); - checkpoint(); + add_term(a); } + } 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()); - } + UNREACHABLE(); break; default: UNREACHABLE(); - return false; + return; } } - visited.reset(); - return true; + visited.reset(); } diff --git a/src/ackr/lackr.h b/src/ackr/lackr.h index 38f810d04..ea1ea7ce2 100644 --- a/src/ackr/lackr.h +++ b/src/ackr/lackr.h @@ -17,16 +17,16 @@ #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" +#include"bv_decl_plugin.h" +#include"lbool.h" +#include"model.h" +#include"solver.h" +#include"util.h" +#include"tactic_exception.h" struct lackr_stats { lackr_stats() : m_it(0), m_ackrs_sz(0) {} @@ -37,8 +37,7 @@ struct lackr_stats { class lackr { public: - lackr(ast_manager& m, params_ref p,lackr_stats& st, - expr_ref _f); + lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref _f); ~lackr(); void updt_params(params_ref const & _p) { ackr_params p(_p); @@ -54,26 +53,14 @@ class lackr { inline model_ref get_model() { return m_model; } // - // timeout mechanisms + // timeout mechanism // void checkpoint() { - //std::cout << "chk\n"; - if (m_m.canceled()) { - std::cout << "canceled\n"; + if (m_m.canceled()) { 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; @@ -88,33 +75,32 @@ class lackr { th_rewriter m_simp; expr_ref_vector m_ackrs; model_ref m_model; - volatile bool m_cancel; bool m_eager; bool m_use_sat; lackr_stats& m_st; - bool init(); + void init(); void setup_sat(); lbool eager(); lbool lazy(); // - // Introduce ackermann lemma for the two given terms. + // 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. // - bool eager_enc(); + void eager_enc(); - bool abstract(); + void abstract(); void add_term(app* a); // - // Collect all uninterpreted terms. + // Collect all uninterpreted terms, skipping 0-arity. // - bool collect_terms(); + void collect_terms(); }; #endif /* LACKR_H_15079 */ diff --git a/src/ackr/lackr_tactic.cpp b/src/ackr/lackr_tactic.cpp index 7f2c6f95b..5e2b88e70 100644 --- a/src/ackr/lackr_tactic.cpp +++ b/src/ackr/lackr_tactic.cpp @@ -36,12 +36,9 @@ 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 ~lackr_tactic() { } virtual void operator()(goal_ref const & g, goal_ref_buffer & result, @@ -57,8 +54,8 @@ public: expr_ref f(m); f = m.mk_and(flas.size(), flas.c_ptr()); // running implementation - m_imp = alloc(lackr, m, m_p, m_st, f); - const lbool o = m_imp->operator()(); + scoped_ptr imp = alloc(lackr, m, m_p, m_st, f); + const lbool o = imp->operator()(); flas.reset(); // report result goal_ref resg(alloc(goal, *g, true)); @@ -66,16 +63,9 @@ public: 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); + model_ref abstr_model = imp->get_model(); + mc = mk_lackr_model_converter(m, imp->get_info(), abstr_model); } - // cleanup - lackr * d = m_imp; - #pragma omp critical (lackr) - { - m_imp = 0; - } - dealloc(d); } virtual void collect_statistics(statistics & st) const { @@ -91,15 +81,9 @@ public: 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; lackr_stats m_st; };