diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2010-06-14 16:06:51 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2010-06-14 16:06:51 +0000 |
commit | e8b6775c1c43a704e4e6afdefad6378fdb200fd0 (patch) | |
tree | 0ee03d658685f0acb55ee2aeb88564c149c8f868 /src/theory/arrays/theory_arrays.h | |
parent | 9da04b35ddb44761285af21519023d88f3adf1b5 (diff) |
Started work on array theory
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6ab0fac90..52e63831c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -22,7 +22,10 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #include "theory/theory.h" -#include "context/context.h" + +namespace context { +class Context; +} namespace CVC4 { namespace theory { @@ -30,15 +33,13 @@ namespace arrays { class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, OutputChannel& out) : - Theory(c, out) { - } - - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } - void check(Effort e) { Unimplemented(); } - void propagate(Effort e) { Unimplemented(); } - void explain(TNode n, Effort e) { Unimplemented(); } + TheoryArrays(context::Context* c, OutputChannel& out); + ~TheoryArrays(); + void preRegisterTerm(TNode n) { } + void registerTerm(TNode n) { } + void check(Effort e); + void propagate(Effort e) { } + void explain(TNode n, Effort e) { } }; }/* CVC4::theory::arrays namespace */ |