1 /********************* */
2 /*! \file theory_arith_type_rules.h
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Tim King, Christopher L. Conway, Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add brief comments here ]]
14 ** [[ Add file-specific comments here ]]
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
20 #define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
22 #include "util/subrange_bound.h"
29 class ArithConstantTypeRule
{
31 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
32 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
33 Assert(n
.getKind() == kind::CONST_RATIONAL
);
34 if(n
.getConst
<Rational
>().isIntegral()){
35 return nodeManager
->integerType();
37 return nodeManager
->realType();
40 };/* class ArithConstantTypeRule */
42 class ArithOperatorTypeRule
{
44 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
45 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
46 TypeNode integerType
= nodeManager
->integerType();
47 TypeNode realType
= nodeManager
->realType();
48 TNode::iterator child_it
= n
.begin();
49 TNode::iterator child_it_end
= n
.end();
50 bool isInteger
= true;
51 for(; child_it
!= child_it_end
; ++child_it
) {
52 TypeNode childType
= (*child_it
).getType(check
);
53 if (!childType
.isInteger()) {
55 if( !check
) { // if we're not checking, nothing left to do
60 if(!childType
.isReal()) {
61 throw TypeCheckingExceptionPrivate(n
, "expecting an arithmetic subterm");
65 switch(Kind k
= n
.getKind()) {
68 case kind::TO_INTEGER
:
71 bool isDivision
= k
== kind::DIVISION
|| k
== kind::DIVISION_TOTAL
;
72 return (isInteger
&& !isDivision
? integerType
: realType
);
76 };/* class ArithOperatorTypeRule */
78 class IntOperatorTypeRule
{
80 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
81 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
82 TNode::iterator child_it
= n
.begin();
83 TNode::iterator child_it_end
= n
.end();
85 for(; child_it
!= child_it_end
; ++child_it
) {
86 TypeNode childType
= (*child_it
).getType(check
);
87 if (!childType
.isInteger()) {
88 throw TypeCheckingExceptionPrivate(n
, "expecting an integer subterm");
92 return nodeManager
->integerType();
94 };/* class IntOperatorTypeRule */
96 class ArithPredicateTypeRule
{
98 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
99 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
101 TypeNode lhsType
= n
[0].getType(check
);
102 if (!lhsType
.isReal()) {
103 Message() << lhsType
<< " : " << n
[0] << std::endl
;
104 throw TypeCheckingExceptionPrivate(n
, "expecting an arithmetic term on the left-hand-side");
106 TypeNode rhsType
= n
[1].getType(check
);
107 if (!rhsType
.isReal()) {
108 throw TypeCheckingExceptionPrivate(n
, "expecting an arithmetic term on the right-hand-side");
111 return nodeManager
->booleanType();
113 };/* class ArithPredicateTypeRule */
115 class ArithUnaryPredicateTypeRule
{
117 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
118 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
120 TypeNode t
= n
[0].getType(check
);
122 throw TypeCheckingExceptionPrivate(n
, "expecting an arithmetic term");
125 return nodeManager
->booleanType();
127 };/* class ArithUnaryPredicateTypeRule */
129 class IntUnaryPredicateTypeRule
{
131 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
132 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
134 TypeNode t
= n
[0].getType(check
);
135 if (!t
.isInteger()) {
136 throw TypeCheckingExceptionPrivate(n
, "expecting an integer term");
139 return nodeManager
->booleanType();
141 };/* class IntUnaryPredicateTypeRule */
143 class SubrangeProperties
{
145 inline static Cardinality
computeCardinality(TypeNode type
) {
146 Assert(type
.getKind() == kind::SUBRANGE_TYPE
);
148 const SubrangeBounds
& bounds
= type
.getConst
<SubrangeBounds
>();
149 if(!bounds
.lower
.hasBound() || !bounds
.upper
.hasBound()) {
150 return Cardinality::INTEGERS
;
152 return Cardinality(bounds
.upper
.getBound() - bounds
.lower
.getBound());
155 inline static Node
mkGroundTerm(TypeNode type
) {
156 Assert(type
.getKind() == kind::SUBRANGE_TYPE
);
158 const SubrangeBounds
& bounds
= type
.getConst
<SubrangeBounds
>();
159 if(bounds
.lower
.hasBound()) {
160 return NodeManager::currentNM()->mkConst(Rational(bounds
.lower
.getBound()));
162 if(bounds
.upper
.hasBound()) {
163 return NodeManager::currentNM()->mkConst(Rational(bounds
.upper
.getBound()));
165 return NodeManager::currentNM()->mkConst(Rational(0));
167 };/* class SubrangeProperties */
169 }/* CVC4::theory::arith namespace */
170 }/* CVC4::theory namespace */
171 }/* CVC4 namespace */
173 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */