diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 8bf8d9e54..76992e1ba 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1013,6 +1013,22 @@ Expr ExprManager::mkRightAssociative(Kind kind, return n.toExpr(); } +Expr ExprManager::mkChain(Kind kind, const std::vector<Expr>& children) +{ + if (children.size() == 2) + { + // if this is the case exactly 1 pair will be generated so the + // AND is not required + return mkExpr(kind, children[0], children[1]); + } + std::vector<Expr> cchildren; + for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++) + { + cchildren.push_back(mkExpr(kind, children[i], children[i + 1])); + } + return mkExpr(kind::AND, cchildren); +} + unsigned ExprManager::minArity(Kind kind) { return metakind::getLowerBoundForKind(kind); } |