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