diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index 25e513b78..c2cfadd14 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -44,6 +44,7 @@ def_module_params('fixedpoint', ('coalesce_rules', BOOL, False, "BMC: coalesce rules"), ('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"), ('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 47655ac7b..73bffd4e4 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1477,6 +1477,10 @@ namespace pdr { if (m_params.inductive_reachability_check()) { m_core_generalizers.push_back(alloc(core_induction_generalizer, *this)); } + if (m_params.use_arith_inductive_generalizer()) { + m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this)); + } + } void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector& rs) const { diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 5a6ab4240..a02a1cb6e 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -28,7 +28,9 @@ Revision History: namespace pdr { - // + // ------------------------ + // core_bool_inductive_generalizer + // main propositional induction generalizer. // drop literals one by one from the core and check if the core is still inductive. // @@ -97,6 +99,9 @@ namespace pdr { } } + // ------------------------ + // core_farkas_generalizer + // // for each disjunct of core: // weaken predecessor. @@ -142,6 +147,158 @@ namespace pdr { } + // ----------------------------- + // core_arith_inductive_generalizer + + core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx): + core_generalizer(ctx), + m(ctx.get_manager()), + a(m), + m_refs(m) {} + + void core_arith_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { + if (core.size() <= 1) { + return; + } + reset(); + expr_ref e(m), t1(m), t2(m), t3(m); + rational r; + + TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; }); + + svector eqs; + get_eqs(core, eqs); + + for (unsigned eq = 0; eq < eqs.size(); ++eq) { + rational r = eqs[eq].m_value; + expr* x = eqs[eq].m_term; + unsigned k = eqs[eq].m_i; + unsigned l = eqs[eq].m_j; + + expr_ref_vector new_core(m); + for (unsigned i = 0; i < core.size(); ++i) { + if (i == k || k == l) { + new_core.push_back(m.mk_true()); + } + else { + if (!substitute_alias(r, x, core[i].get(), e)) { + e = core[i].get(); + } + new_core.push_back(e); + } + } + if (abs(r) >= rational(2) && a.is_int(x)) { + new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true)); + new_core[l] = a.mk_ge(x, a.mk_numeral(r, true)); + } + + bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level); + + IF_VERBOSE(1, + verbose_stream() << (inductive?"":"non") << "inductive\n"; + for (unsigned j = 0; j < new_core.size(); ++j) { + verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; + }); + + if (inductive) { + core.reset(); + core.append(new_core); + } + } + } + + void core_arith_inductive_generalizer::insert_bound(bool is_lower, expr* x, rational const& r, unsigned i) { + if (r.is_neg()) { + expr_ref e(m); + e = a.mk_uminus(x); + m_refs.push_back(e); + x = e; + is_lower = !is_lower; + } + + if (is_lower) { + m_lb.insert(abs(r), std::make_pair(x, i)); + } + else { + m_ub.insert(abs(r), std::make_pair(x, i)); + } + } + + void core_arith_inductive_generalizer::reset() { + m_refs.reset(); + m_lb.reset(); + m_ub.reset(); + } + + void core_arith_inductive_generalizer::get_eqs(expr_ref_vector const& core, svector& eqs) { + expr* e1, *x, *y; + expr_ref e(m); + rational r; + + for (unsigned i = 0; i < core.size(); ++i) { + e = core[i]; + if (m.is_not(e, e1) && a.is_le(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { + // not (<= x r) <=> x >= r + 1 + insert_bound(true, x, r + rational(1), i); + } + else if (m.is_not(e, e1) && a.is_ge(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) { + // not (>= x r) <=> x <= r - 1 + insert_bound(false, x, r - rational(1), i); + } + else if (a.is_le(e, x, y) && a.is_numeral(y, r)) { + insert_bound(false, x, r, i); + } + else if (a.is_ge(e, x, y) && a.is_numeral(y, r)) { + insert_bound(true, x, r, i); + } + } + bounds_t::iterator it = m_lb.begin(), end = m_lb.end(); + for (; it != end; ++it) { + rational r = it->m_key; + vector & terms1 = it->m_value; + vector terms2; + if (r >= rational(2) && m_ub.find(r, terms2)) { + bool done = false; + for (unsigned i = 0; !done && i < terms1.size(); ++i) { + for (unsigned j = 0; !done && j < terms2.size(); ++j) { + expr* t1 = terms1[i].first; + expr* t2 = terms2[j].first; + if (t1 == t2) { + eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); + done = true; + } + else { + e = m.mk_eq(t1, t2); + th_rewriter rw(m); + rw(e); + if (m.is_true(e)) { + eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second)); + done = true; + } + } + } + } + } + } + } + + bool core_arith_inductive_generalizer::substitute_alias(rational const& r, expr* x, expr* e, expr_ref& result) { + rational r2; + expr* y, *z, *e1; + if (m.is_not(e, e1) && substitute_alias(r, x, e1, result)) { + result = m.mk_not(result); + return true; + } + if (a.is_le(e, y, z) && a.is_numeral(z, r2) && r == r2) { + result = a.mk_le(y, x); + return true; + } + if (a.is_ge(e, y, z) && a.is_numeral(z, r2) && r == r2) { + result = a.mk_ge(y, x); + return true; + } + return false; + } // diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 5f3393682..03bd89c4d 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -33,6 +33,37 @@ namespace pdr { virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); }; + template + class r_map : public map { + }; + + class core_arith_inductive_generalizer : public core_generalizer { + typedef std::pair term_loc_t; + typedef r_map > bounds_t; + + ast_manager& m; + arith_util a; + expr_ref_vector m_refs; + bounds_t m_lb; + bounds_t m_ub; + + struct eq { + expr* m_term; + rational m_value; + unsigned m_i; + unsigned m_j; + eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {} + }; + void reset(); + void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i); + void get_eqs(expr_ref_vector const& core, svector& eqs); + bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result); + public: + core_arith_inductive_generalizer(context& ctx); + virtual ~core_arith_inductive_generalizer() {} + virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); + }; + class core_farkas_generalizer : public core_generalizer { farkas_learner m_farkas_learner; public: diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index 42d4b4c20..49ae35423 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -88,7 +88,6 @@ namespace pdr { for (unsigned i = 0; i < assumptions.size(); ++i) { pp.add_assumption(assumptions[i].get()); } - pp.display_smt2(tout, m.mk_true()); static unsigned lemma_id = 0; std::ostringstream strm; @@ -97,6 +96,7 @@ namespace pdr { pp.display_smt2(out, m.mk_true()); out.close(); lemma_id++; + tout << "pdr_check: " << strm.str() << "\n"; }); lbool result = m_context.check(assumptions.size(), assumptions.c_ptr()); if (!m.is_true(m_pred)) {