diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-24 22:51:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-24 22:51:35 +0000 |
commit | 61937ea05bff33070cc8252bc3b6c7d6fed7c9c3 (patch) | |
tree | 2c942f052de4dc9f0385bf01b89ec08d01c165bb /src/expr/expr.h | |
parent | 9d3a76f0e4676dd11e533c370a2f3a3e17ff8329 (diff) |
various fixes and updates to use and support parser
Diffstat (limited to 'src/expr/expr.h')
-rw-r--r-- | src/expr/expr.h | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/expr/expr.h b/src/expr/expr.h index d99708991..19f02650e 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -10,8 +10,8 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#ifndef __CVC4_EXPR_H -#define __CVC4_EXPR_H +#ifndef __CVC4__EXPR_H +#define __CVC4__EXPR_H #include <vector> #include <stdint.h> @@ -74,9 +74,6 @@ public: Expr iffExpr(const Expr& right) const; Expr impExpr(const Expr& right) const; Expr xorExpr(const Expr& right) const; - Expr skolemExpr(int i) const; - Expr substExpr(const std::vector<Expr>& oldTerms, - const std::vector<Expr>& newTerms) const; Expr plusExpr(const Expr& right) const; Expr uMinusExpr() const; @@ -100,4 +97,4 @@ inline Kind Expr::getKind() const { }/* CVC4 namespace */ -#endif /* __CVC4_EXPR_H */ +#endif /* __CVC4__EXPR_H */ |