From bf2e11809489faaf92bb47ca1923628622dcf177 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Jan 2022 13:38:51 -0600
Subject: [PATCH] Add utility expr::isBooleanConnective (#7869)

---
 src/expr/node_algorithm.cpp      |  8 ++++++++
 src/expr/node_algorithm.h        |  3 +++
 src/theory/relevance_manager.cpp | 12 +++---------
 src/theory/relevance_manager.h   |  2 --
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index badf0b75a..a7bea656a 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -856,5 +856,13 @@ bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
   return true;
 }
 
+bool isBooleanConnective(TNode cur)
+{
+  Kind k = cur.getKind();
+  return k == kind::NOT || k == kind::IMPLIES || k == kind::AND || k == kind::OR
+         || (k == kind::ITE && cur.getType().isBoolean()) || k == kind::XOR
+         || (k == kind::EQUAL && cur[0].getType().isBoolean());
+}
+
 }  // namespace expr
 }  // namespace cvc5
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index c3ee4b604..9b109cced 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -257,6 +257,9 @@ void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types);
  */
 bool match(Node n1, Node n2, std::unordered_map<Node, Node>& subs);
 
+/** Is the top symbol of cur a Boolean connective? */
+bool isBooleanConnective(TNode cur);
+
 }  // namespace expr
 }  // namespace cvc5
 
diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 9acf2dffc..87945aa06 100644
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -17,6 +17,7 @@
 
 #include <sstream>
 
+#include "expr/node_algorithm.h"
 #include "expr/term_context_stack.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
@@ -159,13 +160,6 @@ void RelevanceManager::computeRelevance()
   d_success = true;
 }
 
-bool RelevanceManager::isBooleanConnective(TNode cur)
-{
-  Kind k = cur.getKind();
-  return k == NOT || k == IMPLIES || k == AND || k == OR || k == ITE || k == XOR
-         || (k == EQUAL && cur[0].getType().isBoolean());
-}
-
 bool RelevanceManager::updateJustifyLastChild(const RlvPair& cur,
                                               std::vector<int32_t>& childrenJustify)
 {
@@ -174,7 +168,7 @@ bool RelevanceManager::updateJustifyLastChild(const RlvPair& cur,
   // compute the next child, in this case we push the status of the current
   // child to childrenJustify.
   size_t nchildren = cur.first.getNumChildren();
-  Assert(isBooleanConnective(cur.first));
+  Assert(expr::isBooleanConnective(cur.first));
   size_t index = childrenJustify.size();
   Assert(index < nchildren);
   Kind k = cur.first.getKind();
@@ -307,7 +301,7 @@ int32_t RelevanceManager::justify(TNode n)
     if (itc == childJustify.end())
     {
       // are we not a Boolean connective (including NOT)?
-      if (isBooleanConnective(cur.first))
+      if (expr::isBooleanConnective(cur.first))
       {
         // initialize its children justify vector as empty
         childJustify[cur].clear();
diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h
index 582a8a938..284adc855 100644
--- a/src/theory/relevance_manager.h
+++ b/src/theory/relevance_manager.h
@@ -160,8 +160,6 @@ class RelevanceManager : protected EnvObj
    * justified n to be false, 0 means n could not be justified.
    */
   int32_t justify(TNode n);
-  /** Is the top symbol of cur a Boolean connective? */
-  static bool isBooleanConnective(TNode cur);
   /**
    * Update justify last child. This method is a helper function for justify,
    * which is called at the moment that Boolean connective formula cur
-- 
2.30.2