dbd1dcd16593613cbfed7871320a221d89b5750b
1 /********************* */
2 /*! \file sort_inference.cpp
4 ** Original author: Andrew Reynolds
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Kshitij Bansal
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 Sort inference module
14 ** This class implements sort inference, based on a simple algorithm:
15 ** First, we assume all functions and predicates have distinct uninterpreted types.
16 ** One pass is made through the input assertions, while a union-find data structure
17 ** maintains necessary information regarding constraints on these types.
22 #include "util/sort_inference.h"
23 #include "theory/uf/options.h"
24 #include "smt/options.h"
25 #include "theory/rewriter.h"
26 #include "theory/quantifiers/options.h"
33 void SortInference::UnionFind::print(const char * c
){
34 for( std::map
< int, int >::iterator it
= d_eqc
.begin(); it
!= d_eqc
.end(); ++it
){
35 Trace(c
) << "s_" << it
->first
<< " = s_" << it
->second
<< ", ";
37 for( unsigned i
=0; i
<d_deq
.size(); i
++ ){
38 Trace(c
) << "s_" << d_deq
[i
].first
<< " != s_" << d_deq
[i
].second
<< ", ";
40 Trace(c
) << std::endl
;
42 void SortInference::UnionFind::set( UnionFind
& c
) {
44 for( std::map
< int, int >::iterator it
= c
.d_eqc
.begin(); it
!= c
.d_eqc
.end(); ++it
){
45 d_eqc
[ it
->first
] = it
->second
;
47 d_deq
.insert( d_deq
.end(), c
.d_deq
.begin(), c
.d_deq
.end() );
49 int SortInference::UnionFind::getRepresentative( int t
){
50 std::map
< int, int >::iterator it
= d_eqc
.find( t
);
51 if( it
==d_eqc
.end() || it
->second
==t
){
54 int rt
= getRepresentative( it
->second
);
59 void SortInference::UnionFind::setEqual( int t1
, int t2
){
61 int rt1
= getRepresentative( t1
);
62 int rt2
= getRepresentative( t2
);
70 bool SortInference::UnionFind::isValid() {
71 for( unsigned i
=0; i
<d_deq
.size(); i
++ ){
72 if( areEqual( d_deq
[i
].first
, d_deq
[i
].second
) ){
80 void SortInference::recordSubsort( TypeNode tn
, int s
){
81 s
= d_type_union_find
.getRepresentative( s
);
82 if( std::find( d_sub_sorts
.begin(), d_sub_sorts
.end(), s
)==d_sub_sorts
.end() ){
83 d_sub_sorts
.push_back( s
);
84 d_type_sub_sorts
[tn
].push_back( s
);
88 void SortInference::printSort( const char* c
, int t
){
89 int rt
= d_type_union_find
.getRepresentative( t
);
90 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
91 Trace(c
) << d_type_types
[rt
];
93 Trace(c
) << "s_" << rt
;
97 void SortInference::reset() {
99 d_non_monotonic_sorts
.clear();
100 d_type_sub_sorts
.clear();
103 d_type_union_find
.clear();
104 d_type_types
.clear();
105 d_id_for_types
.clear();
106 d_op_return_types
.clear();
107 d_op_arg_types
.clear();
110 d_symbol_map
.clear();
114 bool SortInference::simplify( std::vector
< Node
>& assertions
){
115 Trace("sort-inference") << "Calculating sort inference..." << std::endl
;
116 //process all assertions
117 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
118 Trace("sort-inference-debug") << "Process " << assertions
[i
] << std::endl
;
119 std::map
< Node
, Node
> var_bound
;
120 process( assertions
[i
], var_bound
);
122 for( std::map
< Node
, int >::iterator it
= d_op_return_types
.begin(); it
!= d_op_return_types
.end(); ++it
){
123 Trace("sort-inference") << it
->first
<< " : ";
124 TypeNode retTn
= it
->first
.getType();
125 if( !d_op_arg_types
[ it
->first
].empty() ){
126 Trace("sort-inference") << "( ";
127 for( size_t i
=0; i
<d_op_arg_types
[ it
->first
].size(); i
++ ){
128 recordSubsort( retTn
[i
], d_op_arg_types
[ it
->first
][i
] );
129 printSort( "sort-inference", d_op_arg_types
[ it
->first
][i
] );
130 Trace("sort-inference") << " ";
132 Trace("sort-inference") << ") -> ";
133 retTn
= retTn
[(int)retTn
.getNumChildren()-1];
135 recordSubsort( retTn
, it
->second
);
136 printSort( "sort-inference", it
->second
);
137 Trace("sort-inference") << std::endl
;
139 for( std::map
< Node
, std::map
< Node
, int > >::iterator it
= d_var_types
.begin(); it
!= d_var_types
.end(); ++it
){
140 Trace("sort-inference") << "Quantified formula : " << it
->first
<< " : " << std::endl
;
141 for( unsigned i
=0; i
<it
->first
[0].getNumChildren(); i
++ ){
142 recordSubsort( it
->first
[0][i
].getType(), it
->second
[it
->first
[0][i
]] );
143 printSort( "sort-inference", it
->second
[it
->first
[0][i
]] );
144 Trace("sort-inference") << std::endl
;
146 Trace("sort-inference") << std::endl
;
149 if( !options::ufssSymBreak() ){
150 bool rewritten
= false;
151 //determine monotonicity of sorts
152 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
153 Trace("sort-inference-debug") << "Process monotonicity for " << assertions
[i
] << std::endl
;
154 std::map
< Node
, Node
> var_bound
;
155 processMonotonic( assertions
[i
], true, true, var_bound
);
158 Trace("sort-inference") << "We have " << d_sub_sorts
.size() << " sub-sorts : " << std::endl
;
159 for( unsigned i
=0; i
<d_sub_sorts
.size(); i
++ ){
160 printSort( "sort-inference", d_sub_sorts
[i
] );
161 if( d_type_types
.find( d_sub_sorts
[i
] )!=d_type_types
.end() ){
162 Trace("sort-inference") << " is interpreted." << std::endl
;
163 }else if( d_non_monotonic_sorts
.find( d_sub_sorts
[i
] )==d_non_monotonic_sorts
.end() ){
164 Trace("sort-inference") << " is monotonic." << std::endl
;
166 Trace("sort-inference") << " is not monotonic." << std::endl
;
170 //simplify all assertions by introducing new symbols wherever necessary
171 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
172 Node prev
= assertions
[i
];
173 std::map
< Node
, Node
> var_bound
;
174 Trace("sort-inference-debug") << "Rewrite " << assertions
[i
] << std::endl
;
175 assertions
[i
] = simplify( assertions
[i
], var_bound
);
176 Trace("sort-inference-debug") << "Done." << std::endl
;
177 if( prev
!=assertions
[i
] ){
178 assertions
[i
] = theory::Rewriter::rewrite( assertions
[i
] );
180 Trace("sort-inference-rewrite") << prev
<< std::endl
;
181 Trace("sort-inference-rewrite") << " --> " << assertions
[i
] << std::endl
;
184 //now, ensure constants are distinct
185 for( std::map
< TypeNode
, std::map
< Node
, Node
> >::iterator it
= d_const_map
.begin(); it
!= d_const_map
.end(); ++it
){
186 std::vector
< Node
> consts
;
187 for( std::map
< Node
, Node
>::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
188 consts
.push_back( it2
->second
);
190 //TODO: add lemma enforcing introduced constants to be distinct
193 //enforce constraints based on monotonicity
194 for( std::map
< TypeNode
, std::vector
< int > >::iterator it
= d_type_sub_sorts
.begin(); it
!= d_type_sub_sorts
.end(); ++it
){
196 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
197 if( d_non_monotonic_sorts
.find( it
->second
[i
] )!=d_non_monotonic_sorts
.end() ){
198 nmonSort
= it
->second
[i
];
203 std::vector
< Node
> injections
;
204 TypeNode base_tn
= getOrCreateTypeForId( nmonSort
, it
->first
);
205 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
206 if( it
->second
[i
]!=nmonSort
){
207 TypeNode new_tn
= getOrCreateTypeForId( it
->second
[i
], it
->first
);
208 //make injection to nmonSort
209 Node a1
= mkInjection( new_tn
, base_tn
);
210 injections
.push_back( a1
);
211 if( d_non_monotonic_sorts
.find( it
->second
[i
] )!=d_non_monotonic_sorts
.end() ){
212 //also must make injection from nmonSort to this
213 Node a2
= mkInjection( base_tn
, new_tn
);
214 injections
.push_back( a2
);
218 Trace("sort-inference-rewrite") << "Add the following injections for " << it
->first
<< " to ensure consistency wrt non-monotonic sorts : " << std::endl
;
219 for( unsigned j
=0; j
<injections
.size(); j
++ ){
220 Trace("sort-inference-rewrite") << " " << injections
[j
] << std::endl
;
222 assertions
.insert( assertions
.end(), injections
.begin(), injections
.end() );
223 if( !injections
.empty() ){
228 //no sub-sort information is stored
233 else if( !options::ufssSymBreak() ){
234 //just add the unit lemmas between constants
235 std::map< TypeNode, std::map< int, Node > > constants;
236 for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
237 int rt = d_type_union_find.getRepresentative( it->second );
238 if( d_op_arg_types[ it->first ].empty() ){
239 TypeNode tn = it->first.getType();
240 if( constants[ tn ].find( rt )==constants[ tn ].end() ){
241 constants[ tn ][ rt ] = it->first;
245 //add unit lemmas for each constant
246 for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
248 for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
249 if( first_const.isNull() ){
250 first_const = it2->second;
252 Node eq = first_const.eqNode( it2->second );
253 //eq = Rewriter::rewrite( eq );
254 Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
255 assertions.push_back( eq );
261 initialSortCount
= sortCount
;
265 void SortInference::setEqual( int t1
, int t2
){
267 int rt1
= d_type_union_find
.getRepresentative( t1
);
268 int rt2
= d_type_union_find
.getRepresentative( t2
);
270 Trace("sort-inference-debug") << "Set equal : ";
271 printSort( "sort-inference-debug", rt1
);
272 Trace("sort-inference-debug") << " ";
273 printSort( "sort-inference-debug", rt2
);
274 Trace("sort-inference-debug") << std::endl
;
276 d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
277 d_type_eq_class[rt2].clear();
278 Trace("sort-inference-debug") << "EqClass : { ";
279 for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
280 Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
282 Trace("sort-inference-debug") << "}" << std::endl;
290 d_type_union_find
.d_eqc
[rt1
] = rt2
;
291 std::map
< int, TypeNode
>::iterator it1
= d_type_types
.find( rt1
);
292 if( it1
!=d_type_types
.end() ){
293 Assert( d_type_types
.find( rt2
)==d_type_types
.end() );
294 d_type_types
[rt2
] = it1
->second
;
295 d_type_types
.erase( rt1
);
301 int SortInference::getIdForType( TypeNode tn
){
302 //register the return type
303 std::map
< TypeNode
, int >::iterator it
= d_id_for_types
.find( tn
);
304 if( it
==d_id_for_types
.end() ){
306 d_type_types
[ sortCount
] = tn
;
307 d_id_for_types
[ tn
] = sortCount
;
315 int SortInference::process( Node n
, std::map
< Node
, Node
>& var_bound
){
316 Trace("sort-inference-debug") << "...Process " << n
<< std::endl
;
317 //add to variable bindings
318 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
319 if( d_var_types
.find( n
)!=d_var_types
.end() ){
320 return getIdForType( n
.getType() );
322 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
323 //apply sort inference to quantified variables
324 d_var_types
[n
][ n
[0][i
] ] = sortCount
;
327 //type of the quantified variable must be the same
328 var_bound
[ n
[0][i
] ] = n
;
334 std::vector
< Node
> children
;
335 std::vector
< int > child_types
;
336 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
337 bool processChild
= true;
338 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
339 processChild
= options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE
? i
==1 : i
>=1;
342 children
.push_back( n
[i
] );
343 child_types
.push_back( process( n
[i
], var_bound
) );
347 //remove from variable bindings
348 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
349 //erase from variable bound
350 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
351 var_bound
.erase( n
[0][i
] );
356 if( n
.getKind()==kind::EQUAL
){
357 //we only require that the left and right hand side must be equal
358 setEqual( child_types
[0], child_types
[1] );
359 //int eqType = getIdForType( n[0].getType() );
360 //setEqual( child_types[0], eqType );
361 //setEqual( child_types[1], eqType );
362 retType
= getIdForType( n
.getType() );
363 }else if( n
.getKind()==kind::APPLY_UF
){
364 Node op
= n
.getOperator();
365 if( d_op_return_types
.find( op
)==d_op_return_types
.end() ){
366 if( n
.getType().isBoolean() ){
368 d_op_return_types
[op
] = getIdForType( n
.getType() );
370 //assign arbitrary sort for return type
371 d_op_return_types
[op
] = sortCount
;
374 //d_type_eq_class[sortCount].push_back( op );
375 //assign arbitrary sort for argument types
376 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
377 d_op_arg_types
[op
].push_back( sortCount
);
381 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
382 //the argument of the operator must match the return type of the subterm
383 setEqual( child_types
[i
], d_op_arg_types
[op
][i
] );
385 //return type is the return type
386 retType
= d_op_return_types
[op
];
388 std::map
< Node
, Node
>::iterator it
= var_bound
.find( n
);
389 if( it
!=var_bound
.end() ){
390 Trace("sort-inference-debug") << n
<< " is a bound variable." << std::endl
;
391 //the return type was specified while binding
392 retType
= d_var_types
[it
->second
][n
];
393 }else if( n
.getKind() == kind::VARIABLE
|| n
.getKind()==kind::SKOLEM
){
394 Trace("sort-inference-debug") << n
<< " is a variable." << std::endl
;
395 if( d_op_return_types
.find( n
)==d_op_return_types
.end() ){
396 //assign arbitrary sort
397 d_op_return_types
[n
] = sortCount
;
399 //d_type_eq_class[sortCount].push_back( n );
401 retType
= d_op_return_types
[n
];
402 //}else if( n.isConst() ){
403 // Trace("sort-inference-debug") << n << " is a constant." << std::endl;
404 //can be any type we want
405 // retType = sortCount;
408 Trace("sort-inference-debug") << n
<< " is a interpreted symbol." << std::endl
;
409 //it is an interpretted term
410 for( size_t i
=0; i
<children
.size(); i
++ ){
411 Trace("sort-inference-debug") << children
[i
] << " forced to have " << children
[i
].getType() << std::endl
;
412 //must enforce the actual type of the operator on the children
413 int ct
= getIdForType( children
[i
].getType() );
414 setEqual( child_types
[i
], ct
);
416 //return type must be the actual return type
417 retType
= getIdForType( n
.getType() );
420 Trace("sort-inference-debug") << "...Type( " << n
<< " ) = ";
421 printSort("sort-inference-debug", retType
);
422 Trace("sort-inference-debug") << std::endl
;
426 void SortInference::processMonotonic( Node n
, bool pol
, bool hasPol
, std::map
< Node
, Node
>& var_bound
) {
427 Trace("sort-inference-debug") << "...Process monotonic " << pol
<< " " << hasPol
<< " " << n
<< std::endl
;
428 if( n
.getKind()==kind::FORALL
){
429 for( unsigned i
=0; i
<n
[0].getNumChildren(); i
++ ){
430 var_bound
[n
[0][i
]] = n
;
432 processMonotonic( n
[1], pol
, hasPol
, var_bound
);
433 for( unsigned i
=0; i
<n
[0].getNumChildren(); i
++ ){
434 var_bound
.erase( n
[0][i
] );
436 }else if( n
.getKind()==kind::EQUAL
){
437 if( !hasPol
|| pol
){
438 for( unsigned i
=0; i
<2; i
++ ){
439 if( var_bound
.find( n
[i
] )!=var_bound
.end() ){
440 int sid
= getSortId( var_bound
[n
[i
]], n
[i
] );
441 d_non_monotonic_sorts
[sid
] = true;
447 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
449 bool nhasPol
= hasPol
;
450 if( n
.getKind()==kind::NOT
|| ( n
.getKind()==kind::IMPLIES
&& i
==0 ) ){
453 if( ( n
.getKind()==kind::ITE
&& i
==0 ) || n
.getKind()==kind::XOR
|| n
.getKind()==kind::IFF
){
456 processMonotonic( n
[i
], npol
, nhasPol
, var_bound
);
461 TypeNode
SortInference::getOrCreateTypeForId( int t
, TypeNode pref
){
462 int rt
= d_type_union_find
.getRepresentative( t
);
463 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
464 return d_type_types
[rt
];
467 //see if we can assign pref
468 if( !pref
.isNull() && d_id_for_types
.find( pref
)==d_id_for_types
.end() ){
471 //must create new type
472 std::stringstream ss
;
473 ss
<< "it_" << t
<< "_" << pref
;
474 retType
= NodeManager::currentNM()->mkSort( ss
.str() );
476 Trace("sort-inference") << "-> Make type " << retType
<< " to correspond to ";
477 printSort("sort-inference", t
);
478 Trace("sort-inference") << std::endl
;
479 d_id_for_types
[ retType
] = rt
;
480 d_type_types
[ rt
] = retType
;
485 TypeNode
SortInference::getTypeForId( int t
){
486 int rt
= d_type_union_find
.getRepresentative( t
);
487 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
488 return d_type_types
[rt
];
490 return TypeNode::null();
494 Node
SortInference::getNewSymbol( Node old
, TypeNode tn
){
495 if( tn
==old
.getType() ){
497 }else if( old
.isConst() ){
498 //must make constant of type tn
499 if( d_const_map
[tn
].find( old
)==d_const_map
[tn
].end() ){
500 std::stringstream ss
;
501 ss
<< "ic_" << tn
<< "_" << old
;
502 d_const_map
[tn
][ old
] = NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "constant created during sort inference" ); //use mkConst???
504 return d_const_map
[tn
][ old
];
505 }else if( old
.getKind()==kind::BOUND_VARIABLE
){
506 std::stringstream ss
;
508 return NodeManager::currentNM()->mkBoundVar( ss
.str(), tn
);
510 std::stringstream ss
;
512 return NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "created during sort inference" );
516 Node
SortInference::simplify( Node n
, std::map
< Node
, Node
>& var_bound
){
517 Trace("sort-inference-debug2") << "Simplify " << n
<< std::endl
;
518 std::vector
< Node
> children
;
519 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
520 //recreate based on types of variables
521 std::vector
< Node
> new_children
;
522 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
523 TypeNode tn
= getOrCreateTypeForId( d_var_types
[n
][ n
[0][i
] ], n
[0][i
].getType() );
524 Node v
= getNewSymbol( n
[0][i
], tn
);
525 Trace("sort-inference-debug2") << "Map variable " << n
[0][i
] << " to " << v
<< std::endl
;
526 new_children
.push_back( v
);
527 var_bound
[ n
[0][i
] ] = v
;
529 children
.push_back( NodeManager::currentNM()->mkNode( n
[0].getKind(), new_children
) );
533 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
534 children
.push_back( n
.getOperator() );
536 bool childChanged
= false;
537 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
538 bool processChild
= true;
539 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
540 processChild
= options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE
? i
==1 : i
>=1;
543 Node nc
= simplify( n
[i
], var_bound
);
544 Trace("sort-inference-debug2") << "Simplify " << i
<< " " << n
[i
] << " returned " << nc
<< std::endl
;
545 children
.push_back( nc
);
546 childChanged
= childChanged
|| nc
!=n
[i
];
550 //remove from variable bindings
551 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
552 //erase from variable bound
553 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
554 Trace("sort-inference-debug2") << "Remove bound for " << n
[0][i
] << std::endl
;
555 var_bound
.erase( n
[0][i
] );
557 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
558 }else if( n
.getKind()==kind::EQUAL
){
559 if( children
[0].getType()!=children
[1].getType() ){
560 if( children
[0].isConst() ){
561 children
[0] = getNewSymbol( children
[0], children
[1].getType() );
562 }else if( children
[1].isConst() ){
563 children
[1] = getNewSymbol( children
[1], children
[0].getType() );
565 Trace("sort-inference-warn") << "Sort inference created bad equality: " << children
[0] << " = " << children
[1] << std::endl
;
566 Trace("sort-inference-warn") << " Types : " << children
[0].getType() << " " << children
[1].getType() << std::endl
;
570 return NodeManager::currentNM()->mkNode( kind::EQUAL
, children
);
571 }else if( n
.getKind()==kind::APPLY_UF
){
572 Node op
= n
.getOperator();
573 if( d_symbol_map
.find( op
)==d_symbol_map
.end() ){
574 //make the new operator if necessary
575 bool opChanged
= false;
576 std::vector
< TypeNode
> argTypes
;
577 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
578 TypeNode tn
= getOrCreateTypeForId( d_op_arg_types
[op
][i
], n
[i
].getType() );
579 argTypes
.push_back( tn
);
580 if( tn
!=n
[i
].getType() ){
584 TypeNode retType
= getOrCreateTypeForId( d_op_return_types
[op
], n
.getType() );
585 if( retType
!=n
.getType() ){
589 std::stringstream ss
;
591 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( argTypes
, retType
);
592 d_symbol_map
[op
] = NodeManager::currentNM()->mkSkolem( ss
.str(), typ
, "op created during sort inference" );
593 Trace("setp-model") << "Function " << op
<< " is replaced with " << d_symbol_map
[op
] << std::endl
;
594 d_model_replace_f
[op
] = d_symbol_map
[op
];
596 d_symbol_map
[op
] = op
;
599 children
[0] = d_symbol_map
[op
];
600 //make sure all children have been taken care of
601 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
602 TypeNode tn
= children
[i
+1].getType();
603 TypeNode tna
= getTypeForId( d_op_arg_types
[op
][i
] );
605 if( n
[i
].isConst() ){
606 children
[i
+1] = getNewSymbol( n
[i
], tna
);
608 Trace("sort-inference-warn") << "Sort inference created bad child: " << n
<< " " << n
[i
] << " " << tn
<< " " << tna
<< std::endl
;
613 return NodeManager::currentNM()->mkNode( kind::APPLY_UF
, children
);
615 std::map
< Node
, Node
>::iterator it
= var_bound
.find( n
);
616 if( it
!=var_bound
.end() ){
618 }else if( n
.getKind() == kind::VARIABLE
|| n
.getKind() == kind::SKOLEM
){
619 if( d_symbol_map
.find( n
)==d_symbol_map
.end() ){
620 TypeNode tn
= getOrCreateTypeForId( d_op_return_types
[n
], n
.getType() );
621 d_symbol_map
[n
] = getNewSymbol( n
, tn
);
623 return d_symbol_map
[n
];
624 }else if( n
.isConst() ){
625 //just return n, we will fix at higher scope
629 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
638 Node
SortInference::mkInjection( TypeNode tn1
, TypeNode tn2
) {
639 std::vector
< TypeNode
> tns
;
640 tns
.push_back( tn1
);
641 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( tns
, tn2
);
642 Node f
= NodeManager::currentNM()->mkSkolem( "inj", typ
, "injection for monotonicity constraint" );
643 Trace("sort-inference") << "-> Make injection " << f
<< " from " << tn1
<< " to " << tn2
<< std::endl
;
644 Node v1
= NodeManager::currentNM()->mkBoundVar( "?x", tn1
);
645 Node v2
= NodeManager::currentNM()->mkBoundVar( "?y", tn1
);
646 Node ret
= NodeManager::currentNM()->mkNode( kind::FORALL
,
647 NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST
, v1
, v2
),
648 NodeManager::currentNM()->mkNode( kind::OR
,
649 NodeManager::currentNM()->mkNode( kind::APPLY_UF
, f
, v1
).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF
, f
, v2
) ).negate(),
651 ret
= theory::Rewriter::rewrite( ret
);
655 int SortInference::getSortId( Node n
) {
656 Node op
= n
.getKind()==kind::APPLY_UF
? n
.getOperator() : n
;
657 if( d_op_return_types
.find( op
)!=d_op_return_types
.end() ){
658 return d_type_union_find
.getRepresentative( d_op_return_types
[op
] );
664 int SortInference::getSortId( Node f
, Node v
) {
665 if( d_var_types
.find( f
)!=d_var_types
.end() ){
666 return d_type_union_find
.getRepresentative( d_var_types
[f
][v
] );
672 void SortInference::setSkolemVar( Node f
, Node v
, Node sk
){
673 Trace("sort-inference-temp") << "Set skolem var for " << f
<< ", variable " << v
<< std::endl
;
674 if( isWellSortedFormula( f
) && d_var_types
.find( f
)==d_var_types
.end() ){
675 //calculate the sort for variables if not done so already
676 std::map
< Node
, Node
> var_bound
;
677 process( f
, var_bound
);
679 d_op_return_types
[sk
] = getSortId( f
, v
);
680 Trace("sort-inference-temp") << "Set skolem sort id for " << sk
<< " to " << d_op_return_types
[sk
] << std::endl
;
683 bool SortInference::isWellSortedFormula( Node n
) {
684 if( n
.getType().isBoolean() && n
.getKind()!=kind::APPLY_UF
){
685 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
686 if( !isWellSortedFormula( n
[i
] ) ){
692 return isWellSorted( n
);
696 bool SortInference::isWellSorted( Node n
) {
697 if( getSortId( n
)==0 ){
700 if( n
.getKind()==kind::APPLY_UF
){
701 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
702 int s1
= getSortId( n
[i
] );
703 int s2
= d_type_union_find
.getRepresentative( d_op_arg_types
[ n
.getOperator() ][i
] );
707 if( !isWellSorted( n
[i
] ) ){
716 void SortInference::getSortConstraints( Node n
, UnionFind
& uf
) {
717 if( n
.getKind()==kind::APPLY_UF
){
718 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
719 getSortConstraints( n
[i
], uf
);
720 uf
.setEqual( getSortId( n
[i
] ), d_type_union_find
.getRepresentative( d_op_arg_types
[ n
.getOperator() ][i
] ) );
725 }/* CVC4 namespace */