From 2564d8730f768a8305325d4b6cc08211d8a3281d Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 27 Jul 2010 20:54:33 +0000 Subject: Adding optional 'check' parameter to getType() methods --- src/theory/arith/theory_arith_type_rules.h | 41 ++++++---- src/theory/arrays/theory_arrays_type_rules.h | 32 ++++---- src/theory/booleans/theory_bool_type_rules.h | 33 ++++---- src/theory/builtin/theory_builtin_type_rules.h | 24 +++--- src/theory/bv/theory_bv_type_rules.h | 104 +++++++++++++++---------- src/theory/uf/theory_uf_type_rules.h | 26 ++++--- 6 files changed, 156 insertions(+), 104 deletions(-) (limited to 'src/theory') diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 9fb30bdb4..b8fa85c03 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -28,7 +28,7 @@ namespace arith { class ArithConstantTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); return nodeManager->integerType(); @@ -37,7 +37,7 @@ public: class ArithOperatorTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { TypeNode integerType = nodeManager->integerType(); TypeNode realType = nodeManager->realType(); @@ -45,10 +45,17 @@ public: TNode::iterator child_it_end = n.end(); bool isInteger = true; for(; child_it != child_it_end; ++child_it) { - TypeNode childType = (*child_it).getType(); - if (!childType.isInteger()) isInteger = false; - if(childType != integerType && childType != realType) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); + TypeNode childType = (*child_it).getType(check); + if (!childType.isInteger()) { + isInteger = false; + if( !check ) { // if we're not checking, nothing left to do + break; + } + } + if( check ) { + if(childType != integerType && childType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); + } } } return (isInteger ? integerType : realType); @@ -57,17 +64,19 @@ public: class ArithPredicateTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode integerType = nodeManager->integerType(); - TypeNode realType = nodeManager->realType(); - TypeNode lhsType = n[0].getType(); - if (lhsType != integerType && lhsType != realType) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); - } - TypeNode rhsType = n[1].getType(); - if (rhsType != integerType && rhsType != realType) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side"); + if( check ) { + TypeNode integerType = nodeManager->integerType(); + TypeNode realType = nodeManager->realType(); + TypeNode lhsType = n[0].getType(check); + if (lhsType != integerType && lhsType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); + } + TypeNode rhsType = n[1].getType(check); + if (rhsType != integerType && rhsType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side"); + } } return nodeManager->booleanType(); } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 0eb88d800..5d0713a89 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -26,30 +26,34 @@ namespace theory { namespace arrays { struct ArraySelectTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 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"); + TypeNode arrayType = n[0].getType(check); + if( check ) { + TypeNode indexType = n[1].getType(check); + 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) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) 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"); + TypeNode arrayType = n[0].getType(check); + if( check ) { + TypeNode indexType = n[1].getType(check); + TypeNode valueType = n[2].getType(check); + 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; } diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index b947cee10..fddced8ef 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -27,30 +27,35 @@ namespace boolean { class BooleanTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { TypeNode booleanType = nodeManager->booleanType(); - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - for(; child_it != child_it_end; ++child_it) - if((*child_it).getType() != booleanType) { - throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); + if( check ) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + for(; child_it != child_it_end; ++child_it) { + if((*child_it).getType(check) != booleanType) { + throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); + } } + } return booleanType; } }; class IteTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode booleanType = nodeManager->booleanType(); - if (n[0].getType() != booleanType) { - throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); - } - TypeNode iteType = n[1].getType(); - if (iteType != n[2].getType()) { - throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type"); + TypeNode iteType = n[1].getType(check); + if( check ) { + TypeNode booleanType = nodeManager->booleanType(); + if (n[0].getType(check) != booleanType) { + throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); + } + if (iteType != n[2].getType(check)) { + throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type"); + } } return iteType; } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 19d6e268b..4458931a9 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,9 +31,11 @@ namespace builtin { class EqualityTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { - if (n[0].getType() != n[1].getType()) { - throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { + if( check ) { + if (n[0].getType(check) != n[1].getType(check)) { + throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); + } } return nodeManager->booleanType(); } @@ -41,13 +43,15 @@ class EqualityTypeRule { class DistinctTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - TypeNode firstType = (*child_it).getType(); - for (++child_it; child_it != child_it_end; ++child_it) { - if ((*child_it).getType() != firstType) { - throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + if( check ) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode firstType = (*child_it).getType(check); + for (++child_it; child_it != child_it_end; ++child_it) { + if ((*child_it).getType() != firstType) { + throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); + } } } return nodeManager->booleanType(); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 7aaae7349..9bb9e61df 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -18,6 +18,8 @@ #include "cvc4_private.h" +#include + #ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H #define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H @@ -27,7 +29,7 @@ namespace bv { class BitVectorConstantTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { return nodeManager->mkBitVectorType(n.getConst().getSize()); } @@ -35,12 +37,14 @@ public: class BitVectorCompRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode lhs = n[0].getType(); - TypeNode rhs = n[1].getType(); - if (!lhs.isBitVector() || lhs != rhs) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + if( check ) { + TypeNode lhs = n[0].getType(check); + TypeNode rhs = n[1].getType(check); + if (!lhs.isBitVector() || lhs != rhs) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } } return nodeManager->mkBitVectorType(1); } @@ -48,18 +52,18 @@ public: class BitVectorArithRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { unsigned maxWidth = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); // TODO: optimize unary neg for (; it != it_end; ++ it) { - TypeNode t = (*it).getType(); - if (!t.isBitVector()) { + TypeNode t = (*it).getType(check); + if (check && !t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } - if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize(); + maxWidth = std::max( maxWidth, t.getBitVectorSize() ); } return nodeManager->mkBitVectorType(maxWidth); } @@ -67,17 +71,19 @@ public: class BitVectorFixedWidthTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); - TypeNode t = (*it).getType(); - if (!t.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); - } - for (++ it; it != it_end; ++ it) { - if ((*it).getType() != t) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + TypeNode t = (*it).getType(check); + if( check ) { + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + TNode::iterator it_end = n.end(); + for (++ it; it != it_end; ++ it) { + if ((*it).getType(check) != t) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } } } return t; @@ -86,15 +92,17 @@ public: class BitVectorPredicateTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode lhsType = n[0].getType(); - if (!lhsType.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); - } - TypeNode rhsType = n[1].getType(); - if (lhsType != rhsType) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + if( check ) { + TypeNode lhsType = n[0].getType(check); + if (!lhsType.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + TypeNode rhsType = n[1].getType(check); + if (lhsType != rhsType) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } } return nodeManager->booleanType(); } @@ -102,18 +110,25 @@ public: class BitVectorExtractTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode t = n[0].getType(); - if (!t.isBitVector()) { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); - } BitVectorExtract extractInfo = n.getOperator().getConst(); + + // NOTE: We're throwing a type-checking exception here even + // if check is false, bc if we allow high < low the resulting + // type will be illegal if (extractInfo.high < extractInfo.low) { throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index"); } - if (extractInfo.high >= t.getBitVectorSize()) { - throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); + + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + if (extractInfo.high >= t.getBitVectorSize()) { + throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); + } } return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } @@ -121,13 +136,16 @@ public: class BitVectorConcatRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { unsigned size = 0; TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); for (; it != it_end; ++ it) { - TypeNode t = n[0].getType(); + TypeNode t = n[0].getType(check); + // NOTE: We're throwing a type-checking exception here even + // when check is false, bc if we don't check that the arguments + // are bit-vectors the result type will be inaccurate if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); } @@ -139,9 +157,12 @@ public: class BitVectorRepeatTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode t = n[0].getType(); + TypeNode t = n[0].getType(check); + // NOTE: We're throwing a type-checking exception here even + // when check is false, bc if the argument isn't a bit-vector + // the result type will be inaccurate if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } @@ -152,9 +173,12 @@ public: class BitVectorExtendTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - TypeNode t = n[0].getType(); + TypeNode t = n[0].getType(check); + // NOTE: We're throwing a type-checking exception here even + // when check is false, bc if the argument isn't a bit-vector + // the result type will be inaccurate if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index f09a44d50..38018112a 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -27,20 +27,26 @@ namespace uf { class UfTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { TNode f = n.getOperator(); - TypeNode fType = f.getType(); - if (n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + TypeNode fType = f.getType(check); + if( !fType.isFunction() ) { + throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) - if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + if( check ) { + if (n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) { + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + } + } return fType.getRangeType(); } };/* class UfTypeRule */ -- cgit v1.2.3