From fc741cf01868e12195ff0749df982fd994be8cc2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Jan 2022 14:23:22 -0800
Subject: [PATCH] rename module

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/CMakeLists.txt                          | 2 +-
 src/sat/smt/array_internalize.cpp                   | 2 +-
 src/sat/smt/{smt_relevant.cpp => euf_relevancy.cpp} | 4 ++--
 src/sat/smt/{smt_relevant.h => euf_relevancy.h}     | 7 +++----
 src/sat/smt/euf_solver.h                            | 6 +++---
 src/sat/smt/q_ematch.cpp                            | 6 +++---
 6 files changed, 13 insertions(+), 14 deletions(-)
 rename src/sat/smt/{smt_relevant.cpp => euf_relevancy.cpp} (99%)
 rename src/sat/smt/{smt_relevant.h => euf_relevancy.h} (99%)

diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt
index 3721963c8..a75c0022d 100644
--- a/src/sat/smt/CMakeLists.txt
+++ b/src/sat/smt/CMakeLists.txt
@@ -21,6 +21,7 @@ z3_add_component(sat_smt
     euf_invariant.cpp
     euf_model.cpp
     euf_proof.cpp
+    euf_relevancy.cpp
     euf_solver.cpp
     fpa_solver.cpp
     pb_card.cpp
@@ -38,7 +39,6 @@ z3_add_component(sat_smt
     q_solver.cpp
     recfun_solver.cpp
     sat_th.cpp
-    smt_relevant.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES
     sat
diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp
index 683cc5d07..5e1a76b9f 100644
--- a/src/sat/smt/array_internalize.cpp
+++ b/src/sat/smt/array_internalize.cpp
@@ -86,7 +86,7 @@ namespace array {
         for (auto* arg : euf::enode_args(n))
             ensure_var(arg);  
         internalize_eh(n);
-        if (ctx.is_relevant(n) || !ctx.relevancy().enabled())
+        if (ctx.is_relevant(n))
             relevant_eh(n);
         return true;
     }
diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/euf_relevancy.cpp
similarity index 99%
rename from src/sat/smt/smt_relevant.cpp
rename to src/sat/smt/euf_relevancy.cpp
index 87a85f61b..869df879e 100644
--- a/src/sat/smt/smt_relevant.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -16,10 +16,10 @@ Author:
 --*/
 #include "sat/sat_solver.h"
 #include "sat/smt/euf_solver.h"
-#include "sat/smt/smt_relevant.h"
+#include "sat/smt/euf_relevancy.h"
 
 
-namespace smt {
+namespace euf {
 
     relevancy::relevancy(euf::solver& ctx): ctx(ctx) {
     }
diff --git a/src/sat/smt/smt_relevant.h b/src/sat/smt/euf_relevancy.h
similarity index 99%
rename from src/sat/smt/smt_relevant.h
rename to src/sat/smt/euf_relevancy.h
index e27694ae2..bcbcaf877 100644
--- a/src/sat/smt/smt_relevant.h
+++ b/src/sat/smt/euf_relevancy.h
@@ -97,11 +97,10 @@ Do we need full watch lists instead of 2-watch lists?
 #include "sat/sat_solver.h"
 #include "sat/smt/sat_th.h"
 
-namespace euf {
-    class solver;
-}
 
-namespace smt {
+namespace euf {
+
+    class solver;
 
     class relevancy {
         euf::solver&         ctx;
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 3a48ae3b1..1913e1bd3 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -27,7 +27,7 @@ Author:
 #include "sat/smt/sat_th.h"
 #include "sat/smt/euf_ackerman.h"
 #include "sat/smt/user_solver.h"
-#include "sat/smt/smt_relevant.h"
+#include "sat/smt/euf_relevancy.h"
 #include "smt/params/smt_params.h"
 
 
@@ -92,7 +92,7 @@ namespace euf {
         std::function<::solver*(void)>   m_mk_solver;
         ast_manager&                     m;
         sat::sat_internalizer& si;
-        smt::relevancy         m_relevancy;
+        relevancy              m_relevancy;
         smt_params             m_config;
         euf::egraph            m_egraph;
         trail_stack            m_trail;
@@ -388,7 +388,7 @@ namespace euf {
         bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
         void relevant_eh(euf::enode* n);
 
-        smt::relevancy& relevancy() { return m_relevancy; }
+        relevancy& get_relevancy() { return m_relevancy; }
 
         // model construction
         void update_model(model_ref& mdl);
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 8d3bc5995..1665ec74c 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -69,13 +69,13 @@ namespace q {
             m_mam->add_node(n, false);
         };
         ctx.get_egraph().set_on_merge(_on_merge);
-        if (!ctx.relevancy().enabled())
+        if (!ctx.relevancy_enabled())
             ctx.get_egraph().set_on_make(_on_make);
         m_mam = mam::mk(ctx, *this);
     }
 
     void ematch::relevant_eh(euf::enode* n) {
-        if (ctx.relevancy().enabled())
+        if (ctx.relevancy_enabled())
             m_mam->add_node(n, false);
     }
 
@@ -358,7 +358,7 @@ namespace q {
         if (m_prop_queue.empty())
             return false;
         for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
-            auto [is_conflict, idx, j_idx] = m_prop_queue[i];
+            auto const& [is_conflict, idx, j_idx] = m_prop_queue[i];
             propagate(is_conflict, idx, j_idx);
         }
         m_prop_queue.reset();