diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-10-29 15:25:42 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-29 09:25:42 -0500 |
commit | 0cebb4e9b2a5caa8fafa6ebd562a25aa18de9d43 (patch) | |
tree | 058d6324e256115a56f9d053f2ded4bcf6d03de4 /src/expr | |
parent | c483eeb3505a61aa1b4f8432e07555176dd7598c (diff) |
Add NodeManager::mkOr() (#5360)
This PR adds a convenience method mkOr() just like mkAnd().
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.h | 25 |
1 files changed, 25 insertions, 0 deletions
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); @@ -1407,6 +1418,20 @@ Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& 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> >& children) { |