From d94f1b3fd634a3dd4c2c9edfba4b93a8cbd4e098 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 10:50:03 -0700 Subject: [PATCH 1/7] add normalizer of monomial coefficients Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_util.cpp | 149 ++++++++++++++++++++++++++++++++++++ src/muz_qe/pdr_util.h | 11 +++ src/test/arith_rewriter.cpp | 42 ++++++++++ 3 files changed, 202 insertions(+) diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 9711cffc2..169eeec72 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -42,6 +42,10 @@ Notes: #include "arith_decl_plugin.h" #include "expr_replacer.h" #include "model_smt2_pp.h" +#include "poly_rewriter.h" +#include "poly_rewriter_def.h" +#include "arith_rewriter.h" + namespace pdr { @@ -1278,6 +1282,151 @@ namespace pdr { return test.is_dl(); } + class arith_normalizer : public poly_rewriter { + ast_manager& m; + arith_util m_util; + enum op_kind { LE, GE, EQ }; + public: + arith_normalizer(ast_manager& m, params_ref const& p = params_ref()): poly_rewriter(m, p), m(m), m_util(m) {} + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + br_status st = BR_FAILED; + if (m.is_eq(f)) { + SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result); + } + + if (f->get_family_id() != get_fid()) { + return st; + } + switch (f->get_decl_kind()) { + case OP_NUM: st = BR_FAILED; break; + case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break; + case OP_LE: SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break; + case OP_GE: SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break; + case OP_LT: SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break; + case OP_GT: SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break; + default: st = BR_FAILED; break; + } + return st; + } + + private: + + br_status mk_eq_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, EQ, result); + } + br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, LE, result); + } + br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, GE, result); + } + br_status mk_lt_core(expr* arg1, expr* arg2, expr_ref& result) { + result = m.mk_not(m_util.mk_ge(arg1, arg2)); + return BR_REWRITE2; + } + br_status mk_gt_core(expr* arg1, expr* arg2, expr_ref& result) { + result = m.mk_not(m_util.mk_le(arg1, arg2)); + return BR_REWRITE2; + } + + br_status mk_le_ge_eq_core(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) { + if (m_util.is_real(arg1)) { + numeral g(0); + get_coeffs(arg1, g); + get_coeffs(arg2, g); + if (!g.is_one() && !g.is_zero()) { + SASSERT(g.is_pos()); + expr_ref new_arg1 = rdiv_polynomial(arg1, g); + expr_ref new_arg2 = rdiv_polynomial(arg2, g); + switch(kind) { + case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE; + case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE; + case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE; + } + } + } + return BR_FAILED; + } + + void update_coeff(numeral const& r, numeral& g) { + if (g.is_zero() || abs(r) < g) { + g = abs(r); + } + } + + void get_coeffs(expr* e, numeral& g) { + rational r; + unsigned sz; + expr* const* args = get_monomials(e, sz); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = args[i]; + if (!m_util.is_numeral(arg, r)) { + get_power_product(arg, r); + } + update_coeff(r, g); + } + } + + expr_ref rdiv_polynomial(expr* e, numeral const& g) { + rational r; + SASSERT(g.is_pos()); + SASSERT(!g.is_one()); + expr_ref_vector monomes(m); + unsigned sz; + expr* const* args = get_monomials(e, sz); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = args[i]; + if (m_util.is_numeral(arg, r)) { + monomes.push_back(m_util.mk_numeral(r/g, false)); + } + else { + expr* p = get_power_product(arg, r); + r /= g; + if (r.is_one()) { + monomes.push_back(p); + } + else { + monomes.push_back(m_util.mk_mul(m_util.mk_numeral(r, false), p)); + } + } + } + expr_ref result(m); + mk_add(monomes.size(), monomes.c_ptr(), result); + return result; + } + + }; + + + struct arith_normalizer_cfg: public default_rewriter_cfg { + arith_normalizer m_r; + bool rewrite_patterns() const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + return m_r.mk_app_core(f, num, args, result); + } + arith_normalizer_cfg(ast_manager & m, params_ref const & p):m_r(m,p) {} + }; + + class arith_normalizer_star : public rewriter_tpl { + arith_normalizer_cfg m_cfg; + public: + arith_normalizer_star(ast_manager & m, params_ref const & p): + rewriter_tpl(m, false, m_cfg), + m_cfg(m, p) {} + }; + + + void normalize_arithmetic(expr_ref& t) { + ast_manager& m = t.get_manager(); + datalog::scoped_no_proof _sp(m); + params_ref p; + arith_normalizer_star rw(m, p); + expr_ref tmp(m); + rw(t, tmp); + t = tmp; + } + } template class rewriter_tpl; diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index 5f2d22b76..67be6751b 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -142,6 +142,7 @@ namespace pdr { Assumption: the model satisfies the conjunctions. */ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); + /** @@ -149,6 +150,16 @@ namespace pdr { */ void hoist_non_bool_if(expr_ref& fml); + + /** + \brief normalize coefficients in polynomials so that least coefficient is 1. + */ + void normalize_arithmetic(expr_ref& t); + + + /** + \brief determine if formulas belong to difference logic or UTVPI fragment. + */ bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp index 0933e9d11..9eb9e559b 100644 --- a/src/test/arith_rewriter.cpp +++ b/src/test/arith_rewriter.cpp @@ -2,6 +2,33 @@ #include "bv_decl_plugin.h" #include "ast_pp.h" #include "reg_decl_plugins.h" +#include "th_rewriter.h" +#include "model.h" +#include "pdr_util.h" +#include "smt2parser.h" + + +static expr_ref parse_fml(ast_manager& m, char const* str) { + expr_ref result(m); + cmd_context ctx(false, &m); + ctx.set_ignore_check(true); + std::ostringstream buffer; + buffer << "(declare-const x Real)\n" + << "(declare-const y Real)\n" + << "(declare-const z Real)\n" + << "(declare-const a Real)\n" + << "(declare-const b Real)\n" + << "(assert " << str << ")\n"; + std::istringstream is(buffer.str()); + VERIFY(parse_smt2_commands(ctx, is)); + SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + result = *ctx.begin_assertions(); + return result; +} + +static char const* example1 = "(<= (+ (* 1.3 x y) (* 2.3 y y) (* (- 1.1 x x))) 2.2)"; +static char const* example2 = "(= (+ 4 3 (- (* 3 x x) (* 5 y)) y) 0)"; + void tst_arith_rewriter() { ast_manager m; @@ -14,4 +41,19 @@ void tst_arith_rewriter() { expr* args[2] = { t1, t2 }; ar.mk_mul(2, args, result); std::cout << mk_pp(result, m) << "\n"; + + + th_rewriter rw(m); + expr_ref fml = parse_fml(m, example1); + rw(fml); + std::cout << mk_pp(fml, m) << "\n"; + pdr::normalize_arithmetic(fml); + std::cout << mk_pp(fml, m) << "\n"; + + + fml = parse_fml(m, example2); + rw(fml); + std::cout << mk_pp(fml, m) << "\n"; + pdr::normalize_arithmetic(fml); + std::cout << mk_pp(fml, m) << "\n"; } From e7f458101c5ccfc5bb64449cc5eb928bd3cc6674 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 10:53:46 -0700 Subject: [PATCH 2/7] add normalizer of monomial coefficients Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_util.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 169eeec72..3d93f8104 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -1430,6 +1430,6 @@ namespace pdr { } template class rewriter_tpl; - +template class rewriter_tpl; From a20656de35f664b922c1f5f47212656abeec03b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 10:57:25 -0700 Subject: [PATCH 3/7] fix unused variable warning in unit test Signed-off-by: Nikolaj Bjorner --- src/test/polynorm.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 9853181ca..092ac022a 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -109,10 +109,12 @@ void tst_polynorm() { reg_decl_plugins(m); expr_ref fml(m); - fml = parse_fml(m, example2); - + fml = parse_fml(m, example1); std::cout << mk_pp(fml, m) << "\n"; + nf(fml); + fml = parse_fml(m, example2); + std::cout << mk_pp(fml, m) << "\n"; nf(fml); From 1c3f715e26ad80346e9ce4128e042d27279f05e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 12:21:49 -0700 Subject: [PATCH 4/7] switch between convex and interior hull, add multiple cores Signed-off-by: Nikolaj Bjorner --- src/muz_qe/fixedpoint_params.pyg | 3 +- src/muz_qe/pdr_context.cpp | 11 +++-- src/muz_qe/pdr_generalizers.cpp | 80 +++++++++++++++++++++++++------- src/muz_qe/pdr_generalizers.h | 8 +++- 4 files changed, 80 insertions(+), 22 deletions(-) diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index 860dcb68e..555c44df2 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -49,7 +49,8 @@ def_module_params('fixedpoint', ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"), - ('use_convex_hull_generalizer', BOOL, False, "PDR: generalize using convex hulls of lemmas"), + ('use_convex_closure_generalizer', BOOL, False, "PDR: generalize using convex closures of lemmas"), + ('use_convex_interior_generalizer', BOOL, False, "PDR: generalize using convex interiors of lemmas"), ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"), ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when " "checking for reachability (not only during cube weakening)"), diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 0121e49b8..fd86a4402 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1578,7 +1578,9 @@ namespace pdr { m_fparams.m_arith_auto_config_simplex = true; m_fparams.m_arith_propagate_eqs = false; m_fparams.m_arith_eager_eq_axioms = false; - if (m_params.use_utvpi() && !m_params.use_convex_hull_generalizer()) { + if (m_params.use_utvpi() && + !m_params.use_convex_closure_generalizer() && + !m_params.use_convex_interior_generalizer()) { if (classify.is_dl()) { m_fparams.m_arith_mode = AS_DIFF_LOGIC; m_fparams.m_arith_expand_eqs = true; @@ -1590,8 +1592,11 @@ namespace pdr { } } } - if (m_params.use_convex_hull_generalizer()) { - m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this)); + if (m_params.use_convex_closure_generalizer()) { + m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, true)); + } + if (m_params.use_convex_interior_generalizer()) { + m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, false)); } if (!use_mc && m_params.use_inductive_generalizer()) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index c094b6c7f..2c49917be 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -147,18 +147,23 @@ namespace pdr { } - core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx): + core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx, bool is_closure): core_generalizer(ctx), m(ctx.get_manager()), a(m), m_sigma(m), - m_trail(m) { + m_trail(m), + m_is_closure(is_closure) { m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); } + void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { + method1(n, core, uses_level, new_cores); + } + void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { - method1(n, core, uses_level); + UNREACHABLE(); } // use the entire region as starting point for generalization. @@ -174,20 +179,27 @@ namespace pdr { // If Constraints & Transition(y0, y) is unsat, then // update with new core. // - void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector& core, bool& uses_level) { + void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { manager& pm = n.pt().get_pdr_manager(); expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m); if (core.empty()) { return; } + new_cores.push_back(std::make_pair(core, uses_level)); add_variables(n, eqs); if (!mk_convex(core, 0, conv1)) { IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";); return; } conv1.append(eqs); - conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); - conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + if (m_is_closure) { + conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + } + else { + conv1.push_back(a.mk_ge(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(a.mk_ge(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + } conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get()))); expr_ref fml = n.pt().get_formulas(n.level(), false); expr_ref_vector fmls(m); @@ -202,22 +214,23 @@ namespace pdr { } conv2.append(conv1); expr_ref state = pm.mk_and(conv2); - TRACE("pdr", tout << "Check:\n" << mk_pp(state, m) << "\n"; - tout << "New formula:\n" << mk_pp(pm.mk_and(core), m) << "\n"; - tout << "Old formula:\n" << mk_pp(fml, m) << "\n"; - + TRACE("pdr", + tout << "Check states:\n" << mk_pp(state, m) << "\n"; + tout << "Old states:\n" << mk_pp(fml, m) << "\n"; ); model_node nd(0, state, n.pt(), n.level()); pred_transformer::scoped_farkas sf(n.pt(), true); - if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) { + bool uses_level1 = uses_level; + if (l_false == n.pt().is_reachable(nd, &conv2, uses_level1)) { + new_cores.push_back(std::make_pair(conv2, uses_level1)); + + expr_ref state1 = pm.mk_and(conv2); TRACE("pdr", tout << mk_pp(state, m) << "\n"; - tout << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); + tout << "Generalized to:\n" << mk_pp(state1, m) << "\n";); IF_VERBOSE(0, verbose_stream() << mk_pp(state, m) << "\n"; - verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); - core.reset(); - core.append(conv2); + verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";); } } } @@ -317,12 +330,47 @@ namespace pdr { } } + expr_ref core_convex_hull_generalizer::mk_closure(expr* e) { + expr* e0, *e1, *e2; + expr_ref result(m); + if (a.is_lt(e, e1, e2)) { + result = a.mk_le(e1, e2); + } + else if (a.is_gt(e, e1, e2)) { + result = a.mk_ge(e1, e2); + } + else if (m.is_not(e, e0) && a.is_ge(e0, e1, e2)) { + result = a.mk_le(e1, e2); + } + else if (m.is_not(e, e0) && a.is_le(e0, e1, e2)) { + result = a.mk_ge(e1, e2); + } + else if (a.is_ge(e) || a.is_le(e) || m.is_eq(e) || + (m.is_not(e, e0) && (a.is_gt(e0) || a.is_lt(e0)))) { + result = e; + } + else { + IF_VERBOSE(1, verbose_stream() << "Cannot close: " << mk_pp(e, m) << "\n";); + } + return result; + } + + bool core_convex_hull_generalizer::mk_closure(expr_ref_vector& conj) { + for (unsigned i = 0; i < conj.size(); ++i) { + conj[i] = mk_closure(conj[i].get()); + if (!conj[i].get()) { + return false; + } + } + return true; + } + bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) { conv.reset(); for (unsigned i = 0; i < core.size(); ++i) { mk_convex(core[i], index, conv); } - return !conv.empty(); + return !conv.empty() && mk_closure(conv); } void core_convex_hull_generalizer::mk_convex(expr* fml, unsigned index, expr_ref_vector& conv) { diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 0aee94c16..ece1f51f1 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -81,16 +81,20 @@ namespace pdr { obj_map m_left; obj_map m_right; obj_map m_models; + bool m_is_closure; + expr_ref mk_closure(expr* e); + bool mk_closure(expr_ref_vector& conj); bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv); void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv); bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result); bool translate(func_decl* fn, unsigned index, expr_ref& result); - void method1(model_node& n, expr_ref_vector& core, bool& uses_level); + void method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); void method2(model_node& n, expr_ref_vector& core, bool& uses_level); void add_variables(model_node& n, expr_ref_vector& eqs); public: - core_convex_hull_generalizer(context& ctx); + core_convex_hull_generalizer(context& ctx, bool is_closure); virtual ~core_convex_hull_generalizer() {} + virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); }; From 0f83e7a251a4d1f094d3abba2c76e6c7512e032f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Aug 2013 12:23:34 -0700 Subject: [PATCH 5/7] fix bug masked by default configuration Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index bce59657a..d08e6f13a 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -118,7 +118,7 @@ public: void mk_eq(expr * arg1, expr * arg2, expr_ref & result) { if (mk_eq_core(arg1, arg2, result) == BR_FAILED) - result = m_util.mk_le(arg1, arg2); + result = m_util.mk_eq(arg1, arg2); } void mk_le(expr * arg1, expr * arg2, expr_ref & result) { if (mk_le_core(arg1, arg2, result) == BR_FAILED) From 6a820adfed83a4db4cc520f877deec4d73c8dfc9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Aug 2013 09:43:17 -0700 Subject: [PATCH 6/7] fix logic for adding cores Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_generalizers.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 2c49917be..bf1693ce3 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -182,12 +182,14 @@ namespace pdr { void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) { manager& pm = n.pt().get_pdr_manager(); expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m); + unsigned orig_size = new_cores.size(); if (core.empty()) { + new_cores.push_back(std::make_pair(core, uses_level)); return; } - new_cores.push_back(std::make_pair(core, uses_level)); add_variables(n, eqs); if (!mk_convex(core, 0, conv1)) { + new_cores.push_back(std::make_pair(core, uses_level)); IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";); return; } @@ -233,6 +235,10 @@ namespace pdr { verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";); } } + if (!m_is_closure || new_cores.empty()) { + new_cores.push_back(std::make_pair(core, uses_level)); + } + } // take as starting point two points from different regions. From 661fe7eec9b4db7f86681953248a242d24754992 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Aug 2013 19:10:46 -0700 Subject: [PATCH 7/7] add missing detach in coi_filter Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_coi_filter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp index 7bbb14353..a0fc845bf 100644 --- a/src/muz_qe/dl_mk_coi_filter.cpp +++ b/src/muz_qe/dl_mk_coi_filter.cpp @@ -42,7 +42,7 @@ namespace datalog { scoped_ptr result1 = top_down(source); scoped_ptr result2 = bottom_up(result1?*result1:source); if (!result2) { - result2 = result1; + result2 = result1.detach(); } return result2.detach(); }