Add NodeManager::mkOr() (#5360)

This PR adds a convenience method mkOr() just like mkAnd().

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8f223752389ffa76a9e4f7a2dd8b0b7befda4e60..5cf19aab9843d90fc316e667df9ec1d89c840b2d 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -484,6 +484,17 @@ class NodeManager {
   template <bool ref_count>
   Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children);
 
+  /**
+   * Create an OR node with arbitrary number of children. This returns the
+   * false node if children is empty, or the single node in children if
+   * it contains only one node.
+   *
+   * We define construction of OR as a special case here since it is widely
+   * used for e.g. constructing explanations or lemmas.
+   */
+  template <bool ref_count>
+  Node mkOr(const std::vector<NodeTemplate<ref_count> >& children);
+
   /** Create a node (with no children) by operator. */
   Node mkNode(TNode opNode);
   Node* mkNodePtr(TNode opNode);
@@ -1406,6 +1417,20 @@ Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children)
   return mkNode(kind::AND, children);
 }
 
+template <bool ref_count>
+Node NodeManager::mkOr(const std::vector<NodeTemplate<ref_count> >& children)
+{
+  if (children.empty())
+  {
+    return mkConst(false);
+  }
+  else if (children.size() == 1)
+  {
+    return children[0];
+  }
+  return mkNode(kind::OR, children);
+}
+
 template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(Kind kind,
                                 const std::vector<NodeTemplate<ref_count> >&