1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Theory of quantifiers. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/theory_quantifiers_type_rules.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace theory { |
20 |
|
namespace quantifiers { |
21 |
|
|
22 |
52725 |
TypeNode QuantifierTypeRule::computeType(NodeManager* nodeManager, |
23 |
|
TNode n, |
24 |
|
bool check) |
25 |
|
{ |
26 |
52725 |
Debug("typecheck-q") << "type check for fa " << n << std::endl; |
27 |
52725 |
Assert((n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) |
28 |
|
&& n.getNumChildren() > 0); |
29 |
52725 |
if (check) |
30 |
|
{ |
31 |
52725 |
if (n[0].getType(check) != nodeManager->boundVarListType()) |
32 |
|
{ |
33 |
|
throw TypeCheckingExceptionPrivate( |
34 |
|
n, "first argument of quantifier is not bound var list"); |
35 |
|
} |
36 |
52725 |
if (n[1].getType(check) != nodeManager->booleanType()) |
37 |
|
{ |
38 |
|
throw TypeCheckingExceptionPrivate(n, |
39 |
|
"body of quantifier is not boolean"); |
40 |
|
} |
41 |
52725 |
if (n.getNumChildren() == 3) |
42 |
|
{ |
43 |
6415 |
if (n[2].getType(check) != nodeManager->instPatternListType()) |
44 |
|
{ |
45 |
|
throw TypeCheckingExceptionPrivate( |
46 |
|
n, |
47 |
|
"third argument of quantifier is not instantiation " |
48 |
|
"pattern list"); |
49 |
|
} |
50 |
13375 |
for (const Node& p : n[2]) |
51 |
|
{ |
52 |
13920 |
if (p.getKind() == kind::INST_POOL |
53 |
13920 |
&& p.getNumChildren() != n[0].getNumChildren()) |
54 |
|
{ |
55 |
|
throw TypeCheckingExceptionPrivate( |
56 |
|
n, |
57 |
|
"expected number of arguments to pool to be the same as the " |
58 |
|
"number of bound variables of the quantified formula"); |
59 |
|
} |
60 |
|
} |
61 |
|
} |
62 |
|
} |
63 |
52725 |
return nodeManager->booleanType(); |
64 |
|
} |
65 |
|
|
66 |
36002 |
TypeNode QuantifierBoundVarListTypeRule::computeType(NodeManager* nodeManager, |
67 |
|
TNode n, |
68 |
|
bool check) |
69 |
|
{ |
70 |
36002 |
Assert(n.getKind() == kind::BOUND_VAR_LIST); |
71 |
36002 |
if (check) |
72 |
|
{ |
73 |
137744 |
for (int i = 0; i < (int)n.getNumChildren(); i++) |
74 |
|
{ |
75 |
101742 |
if (n[i].getKind() != kind::BOUND_VARIABLE) |
76 |
|
{ |
77 |
|
throw TypeCheckingExceptionPrivate( |
78 |
|
n, "argument of bound var list is not bound variable"); |
79 |
|
} |
80 |
|
} |
81 |
|
} |
82 |
36002 |
return nodeManager->boundVarListType(); |
83 |
|
} |
84 |
|
|
85 |
2893 |
TypeNode QuantifierInstPatternTypeRule::computeType(NodeManager* nodeManager, |
86 |
|
TNode n, |
87 |
|
bool check) |
88 |
|
{ |
89 |
2893 |
Assert(n.getKind() == kind::INST_PATTERN); |
90 |
2893 |
if (check) |
91 |
|
{ |
92 |
5786 |
TypeNode tn = n[0].getType(check); |
93 |
|
// this check catches the common mistake writing :pattern (f x) instead of |
94 |
|
// :pattern ((f x)) |
95 |
8683 |
if (n[0].isVar() && n[0].getKind() != kind::BOUND_VARIABLE |
96 |
8681 |
&& tn.isFunction()) |
97 |
|
{ |
98 |
|
throw TypeCheckingExceptionPrivate( |
99 |
|
n[0], "Pattern must be a list of fully-applied terms."); |
100 |
|
} |
101 |
|
} |
102 |
2893 |
return nodeManager->instPatternType(); |
103 |
|
} |
104 |
|
|
105 |
1103 |
TypeNode QuantifierAnnotationTypeRule::computeType(NodeManager* nodeManager, |
106 |
|
TNode n, |
107 |
|
bool check) |
108 |
|
{ |
109 |
1103 |
if (n.getKind() == kind::INST_ATTRIBUTE) |
110 |
|
{ |
111 |
1088 |
if (n.getNumChildren() > 1) |
112 |
|
{ |
113 |
|
// first must be a keyword |
114 |
77 |
if (n[0].getKind() != kind::CONST_STRING) |
115 |
|
{ |
116 |
|
throw TypeCheckingExceptionPrivate( |
117 |
|
n[0], "Expecting a keyword at the head of INST_ATTRIBUTE."); |
118 |
|
} |
119 |
|
} |
120 |
|
} |
121 |
1103 |
return nodeManager->instPatternType(); |
122 |
|
} |
123 |
|
|
124 |
3851 |
TypeNode QuantifierInstPatternListTypeRule::computeType( |
125 |
|
NodeManager* nodeManager, TNode n, bool check) |
126 |
|
{ |
127 |
3851 |
Assert(n.getKind() == kind::INST_PATTERN_LIST); |
128 |
3851 |
if (check) |
129 |
|
{ |
130 |
8049 |
for (const Node& nc : n) |
131 |
|
{ |
132 |
4198 |
Kind k = nc.getKind(); |
133 |
4198 |
if (k != kind::INST_PATTERN && k != kind::INST_NO_PATTERN |
134 |
1292 |
&& k != kind::INST_ATTRIBUTE && k != kind::INST_POOL |
135 |
8 |
&& k != kind::INST_ADD_TO_POOL && k != kind::SKOLEM_ADD_TO_POOL) |
136 |
|
{ |
137 |
|
throw TypeCheckingExceptionPrivate( |
138 |
|
n, |
139 |
|
"argument of inst pattern list is not a legal quantifiers " |
140 |
|
"annotation"); |
141 |
|
} |
142 |
|
} |
143 |
|
} |
144 |
3851 |
return nodeManager->instPatternListType(); |
145 |
|
} |
146 |
|
|
147 |
|
} // namespace quantifiers |
148 |
|
} // namespace theory |
149 |
22746 |
} // namespace cvc5 |