From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 29 Oct 2020 14:25:42 +0000 (+0100)
Subject: Add NodeManager::mkOr() (#5360)
X-Git-Tag: cvc5-1.0.0~2648
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0cebb4e9b2a5caa8fafa6ebd562a25aa18de9d43;p=cvc5.git

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 8f2237523..5cf19aab9 100644
--- 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> >&