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 | |
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')
-rw-r--r-- | src/theory/arrays/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 21 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 62 |
4 files changed, 86 insertions, 4 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 84b9faaf4..0c6e9006f 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ + theory_arrays_type_rules.h \ theory_arrays.h \ theory_arrays.cpp diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 742b924c6..68daa8cb5 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -5,5 +5,11 @@ # theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" + +operator ARRAY_TYPE 2 "array type" + +# select a i is a[i] operator SELECT 2 "array select" + +# store a i e is a[i] <= e operator STORE 3 "array store" 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 */ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h new file mode 100644 index 000000000..0eb88d800 --- /dev/null +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file theory_arrays_type_rules.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** 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 Theory of arrays. + ** + ** Theory of arrays. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ +#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace arrays { + +struct ArraySelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::SELECT); + TypeNode arrayType = n[0].getType(); + TypeNode indexType = n[1].getType(); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); + } + return arrayType.getArrayConstituentType(); + } +};/* struct ArraySelectTypeRule */ + +struct ArrayStoreTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::STORE); + TypeNode arrayType = n[0].getType(); + TypeNode indexType = n[1].getType(); + TypeNode valueType = n[2].getType(); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); + } + if(arrayType.getArrayConstituentType() != valueType) { + throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + } + return arrayType; + } +};/* struct ArrayStoreTypeRule */ + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ */ |