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.cpp | |
parent | 9da04b35ddb44761285af21519023d88f3adf1b5 (diff) |
Started work on array theory
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 43 |
1 files changed, 43 insertions, 0 deletions
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; +} |