diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index c8c1e3b2a..89562fd95 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -33,7 +33,6 @@ Notes: #include "pdr_prop_solver.h" #include "pdr_context.h" #include "pdr_generalizers.h" -#include "datatype_decl_plugin.h" #include "for_each_expr.h" #include "dl_rule_set.h" #include "unit_subsumption_tactic.h" @@ -1682,7 +1681,8 @@ namespace pdr { case l_false: { core_generalizer::cores cores; cores.push_back(std::make_pair(cube, uses_level)); - + TRACE("pdr", tout << "cube:\n"; + for (unsigned j = 0; j < cube.size(); ++j) tout << mk_pp(cube[j].get(), m) << "\n";); for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) { core_generalizer::cores new_cores; for (unsigned j = 0; j < cores.size(); ++j) { diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 06b8f5eeb..b8e043806 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -398,6 +398,11 @@ namespace pdr { for (unsigned i = 0; i < r->size(); ++i) { lemmas.push_back(r->form(i)); } + TRACE("farkas_simplify_lemmas", + tout << "simplified:\n"; + for (unsigned i = 0; i < lemmas.size(); ++i) { + tout << mk_pp(lemmas[i].get(), m) << "\n"; + }); } diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp index 43d75b7bf..daa52992f 100644 --- a/src/muz_qe/pdr_prop_solver.cpp +++ b/src/muz_qe/pdr_prop_solver.cpp @@ -46,7 +46,6 @@ namespace pdr { expr_ref_vector m_assumptions; obj_map m_proxies2expr; obj_map m_expr2proxies; - obj_hashtable m_implies; unsigned m_num_proxies; app * mk_proxy(expr* literal) { @@ -72,7 +71,6 @@ namespace pdr { expr_ref implies(m.mk_or(m.mk_not(res), literal), m); s.m_ctx->assert_expr(implies); m_assumptions.push_back(implies); - m_implies.insert(implies); TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, m) << "\n";); return res; } @@ -92,6 +90,19 @@ namespace pdr { m_assumptions.append(conjs); } + expr* apply_accessor( + ptr_vector const& acc, + unsigned j, + func_decl* f, + expr* c) { + if (is_app(c) && to_app(c)->get_decl() == f) { + return to_app(c)->get_arg(j); + } + else { + return m.mk_app(acc[j], c); + } + } + void expand_literals(expr_ref_vector& conjs) { arith_util arith(m); datatype_util dt(m); @@ -100,6 +111,12 @@ namespace pdr { rational r; unsigned bv_size; + TRACE("pdr", + tout << "begin expand\n"; + for (unsigned i = 0; i < conjs.size(); ++i) { + tout << mk_pp(conjs[i].get(), m) << "\n"; + }); + for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) { @@ -117,10 +134,10 @@ namespace pdr { (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){ func_decl* f = to_app(val)->get_decl(); func_decl* r = dt.get_constructor_recognizer(f); - conjs[i] = m.mk_app(r,c); + conjs[i] = m.mk_app(r, c); ptr_vector const& acc = *dt.get_constructor_accessors(f); - for (unsigned i = 0; i < acc.size(); ++i) { - conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i))); + for (unsigned j = 0; j < acc.size(); ++j) { + conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j))); } } else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || @@ -142,6 +159,11 @@ namespace pdr { } } } + TRACE("pdr", + tout << "end expand\n"; + for (unsigned i = 0; i < conjs.size(); ++i) { + tout << mk_pp(conjs[i].get(), m) << "\n"; + }); } public: @@ -190,12 +212,7 @@ namespace pdr { expr_ref e(m); for (unsigned i = 0; i < es.size(); ++i) { e = es[i].get(); - if (m_implies.contains(e)) { - e = m.mk_true(); - } - else { - rep(e); - } + rep(e); es[i] = e; if (m.is_true(e)) { es[i] = es.back(); diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index ca308954c..42d4b4c20 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -20,6 +20,7 @@ Revision History: #include "pdr_smt_context_manager.h" #include "has_free_vars.h" #include "ast_pp.h" +#include "ast_smt_pp.h" #include #include "smt_params.h" @@ -78,6 +79,25 @@ namespace pdr { if (!m.is_true(m_pred)) { assumptions.push_back(m_pred); } + TRACE("pdr_check", + { + ast_smt_pp pp(m); + for (unsigned i = 0; i < m_context.size(); ++i) { + pp.add_assumption(m_context.get_formulas()[i]); + } + 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; + strm << "pdr-lemma-" << lemma_id << ".smt2"; + std::ofstream out(strm.str().c_str()); + pp.display_smt2(out, m.mk_true()); + out.close(); + lemma_id++; + }); lbool result = m_context.check(assumptions.size(), assumptions.c_ptr()); if (!m.is_true(m_pred)) { assumptions.pop_back(); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 8ecd079bf..d78b82cc6 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -69,10 +69,6 @@ namespace smt { return m_kernel.get_asserted_formulas(); } - bool reduce() { - return m_kernel.reduce_assertions(); - } - void push() { TRACE("smt_kernel", tout << "push()\n";); m_kernel.push(); @@ -221,9 +217,6 @@ namespace smt { return m_imp->get_formulas(); } - bool kernel::reduce() { - return m_imp->reduce(); - } void kernel::push() { m_imp->push(); diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 37b044af1..215f11cbf 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -84,15 +84,6 @@ namespace smt { */ expr * const * get_formulas() const; - /** - \brief Reduce the set of asserted formulas using preprocessors. - Return true if an inconsistency is detected. - - \remark This is mainly used by dl_smt_relation. This method - seens to be misplaced. This is not the right place. - */ - bool reduce(); - /** \brief Create a backtracking point (aka scope level). */