1 files changed, 12 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 5ef6ef984..b3a1b68df 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -96,6 +96,9 @@ public:
   /** Get the type for integers */
   IntegerType integerType() const;
 
+  /** The the type for bit-vectors */
+  BitVectorType bitVectorType(unsigned size) const;
+
   /**
    * Make a unary expression of a given kind (TRUE, FALSE,...).
    * @param kind the kind of expression
@@ -163,6 +166,15 @@ public:
    */
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
+  /**
+   * Make an n-ary expression of given tre operator to appply and a vector of
+   * it's children
+   * @param opExpr the operator expression
+   * @param children the subexpressions
+   * @return the n-ary expression
+   */
+  Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
+
   /** Create a constant of type T */
   template <class T>
   Expr mkConst(const T&);