1 /********************* */
2 /*! \file theory_sep_type_rules.h
4 ** Original author: Andrew Reynolds
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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 Typing and cardinality rules for the theory of sep
14 ** Typing and cardinality rules for the theory of sep.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
20 #define __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H
22 #include "theory/type_enumerator.h"
28 class SepEmpTypeRule
{
30 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
31 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
32 Assert(n
.getKind() == kind::SEP_EMP
);
33 return nodeManager
->booleanType();
37 struct SepPtoTypeRule
{
38 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
39 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
40 Assert(n
.getKind() == kind::SEP_PTO
);
42 TypeNode refType
= n
[0].getType(check
);
43 TypeNode ptType
= n
[1].getType(check
);
45 return nodeManager
->booleanType();
47 };/* struct SepSelectTypeRule */
49 struct SepStarTypeRule
{
50 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
51 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
52 TypeNode btype
= nodeManager
->booleanType();
53 Assert(n
.getKind() == kind::SEP_STAR
);
55 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
56 TypeNode ctype
= n
[i
].getType( check
);
58 throw TypeCheckingExceptionPrivate(n
, "child of sep star is not Boolean");
64 };/* struct SepStarTypeRule */
66 struct SepWandTypeRule
{
67 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
68 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
69 TypeNode btype
= nodeManager
->booleanType();
70 Assert(n
.getKind() == kind::SEP_WAND
);
72 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
73 TypeNode ctype
= n
[i
].getType( check
);
75 throw TypeCheckingExceptionPrivate(n
, "child of sep magic wand is not Boolean");
81 };/* struct SepWandTypeRule */
83 struct SepLabelTypeRule
{
84 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
85 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
86 TypeNode btype
= nodeManager
->booleanType();
87 Assert(n
.getKind() == kind::SEP_LABEL
);
89 TypeNode ctype
= n
[0].getType( check
);
91 throw TypeCheckingExceptionPrivate(n
, "child of sep label is not Boolean");
93 TypeNode stype
= n
[1].getType( check
);
95 throw TypeCheckingExceptionPrivate(n
, "label of sep label is not a set");
100 };/* struct SepLabelTypeRule */
102 struct SepNilTypeRule
{
103 inline static TypeNode
computeType(NodeManager
* nodeManager
, TNode n
, bool check
)
104 throw (TypeCheckingExceptionPrivate
, AssertionException
) {
105 Assert(n
.getKind() == kind::SEP_NIL
);
107 TypeNode type
= n
.getType();
110 };/* struct SepLabelTypeRule */
113 }/* CVC4::theory::sep namespace */
114 }/* CVC4::theory namespace */
115 }/* CVC4 namespace */
117 #endif /* __CVC4__THEORY__SEP__THEORY_SEP_TYPE_RULES_H */