datatype stuff in compatibility interface implemented

2 files changed, 40 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 624fbd9a2..12a60021e 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -268,6 +268,33 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   }
 }
 
+Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren) {
+  const unsigned n = otherChildren.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+
+  NodeManagerScope nms(d_nodeManager);
+
+  vector<Node> nodes;
+  nodes.push_back(child1.getNode());
+
+  vector<Expr>::const_iterator it = otherChildren.begin();
+  vector<Expr>::const_iterator it_end = otherChildren.end();
+  while(it != it_end) {
+    nodes.push_back(it->getNode());
+    ++it;
+  }
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 Expr ExprManager::mkExpr(Expr opExpr) {
   const unsigned n = 0;
   Kind kind = kind::operatorKindToKind(opExpr.getKind());
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 184556887..ade9a334d 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -194,6 +194,19 @@ public:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
+   * Make an n-ary expression of given kind given a first arg and
+   * a vector of its remaining children (this can be useful where the
+   * kind is parameterized operator, so the first arg is really an
+   * arg to the kind to construct an operator)
+   *
+   * @param kind the kind of expression to build
+   * @param child1 the first subexpression
+   * @param children the remaining subexpressions
+   * @return the n-ary expression
+   */
+  Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
+
+  /**
    * Make a nullary parameterized expression with the given operator.
    *
    * @param opExpr the operator expression