sat.euf add missing function

Z3Prover · Jul 23, 2021 · 32beb91 · 32beb91
1 parent 800fef6
commit 32beb91
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
@@ -129,7 +129,7 @@ namespace euf {
         return n;
     }
 
-    egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) {
+    egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m) {
         m_tmp_eq = enode::mk_tmp(m_region, 2);
     }
 
@@ -418,12 +418,10 @@ namespace euf {
             std::swap(n1, n2);
         }
         if (m.is_false(r2->get_expr()) && r1->value() == l_true) {
-            std::cout << "value assign conflict\n";
             set_conflict(n1, n2, j);
             return;
         }
         if (m.is_true(r2->get_expr()) && r1->value() == l_false) {
-            std::cout << "value assign conflict\n";
             set_conflict(n1, n2, j);
             return;
         }
@@ -604,6 +602,12 @@ namespace euf {
         return false;
     }
 
+    enode* egraph::get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args) {
+        m_tmp_app.set_decl(f);
+        m_tmp_app.set_num_args(num_args);
+        return find(m_tmp_app.get_app(), num_args, args);
+    }
+
     /**
        \brief generate an explanation for a congruence.
        Each pair of children under a congruence have the same roots

diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
@@ -159,6 +159,7 @@ namespace euf {
         enode*                 m_tmp_eq = nullptr;
         enode*                 m_tmp_node = nullptr;
         unsigned               m_tmp_node_capacity = 0;
+        tmp_app                m_tmp_app;
         enode_vector           m_nodes;
         expr_ref_vector        m_exprs;
         vector<enode_vector>   m_decl2enodes;
@@ -261,7 +262,7 @@ namespace euf {
         */
         bool are_diseq(enode* a, enode* b) const;
 
-        enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { UNREACHABLE(); return nullptr; }
+        enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args);
 
         /**
            \brief Maintain and update cursor into propagated consequences.