From 32beb91efac2648afef01084af65a02c9e1d76ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Jul 2021 19:17:17 -0700
Subject: [PATCH] sat.euf add missing function

---
 src/ast/euf/euf_egraph.cpp | 10 +++++++---
 src/ast/euf/euf_egraph.h   |  3 ++-
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 0f82c2e6c06..bbb63540ef9 100644
--- 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
index 9533a83e6e2..1ac54f6f097 100644
--- 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.