diff options
Diffstat (limited to 'src/expr/node_manager.h')
-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 592b5e7e9..abbe998b5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -473,6 +473,17 @@ class NodeManager { template <bool ref_count> Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children); + /** + * Create an AND node with arbitrary number of children. This returns the + * true node if children is empty, or the single node in children if + * it contains only one node. + * + * We define construction of AND as a special case here since it is widely + * used for e.g. constructing explanations. + */ + template <bool ref_count> + Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children); + /** Create a node (with no children) by operator. */ Node mkNode(TNode opNode); Node* mkNodePtr(TNode opNode); @@ -1360,6 +1371,20 @@ inline Node NodeManager::mkNode(Kind kind, } template <bool ref_count> +Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + +template <bool ref_count> inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { |