From 657ed4db7a4d390ca7061955cc1f8eaaf4855b0e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Jan 2021 07:19:57 -0800
Subject: [PATCH] fix relevancy bug for recfun

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/euf/euf_egraph.cpp | 5 ++++-
 src/ast/euf/euf_egraph.h   | 2 ++
 src/sat/smt/q_ematch.cpp   | 6 +++++-
 src/smt/theory_recfun.cpp  | 3 +++
 src/util/zstring.cpp       | 2 --
 5 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 3bb35320b..eb393188c 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -106,10 +106,13 @@ namespace euf {
         SASSERT(!find(f));
         force_push();
         enode *n = mk_enode(f, generation, num_args, args);
+        
         SASSERT(n->class_size() == 1);        
         if (num_args == 0 && m.is_unique_value(f))
             n->mark_interpreted();
-        if (num_args == 0) 
+        if (m_on_make)
+            m_on_make(n);
+        if (num_args == 0)             
             return n;
         if (m.is_eq(f)) {
             n->set_is_equality();
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index b475600e7..d908baf87 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -168,6 +168,7 @@ namespace euf {
         stats                  m_stats;
         bool                   m_uses_congruence { false };
         std::function<void(enode*,enode*)>     m_on_merge;
+        std::function<void(enode*)>            m_on_make;
         std::function<void(expr*,expr*,expr*)> m_used_eq;
         std::function<void(app*,app*)>         m_used_cc;  
         std::function<void(std::ostream&, void*)>   m_display_justification;
@@ -277,6 +278,7 @@ namespace euf {
         void set_bool_var(enode* n, unsigned v) { n->set_bool_var(v); }
 
         void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge = on_merge; }
+        void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
         void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
         void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
         void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; }
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 143ea7679..bab662b04 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -57,7 +57,12 @@ namespace q {
             [&](euf::enode* root, euf::enode* other) { 
             on_merge(root, other); 
         };
+        std::function<void(euf::enode*)> _on_make = 
+            [&](euf::enode* n) {
+            m_mam->relevant_eh(n, false);
+        };
         ctx.get_egraph().set_on_merge(_on_merge);
+        ctx.get_egraph().set_on_make(_on_make);
         m_mam = mam::mk(ctx, *this);
     }
 
@@ -230,7 +235,6 @@ namespace q {
         m_mam->on_merge(root, other);
         if (m_lazy_mam)
             m_lazy_mam->on_merge(root, other);
-        m_mam->relevant_eh(other, false);
     }
 
     // watch only nodes introduced in bindings or ground arguments of functions
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index d8a1414f1..1348da985 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -296,9 +296,12 @@ namespace smt {
     }
         
     literal theory_recfun::mk_literal(expr* e) {
+        bool is_not = m.is_not(e, e);
         ctx.internalize(e, false);
         literal lit = ctx.get_literal(e);
         ctx.mark_as_relevant(lit);
+        if (is_not)
+            lit.neg();
         return lit;
     }
 
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index 941a05f4a..115643bad 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -16,7 +16,6 @@ Author:
 --*/
 #include "util/gparams.h"
 #include "util/zstring.h"
-#include "util/trace.h"
 
 static bool is_hex_digit(char ch, unsigned& d) {
     if ('0' <= ch && ch <= '9') {
@@ -148,7 +147,6 @@ std::string zstring::encode() const {
         }
     }
     _flush();
-    TRACE("seq", tout << "encode " << strm.str() << "\n";);
     return strm.str();
 }