1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Paul Meng, Mathias Preiner |
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 |
|
* Sort inference module. |
14 |
|
* |
15 |
|
* This class implements sort inference, based on a simple algorithm: |
16 |
|
* First, we assume all functions and predicates have distinct uninterpreted |
17 |
|
* types. |
18 |
|
* One pass is made through the input assertions, while a union-find data |
19 |
|
* structure maintains necessary information regarding constraints on these |
20 |
|
* types. |
21 |
|
*/ |
22 |
|
|
23 |
|
#include "theory/sort_inference.h" |
24 |
|
|
25 |
|
#include <sstream> |
26 |
|
#include <vector> |
27 |
|
|
28 |
|
#include "expr/skolem_manager.h" |
29 |
|
#include "options/quantifiers_options.h" |
30 |
|
#include "options/smt_options.h" |
31 |
|
#include "options/uf_options.h" |
32 |
|
#include "theory/quantifiers/quant_util.h" |
33 |
|
#include "theory/rewriter.h" |
34 |
|
|
35 |
|
using namespace cvc5; |
36 |
|
using namespace cvc5::kind; |
37 |
|
using namespace std; |
38 |
|
|
39 |
|
namespace cvc5 { |
40 |
|
namespace theory { |
41 |
|
|
42 |
|
void SortInference::UnionFind::print(const char * c){ |
43 |
|
for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){ |
44 |
|
Trace(c) << "s_" << it->first << " = s_" << it->second << ", "; |
45 |
|
} |
46 |
|
for( unsigned i=0; i<d_deq.size(); i++ ){ |
47 |
|
Trace(c) << "s_" << d_deq[i].first << " != s_" << d_deq[i].second << ", "; |
48 |
|
} |
49 |
|
Trace(c) << std::endl; |
50 |
|
} |
51 |
|
void SortInference::UnionFind::set( UnionFind& c ) { |
52 |
|
clear(); |
53 |
|
for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){ |
54 |
|
d_eqc[ it->first ] = it->second; |
55 |
|
} |
56 |
|
d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() ); |
57 |
|
} |
58 |
2254 |
int SortInference::UnionFind::getRepresentative( int t ){ |
59 |
2254 |
std::map< int, int >::iterator it = d_eqc.find( t ); |
60 |
2254 |
if( it==d_eqc.end() || it->second==t ){ |
61 |
1580 |
return t; |
62 |
|
}else{ |
63 |
674 |
int rt = getRepresentative( it->second ); |
64 |
674 |
d_eqc[t] = rt; |
65 |
674 |
return rt; |
66 |
|
} |
67 |
|
} |
68 |
|
void SortInference::UnionFind::setEqual( int t1, int t2 ){ |
69 |
|
if( t1!=t2 ){ |
70 |
|
int rt1 = getRepresentative( t1 ); |
71 |
|
int rt2 = getRepresentative( t2 ); |
72 |
|
if( rt1>rt2 ){ |
73 |
|
d_eqc[rt1] = rt2; |
74 |
|
}else{ |
75 |
|
d_eqc[rt2] = rt1; |
76 |
|
} |
77 |
|
} |
78 |
|
} |
79 |
|
bool SortInference::UnionFind::isValid() { |
80 |
|
for( unsigned i=0; i<d_deq.size(); i++ ){ |
81 |
|
if( areEqual( d_deq[i].first, d_deq[i].second ) ){ |
82 |
|
return false; |
83 |
|
} |
84 |
|
} |
85 |
|
return true; |
86 |
|
} |
87 |
|
|
88 |
|
|
89 |
96 |
void SortInference::recordSubsort( TypeNode tn, int s ){ |
90 |
96 |
s = d_type_union_find.getRepresentative( s ); |
91 |
96 |
if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){ |
92 |
28 |
d_sub_sorts.push_back( s ); |
93 |
28 |
d_type_sub_sorts[tn].push_back( s ); |
94 |
|
} |
95 |
96 |
} |
96 |
|
|
97 |
704 |
void SortInference::printSort( const char* c, int t ){ |
98 |
704 |
int rt = d_type_union_find.getRepresentative( t ); |
99 |
704 |
if( d_type_types.find( rt )!=d_type_types.end() ){ |
100 |
292 |
Trace(c) << d_type_types[rt]; |
101 |
|
}else{ |
102 |
412 |
Trace(c) << "s_" << rt; |
103 |
|
} |
104 |
704 |
} |
105 |
|
|
106 |
20 |
void SortInference::reset() { |
107 |
20 |
d_sub_sorts.clear(); |
108 |
20 |
d_non_monotonic_sorts.clear(); |
109 |
20 |
d_type_sub_sorts.clear(); |
110 |
|
//reset info |
111 |
20 |
d_sortCount = 1; |
112 |
20 |
d_type_union_find.clear(); |
113 |
20 |
d_type_types.clear(); |
114 |
20 |
d_id_for_types.clear(); |
115 |
20 |
d_op_return_types.clear(); |
116 |
20 |
d_op_arg_types.clear(); |
117 |
20 |
d_var_types.clear(); |
118 |
|
//for rewriting |
119 |
20 |
d_symbol_map.clear(); |
120 |
20 |
d_const_map.clear(); |
121 |
20 |
} |
122 |
|
|
123 |
20 |
void SortInference::initialize(const std::vector<Node>& assertions) |
124 |
|
{ |
125 |
20 |
Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl; |
126 |
|
// process all assertions |
127 |
40 |
std::map<Node, int> visited; |
128 |
20 |
NodeManager * nm = NodeManager::currentNM(); |
129 |
20 |
int btId = getIdForType( nm->booleanType() ); |
130 |
98 |
for (const Node& a : assertions) |
131 |
|
{ |
132 |
78 |
Trace("sort-inference-debug") << "Process " << a << std::endl; |
133 |
156 |
std::map<Node, Node> var_bound; |
134 |
78 |
int pid = process(a, var_bound, visited); |
135 |
|
// the type of the topmost term must be Boolean |
136 |
78 |
setEqual( pid, btId ); |
137 |
|
} |
138 |
20 |
Trace("sort-inference-proc") << "...done" << std::endl; |
139 |
80 |
for (const std::pair<const Node, int>& rt : d_op_return_types) |
140 |
|
{ |
141 |
60 |
Trace("sort-inference") << rt.first << " : "; |
142 |
120 |
TypeNode retTn = rt.first.getType(); |
143 |
60 |
if (!d_op_arg_types[rt.first].empty()) |
144 |
|
{ |
145 |
14 |
Trace("sort-inference") << "( "; |
146 |
30 |
for (size_t i = 0; i < d_op_arg_types[rt.first].size(); i++) |
147 |
|
{ |
148 |
16 |
recordSubsort(retTn[i], d_op_arg_types[rt.first][i]); |
149 |
16 |
printSort("sort-inference", d_op_arg_types[rt.first][i]); |
150 |
16 |
Trace("sort-inference") << " "; |
151 |
|
} |
152 |
14 |
Trace("sort-inference") << ") -> "; |
153 |
14 |
retTn = retTn[(int)retTn.getNumChildren() - 1]; |
154 |
|
} |
155 |
60 |
recordSubsort(retTn, rt.second); |
156 |
60 |
printSort("sort-inference", rt.second); |
157 |
60 |
Trace("sort-inference") << std::endl; |
158 |
|
} |
159 |
30 |
for (std::pair<const Node, std::map<Node, int> >& vt : d_var_types) |
160 |
|
{ |
161 |
20 |
Trace("sort-inference") |
162 |
10 |
<< "Quantified formula : " << vt.first << " : " << std::endl; |
163 |
30 |
for (const Node& v : vt.first[0]) |
164 |
|
{ |
165 |
20 |
recordSubsort(v.getType(), vt.second[v]); |
166 |
20 |
printSort("sort-inference", vt.second[v]); |
167 |
20 |
Trace("sort-inference") << std::endl; |
168 |
|
} |
169 |
10 |
Trace("sort-inference") << std::endl; |
170 |
|
} |
171 |
|
|
172 |
|
// determine monotonicity of sorts |
173 |
40 |
Trace("sort-inference-proc") |
174 |
20 |
<< "Calculating monotonicty for subsorts..." << std::endl; |
175 |
40 |
std::map<Node, std::map<int, bool> > visitedm; |
176 |
98 |
for (const Node& a : assertions) |
177 |
|
{ |
178 |
156 |
Trace("sort-inference-debug") |
179 |
78 |
<< "Process monotonicity for " << a << std::endl; |
180 |
156 |
std::map<Node, Node> var_bound; |
181 |
78 |
processMonotonic(a, true, true, var_bound, visitedm); |
182 |
|
} |
183 |
20 |
Trace("sort-inference-proc") << "...done" << std::endl; |
184 |
|
|
185 |
40 |
Trace("sort-inference") << "We have " << d_sub_sorts.size() |
186 |
20 |
<< " sub-sorts : " << std::endl; |
187 |
48 |
for (unsigned i = 0, size = d_sub_sorts.size(); i < size; i++) |
188 |
|
{ |
189 |
28 |
printSort("sort-inference", d_sub_sorts[i]); |
190 |
28 |
if (d_type_types.find(d_sub_sorts[i]) != d_type_types.end()) |
191 |
|
{ |
192 |
18 |
Trace("sort-inference") << " is interpreted." << std::endl; |
193 |
|
} |
194 |
30 |
else if (d_non_monotonic_sorts.find(d_sub_sorts[i]) |
195 |
30 |
== d_non_monotonic_sorts.end()) |
196 |
|
{ |
197 |
8 |
Trace("sort-inference") << " is monotonic." << std::endl; |
198 |
|
} |
199 |
|
else |
200 |
|
{ |
201 |
2 |
Trace("sort-inference") << " is not monotonic." << std::endl; |
202 |
|
} |
203 |
|
} |
204 |
20 |
} |
205 |
|
|
206 |
78 |
Node SortInference::simplify(Node n, |
207 |
|
std::map<Node, Node>& model_replace_f, |
208 |
|
std::map<Node, std::map<TypeNode, Node> >& visited) |
209 |
|
{ |
210 |
78 |
Trace("sort-inference-debug") << "Simplify " << n << std::endl; |
211 |
156 |
std::map<Node, Node> var_bound; |
212 |
156 |
TypeNode tnn; |
213 |
78 |
Node ret = simplifyNode(n, var_bound, tnn, model_replace_f, visited); |
214 |
78 |
ret = theory::Rewriter::rewrite(ret); |
215 |
156 |
return ret; |
216 |
|
} |
217 |
|
|
218 |
20 |
void SortInference::getNewAssertions(std::vector<Node>& new_asserts) |
219 |
|
{ |
220 |
20 |
NodeManager* nm = NodeManager::currentNM(); |
221 |
|
// now, ensure constants are distinct |
222 |
22 |
for (const std::pair<const TypeNode, std::map<Node, Node> >& cm : d_const_map) |
223 |
|
{ |
224 |
4 |
std::vector<Node> consts; |
225 |
4 |
for (const std::pair<const Node, Node>& c : cm.second) |
226 |
|
{ |
227 |
2 |
Assert(c.first.isConst()); |
228 |
2 |
consts.push_back(c.second); |
229 |
|
} |
230 |
|
// add lemma enforcing introduced constants to be distinct |
231 |
2 |
if (consts.size() > 1) |
232 |
|
{ |
233 |
|
Node distinct_const = nm->mkNode(kind::DISTINCT, consts); |
234 |
|
Trace("sort-inference-rewrite") |
235 |
|
<< "Add the constant distinctness lemma: " << std::endl; |
236 |
|
Trace("sort-inference-rewrite") << " " << distinct_const << std::endl; |
237 |
|
new_asserts.push_back(distinct_const); |
238 |
|
} |
239 |
|
} |
240 |
|
|
241 |
|
// enforce constraints based on monotonicity |
242 |
20 |
Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl; |
243 |
|
|
244 |
24 |
for (const std::pair<const TypeNode, std::vector<int> >& tss : |
245 |
20 |
d_type_sub_sorts) |
246 |
|
{ |
247 |
24 |
int nmonSort = -1; |
248 |
24 |
unsigned nsorts = tss.second.size(); |
249 |
46 |
for (unsigned i = 0; i < nsorts; i++) |
250 |
|
{ |
251 |
78 |
if (d_non_monotonic_sorts.find(tss.second[i]) |
252 |
78 |
!= d_non_monotonic_sorts.end()) |
253 |
|
{ |
254 |
4 |
nmonSort = tss.second[i]; |
255 |
4 |
break; |
256 |
|
} |
257 |
|
} |
258 |
24 |
if (nmonSort != -1) |
259 |
|
{ |
260 |
8 |
std::vector<Node> injections; |
261 |
8 |
TypeNode base_tn = getOrCreateTypeForId(nmonSort, tss.first); |
262 |
10 |
for (unsigned i = 0; i < nsorts; i++) |
263 |
|
{ |
264 |
6 |
if (tss.second[i] != nmonSort) |
265 |
|
{ |
266 |
4 |
TypeNode new_tn = getOrCreateTypeForId(tss.second[i], tss.first); |
267 |
|
// make injection to nmonSort |
268 |
4 |
Node a1 = mkInjection(new_tn, base_tn); |
269 |
2 |
injections.push_back(a1); |
270 |
6 |
if (d_non_monotonic_sorts.find(tss.second[i]) |
271 |
6 |
!= d_non_monotonic_sorts.end()) |
272 |
|
{ |
273 |
|
// also must make injection from nmonSort to this |
274 |
|
Node a2 = mkInjection(base_tn, new_tn); |
275 |
|
injections.push_back(a2); |
276 |
|
} |
277 |
|
} |
278 |
|
} |
279 |
4 |
if (Trace.isOn("sort-inference-rewrite")) |
280 |
|
{ |
281 |
|
Trace("sort-inference-rewrite") |
282 |
|
<< "Add the following injections for " << tss.first |
283 |
|
<< " to ensure consistency wrt non-monotonic sorts : " << std::endl; |
284 |
|
for (const Node& i : injections) |
285 |
|
{ |
286 |
|
Trace("sort-inference-rewrite") << " " << i << std::endl; |
287 |
|
} |
288 |
|
} |
289 |
4 |
new_asserts.insert( |
290 |
8 |
new_asserts.end(), injections.begin(), injections.end()); |
291 |
|
} |
292 |
|
} |
293 |
20 |
Trace("sort-inference-proc") << "...done" << std::endl; |
294 |
|
// no sub-sort information is stored |
295 |
20 |
reset(); |
296 |
20 |
Trace("sort-inference-debug") << "Finished sort inference" << std::endl; |
297 |
20 |
} |
298 |
|
|
299 |
4 |
void SortInference::computeMonotonicity(const std::vector<Node>& assertions) |
300 |
|
{ |
301 |
8 |
std::map<Node, std::map<int, bool> > visitedmt; |
302 |
8 |
Trace("sort-inference-proc") |
303 |
4 |
<< "Calculating monotonicty for types..." << std::endl; |
304 |
18 |
for (const Node& a : assertions) |
305 |
|
{ |
306 |
28 |
Trace("sort-inference-debug") |
307 |
14 |
<< "Process type monotonicity for " << a << std::endl; |
308 |
28 |
std::map<Node, Node> var_bound; |
309 |
14 |
processMonotonic(a, true, true, var_bound, visitedmt, true); |
310 |
|
} |
311 |
4 |
Trace("sort-inference-proc") << "...done" << std::endl; |
312 |
4 |
} |
313 |
|
|
314 |
338 |
void SortInference::setEqual( int t1, int t2 ){ |
315 |
338 |
if( t1!=t2 ){ |
316 |
212 |
int rt1 = d_type_union_find.getRepresentative( t1 ); |
317 |
212 |
int rt2 = d_type_union_find.getRepresentative( t2 ); |
318 |
212 |
if( rt1!=rt2 ){ |
319 |
132 |
Trace("sort-inference-debug") << "Set equal : "; |
320 |
132 |
printSort( "sort-inference-debug", rt1 ); |
321 |
132 |
Trace("sort-inference-debug") << " "; |
322 |
132 |
printSort( "sort-inference-debug", rt2 ); |
323 |
132 |
Trace("sort-inference-debug") << std::endl; |
324 |
|
/* |
325 |
|
d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() ); |
326 |
|
d_type_eq_class[rt2].clear(); |
327 |
|
Trace("sort-inference-debug") << "EqClass : { "; |
328 |
|
for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){ |
329 |
|
Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", "; |
330 |
|
} |
331 |
|
Trace("sort-inference-debug") << "}" << std::endl; |
332 |
|
*/ |
333 |
132 |
if( rt2>rt1 ){ |
334 |
|
//swap |
335 |
56 |
int swap = rt1; |
336 |
56 |
rt1 = rt2; |
337 |
56 |
rt2 = swap; |
338 |
|
} |
339 |
132 |
std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 ); |
340 |
132 |
if( it1!=d_type_types.end() ){ |
341 |
14 |
if( d_type_types.find( rt2 )==d_type_types.end() ){ |
342 |
14 |
d_type_types[rt2] = it1->second; |
343 |
14 |
d_type_types.erase( rt1 ); |
344 |
|
}else{ |
345 |
|
Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl; |
346 |
|
return; |
347 |
|
} |
348 |
|
} |
349 |
132 |
d_type_union_find.d_eqc[rt1] = rt2; |
350 |
|
} |
351 |
|
} |
352 |
|
} |
353 |
|
|
354 |
262 |
int SortInference::getIdForType( TypeNode tn ){ |
355 |
|
//register the return type |
356 |
262 |
std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn ); |
357 |
262 |
if( it==d_id_for_types.end() ){ |
358 |
38 |
int sc = d_sortCount; |
359 |
38 |
d_type_types[d_sortCount] = tn; |
360 |
38 |
d_id_for_types[tn] = d_sortCount; |
361 |
38 |
d_sortCount++; |
362 |
38 |
return sc; |
363 |
|
}else{ |
364 |
224 |
return it->second; |
365 |
|
} |
366 |
|
} |
367 |
|
|
368 |
382 |
int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited ){ |
369 |
382 |
std::map< Node, int >::iterator itv = visited.find( n ); |
370 |
382 |
if( itv!=visited.end() ){ |
371 |
76 |
return itv->second; |
372 |
|
}else{ |
373 |
|
//add to variable bindings |
374 |
306 |
bool use_new_visited = false; |
375 |
612 |
std::map< Node, int > new_visited; |
376 |
306 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
377 |
10 |
if( d_var_types.find( n )!=d_var_types.end() ){ |
378 |
|
return getIdForType( n.getType() ); |
379 |
|
}else{ |
380 |
|
//apply sort inference to quantified variables |
381 |
30 |
for( size_t i=0; i<n[0].getNumChildren(); i++ ){ |
382 |
40 |
TypeNode nitn = n[0][i].getType(); |
383 |
20 |
if( !nitn.isSort() ) |
384 |
|
{ |
385 |
|
// If the variable is of an interpreted sort, we assume the |
386 |
|
// the sort of the variable will stay the same sort. |
387 |
6 |
d_var_types[n][n[0][i]] = getIdForType( nitn ); |
388 |
|
} |
389 |
|
else |
390 |
|
{ |
391 |
|
// If it is of an uninterpreted sort, infer subsorts. |
392 |
14 |
d_var_types[n][n[0][i]] = d_sortCount; |
393 |
14 |
d_sortCount++; |
394 |
|
} |
395 |
20 |
var_bound[ n[0][i] ] = n; |
396 |
|
} |
397 |
|
} |
398 |
10 |
use_new_visited = true; |
399 |
|
} |
400 |
|
|
401 |
|
//process children |
402 |
612 |
std::vector< Node > children; |
403 |
612 |
std::vector< int > child_types; |
404 |
620 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
405 |
314 |
bool processChild = true; |
406 |
314 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
407 |
20 |
processChild = |
408 |
20 |
options::userPatternsQuant() == options::UserPatMode::IGNORE |
409 |
20 |
? i == 1 |
410 |
|
: i >= 1; |
411 |
|
} |
412 |
314 |
if( processChild ){ |
413 |
304 |
children.push_back( n[i] ); |
414 |
304 |
child_types.push_back( process( n[i], var_bound, use_new_visited ? new_visited : visited ) ); |
415 |
|
} |
416 |
|
} |
417 |
|
|
418 |
|
//remove from variable bindings |
419 |
306 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
420 |
|
//erase from variable bound |
421 |
30 |
for( size_t i=0; i<n[0].getNumChildren(); i++ ){ |
422 |
20 |
var_bound.erase( n[0][i] ); |
423 |
|
} |
424 |
|
} |
425 |
306 |
Trace("sort-inference-debug") << "...Process " << n << std::endl; |
426 |
|
|
427 |
|
int retType; |
428 |
306 |
if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){ |
429 |
54 |
Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl; |
430 |
|
//if original types are mixed (e.g. Int/Real), don't commit type equality in either direction |
431 |
54 |
if( n[0].getType()!=n[1].getType() ){ |
432 |
|
//for now, assume the original types |
433 |
12 |
for( unsigned i=0; i<2; i++ ){ |
434 |
8 |
int ct = getIdForType( n[i].getType() ); |
435 |
8 |
setEqual( child_types[i], ct ); |
436 |
|
} |
437 |
|
}else{ |
438 |
|
//we only require that the left and right hand side must be equal |
439 |
50 |
setEqual( child_types[0], child_types[1] ); |
440 |
|
} |
441 |
54 |
d_equality_types[n] = child_types[0]; |
442 |
54 |
retType = getIdForType( n.getType() ); |
443 |
|
} |
444 |
252 |
else if (isHandledApplyUf(n.getKind())) |
445 |
|
{ |
446 |
136 |
Node op = n.getOperator(); |
447 |
136 |
TypeNode tn_op = op.getType(); |
448 |
68 |
if( d_op_return_types.find( op )==d_op_return_types.end() ){ |
449 |
14 |
if( n.getType().isBoolean() ){ |
450 |
|
//use booleans |
451 |
|
d_op_return_types[op] = getIdForType( n.getType() ); |
452 |
|
}else{ |
453 |
|
//assign arbitrary sort for return type |
454 |
14 |
d_op_return_types[op] = d_sortCount; |
455 |
14 |
d_sortCount++; |
456 |
|
} |
457 |
|
// d_type_eq_class[d_sortCount].push_back( op ); |
458 |
|
// assign arbitrary sort for argument types |
459 |
30 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
460 |
16 |
d_op_arg_types[op].push_back(d_sortCount); |
461 |
16 |
d_sortCount++; |
462 |
|
} |
463 |
|
} |
464 |
166 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
465 |
|
//the argument of the operator must match the return type of the subterm |
466 |
98 |
if( n[i].getType()!=tn_op[i] ){ |
467 |
|
//if type mismatch, assume original types |
468 |
6 |
Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType(); |
469 |
6 |
Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl; |
470 |
6 |
int ct1 = getIdForType( n[i].getType() ); |
471 |
6 |
setEqual( child_types[i], ct1 ); |
472 |
6 |
int ct2 = getIdForType( tn_op[i] ); |
473 |
6 |
setEqual( d_op_arg_types[op][i], ct2 ); |
474 |
|
}else{ |
475 |
92 |
setEqual( child_types[i], d_op_arg_types[op][i] ); |
476 |
|
} |
477 |
|
} |
478 |
|
//return type is the return type |
479 |
68 |
retType = d_op_return_types[op]; |
480 |
|
}else{ |
481 |
184 |
std::map< Node, Node >::iterator it = var_bound.find( n ); |
482 |
184 |
if( it!=var_bound.end() ){ |
483 |
20 |
Trace("sort-inference-debug") << n << " is a bound variable." << std::endl; |
484 |
|
//the return type was specified while binding |
485 |
20 |
retType = d_var_types[it->second][n]; |
486 |
164 |
}else if( n.isVar() ){ |
487 |
48 |
Trace("sort-inference-debug") << n << " is a variable." << std::endl; |
488 |
48 |
if( d_op_return_types.find( n )==d_op_return_types.end() ){ |
489 |
|
//assign arbitrary sort |
490 |
46 |
d_op_return_types[n] = d_sortCount; |
491 |
46 |
d_sortCount++; |
492 |
|
// d_type_eq_class[d_sortCount].push_back( n ); |
493 |
|
} |
494 |
48 |
retType = d_op_return_types[n]; |
495 |
116 |
}else if( n.isConst() ){ |
496 |
52 |
Trace("sort-inference-debug") << n << " is a constant." << std::endl; |
497 |
|
//can be any type we want |
498 |
52 |
retType = d_sortCount; |
499 |
52 |
d_sortCount++; |
500 |
|
}else{ |
501 |
64 |
Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl; |
502 |
|
//it is an interpreted term |
503 |
162 |
for( size_t i=0; i<children.size(); i++ ){ |
504 |
98 |
Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl; |
505 |
|
//must enforce the actual type of the operator on the children |
506 |
98 |
int ct = getIdForType( children[i].getType() ); |
507 |
98 |
setEqual( child_types[i], ct ); |
508 |
|
} |
509 |
|
//return type must be the actual return type |
510 |
64 |
retType = getIdForType( n.getType() ); |
511 |
|
} |
512 |
|
} |
513 |
306 |
Trace("sort-inference-debug") << "...Type( " << n << " ) = "; |
514 |
306 |
printSort("sort-inference-debug", retType ); |
515 |
306 |
Trace("sort-inference-debug") << std::endl; |
516 |
306 |
visited[n] = retType; |
517 |
306 |
return retType; |
518 |
|
} |
519 |
|
} |
520 |
|
|
521 |
928 |
void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map< Node, std::map< int, bool > >& visited, bool typeMode ) { |
522 |
928 |
int pindex = hasPol ? ( pol ? 1 : -1 ) : 0; |
523 |
928 |
if( visited[n].find( pindex )==visited[n].end() ){ |
524 |
708 |
visited[n][pindex] = true; |
525 |
708 |
Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl; |
526 |
708 |
if( n.getKind()==kind::FORALL ){ |
527 |
|
//only consider variables universally if it is possible this quantified formula is asserted positively |
528 |
36 |
if( !hasPol || pol ){ |
529 |
50 |
for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ |
530 |
30 |
var_bound[n[0][i]] = n; |
531 |
|
} |
532 |
|
} |
533 |
36 |
processMonotonic( n[1], pol, hasPol, var_bound, visited, typeMode ); |
534 |
36 |
if( !hasPol || pol ){ |
535 |
50 |
for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ |
536 |
30 |
var_bound.erase( n[0][i] ); |
537 |
|
} |
538 |
|
} |
539 |
72 |
return; |
540 |
672 |
}else if( n.getKind()==kind::EQUAL ){ |
541 |
124 |
if( !hasPol || pol ){ |
542 |
262 |
for( unsigned i=0; i<2; i++ ){ |
543 |
176 |
if( var_bound.find( n[i] )!=var_bound.end() ){ |
544 |
4 |
if( !typeMode ){ |
545 |
4 |
int sid = getSortId( var_bound[n[i]], n[i] ); |
546 |
4 |
d_non_monotonic_sorts[sid] = true; |
547 |
|
}else{ |
548 |
|
d_non_monotonic_sorts_orig[n[i].getType()] = true; |
549 |
|
} |
550 |
4 |
break; |
551 |
|
} |
552 |
|
} |
553 |
|
} |
554 |
|
} |
555 |
1472 |
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
556 |
|
bool npol; |
557 |
|
bool nhasPol; |
558 |
800 |
theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol ); |
559 |
800 |
processMonotonic( n[i], npol, nhasPol, var_bound, visited, typeMode ); |
560 |
|
} |
561 |
|
} |
562 |
|
} |
563 |
|
|
564 |
|
|
565 |
254 |
TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){ |
566 |
254 |
int rt = d_type_union_find.getRepresentative( t ); |
567 |
254 |
if( d_type_types.find( rt )!=d_type_types.end() ){ |
568 |
244 |
return d_type_types[rt]; |
569 |
|
}else{ |
570 |
20 |
TypeNode retType; |
571 |
|
// See if we can assign pref. This is an optimization for reusing an |
572 |
|
// uninterpreted sort as the first subsort, so that fewer symbols needed |
573 |
|
// to be rewritten in the sort-inferred signature. Notice we only assign |
574 |
|
// pref here if it is an uninterpreted sort. |
575 |
30 |
if (!pref.isNull() && d_id_for_types.find(pref) == d_id_for_types.end() |
576 |
16 |
&& pref.isSort()) |
577 |
|
{ |
578 |
2 |
retType = pref; |
579 |
|
}else{ |
580 |
|
//must create new type |
581 |
16 |
std::stringstream ss; |
582 |
8 |
ss << "it_" << t << "_" << pref; |
583 |
8 |
retType = NodeManager::currentNM()->mkSort(ss.str()); |
584 |
|
} |
585 |
10 |
Trace("sort-inference") << "-> Make type " << retType << " to correspond to "; |
586 |
10 |
printSort("sort-inference", t ); |
587 |
10 |
Trace("sort-inference") << std::endl; |
588 |
10 |
d_id_for_types[ retType ] = rt; |
589 |
10 |
d_type_types[ rt ] = retType; |
590 |
10 |
return retType; |
591 |
|
} |
592 |
|
} |
593 |
|
|
594 |
98 |
TypeNode SortInference::getTypeForId( int t ){ |
595 |
98 |
int rt = d_type_union_find.getRepresentative( t ); |
596 |
98 |
if( d_type_types.find( rt )!=d_type_types.end() ){ |
597 |
98 |
return d_type_types[rt]; |
598 |
|
}else{ |
599 |
|
return TypeNode::null(); |
600 |
|
} |
601 |
|
} |
602 |
|
|
603 |
124 |
Node SortInference::getNewSymbol( Node old, TypeNode tn ){ |
604 |
124 |
NodeManager* nm = NodeManager::currentNM(); |
605 |
124 |
SkolemManager* sm = nm->getSkolemManager(); |
606 |
|
// if no sort was inferred for this node, return original |
607 |
124 |
if( tn.isNull() || tn.isComparableTo( old.getType() ) ){ |
608 |
102 |
return old; |
609 |
22 |
}else if( old.isConst() ){ |
610 |
|
//must make constant of type tn |
611 |
2 |
if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ |
612 |
4 |
std::stringstream ss; |
613 |
2 |
ss << "ic_" << tn << "_" << old; |
614 |
6 |
d_const_map[tn][old] = sm->mkDummySkolem( |
615 |
4 |
ss.str(), |
616 |
|
tn, |
617 |
|
"constant created during sort inference"); // use mkConst??? |
618 |
|
} |
619 |
2 |
return d_const_map[tn][ old ]; |
620 |
20 |
}else if( old.getKind()==kind::BOUND_VARIABLE ){ |
621 |
12 |
std::stringstream ss; |
622 |
6 |
ss << "b_" << old; |
623 |
6 |
return nm->mkBoundVar(ss.str(), tn); |
624 |
|
} |
625 |
28 |
std::stringstream ss; |
626 |
14 |
ss << "i_" << old; |
627 |
14 |
return sm->mkDummySkolem(ss.str(), tn, "created during sort inference"); |
628 |
|
} |
629 |
|
|
630 |
382 |
Node SortInference::simplifyNode( |
631 |
|
Node n, |
632 |
|
std::map<Node, Node>& var_bound, |
633 |
|
TypeNode tnn, |
634 |
|
std::map<Node, Node>& model_replace_f, |
635 |
|
std::map<Node, std::map<TypeNode, Node> >& visited) |
636 |
|
{ |
637 |
382 |
std::map< TypeNode, Node >::iterator itv = visited[n].find( tnn ); |
638 |
382 |
if( itv!=visited[n].end() ){ |
639 |
68 |
return itv->second; |
640 |
|
}else{ |
641 |
314 |
NodeManager* nm = NodeManager::currentNM(); |
642 |
314 |
SkolemManager* sm = nm->getSkolemManager(); |
643 |
314 |
Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl; |
644 |
628 |
std::vector< Node > children; |
645 |
628 |
std::map< Node, std::map< TypeNode, Node > > new_visited; |
646 |
314 |
bool use_new_visited = false; |
647 |
314 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
648 |
|
//recreate based on types of variables |
649 |
20 |
std::vector< Node > new_children; |
650 |
30 |
for( size_t i=0; i<n[0].getNumChildren(); i++ ){ |
651 |
40 |
TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() ); |
652 |
40 |
Node v = getNewSymbol( n[0][i], tn ); |
653 |
20 |
Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl; |
654 |
20 |
new_children.push_back( v ); |
655 |
20 |
var_bound[ n[0][i] ] = v; |
656 |
|
} |
657 |
10 |
children.push_back(nm->mkNode(n[0].getKind(), new_children)); |
658 |
10 |
use_new_visited = true; |
659 |
|
} |
660 |
|
|
661 |
|
//process children |
662 |
314 |
if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ |
663 |
72 |
children.push_back( n.getOperator() ); |
664 |
|
} |
665 |
628 |
Node op; |
666 |
314 |
if( n.hasOperator() ){ |
667 |
186 |
op = n.getOperator(); |
668 |
|
} |
669 |
314 |
bool childChanged = false; |
670 |
628 |
TypeNode tnnc; |
671 |
628 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
672 |
314 |
bool processChild = true; |
673 |
314 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
674 |
20 |
processChild = |
675 |
20 |
options::userPatternsQuant() == options::UserPatMode::IGNORE |
676 |
40 |
? i == 1 |
677 |
20 |
: i >= 1; |
678 |
|
} |
679 |
314 |
if( processChild ){ |
680 |
304 |
if (isHandledApplyUf(n.getKind())) |
681 |
|
{ |
682 |
98 |
Assert(d_op_arg_types.find(op) != d_op_arg_types.end()); |
683 |
98 |
tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); |
684 |
98 |
Assert(!tnnc.isNull()); |
685 |
|
} |
686 |
540 |
else if (n.getKind() == kind::EQUAL && !n[0].getType().isBoolean() |
687 |
520 |
&& i == 0) |
688 |
|
{ |
689 |
54 |
Assert(d_equality_types.find(n) != d_equality_types.end()); |
690 |
54 |
tnnc = getOrCreateTypeForId( d_equality_types[n], n[0].getType() ); |
691 |
54 |
Assert(!tnnc.isNull()); |
692 |
|
} |
693 |
|
Node nc = simplifyNode(n[i], |
694 |
|
var_bound, |
695 |
|
tnnc, |
696 |
|
model_replace_f, |
697 |
608 |
use_new_visited ? new_visited : visited); |
698 |
304 |
Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl; |
699 |
304 |
children.push_back( nc ); |
700 |
304 |
childChanged = childChanged || nc!=n[i]; |
701 |
|
} |
702 |
|
} |
703 |
|
|
704 |
|
//remove from variable bindings |
705 |
628 |
Node ret; |
706 |
314 |
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ |
707 |
|
//erase from variable bound |
708 |
30 |
for( size_t i=0; i<n[0].getNumChildren(); i++ ){ |
709 |
20 |
Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl; |
710 |
20 |
var_bound.erase( n[0][i] ); |
711 |
|
} |
712 |
10 |
ret = nm->mkNode(n.getKind(), children); |
713 |
304 |
}else if( n.getKind()==kind::EQUAL ){ |
714 |
128 |
TypeNode tn1 = children[0].getType(); |
715 |
128 |
TypeNode tn2 = children[1].getType(); |
716 |
64 |
if( !tn1.isComparableTo( tn2 ) ){ |
717 |
|
Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl; |
718 |
|
Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; |
719 |
|
Assert(false); |
720 |
|
} |
721 |
64 |
ret = nm->mkNode(kind::EQUAL, children); |
722 |
|
} |
723 |
240 |
else if (isHandledApplyUf(n.getKind())) |
724 |
|
{ |
725 |
68 |
if( d_symbol_map.find( op )==d_symbol_map.end() ){ |
726 |
|
//make the new operator if necessary |
727 |
14 |
bool opChanged = false; |
728 |
28 |
std::vector< TypeNode > argTypes; |
729 |
30 |
for( size_t i=0; i<n.getNumChildren(); i++ ){ |
730 |
32 |
TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); |
731 |
16 |
argTypes.push_back( tn ); |
732 |
16 |
if( tn!=n[i].getType() ){ |
733 |
4 |
opChanged = true; |
734 |
|
} |
735 |
|
} |
736 |
28 |
TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() ); |
737 |
14 |
if( retType!=n.getType() ){ |
738 |
6 |
opChanged = true; |
739 |
|
} |
740 |
14 |
if( opChanged ){ |
741 |
20 |
std::stringstream ss; |
742 |
10 |
ss << "io_" << op; |
743 |
20 |
TypeNode typ = nm->mkFunctionType(argTypes, retType); |
744 |
30 |
d_symbol_map[op] = sm->mkDummySkolem( |
745 |
20 |
ss.str(), typ, "op created during sort inference"); |
746 |
10 |
Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; |
747 |
10 |
model_replace_f[op] = d_symbol_map[op]; |
748 |
|
}else{ |
749 |
4 |
d_symbol_map[op] = op; |
750 |
|
} |
751 |
|
} |
752 |
68 |
children[0] = d_symbol_map[op]; |
753 |
|
// make sure all children have been given proper types |
754 |
166 |
for (size_t i = 0, size = n.getNumChildren(); i < size; i++) |
755 |
|
{ |
756 |
196 |
TypeNode tn = children[i+1].getType(); |
757 |
196 |
TypeNode tna = getTypeForId( d_op_arg_types[op][i] ); |
758 |
98 |
if (!tn.isSubtypeOf(tna)) |
759 |
|
{ |
760 |
|
Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl; |
761 |
|
Assert(false); |
762 |
|
} |
763 |
|
} |
764 |
68 |
ret = nm->mkNode(kind::APPLY_UF, children); |
765 |
|
}else{ |
766 |
172 |
std::map< Node, Node >::iterator it = var_bound.find( n ); |
767 |
172 |
if( it!=var_bound.end() ){ |
768 |
22 |
ret = it->second; |
769 |
150 |
}else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){ |
770 |
48 |
if( d_symbol_map.find( n )==d_symbol_map.end() ){ |
771 |
92 |
TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() ); |
772 |
46 |
d_symbol_map[n] = getNewSymbol( n, tn ); |
773 |
|
} |
774 |
48 |
ret = d_symbol_map[n]; |
775 |
102 |
}else if( n.isConst() ){ |
776 |
|
//type is determined by context |
777 |
58 |
ret = getNewSymbol( n, tnn ); |
778 |
44 |
}else if( childChanged ){ |
779 |
24 |
ret = nm->mkNode(n.getKind(), children); |
780 |
|
}else{ |
781 |
20 |
ret = n; |
782 |
|
} |
783 |
|
} |
784 |
314 |
visited[n][tnn] = ret; |
785 |
314 |
return ret; |
786 |
|
} |
787 |
|
} |
788 |
|
|
789 |
2 |
Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { |
790 |
2 |
NodeManager* nm = NodeManager::currentNM(); |
791 |
2 |
SkolemManager* sm = nm->getSkolemManager(); |
792 |
4 |
std::vector< TypeNode > tns; |
793 |
2 |
tns.push_back( tn1 ); |
794 |
4 |
TypeNode typ = nm->mkFunctionType(tns, tn2); |
795 |
|
Node f = |
796 |
4 |
sm->mkDummySkolem("inj", typ, "injection for monotonicity constraint"); |
797 |
2 |
Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; |
798 |
4 |
Node v1 = nm->mkBoundVar("?x", tn1); |
799 |
4 |
Node v2 = nm->mkBoundVar("?y", tn1); |
800 |
|
Node ret = |
801 |
|
nm->mkNode(kind::FORALL, |
802 |
4 |
nm->mkNode(kind::BOUND_VAR_LIST, v1, v2), |
803 |
8 |
nm->mkNode(kind::OR, |
804 |
4 |
nm->mkNode(kind::APPLY_UF, f, v1) |
805 |
4 |
.eqNode(nm->mkNode(kind::APPLY_UF, f, v2)) |
806 |
4 |
.negate(), |
807 |
10 |
v1.eqNode(v2))); |
808 |
2 |
ret = theory::Rewriter::rewrite( ret ); |
809 |
4 |
return ret; |
810 |
|
} |
811 |
|
|
812 |
96 |
int SortInference::getSortId( Node n ) { |
813 |
192 |
Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n; |
814 |
96 |
if( d_op_return_types.find( op )!=d_op_return_types.end() ){ |
815 |
|
return d_type_union_find.getRepresentative( d_op_return_types[op] ); |
816 |
|
}else{ |
817 |
96 |
return 0; |
818 |
|
} |
819 |
|
} |
820 |
|
|
821 |
4 |
int SortInference::getSortId( Node f, Node v ) { |
822 |
4 |
if( d_var_types.find( f )!=d_var_types.end() ){ |
823 |
4 |
return d_type_union_find.getRepresentative( d_var_types[f][v] ); |
824 |
|
}else{ |
825 |
|
return 0; |
826 |
|
} |
827 |
|
} |
828 |
|
|
829 |
|
void SortInference::setSkolemVar( Node f, Node v, Node sk ){ |
830 |
|
Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl; |
831 |
|
if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){ |
832 |
|
//calculate the sort for variables if not done so already |
833 |
|
std::map< Node, Node > var_bound; |
834 |
|
std::map< Node, int > visited; |
835 |
|
process( f, var_bound, visited ); |
836 |
|
} |
837 |
|
d_op_return_types[sk] = getSortId( f, v ); |
838 |
|
Trace("sort-inference-temp") << "Set skolem sort id for " << sk << " to " << d_op_return_types[sk] << std::endl; |
839 |
|
} |
840 |
|
|
841 |
|
bool SortInference::isWellSortedFormula( Node n ) { |
842 |
|
if (n.getType().isBoolean() && !isHandledApplyUf(n.getKind())) |
843 |
|
{ |
844 |
|
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
845 |
|
if( !isWellSortedFormula( n[i] ) ){ |
846 |
|
return false; |
847 |
|
} |
848 |
|
} |
849 |
|
return true; |
850 |
|
}else{ |
851 |
|
return isWellSorted( n ); |
852 |
|
} |
853 |
|
} |
854 |
|
|
855 |
|
bool SortInference::isWellSorted( Node n ) { |
856 |
|
if( getSortId( n )==0 ){ |
857 |
|
return false; |
858 |
|
}else{ |
859 |
|
if (isHandledApplyUf(n.getKind())) |
860 |
|
{ |
861 |
|
for( unsigned i=0; i<n.getNumChildren(); i++ ){ |
862 |
|
int s1 = getSortId( n[i] ); |
863 |
|
int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ); |
864 |
|
if( s1!=s2 ){ |
865 |
|
return false; |
866 |
|
} |
867 |
|
if( !isWellSorted( n[i] ) ){ |
868 |
|
return false; |
869 |
|
} |
870 |
|
} |
871 |
|
} |
872 |
|
return true; |
873 |
|
} |
874 |
|
} |
875 |
|
|
876 |
|
bool SortInference::isMonotonic( TypeNode tn ) { |
877 |
|
Assert(tn.isSort()); |
878 |
|
return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end(); |
879 |
|
} |
880 |
|
|
881 |
796 |
bool SortInference::isHandledApplyUf(Kind k) const |
882 |
|
{ |
883 |
796 |
return k == APPLY_UF && !options::ufHo(); |
884 |
|
} |
885 |
|
|
886 |
|
} // namespace theory |
887 |
28194 |
} // namespace cvc5 |