diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-19 22:07:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-19 22:07:01 +0000 |
commit | cd98370b338a0cc5343067151884a06431a1d92c (patch) | |
tree | 7e61d8cf61ada9fef8f470a3c781a07a5df5a0fc /src/include | |
parent | 394791604a62e19763a8a45328bc5177d91fabf9 (diff) |
testing framework, configure fixes, incorporations from meeting, continued work
Diffstat (limited to 'src/include')
-rw-r--r-- | src/include/cvc4.h | 10 | ||||
-rw-r--r-- | src/include/cvc4_expr.h | 24 |
2 files changed, 26 insertions, 8 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 109496001..c5e3bb013 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -9,10 +9,10 @@ ** **/ -#ifndef __CVC4_VC_H -#define __CVC4_VC_H +#ifndef __CVC4_H +#define __CVC4_H -#include "command.h" +#include "util/command.h" #include "cvc4_expr.h" /* TODO provide way of querying whether you fall into a fragment / @@ -37,6 +37,6 @@ public: void query(Expr); }; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_VC_H */ +#endif /* __CVC4_H */ diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index 3d7a35fc8..1f5ac659d 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -15,10 +15,15 @@ #include <vector> #include <stdint.h> +#include "expr/kind.h" namespace CVC4 { -class ExprValue; +namespace expr { + class ExprValue; +}/* CVC4::expr namespace */ + +using CVC4::expr::ExprValue; /** * Encapsulation of an ExprValue pointer. The reference count is @@ -41,6 +46,8 @@ class Expr { typedef Expr* iterator; typedef Expr const* const_iterator; + friend class ExprBuilder; + public: Expr(const Expr&); @@ -69,11 +76,22 @@ public: Expr substExpr(const std::vector<Expr>& oldTerms, const std::vector<Expr>& newTerms) const; + inline Kind getKind() const; + static Expr null() { return s_null; } - friend class ExprBuilder; };/* class Expr */ -} /* CVC4 namespace */ +}/* CVC4 namespace */ + +#include "expr/expr_value.h" + +namespace CVC4 { + +inline Kind Expr::getKind() const { + return Kind(d_ev->d_kind); +} + +}/* CVC4 namespace */ #endif /* __CVC4_EXPR_H */ |