Add utility expr::isBooleanConnective (#7869)

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index badf0b75a4420854e2a548a62519c4ea685e29d1..a7bea656a9885cdaebe6c9e97e2686486166d63e 100644 (file)
--- 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 c3ee4b60421b5188ec7a38ec463864d7854435bd..9b109cced24e3f82a6160e199e4701a1a16c66c7 100644 (file)
--- 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 9acf2dffc066c943c96283f2f020fd46dccf6f0a..87945aa0644736e0d481d4fde63c40182285244c 100644 (file)
--- 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 582a8a938c6c705affd123fddba9590cac4b7b0d..284adc8555abb1401ab5fd60a5acbd5924b65324 100644 (file)
--- 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