diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-04 03:42:56 +0000 |
commit | 1ce8e28d5976e1ab30099cb9e6943514497d2980 (patch) | |
tree | 1a9382fb62b38e3b5768da951b7c684f1b8688e7 /src/theory | |
parent | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (diff) |
Type-checking classes and hooks (not tested yet).
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 74 | ||||
-rw-r--r-- | src/theory/booleans/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_type_rules.h | 56 | ||||
-rw-r--r-- | src/theory/bv/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 170 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 47 |
8 files changed, 354 insertions, 3 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7c3e76d0a..0428bf84e 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -8,6 +8,7 @@ noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ theory_arith.h \ theory_arith.cpp \ + theory_arith_type_rules.h \ arith_rewriter.h \ arith_rewriter.cpp \ arith_utilities.h \ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h new file mode 100644 index 000000000..e97af08ee --- /dev/null +++ b/src/theory/arith/theory_arith_type_rules.h @@ -0,0 +1,74 @@ +/********************* */ +/** theory_arith_type_rules.cpp + ** Original author: dejan + ** Major contributors: 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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_ +#define __CVC4__THEORY_ARITH_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace arith { + + +class ArithConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); + return nodeManager->integerType(); + } +}; + +class ArithOperatorTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode integerType = nodeManager->integerType(); + TypeNode realType = nodeManager->realType(); + TNode::iterator child_it = n.begin(); + 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"); + } + } + return (isInteger ? integerType : realType); + } +}; + +class ArithPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + return nodeManager->booleanType(); + } +}; + +} +} +} + +#endif /* THEORY_ARITH_TYPE_RULES_H_ */ diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 690299630..a1b3e097a 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ - theory_bool.h + theory_bool.h \ + theory_bool_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h new file mode 100644 index 000000000..4cfc2f87f --- /dev/null +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -0,0 +1,56 @@ +/********************* */ +/** theory_bool_type_rules.cpp + ** Original author: dejan + ** Major contributors: 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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_ +#define __CVC4__THEORY_BOOL_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace boolean { + +class BooleanTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + return booleanType; + } +}; + +class IteTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) { + 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"); + } + return iteType; + } +}; + +} // boolean namespace +} // theory namespace +} // CVC4 namespace + +#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */ diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index d90472fd3..6f9a51dc3 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ - theory_bv.h + theory_bv.h \ + theory_bv_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h new file mode 100644 index 000000000..c9a7c1f2c --- /dev/null +++ b/src/theory/bv/theory_bv_type_rules.h @@ -0,0 +1,170 @@ +/********************* */ +/** theory_bv_types.h + ** Original author: dejan + ** 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. + ** + ** Bitvector theory. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ +#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace bv { + +class BitVectorConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + return nodeManager->bitVectorType(n.getConst<BitVector>().getSize()); + } +}; + +class BitVectorCompRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + return nodeManager->bitVectorType(1); + } +}; + +class BitVectorArithRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize(); + } + return nodeManager->bitVectorType(maxWidth); + } +}; + +class BitVectorFixedWidthTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + } + return t; + } +}; + +class BitVectorPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + return nodeManager->booleanType(); + } +}; + +class BitVectorExtractTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + BitVectorExtract extractInfo = n.getOperator().getConst<BitVectorExtract>(); + 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"); + } + return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1); + } +}; + +class BitVectorConcatRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + unsigned size = 0; + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + size += t.getBitVectorSize(); + } + return nodeManager->bitVectorType(size); + } +}; + +class BitVectorRepeatTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>(); + return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize()); + } +}; + +class BitVectorExtendTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ? + (unsigned) n.getOperator().getConst<BitVectorSignExtend>() : + (unsigned) n.getOperator().getConst<BitVectorZeroExtend>(); + + return nodeManager->bitVectorType(extendAmount + t.getBitVectorSize()); + } +}; + +} +} +} + +#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index e0aa3a1df..e40359521 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -9,6 +9,7 @@ libuf_la_SOURCES = \ ecdata.h \ ecdata.cpp \ theory_uf.h \ - theory_uf.cpp + theory_uf.cpp \ + theory_uf_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h new file mode 100644 index 000000000..8c05591d6 --- /dev/null +++ b/src/theory/uf/theory_uf_type_rules.h @@ -0,0 +1,47 @@ +/********************* */ +/** theory_uf_type_rules.h + ** Original author: dejan + ** Major contributors: 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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_ +#define __CVC4__THEORY_UF_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace uf { + +class UfTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + 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"); + } + 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(); + } +}; + +} +} +} + + +#endif /* THEORY_UF_TYPE_RULES_H_ */ |