diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 3a2f6fc85..534e3740b 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -32,6 +32,7 @@ Notes: #include "util/gparams.h" #include "qe/qe_mbp.h" #include "qe/qe_mbi.h" +#include "qe/qe_term_graph.h" BINARY_SYM_CMD(get_quantifier_body_cmd, @@ -440,6 +441,42 @@ public: }; +class euf_project_cmd : public cmd { + unsigned m_arg_index; + ptr_vector m_lits; + ptr_vector m_vars; +public: + euf_project_cmd():cmd("euf-project") {} + char const * get_usage() const override { return "(exprs) (vars)"; } + char const * get_descr(cmd_context & ctx) const override { return "perform congruence projection"; } + unsigned get_arity() const override { return 2; } + cmd_arg_kind next_arg_kind(cmd_context& ctx) const override { + if (m_arg_index == 0) return CPK_EXPR_LIST; + return CPK_FUNC_DECL_LIST; + } + void set_next_arg(cmd_context& ctx, unsigned num, expr * const* args) override { + m_lits.append(num, args); + m_arg_index = 1; + } + void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * ts) override { + m_vars.append(num, ts); + } + void prepare(cmd_context & ctx) override { m_arg_index = 0; m_lits.reset(); m_vars.reset(); } + void execute(cmd_context & ctx) override { + ast_manager& m = ctx.m(); + func_decl_ref_vector vars(m); + expr_ref_vector lits(m); + for (func_decl* v : m_vars) vars.push_back(v); + for (expr* e : m_lits) lits.push_back(e); + qe::term_graph tg(m); + tg.add_lits(lits); + expr_ref_vector p = tg.project(vars, false); + ctx.regular_stream() << p << "\n"; + } + +}; + + void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(print_dimacs_cmd)); ctx.insert(alloc(get_quantifier_body_cmd)); diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 5ef543868..03d2f082e 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -365,10 +365,12 @@ term *term_graph::mk_term(expr *a) { return t; } -term *term_graph::internalize_term(expr *t) { +term* term_graph::internalize_term(expr *t) { + + term* res = get_term(t); + if (res) return res; ptr_buffer todo; todo.push_back(t); - term* res = nullptr; while (!todo.empty()) { term* res = get_term(t); if (res) { @@ -390,9 +392,7 @@ term *term_graph::internalize_term(expr *t) { } void term_graph::internalize_eq(expr *a1, expr* a2) { - internalize_term(a1); - internalize_term(a2); - merge(get_term(a1)->get_root(), get_term(a2)->get_root()); + merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root()); } void term_graph::internalize_lit(expr* lit) { @@ -600,9 +600,25 @@ void term_graph::reset() { m_lits.reset(); } +expr_ref term_graph::mk_pure(term& t) { + expr* e = t.get_app(); + if (m_term2app.find(t.get_id(), e)) return expr_ref(e, m); + if (!is_app(e)) return expr_ref(m); + app* a = ::to_app(e); + expr_ref_vector kids(m); + for (term* ch : term::children(t)) { + if (!ch->get_root().is_marked()) return expr_ref(m); + kids.push_back(mk_pure(ch->get_root())); + } + expr_ref result(m.mk_app(a->get_decl(), kids.size(), kids.c_ptr()), m); + m_pinned.push_back(result); + m_term2app.insert(t.get_id(), result); + return result; +} + expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { - uint_set _decls; - for (func_decl* f : decls) _decls.insert(f->get_id()); + u_map _decls; + for (func_decl* f : decls) _decls.insert(f->get_id(), true); // . propagate representatives up over parents. // use work-list + marking to propagate. // . produce equalities over represented classes. @@ -632,7 +648,8 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl // make this the new root. term* r = t; do { - r->set_root(*t); + r->set_root(*t); // TBD: invalidates hash-table, only one-shot + // TBD: optimize worklist traversal? for (term* p : term::parents(r)) { worklist.push_back(p); } @@ -641,12 +658,47 @@ expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool excl while (t != r); t->set_mark(true); } - // Now, marked roots in m_terms can be used in projection - + // marked roots in m_terms can be used in projection + // walk each root. Then traverse each term in the equivalence class + // create pure variant of the terms (if possible) + // equate t0 (that comes from the root, which can be purified) + // with any other t1. expr_ref_vector result(m); - + m_term2app.reset(); + m_pinned.reset(); + for (term * t : m_terms) { + if (!t->is_root() || !t->is_marked() || t->get_class_size() == 1) continue; + term* r = t; + expr_ref t0 = mk_pure(*t); + SASSERT(t0); + obj_hashtable roots; + roots.insert(t0); + for (term* r = &t->get_next(); r != t; r = &r->get_next()) { + // main symbol of term must be consistent with what is included/excluded + if (exclude != _decls.contains(r->get_decl_id())) { + continue; + } + expr_ref t1 = mk_pure(*r); + if (t1 && !roots.contains(t1)) { + result.push_back(m.mk_eq(t0, t1)); + roots.insert(t1); + } + } + } + // walk disequalities and expose projected disequality + for (expr* e : m_lits) { + expr* e1 = nullptr, *e2 = nullptr; + if (m.is_not(e, e) && m.is_eq(e, e1, e2)) { + expr_ref t1 = mk_pure(*get_term(e1)); + expr_ref t2 = mk_pure(*get_term(e2)); + if (t1 && t2) { + result.push_back(m.mk_not(m.mk_eq(t1, t2))); + } + } + } reset_marks(); - NOT_IMPLEMENTED_YET(); + m_term2app.reset(); + m_pinned.reset(); return result; } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 5319c410a..8e8f54c8c 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -67,12 +67,13 @@ namespace qe { expr* mk_app_core(expr* a); expr_ref mk_app(term const &t); + expr_ref mk_pure(term& t); expr_ref mk_app(expr *a); void mk_equalities(term const &t, app_ref_vector &out); void mk_all_equalities(term const &t, app_ref_vector &out); void display(std::ostream &out); public: - term_graph(ast_manager &man); + term_graph(ast_manager &m); ~term_graph(); ast_manager& get_ast_manager() const { return m;}