1 files changed, 43 insertions, 85 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 4255e3454..b530d13b2 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -161,16 +161,12 @@ struct ExprHashFunction {
   size_t operator()(CVC4::Expr e) const;
 };/* struct ExprHashFunction */
 
-class BoolExpr;
-
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
  */
 class CVC4_PUBLIC Expr {
 
-  friend class BoolExpr;
-
   /** The internal expression representation */
   NodeTemplate<true>* d_node;
 
@@ -313,6 +309,48 @@ public:
   }
 
   /**
+   * Returns the Boolean negation of this Expr.
+   */
+  Expr notExpr() const;
+
+  /**
+   * Returns the conjunction of this expression and
+   * the given expression.
+   */
+  Expr andExpr(const Expr& e) const;
+
+  /**
+   * Returns the disjunction of this expression and
+   * the given expression.
+   */
+  Expr orExpr(const Expr& e) const;
+
+  /**
+   * Returns the exclusive disjunction of this expression and
+   * the given expression.
+   */
+  Expr xorExpr(const Expr& e) const;
+
+  /**
+   * Returns the Boolean equivalence of this expression and
+   * the given expression.
+   */
+  Expr iffExpr(const Expr& e) const;
+
+  /**
+   * Returns the implication of this expression and
+   * the given expression.
+   */
+  Expr impExpr(const Expr& e) const;
+
+  /**
+   * Returns the if-then-else expression with this expression
+   * as the Boolean condition and the given expressions as
+   * the "then" and "else" expressions.
+   */
+  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
+
+  /**
    * Iterator type for the children of an Expr.
    */
   class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
@@ -562,86 +600,6 @@ private:
 
 };/* class Expr */
 
-/**
- * Extending the expression with the capability to construct Boolean
- * expressions.
- */
-class CVC4_PUBLIC BoolExpr : public Expr {
-
-public:
-
-  /** Default constructor, makes a null expression */
-  BoolExpr();
-
-  /**
-   * Convert an expression to a Boolean expression
-   */
-  BoolExpr(const Expr& e);
-
-  /**
-   * Negate this expression.
-   * @return the logical negation of this expression.
-   */
-  BoolExpr notExpr() const;
-
-  /**
-   * Conjunct the given expression to this expression.
-   * @param e the expression to conjunct
-   * @return the conjunction of this expression and e
-   */
-  BoolExpr andExpr(const BoolExpr& e) const;
-
-  /**
-   * Disjunct the given expression to this expression.
-   * @param e the expression to disjunct
-   * @return the disjunction of this expression and e
-   */
-  BoolExpr orExpr(const BoolExpr& e) const;
-
-  /**
-   * Make an exclusive or expression out of this expression and the given
-   * expression.
-   * @param e the right side of the xor
-   * @return the xor of this expression and e
-   */
-  BoolExpr xorExpr(const BoolExpr& e) const;
-
-  /**
-   * Make an equivalence expression out of this expression and the given
-   * expression.
-   * @param e the right side of the equivalence
-   * @return the equivalence expression
-   */
-  BoolExpr iffExpr(const BoolExpr& e) const;
-
-  /**
-   * Make an implication expression out of this expression and the given
-   * expression.
-   * @param e the right side of the equivalence
-   * @return the equivalence expression
-   */
-  BoolExpr impExpr(const BoolExpr& e) const;
-
-  /**
-   * Make a Boolean if-then-else expression using this expression as the
-   * condition, and given the then and else parts.
-   * @param then_e the then branch expression
-   * @param else_e the else branch expression
-   * @return the if-then-else expression
-   */
-  BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
-
-  /**
-   * Make a term if-then-else expression using this expression as the
-   * condition, and given the then and else parts.
-   * @param then_e the then branch expression
-   * @param else_e the else branch expression
-   * @return the if-then-else expression
-   */
-  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
-
-};/* class BoolExpr */
-
 namespace expr {
 
 /**
@@ -968,7 +926,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 959 "${template}"
+#line 930 "${template}"
 
 namespace expr {