prepare term-graph unit testing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<expr>      m_lits;
+    ptr_vector<func_decl> 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));

src/qe/qe_term_graph.cpp

@@ -366,9 +366,11 @@ term *term_graph::mk_term(expr *a) {
 }
 
 term* term_graph::internalize_term(expr *t) {
+    
+    term* res = get_term(t);
+    if (res) return res;
     ptr_buffer<expr> 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);
+    merge(internalize_term(a1)->get_root(), internalize_term(a2)->get_root());
-    internalize_term(a2);
-    merge(get_term(a1)->get_root(), get_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;
+    u_map<bool> _decls;
-    for (func_decl* f : decls) _decls.insert(f->get_id());
+    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<expr> 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;
 }
 

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;}