diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
commit | 4375b60d5df794b2c6193f3892185ea181a0748d (patch) | |
tree | d346f9dc6bde42c3def6e0aac3b2711418e3d491 /src/theory/arrays/theory_arrays.h | |
parent | 4206a75e7a1635d04bb69084404a75670e164b62 (diff) |
* theory "tree" rewriting implemented and works
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 52e63831c..69498cfb2 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -23,9 +23,7 @@ #include "theory/theory.h" -namespace context { -class Context; -} +#include <iostream> namespace CVC4 { namespace theory { @@ -37,10 +35,25 @@ public: ~TheoryArrays(); void preRegisterTerm(TNode n) { } void registerTerm(TNode n) { } + + RewriteResponse preRewrite(TNode in, bool topLevel) { + Debug("arrays-rewrite") << "pre-rewriting " << in + << " topLevel==" << topLevel << std::endl; + return RewritingComplete(in); + } + + RewriteResponse postRewrite(TNode in, bool topLevel) { + Debug("arrays-rewrite") << "post-rewriting " << in + << " topLevel==" << topLevel << std::endl; + return RewritingComplete(in); + } + void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } -}; + void shutdown() { } + std::string identify() const { return std::string("TheoryArrays"); } +};/* class TheoryArrays */ }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ |