1 /********************* */
2 /*! \file theory_uf_type_rules.h
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add brief comments here ]]
16 ** [[ Add file-specific comments here ]]
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
22 #define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
30 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
31 throw (TypeCheckingExceptionPrivate
) {
32 TNode f
= n
.getOperator();
33 TypeNode fType
= f
.getType(check
);
34 if( !fType
.isFunction() ) {
35 throw TypeCheckingExceptionPrivate(n
, "operator does not have function type");
38 if (n
.getNumChildren() != fType
.getNumChildren() - 1) {
39 throw TypeCheckingExceptionPrivate(n
, "number of arguments does not match the function type");
41 TNode::iterator argument_it
= n
.begin();
42 TNode::iterator argument_it_end
= n
.end();
43 TypeNode::iterator argument_type_it
= fType
.begin();
44 for(; argument_it
!= argument_it_end
; ++argument_it
) {
45 if((*argument_it
).getType() != *argument_type_it
) {
46 throw TypeCheckingExceptionPrivate(n
, "argument types do not match the function type");
50 return fType
.getRangeType();
52 };/* class UfTypeRule */
54 }/* CVC4::theory::uf namespace */
55 }/* CVC4::theory namespace */
58 #endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */