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 | |
parent | 9da04b35ddb44761285af21519023d88f3adf1b5 (diff) |
Started work on array theory
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 43 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 21 |
3 files changed, 56 insertions, 11 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 5d3514dda..813a91314 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ - theory_arrays.h + theory_arrays.h \ + theory_arrays.cpp EXTRA_DIST = kinds diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp new file mode 100644 index 000000000..106d1a8da --- /dev/null +++ b/src/theory/arrays/theory_arrays.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file theory_arrays.cpp + ** \verbatim + ** Original author: barrett + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the theory of arrays. + ** + ** Implementation of the theory of arrays. + **/ + +#include "theory/arrays/theory_arrays.h" +#include "expr/kind.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) : + Theory(c, out) +{ +} + +TheoryArrays::~TheoryArrays() { +} + +void TheoryArrays::check(Effort e) { + while(!done()) { + Node assertion = get(); + Debug("arrays") << "TheoryArrays::check(): " << assertion << endl; + } + Debug("arrays") << "TheoryArrays::check(): done" << endl; +} 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 */ |