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/expr/node_manager.cpp | |
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/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6e2141351..8f7196e0c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -20,10 +20,11 @@ #include "node_manager.h" -#include "expr/builtin_type_rules.h" +#include "theory/builtin/theory_builtin_type_rules.h" #include "theory/booleans/theory_bool_type_rules.h" #include "theory/uf/theory_uf_type_rules.h" #include "theory/arith/theory_arith_type_rules.h" +#include "theory/arrays/theory_arrays_type_rules.h" #include "theory/bv/theory_bv_type_rules.h" #include <ext/hash_set> @@ -181,17 +182,19 @@ void NodeManager::reclaimZombies() { } }/* NodeManager::reclaimZombies() */ -TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { +TypeNode NodeManager::getType(TNode n) + throw (TypeCheckingExceptionPrivate, AssertionException) { TypeNode typeNode; bool hasType = getAttribute(n, TypeAttr(), typeNode); - if (!hasType) { + Debug("getType") << "getting type for " << n << std::endl; + if(!hasType) { // Infer the type - switch (n.getKind()) { + switch(n.getKind()) { case kind::EQUAL: - typeNode = CVC4::EqualityTypeRule::computeType(this, n); + typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n); break; case kind::DISTINCT: - typeNode = CVC4::DistinctTypeRule::computeType(this, n); + typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n); break; case kind::CONST_BOOLEAN: typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); @@ -253,6 +256,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { case kind::GEQ: typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); break; + case kind::SELECT: + typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n); + break; + case kind::STORE: + typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n); + break; case kind::BITVECTOR_CONST: typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n); break; @@ -362,10 +371,12 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n); break; default: + Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); } setAttribute(n, TypeAttr(), typeNode); } + Debug("getType") << "type of " << n << " is " << typeNode << std::endl; return typeNode; } |