From 7844476a7d47e114a3488a0b27e066ead50d1fd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jun 2018 17:04:47 -0700 Subject: [PATCH] fixes to term-graph, add proof-checker routines for PR_BIND, remove orphaned file Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 +- src/ast/proofs/proof_checker.cpp | 13 ++ src/muz/spacer/spacer_util.cpp | 2 +- src/muz/transforms/dl_mk_coi_filter.cpp | 1 - src/qe/qe_term_graph.cpp | 155 ++++++++++++++++++++---- src/qe/qe_term_graph.h | 2 +- src/tactic/extension_model_converter.h | 49 -------- 7 files changed, 153 insertions(+), 79 deletions(-) delete mode 100644 src/tactic/extension_model_converter.h diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d451c2c05..0ea2f3cd5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1122,11 +1122,11 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : nullptr; case OP_DISTINCT: return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); - case PR_BIND: { - ptr_buffer sorts; - for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i])); - return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); - } + case PR_BIND: { + ptr_buffer sorts; + for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i])); + return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); + } default: break; } diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index c98f63d28..b8d7b2b46 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -335,6 +335,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { return false; } case PR_QUANT_INTRO: { + if (match_proof(p, p1) && + match_fact(p, fact) && + match_fact(p1.get(), fml) && + (is_lambda(fact) || is_lambda(fml))) + return true; + if (match_proof(p, p1) && match_fact(p, fact) && match_fact(p1.get(), fml) && @@ -361,6 +367,13 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { UNREACHABLE(); return false; } + case PR_BIND: + // it is a lambda expression returning a proof object. + if (!is_lambda(to_app(p)->get_arg(0))) + return false; + // check that body is a proof object. + return true; + case PR_DISTRIBUTIVITY: { if (match_fact(p, fact) && match_proof(p) && diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 146434c0a..42b40c665 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -690,7 +690,7 @@ namespace { qe::term_graph egraph(out.m()); for (expr* e : v) egraph.add_lit(to_app(e)); tout << "Reduced app:\n" - << mk_pp(egraph.to_app(), out.m()) << "\n";); + << mk_pp(egraph.to_expr(), out.m()) << "\n";); out = mk_and(v); } } diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index e37444c5e..457905a56 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -23,7 +23,6 @@ Author: #include "ast/ast_pp.h" #include "tactic/generic_model_converter.h" #include "ast/ast_util.h" -#include "tactic/extension_model_converter.h" namespace datalog { rule_set * mk_coi_filter::operator()(rule_set const & source) { diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 81729fb37..5cf1206a3 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -200,13 +200,12 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - out << "expr: " << m_expr << " class: "; - term const* r = this; - do { + out << get_id() << ": " << m_expr << " - "; + term const* r = &this->get_next(); + while (r != this) { out << r->get_id() << " "; r = &r->get_next(); } - while (r != this); out << "\n"; return out; } @@ -554,7 +553,7 @@ namespace qe { } } - expr_ref term_graph::to_app() { + expr_ref term_graph::to_expr() { expr_ref_vector lits(m); to_lits(lits); return mk_and(lits); @@ -587,8 +586,15 @@ namespace qe { app* a = ::to_app(e); expr_ref_buffer kids(m); for (term* ch : term::children(t)) { - if (!m_root2rep.find(ch->get_root().get_id(), e)) return nullptr; - kids.push_back(e); + // prefer a node that resembles current child, + // otherwise, pick a root representative, if present. + if (m_term2app.find(ch->get_id(), e)) + kids.push_back(e); + else if (m_root2rep.find(ch->get_root().get_id(), e)) + kids.push_back(e); + else + return nullptr; + TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";); } expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.c_ptr()); m_pinned.push_back(pure); @@ -602,6 +608,12 @@ namespace qe { return m.is_unique_value(t1) && !m.is_unique_value(t2); } + struct term_depth { + bool operator()(term const* t1, term const* t2) const { + return get_depth(t1->get_expr()) < get_depth(t2->get_expr()); + } + }; + void purify() { // - propagate representatives up over parents. // use work-list + marking to propagate. @@ -615,10 +627,12 @@ namespace qe { worklist.push_back(t); t->set_mark(true); } + // traverse worklist in order of depth. + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); - while (!worklist.empty()) { - term* t = worklist.back(); - worklist.pop_back(); + for (unsigned i = 0; i < worklist.size(); ++i) { + term* t = worklist[i]; t->set_mark(false); if (m_term2app.contains(t->get_id())) continue; @@ -629,8 +643,8 @@ namespace qe { if (!pure) continue; m_term2app.insert(t->get_id(), pure); - expr* rep = nullptr; - // ensure that the root has a representative + TRACE("qe_verbose", tout << "purified " << *t << " " << mk_pp(pure, m) << "\n";); + expr* rep = nullptr; // ensure that the root has a representative m_root2rep.find(t->get_root().get_id(), rep); // update rep with pure if it is better @@ -653,7 +667,7 @@ namespace qe { // and can be mined using other means, such as theory // aware core minimization m_tg.reset_marks(); - TRACE("qe", m_tg.display(tout << "after purify\n");); + TRACE("qe", display(tout << "after purify\n");); } void solve_core() { @@ -664,10 +678,11 @@ namespace qe { worklist.push_back(t); t->set_mark(true); } + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); - while (!worklist.empty()) { - term* t = worklist.back(); - worklist.pop_back(); + for (unsigned i = 0; i < worklist.size(); ++i) { + term* t = worklist[i]; t->set_mark(false); if (m_term2app.contains(t->get_id())) continue; @@ -695,11 +710,16 @@ namespace qe { } bool find_app(term &t, expr *&res) { - return m_root2rep.find(t.get_root().get_id(), res); + return + m_term2app.find(t.get_id(), res) || + m_root2rep.find(t.get_root().get_id(), res); } bool find_app(expr *lit, expr *&res) { - return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res); + term const* t = m_tg.get_term(lit); + return + m_term2app.find(t->get_id(), res) || + m_root2rep.find(t->get_root().get_id(), res); } void mk_lits(expr_ref_vector &res) { @@ -711,6 +731,90 @@ namespace qe { TRACE("qe", tout << "literals: " << res << "\n";); } + void lits2pure(expr_ref_vector& res) { + expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr; + for (auto *lit : m_tg.m_lits) { + if (m.is_eq(lit, e1, e2)) { + if (find_app(e1, p1) && find_app(e2, p2)) { + if (p1 != p2) + res.push_back(m.mk_eq(p1, p2)); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + else if (m.is_distinct(lit)) { + ptr_buffer diff; + for (expr* arg : *to_app(lit)) { + if (find_app(arg, p1)) { + diff.push_back(p1); + } + } + if (diff.size() > 1) { + res.push_back(m.mk_distinct(diff.size(), diff.c_ptr())); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + else if (find_app(lit, p1)) { + res.push_back(p1); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + TRACE("qe", tout << "literals: " << res << "\n";); + } + + void mk_distinct(expr_ref_vector& res) { + vector> decl2terms; // terms that use function f + ptr_vector decls; + decl2terms.reset(); + // Collect the projected function symbols. + for (term *t : m_tg.m_terms) { + expr* e = t->get_expr(); + if (!is_app(e)) continue; + if (!is_projected(*t)) continue; + app* a = to_app(e); + func_decl* d = a->get_decl(); + if (d->get_arity() == 0) continue; + unsigned id = d->get_decl_id(); + decl2terms.reserve(id+1); + if (decl2terms[id].empty()) decls.push_back(d); + decl2terms[id].push_back(t); + } + + // + // for each projected function that occurs + // (may occur) in multiple congruence classes, + // produce assertions that non-congruent arguments + // are forced distinct. + // + for (func_decl* d : decls) { + unsigned id = d->get_decl_id(); + ptr_vector const& terms = decl2terms[id]; + if (terms.size() <= 1) continue; + unsigned arity = d->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + obj_hashtable roots; + for (term* t : terms) { + expr* arg = to_app(t->get_expr())->get_arg(i); + term const& root = m_tg.get_term(arg)->get_root(); + roots.insert(root.get_expr()); + } + if (roots.size() > 1) { + ptr_buffer args; + for (expr* r : roots) { + args.push_back(r); + } + res.push_back(m.mk_distinct(args.size(), args.c_ptr())); + } + } + } + TRACE("qe", tout << res << "\n";); + } + void mk_pure_equalities(const term &t, expr_ref_vector &res) { SASSERT(t.is_root()); expr *rep = nullptr; @@ -830,7 +934,15 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - + m_tg.display(out); + out << "term2app:\n"; + for (auto const& kv : m_term2app) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } + out << "root2rep:\n"; + for (auto const& kv : m_root2rep) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } return out; } @@ -849,9 +961,8 @@ namespace qe { expr_ref_vector project() { expr_ref_vector res(m); purify(); - mk_lits(res); - mk_pure_equalities(res); - model_complete(res); + lits2pure(res); + mk_distinct(res); reset(); return res; } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 19b694a76..2ab234a96 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -102,7 +102,7 @@ namespace qe { // deprecate? void to_lits(expr_ref_vector &lits, bool all_equalities = false); - expr_ref to_app(); + expr_ref to_expr(); /** * Return literals obtained by projecting added literals diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h deleted file mode 100644 index 0816fdd8b..000000000 --- a/src/tactic/extension_model_converter.h +++ /dev/null @@ -1,49 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - extension_model_converter.h - -Abstract: - - Model converter that introduces new interpretations into a model. - It used to be called elim_var_model_converter - -Author: - - Leonardo (leonardo) 2011-10-21 - -Notes: - ---*/ -#ifndef EXTENSION_MODEL_CONVERTER_H_ -#define EXTENSION_MODEL_CONVERTER_H_ - -#include "ast/ast.h" -#include "tactic/model_converter.h" - - -class extension_model_converter : public model_converter { - func_decl_ref_vector m_vars; - expr_ref_vector m_defs; -public: - extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) { - } - - ~extension_model_converter() override; - - ast_manager & m() const { return m_vars.get_manager(); } - - void operator()(model_ref & md) override; - - void display(std::ostream & out) override; - - // register a variable that was eliminated - void insert(func_decl * v, expr * def); - - model_converter * translate(ast_translation & translator) override; -}; - - -#endif