diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-05 22:07:16 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-05 22:07:16 +0000 |
commit | 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 (patch) | |
tree | d0cfcf60cbf9600c52dcb728744802ad27a5c3e1 /src/expr/expr_template.h | |
parent | 7a9899f394476e53b7f759e698c7e10c8388fd57 (diff) |
BoolExpr removed and replaced with Expr
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r-- | src/expr/expr_template.h | 128 |
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 { |