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/arith | |
parent | 69c2d3e702f8ec0bd0eec4a481a07571131aabeb (diff) |
Type-checking classes and hooks (not tested yet).
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 74 |
2 files changed, 75 insertions, 0 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_ */ |