From bbe93ef61096578a11ee531e9a18b4a247b50089 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2013 18:26:22 -0700 Subject: [PATCH 1/4] fix build warning, make context simplifier traverse subterms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/float_rewriter.cpp | 1 - src/muz_qe/hnf.cpp | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 70 +++++++++++++------ 3 files changed, 49 insertions(+), 24 deletions(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 10311598b..70ba09581 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -226,7 +226,6 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) { result = arg1; return BR_DONE; } - sort * s = m().get_sort(arg1); result = m().mk_ite(m_util.mk_is_sign_minus(arg1), m_util.mk_uminus(arg1), arg1); diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp index 47370e0e6..5a7d1c4ba 100644 --- a/src/muz_qe/hnf.cpp +++ b/src/muz_qe/hnf.cpp @@ -80,8 +80,8 @@ public: m_todo(m), m_proofs(m), m_refs(m), - m_qh(m), m_name("P"), + m_qh(m), m_fresh_predicates(m) { } diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 0092cdd38..5668ca455 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -33,10 +33,14 @@ class ctx_solver_simplify_tactic : public tactic { arith_util m_arith; mk_simplified_app m_mk_app; func_decl_ref m_fn; + obj_map m_fns; unsigned m_num_steps; + volatile bool m_cancel; public: ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()): - m(m), m_params(p), m_solver(m, m_front_p), m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0) { + m(m), m_params(p), m_solver(m, m_front_p), + m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0), + m_cancel(false) { sort* i_sort = m_arith.mk_int(); m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort()); } @@ -45,7 +49,13 @@ public: return alloc(ctx_solver_simplify_tactic, m, m_params); } - virtual ~ctx_solver_simplify_tactic() {} + virtual ~ctx_solver_simplify_tactic() { + obj_map::iterator it = m_fns.begin(), end = m_fns.end(); + for (; it != end; ++it) { + m.dec_ref(it->m_value); + } + m_fns.reset(); + } virtual void updt_params(params_ref const & p) { m_solver.updt_params(p); @@ -76,15 +86,18 @@ public: virtual void cleanup() { reset_statistics(); m_solver.reset(); + m_cancel = false; } + protected: + virtual void set_cancel(bool f) { m_solver.set_cancel(f); + m_cancel = false; } void reduce(goal& g) { SASSERT(g.is_well_sorted()); - m_num_steps = 0; expr_ref fml(m); tactic_report report("ctx-solver-simplify", g); if (g.inconsistent()) @@ -134,15 +147,16 @@ protected: svector parent_ids, self_ids; expr_ref_vector fresh_vars(m), trail(m); expr_ref res(m), tmp(m); - obj_map > cache; + obj_map > cache; unsigned id = 1; - expr* n2, *fml; + expr_ref n2(m), fml(m); unsigned path_id = 0, self_pos = 0; app * a; unsigned sz; std::pair path_r; ptr_vector found; - expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); + expr_ref_vector args(m); + expr_ref n = mk_fresh(id, m.mk_bool_sort()); trail.push_back(n); fml = result.get(); @@ -156,9 +170,9 @@ protected: self_ids.push_back(0); m_solver.push(); - while (!todo.empty()) { + while (!todo.empty() && !m_cancel) { expr_ref res(m); - ptr_buffer args; + args.reset(); expr* e = todo.back(); unsigned pos = parent_ids.back(); n = names.back(); @@ -167,10 +181,6 @@ protected: if (cache.contains(e)) { goto done; } - if (!m.is_bool(e)) { - res = e; - goto done; - } if (m.is_bool(e) && !checked && simplify_bool(n, res)) { TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";); goto done; @@ -193,14 +203,11 @@ protected: found.reset(); // arguments already simplified. for (unsigned i = 0; i < sz; ++i) { expr* arg = a->get_arg(i); - if (!m.is_bool(arg)) { - args.push_back(arg); - } - else if (cache.find(arg, path_r) && !found.contains(arg)) { + if (cache.find(arg, path_r) && !found.contains(arg)) { // // This is a single traversal version of the context // simplifier. It simplifies only the first occurrence of - // a formula with respect to the context. + // a sub-term with respect to the context. // found.push_back(arg); @@ -208,15 +215,18 @@ protected: TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";); args.push_back(path_r.second); } - else { + else if (m.is_bool(arg)) { res = local_simplify(a, n, id, i); TRACE("ctx_solver_simplify_tactic", tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";); + args.push_back(res); + } + else { args.push_back(arg); } } else if (!n2 && !found.contains(arg)) { - n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); + n2 = mk_fresh(id, m.get_sort(arg)); trail.push_back(n2); todo.push_back(arg); parent_ids.push_back(self_pos); @@ -254,8 +264,10 @@ protected: is_checked.pop_back(); m_solver.pop(1); } - VERIFY(cache.find(fml, path_r)); - result = path_r.second; + if (!m_cancel) { + VERIFY(cache.find(fml, path_r)); + result = path_r.second; + } } bool simplify_bool(expr* n, expr_ref& res) { @@ -282,11 +294,25 @@ protected: return false; } + expr_ref mk_fresh(unsigned& id, sort* s) { + func_decl* fn; + if (m.is_bool(s)) { + fn = m_fn; + } + else if (!m_fns.find(s, fn)) { + fn = m.mk_func_decl(symbol(0xbeef101 + id), m_arith.mk_int(), s); + m.inc_ref(fn); + m_fns.insert(s, fn); + } + return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m); + } + + expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) { SASSERT(index < a->get_num_args()); SASSERT(m.is_bool(a->get_arg(index))); expr_ref n2(m), result(m), tmp(m); - n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); + n2 = mk_fresh(id, m.get_sort(a->get_arg(index))); ptr_buffer args; for (unsigned i = 0; i < a->get_num_args(); ++i) { if (i == index) { From b427958b9eef053488a57f67cc0125c5f0141e55 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 09:53:11 -0700 Subject: [PATCH 2/4] qe_lite> fix crash in is_var_eq() (by me & Nikolaj) Signed-off-by: Nuno Lopes --- src/muz_qe/qe_lite.cpp | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index be3f80f92..ff49584ff 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -201,9 +201,15 @@ namespace eq { return (*m_is_variable)(e); } - bool is_neg_var(ast_manager & m, expr * e) { + bool is_neg_var(ast_manager & m, expr * e, var*& v) { expr* e1; - return m.is_not(e, e1) && is_variable(e1); + if (m.is_not(e, e1) && is_variable(e1)) { + v = to_var(e1); + return true; + } + else { + return false; + } } @@ -328,18 +334,19 @@ namespace eq { bool is_var_eq(expr * e, ptr_vector& vs, expr_ref_vector & ts) { expr* lhs, *rhs; + var* v; // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { // (iff (not VAR) t) (iff t (not VAR)) cases if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { - if (!is_neg_var(m, lhs)) { + if (!is_neg_var(m, lhs, v)) { std::swap(lhs, rhs); } - if (!is_neg_var(m, lhs)) { + if (!is_neg_var(m, lhs, v)) { return false; } - vs.push_back(to_var(lhs)); + vs.push_back(v); ts.push_back(m.mk_not(rhs)); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; @@ -378,9 +385,9 @@ namespace eq { } // VAR = false case - if (is_neg_var(m, e)) { + if (is_neg_var(m, e, v)) { ts.push_back(m.mk_false()); - vs.push_back(to_var(to_app(e)->get_arg(0))); + vs.push_back(v); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } From df35da1acfece2af81c7bcbab774a86b835f80b2 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 10:48:48 -0700 Subject: [PATCH 3/4] rule_manager::mk(): default initialization of m_proof to null Signed-off-by: Nuno Lopes --- src/muz_qe/dl_rule.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index a13229e7a..14a316e48 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -502,6 +502,7 @@ namespace datalog { r->m_tail_size = n; r->m_positive_cnt = source->m_positive_cnt; r->m_uninterp_cnt = source->m_uninterp_cnt; + r->m_proof = 0; m.inc_ref(r->m_head); for (unsigned i = 0; i < n; i++) { r->m_tail[i] = source->m_tail[i]; From da83a6b28c01bbe9b2dfb25d734d2b2fa6c906d9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 14:48:22 -0700 Subject: [PATCH 4/4] dl_bit_blasting: run simplifier before bit-blasting, in order to comply with its precondition Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_bit_blast.cpp | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 1e984f254..e6612022f 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast_pp.h" #include "expr_safe_replace.h" #include "filter_model_converter.h" +#include "dl_mk_interp_tail_simplifier.h" namespace datalog { @@ -212,18 +213,23 @@ namespace datalog { ast_manager & m; params_ref m_params; rule_ref_vector m_rules; + mk_interp_tail_simplifier m_simplifier; bit_blaster_rewriter m_blaster; expand_mkbv m_rewriter; - bool blast(expr_ref& fml) { + bool blast(rule *r, expr_ref& fml) { proof_ref pr(m); - expr_ref fml1(m), fml2(m); - m_blaster(fml, fml1, pr); - m_rewriter(fml1, fml2); - TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";); - if (fml2 != fml) { - fml = fml2; + expr_ref fml1(m), fml2(m), fml3(m); + rule_ref r2(m_context.get_rule_manager()); + // We need to simplify rule before bit-blasting. + m_simplifier.transform_rule(r, r2); + r2->to_formula(fml1); + m_blaster(fml1, fml2, pr); + m_rewriter(fml2, fml3); + TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";); + if (fml3 != fml) { + fml = fml3; return true; } else { @@ -241,6 +247,7 @@ namespace datalog { m(ctx.get_manager()), m_params(ctx.get_params().p), m_rules(ctx.get_rule_manager()), + m_simplifier(ctx), m_blaster(ctx.get_manager(), m_params), m_rewriter(ctx.get_manager(), ctx, m_rules) { m_params.set_bool("blast_full", true); @@ -261,12 +268,12 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { rule * r = source.get_rule(i); r->to_formula(fml); - if (blast(fml)) { + if (blast(r, fml)) { proof_ref pr(m); if (m_context.generate_proof_trace()) { pr = m.mk_asserted(fml); // loses original proof of r. } - rm.mk_rule(fml, pr, m_rules, r->name()); + rm.mk_rule(fml, pr, m_rules, r->name()); } else { m_rules.push_back(r);