From b427958b9eef053488a57f67cc0125c5f0141e55 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 09:53:11 -0700 Subject: [PATCH 1/7] 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 2/7] 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 9abcde9a358f883befbcad910e880263182e5577 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Mar 2013 14:42:18 -0700 Subject: [PATCH 3/7] Fix typos Signed-off-by: Leonardo de Moura --- src/smt/asserted_formulas.cpp | 2 +- src/tactic/bv/max_bv_sharing_tactic.cpp | 2 +- src/tactic/core/propagate_values_tactic.cpp | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3155d9c58..c5d3c08cf 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -653,7 +653,7 @@ void asserted_formulas::propagate_values() { // will be (silently) eliminated, and models produced by Z3 will not contain them. flush_cache(); } - TRACE("propagate_values", tout << "afer:\n"; display(tout);); + TRACE("propagate_values", tout << "after:\n"; display(tout);); } void asserted_formulas::propagate_booleans() { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 251e2b754..f60487d60 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -269,7 +269,7 @@ class max_bv_sharing_tactic : public tactic { m_rw.cfg().cleanup(); g->inc_depth(); result.push_back(g.get()); - TRACE("qe", g->display(tout);); + TRACE("max_bv_sharing", g->display(tout);); SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 6d9e6ccbd..1e358177f 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -165,7 +165,7 @@ class propagate_values_tactic : public tactic { m_occs(*m_goal); while (true) { - TRACE("propagate_values", m_goal->display(tout);); + TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display(tout);); if (forward) { for (; m_idx < size; m_idx++) { process_current(); @@ -201,14 +201,14 @@ class propagate_values_tactic : public tactic { if (round >= m_max_rounds) break; IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;); - TRACE("propgate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";); + TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";); } end: m_goal->elim_redundancies(); m_goal->inc_depth(); result.push_back(m_goal); SASSERT(m_goal->is_well_sorted()); - TRACE("propagate_values", m_goal->display(tout);); + TRACE("propagate_values", tout << "end\n"; m_goal->display(tout);); TRACE("propagate_values_core", m_goal->display_with_dependencies(tout);); m_goal = 0; } From da83a6b28c01bbe9b2dfb25d734d2b2fa6c906d9 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 14:48:22 -0700 Subject: [PATCH 4/7] 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); From f32eaee62ef61ae8fb6d09593bb71f551413c10f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Mar 2013 15:40:52 -0700 Subject: [PATCH 5/7] Replace std::sort with std::stable_sort when the given relation is just a partial order. This change avoids discrepancies when using different implmentations of std::sort. Signed-off-by: Leonardo de Moura --- src/ast/simplifier/poly_simplifier_plugin.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp index 13e5748dc..402b078a8 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ b/src/ast/simplifier/poly_simplifier_plugin.cpp @@ -18,6 +18,7 @@ Author: #include"ast_pp.h" #include"ast_util.h" #include"ast_smt2_pp.h" +#include"ast_ll_pp.h" poly_simplifier_plugin::poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, decl_kind num): @@ -173,7 +174,7 @@ void poly_simplifier_plugin::mk_monomial(unsigned num_args, expr * * args, expr_ result = args[0]; break; default: - std::sort(args, args + num_args, monomial_element_lt_proc(*this)); + std::stable_sort(args, args + num_args, monomial_element_lt_proc(*this)); result = mk_mul(num_args, args); SASSERT(wf_monomial(result)); break; @@ -465,7 +466,9 @@ void poly_simplifier_plugin::mk_sum_of_monomials(expr_ref_vector & monomials, ex result = monomials.get(0); break; default: { - std::sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this)); + TRACE("mk_sum_sort", tout << "before\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); + std::stable_sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this)); + TRACE("mk_sum_sort", tout << "after\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";); if (is_simple_sum_of_monomials(monomials)) { mk_sum_of_monomials_core(monomials.size(), monomials.c_ptr(), result); return; From 25a41d48dc7367d9042661562380664dbd606e2e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 25 Mar 2013 15:41:52 -0700 Subject: [PATCH 6/7] speedup bit_vector::num_words() Proof of equivalence w.r.t. previous code: http://rise4fun.com/Z3/aiLV Signed-off-by: Nuno Lopes --- src/util/bit_vector.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 2e7becee7..1d6083717 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -37,7 +37,8 @@ class bit_vector { } static unsigned num_words(unsigned num_bits) { - return (num_bits % 32) == 0 ? (num_bits / 32) : ((num_bits / 32) + 1); + // return (num_bits % 32) == 0 ? (num_bits / 32) : ((num_bits / 32) + 1); + return (num_bits + 31) / 32; } void expand_to(unsigned new_capacity); From b417ca657d388a3f635b19f371b5d3975835f412 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Mar 2013 16:52:08 -0700 Subject: [PATCH 7/7] Fix set_interruptable usage Signed-off-by: Leonardo de Moura --- src/api/api_algebraic.cpp | 4 ++-- src/api/api_ast.cpp | 2 +- src/api/api_datalog.cpp | 4 ++-- src/api/api_polynomial.cpp | 2 +- src/api/api_solver.cpp | 2 +- src/api/api_solver_old.cpp | 4 ++-- src/api/api_tactic.cpp | 2 +- 7 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 7716cbb59..d03a6aff4 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -373,7 +373,7 @@ extern "C" { scoped_anum_vector roots(_am); { cancel_eh eh(_am); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh); vector_var2anum v2a(as); _am.isolate_roots(_p, v2a, roots); @@ -408,7 +408,7 @@ extern "C" { } { cancel_eh eh(_am); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh); vector_var2anum v2a(as); int r = _am.eval_sign_at(_p, v2a); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index e93e1a178..680b59c68 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -681,7 +681,7 @@ extern "C" { th_rewriter m_rw(m, p); expr_ref result(m); cancel_eh eh(m_rw); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_timer timer(timeout, &eh); diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 28fe3ed33..0f100e747 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -266,7 +266,7 @@ extern "C" { lbool r = l_undef; cancel_eh eh(*to_fixedpoint_ref(d)); unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); try { @@ -291,7 +291,7 @@ extern "C" { lbool r = l_undef; unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); cancel_eh eh(*to_fixedpoint_ref(d)); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); try { diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 3148f972b..25d4ca292 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -67,7 +67,7 @@ extern "C" { expr_ref _r(mk_c(c)->m()); { cancel_eh eh(pm); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); scoped_timer timer(mk_c(c)->params().m_timeout, &eh); pm.psc_chain(_p, _q, v_x, rs); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9ace149af..ac30a0c21 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -243,7 +243,7 @@ extern "C" { unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false); cancel_eh eh(*to_solver_ref(s)); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); lbool result; { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index c89f89873..e0533fbd9 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -73,7 +73,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_SEARCHING(c); cancel_eh eh(mk_c(c)->get_smt_kernel()); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); flet _model(mk_c(c)->fparams().m_model, true); lbool result; try { @@ -123,7 +123,7 @@ extern "C" { expr * const* _assumptions = to_exprs(assumptions); flet _model(mk_c(c)->fparams().m_model, true); cancel_eh eh(mk_c(c)->get_smt_kernel()); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); lbool result; result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions); if (result != l_false && m) { diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 5bce218e6..911360047 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -410,7 +410,7 @@ extern "C" { to_tactic_ref(t)->updt_params(p); - api::context::set_interruptable(*(mk_c(c)), eh); + api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); scoped_timer timer(timeout, &eh);