1 /********************* */
2 /*! \file sort_inference.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Paul Meng, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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.\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.
20 #include "theory/sort_inference.h"
24 #include "options/quantifiers_options.h"
25 #include "options/smt_options.h"
26 #include "options/uf_options.h"
27 #include "proof/proof_manager.h"
28 #include "theory/rewriter.h"
29 #include "theory/quantifiers/quant_util.h"
36 void SortInference::UnionFind::print(const char * c
){
37 for( std::map
< int, int >::iterator it
= d_eqc
.begin(); it
!= d_eqc
.end(); ++it
){
38 Trace(c
) << "s_" << it
->first
<< " = s_" << it
->second
<< ", ";
40 for( unsigned i
=0; i
<d_deq
.size(); i
++ ){
41 Trace(c
) << "s_" << d_deq
[i
].first
<< " != s_" << d_deq
[i
].second
<< ", ";
43 Trace(c
) << std::endl
;
45 void SortInference::UnionFind::set( UnionFind
& c
) {
47 for( std::map
< int, int >::iterator it
= c
.d_eqc
.begin(); it
!= c
.d_eqc
.end(); ++it
){
48 d_eqc
[ it
->first
] = it
->second
;
50 d_deq
.insert( d_deq
.end(), c
.d_deq
.begin(), c
.d_deq
.end() );
52 int SortInference::UnionFind::getRepresentative( int t
){
53 std::map
< int, int >::iterator it
= d_eqc
.find( t
);
54 if( it
==d_eqc
.end() || it
->second
==t
){
57 int rt
= getRepresentative( it
->second
);
62 void SortInference::UnionFind::setEqual( int t1
, int t2
){
64 int rt1
= getRepresentative( t1
);
65 int rt2
= getRepresentative( t2
);
73 bool SortInference::UnionFind::isValid() {
74 for( unsigned i
=0; i
<d_deq
.size(); i
++ ){
75 if( areEqual( d_deq
[i
].first
, d_deq
[i
].second
) ){
83 void SortInference::recordSubsort( TypeNode tn
, int s
){
84 s
= d_type_union_find
.getRepresentative( s
);
85 if( std::find( d_sub_sorts
.begin(), d_sub_sorts
.end(), s
)==d_sub_sorts
.end() ){
86 d_sub_sorts
.push_back( s
);
87 d_type_sub_sorts
[tn
].push_back( s
);
91 void SortInference::printSort( const char* c
, int t
){
92 int rt
= d_type_union_find
.getRepresentative( t
);
93 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
94 Trace(c
) << d_type_types
[rt
];
96 Trace(c
) << "s_" << rt
;
100 void SortInference::reset() {
102 d_non_monotonic_sorts
.clear();
103 d_type_sub_sorts
.clear();
106 d_type_union_find
.clear();
107 d_type_types
.clear();
108 d_id_for_types
.clear();
109 d_op_return_types
.clear();
110 d_op_arg_types
.clear();
113 d_symbol_map
.clear();
117 void SortInference::simplify( std::vector
< Node
>& assertions
, bool doSortInference
, bool doMonotonicyInference
){
118 if( doSortInference
){
119 Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl
;
120 //process all assertions
121 std::map
< Node
, int > visited
;
122 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
123 Trace("sort-inference-debug") << "Process " << assertions
[i
] << std::endl
;
124 std::map
< Node
, Node
> var_bound
;
125 process( assertions
[i
], var_bound
, visited
);
127 Trace("sort-inference-proc") << "...done" << std::endl
;
128 for( std::map
< Node
, int >::iterator it
= d_op_return_types
.begin(); it
!= d_op_return_types
.end(); ++it
){
129 Trace("sort-inference") << it
->first
<< " : ";
130 TypeNode retTn
= it
->first
.getType();
131 if( !d_op_arg_types
[ it
->first
].empty() ){
132 Trace("sort-inference") << "( ";
133 for( size_t i
=0; i
<d_op_arg_types
[ it
->first
].size(); i
++ ){
134 recordSubsort( retTn
[i
], d_op_arg_types
[ it
->first
][i
] );
135 printSort( "sort-inference", d_op_arg_types
[ it
->first
][i
] );
136 Trace("sort-inference") << " ";
138 Trace("sort-inference") << ") -> ";
139 retTn
= retTn
[(int)retTn
.getNumChildren()-1];
141 recordSubsort( retTn
, it
->second
);
142 printSort( "sort-inference", it
->second
);
143 Trace("sort-inference") << std::endl
;
145 for( std::map
< Node
, std::map
< Node
, int > >::iterator it
= d_var_types
.begin(); it
!= d_var_types
.end(); ++it
){
146 Trace("sort-inference") << "Quantified formula : " << it
->first
<< " : " << std::endl
;
147 for( unsigned i
=0; i
<it
->first
[0].getNumChildren(); i
++ ){
148 recordSubsort( it
->first
[0][i
].getType(), it
->second
[it
->first
[0][i
]] );
149 printSort( "sort-inference", it
->second
[it
->first
[0][i
]] );
150 Trace("sort-inference") << std::endl
;
152 Trace("sort-inference") << std::endl
;
155 if( !options::ufssSymBreak() ){
156 bool rewritten
= false;
157 //determine monotonicity of sorts
158 Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..." << std::endl
;
159 std::map
< Node
, std::map
< int, bool > > visited
;
160 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
161 Trace("sort-inference-debug") << "Process monotonicity for " << assertions
[i
] << std::endl
;
162 std::map
< Node
, Node
> var_bound
;
163 processMonotonic( assertions
[i
], true, true, var_bound
, visited
);
165 Trace("sort-inference-proc") << "...done" << std::endl
;
167 Trace("sort-inference") << "We have " << d_sub_sorts
.size() << " sub-sorts : " << std::endl
;
168 for( unsigned i
=0; i
<d_sub_sorts
.size(); i
++ ){
169 printSort( "sort-inference", d_sub_sorts
[i
] );
170 if( d_type_types
.find( d_sub_sorts
[i
] )!=d_type_types
.end() ){
171 Trace("sort-inference") << " is interpreted." << std::endl
;
172 }else if( d_non_monotonic_sorts
.find( d_sub_sorts
[i
] )==d_non_monotonic_sorts
.end() ){
173 Trace("sort-inference") << " is monotonic." << std::endl
;
175 Trace("sort-inference") << " is not monotonic." << std::endl
;
179 //simplify all assertions by introducing new symbols wherever necessary
180 Trace("sort-inference-proc") << "Perform simplification..." << std::endl
;
181 std::map
< Node
, std::map
< TypeNode
, Node
> > visited2
;
182 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
183 Node prev
= assertions
[i
];
184 std::map
< Node
, Node
> var_bound
;
185 Trace("sort-inference-debug") << "Simplify " << assertions
[i
] << std::endl
;
187 Node curr
= simplifyNode( assertions
[i
], var_bound
, tnn
, visited2
);
188 Trace("sort-inference-debug") << "Done." << std::endl
;
189 if( curr
!=assertions
[i
] ){
190 Trace("sort-inference-debug") << "Rewrite " << curr
<< std::endl
;
191 curr
= theory::Rewriter::rewrite( curr
);
193 Trace("sort-inference-rewrite") << assertions
<< std::endl
;
194 Trace("sort-inference-rewrite") << " --> " << curr
<< std::endl
;
195 PROOF( ProofManager::currentPM()->addDependence(curr
, assertions
[i
]); );
196 assertions
[i
] = curr
;
199 Trace("sort-inference-proc") << "...done" << std::endl
;
200 //now, ensure constants are distinct
201 for( std::map
< TypeNode
, std::map
< Node
, Node
> >::iterator it
= d_const_map
.begin(); it
!= d_const_map
.end(); ++it
){
202 std::vector
< Node
> consts
;
203 for( std::map
< Node
, Node
>::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
204 Assert( it2
->first
.isConst() );
205 consts
.push_back( it2
->second
);
207 //add lemma enforcing introduced constants to be distinct
208 if( consts
.size()>1 ){
209 Node distinct_const
= NodeManager::currentNM()->mkNode( kind::DISTINCT
, consts
);
210 Trace("sort-inference-rewrite") << "Add the constant distinctness lemma: " << std::endl
;
211 Trace("sort-inference-rewrite") << " " << distinct_const
<< std::endl
;
212 assertions
.push_back( distinct_const
);
217 //enforce constraints based on monotonicity
218 Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl
;
219 for( std::map
< TypeNode
, std::vector
< int > >::iterator it
= d_type_sub_sorts
.begin(); it
!= d_type_sub_sorts
.end(); ++it
){
221 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
222 if( d_non_monotonic_sorts
.find( it
->second
[i
] )!=d_non_monotonic_sorts
.end() ){
223 nmonSort
= it
->second
[i
];
228 std::vector
< Node
> injections
;
229 TypeNode base_tn
= getOrCreateTypeForId( nmonSort
, it
->first
);
230 for( unsigned i
=0; i
<it
->second
.size(); i
++ ){
231 if( it
->second
[i
]!=nmonSort
){
232 TypeNode new_tn
= getOrCreateTypeForId( it
->second
[i
], it
->first
);
233 //make injection to nmonSort
234 Node a1
= mkInjection( new_tn
, base_tn
);
235 injections
.push_back( a1
);
236 if( d_non_monotonic_sorts
.find( it
->second
[i
] )!=d_non_monotonic_sorts
.end() ){
237 //also must make injection from nmonSort to this
238 Node a2
= mkInjection( base_tn
, new_tn
);
239 injections
.push_back( a2
);
243 Trace("sort-inference-rewrite") << "Add the following injections for " << it
->first
<< " to ensure consistency wrt non-monotonic sorts : " << std::endl
;
244 for( unsigned j
=0; j
<injections
.size(); j
++ ){
245 Trace("sort-inference-rewrite") << " " << injections
[j
] << std::endl
;
247 assertions
.insert( assertions
.end(), injections
.begin(), injections
.end() );
248 if( !injections
.empty() ){
253 Trace("sort-inference-proc") << "...done" << std::endl
;
254 //no sub-sort information is stored
256 Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten
<< std::endl
;
258 initialSortCount
= sortCount
;
260 if( doMonotonicyInference
){
261 std::map
< Node
, std::map
< int, bool > > visited
;
262 Trace("sort-inference-proc") << "Calculating monotonicty for types..." << std::endl
;
263 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
264 Trace("sort-inference-debug") << "Process type monotonicity for " << assertions
[i
] << std::endl
;
265 std::map
< Node
, Node
> var_bound
;
266 processMonotonic( assertions
[i
], true, true, var_bound
, visited
, true );
268 Trace("sort-inference-proc") << "...done" << std::endl
;
272 void SortInference::setEqual( int t1
, int t2
){
274 int rt1
= d_type_union_find
.getRepresentative( t1
);
275 int rt2
= d_type_union_find
.getRepresentative( t2
);
277 Trace("sort-inference-debug") << "Set equal : ";
278 printSort( "sort-inference-debug", rt1
);
279 Trace("sort-inference-debug") << " ";
280 printSort( "sort-inference-debug", rt2
);
281 Trace("sort-inference-debug") << std::endl
;
283 d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
284 d_type_eq_class[rt2].clear();
285 Trace("sort-inference-debug") << "EqClass : { ";
286 for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
287 Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
289 Trace("sort-inference-debug") << "}" << std::endl;
297 std::map
< int, TypeNode
>::iterator it1
= d_type_types
.find( rt1
);
298 if( it1
!=d_type_types
.end() ){
299 if( d_type_types
.find( rt2
)==d_type_types
.end() ){
300 d_type_types
[rt2
] = it1
->second
;
301 d_type_types
.erase( rt1
);
303 Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types
[rt1
] << " and " << d_type_types
[rt2
] << std::endl
;
307 d_type_union_find
.d_eqc
[rt1
] = rt2
;
312 int SortInference::getIdForType( TypeNode tn
){
313 //register the return type
314 std::map
< TypeNode
, int >::iterator it
= d_id_for_types
.find( tn
);
315 if( it
==d_id_for_types
.end() ){
317 d_type_types
[ sortCount
] = tn
;
318 d_id_for_types
[ tn
] = sortCount
;
326 int SortInference::process( Node n
, std::map
< Node
, Node
>& var_bound
, std::map
< Node
, int >& visited
){
327 std::map
< Node
, int >::iterator itv
= visited
.find( n
);
328 if( itv
!=visited
.end() ){
331 //add to variable bindings
332 bool use_new_visited
= false;
333 std::map
< Node
, int > new_visited
;
334 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
335 if( d_var_types
.find( n
)!=d_var_types
.end() ){
336 return getIdForType( n
.getType() );
338 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
339 //apply sort inference to quantified variables
340 d_var_types
[n
][ n
[0][i
] ] = sortCount
;
343 //type of the quantified variable must be the same
344 var_bound
[ n
[0][i
] ] = n
;
347 use_new_visited
= true;
351 std::vector
< Node
> children
;
352 std::vector
< int > child_types
;
353 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
354 bool processChild
= true;
355 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
356 processChild
= options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE
? i
==1 : i
>=1;
359 children
.push_back( n
[i
] );
360 child_types
.push_back( process( n
[i
], var_bound
, use_new_visited
? new_visited
: visited
) );
364 //remove from variable bindings
365 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
366 //erase from variable bound
367 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
368 var_bound
.erase( n
[0][i
] );
371 Trace("sort-inference-debug") << "...Process " << n
<< std::endl
;
374 if( n
.getKind()==kind::EQUAL
&& !n
[0].getType().isBoolean() ){
375 Trace("sort-inference-debug") << "For equality " << n
<< ", set equal types from : " << n
[0].getType() << " " << n
[1].getType() << std::endl
;
376 //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
377 if( n
[0].getType()!=n
[1].getType() ){
378 //for now, assume the original types
379 for( unsigned i
=0; i
<2; i
++ ){
380 int ct
= getIdForType( n
[i
].getType() );
381 setEqual( child_types
[i
], ct
);
384 //we only require that the left and right hand side must be equal
385 setEqual( child_types
[0], child_types
[1] );
387 d_equality_types
[n
] = child_types
[0];
388 retType
= getIdForType( n
.getType() );
389 }else if( n
.getKind()==kind::APPLY_UF
){
390 Node op
= n
.getOperator();
391 TypeNode tn_op
= op
.getType();
392 if( d_op_return_types
.find( op
)==d_op_return_types
.end() ){
393 if( n
.getType().isBoolean() ){
395 d_op_return_types
[op
] = getIdForType( n
.getType() );
397 //assign arbitrary sort for return type
398 d_op_return_types
[op
] = sortCount
;
401 //d_type_eq_class[sortCount].push_back( op );
402 //assign arbitrary sort for argument types
403 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
404 d_op_arg_types
[op
].push_back( sortCount
);
408 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
409 //the argument of the operator must match the return type of the subterm
410 if( n
[i
].getType()!=tn_op
[i
] ){
411 //if type mismatch, assume original types
412 Trace("sort-inference-debug") << "Argument " << i
<< " of " << op
<< " " << n
[i
] << " has type " << n
[i
].getType();
413 Trace("sort-inference-debug") << ", while operator arg has type " << tn_op
[i
] << std::endl
;
414 int ct1
= getIdForType( n
[i
].getType() );
415 setEqual( child_types
[i
], ct1
);
416 int ct2
= getIdForType( tn_op
[i
] );
417 setEqual( d_op_arg_types
[op
][i
], ct2
);
419 setEqual( child_types
[i
], d_op_arg_types
[op
][i
] );
422 //return type is the return type
423 retType
= d_op_return_types
[op
];
425 std::map
< Node
, Node
>::iterator it
= var_bound
.find( n
);
426 if( it
!=var_bound
.end() ){
427 Trace("sort-inference-debug") << n
<< " is a bound variable." << std::endl
;
428 //the return type was specified while binding
429 retType
= d_var_types
[it
->second
][n
];
430 }else if( n
.getKind() == kind::VARIABLE
|| n
.getKind()==kind::SKOLEM
){
431 Trace("sort-inference-debug") << n
<< " is a variable." << std::endl
;
432 if( d_op_return_types
.find( n
)==d_op_return_types
.end() ){
433 //assign arbitrary sort
434 d_op_return_types
[n
] = sortCount
;
436 //d_type_eq_class[sortCount].push_back( n );
438 retType
= d_op_return_types
[n
];
439 }else if( n
.isConst() ){
440 Trace("sort-inference-debug") << n
<< " is a constant." << std::endl
;
441 //can be any type we want
445 Trace("sort-inference-debug") << n
<< " is a interpreted symbol." << std::endl
;
446 //it is an interpreted term
447 for( size_t i
=0; i
<children
.size(); i
++ ){
448 Trace("sort-inference-debug") << children
[i
] << " forced to have " << children
[i
].getType() << std::endl
;
449 //must enforce the actual type of the operator on the children
450 int ct
= getIdForType( children
[i
].getType() );
451 setEqual( child_types
[i
], ct
);
453 //return type must be the actual return type
454 retType
= getIdForType( n
.getType() );
457 Trace("sort-inference-debug") << "...Type( " << n
<< " ) = ";
458 printSort("sort-inference-debug", retType
);
459 Trace("sort-inference-debug") << std::endl
;
460 visited
[n
] = retType
;
465 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
) {
466 int pindex
= hasPol
? ( pol
? 1 : -1 ) : 0;
467 if( visited
[n
].find( pindex
)==visited
[n
].end() ){
468 visited
[n
][pindex
] = true;
469 Trace("sort-inference-debug") << "...Process monotonic " << pol
<< " " << hasPol
<< " " << n
<< std::endl
;
470 if( n
.getKind()==kind::FORALL
){
471 //only consider variables universally if it is possible this quantified formula is asserted positively
472 if( !hasPol
|| pol
){
473 for( unsigned i
=0; i
<n
[0].getNumChildren(); i
++ ){
474 var_bound
[n
[0][i
]] = n
;
477 processMonotonic( n
[1], pol
, hasPol
, var_bound
, visited
, typeMode
);
478 if( !hasPol
|| pol
){
479 for( unsigned i
=0; i
<n
[0].getNumChildren(); i
++ ){
480 var_bound
.erase( n
[0][i
] );
484 }else if( n
.getKind()==kind::EQUAL
){
485 if( !hasPol
|| pol
){
486 for( unsigned i
=0; i
<2; i
++ ){
487 if( var_bound
.find( n
[i
] )!=var_bound
.end() ){
489 int sid
= getSortId( var_bound
[n
[i
]], n
[i
] );
490 d_non_monotonic_sorts
[sid
] = true;
492 d_non_monotonic_sorts_orig
[n
[i
].getType()] = true;
499 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
502 theory::QuantPhaseReq::getPolarity( n
, i
, hasPol
, pol
, nhasPol
, npol
);
503 processMonotonic( n
[i
], npol
, nhasPol
, var_bound
, visited
, typeMode
);
509 TypeNode
SortInference::getOrCreateTypeForId( int t
, TypeNode pref
){
510 int rt
= d_type_union_find
.getRepresentative( t
);
511 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
512 return d_type_types
[rt
];
515 //see if we can assign pref
516 if( !pref
.isNull() && d_id_for_types
.find( pref
)==d_id_for_types
.end() ){
519 //must create new type
520 std::stringstream ss
;
521 ss
<< "it_" << t
<< "_" << pref
;
522 retType
= NodeManager::currentNM()->mkSort( ss
.str() );
524 Trace("sort-inference") << "-> Make type " << retType
<< " to correspond to ";
525 printSort("sort-inference", t
);
526 Trace("sort-inference") << std::endl
;
527 d_id_for_types
[ retType
] = rt
;
528 d_type_types
[ rt
] = retType
;
533 TypeNode
SortInference::getTypeForId( int t
){
534 int rt
= d_type_union_find
.getRepresentative( t
);
535 if( d_type_types
.find( rt
)!=d_type_types
.end() ){
536 return d_type_types
[rt
];
538 return TypeNode::null();
542 Node
SortInference::getNewSymbol( Node old
, TypeNode tn
){
543 if( tn
.isNull() || tn
==old
.getType() ){
545 }else if( old
.isConst() ){
546 //must make constant of type tn
547 if( d_const_map
[tn
].find( old
)==d_const_map
[tn
].end() ){
548 std::stringstream ss
;
549 ss
<< "ic_" << tn
<< "_" << old
;
550 d_const_map
[tn
][ old
] = NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "constant created during sort inference" ); //use mkConst???
552 return d_const_map
[tn
][ old
];
553 }else if( old
.getKind()==kind::BOUND_VARIABLE
){
554 std::stringstream ss
;
556 return NodeManager::currentNM()->mkBoundVar( ss
.str(), tn
);
558 std::stringstream ss
;
560 return NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "created during sort inference" );
564 Node
SortInference::simplifyNode( Node n
, std::map
< Node
, Node
>& var_bound
, TypeNode tnn
, std::map
< Node
, std::map
< TypeNode
, Node
> >& visited
){
565 std::map
< TypeNode
, Node
>::iterator itv
= visited
[n
].find( tnn
);
566 if( itv
!=visited
[n
].end() ){
569 Trace("sort-inference-debug2") << "Simplify " << n
<< ", type context=" << tnn
<< std::endl
;
570 std::vector
< Node
> children
;
571 std::map
< Node
, std::map
< TypeNode
, Node
> > new_visited
;
572 bool use_new_visited
= false;
573 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
574 //recreate based on types of variables
575 std::vector
< Node
> new_children
;
576 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
577 TypeNode tn
= getOrCreateTypeForId( d_var_types
[n
][ n
[0][i
] ], n
[0][i
].getType() );
578 Node v
= getNewSymbol( n
[0][i
], tn
);
579 Trace("sort-inference-debug2") << "Map variable " << n
[0][i
] << " to " << v
<< std::endl
;
580 new_children
.push_back( v
);
581 var_bound
[ n
[0][i
] ] = v
;
583 children
.push_back( NodeManager::currentNM()->mkNode( n
[0].getKind(), new_children
) );
584 use_new_visited
= true;
588 if( n
.getMetaKind() == kind::metakind::PARAMETERIZED
){
589 children
.push_back( n
.getOperator() );
592 if( n
.hasOperator() ){
593 op
= n
.getOperator();
595 bool childChanged
= false;
597 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
598 bool processChild
= true;
599 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
600 processChild
= options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE
? i
==1 : i
>=1;
603 if( n
.getKind()==kind::APPLY_UF
){
604 Assert( d_op_arg_types
.find( op
)!=d_op_arg_types
.end() );
605 tnnc
= getOrCreateTypeForId( d_op_arg_types
[op
][i
], n
[i
].getType() );
606 Assert( !tnnc
.isNull() );
607 }else if( n
.getKind()==kind::EQUAL
&& i
==0 ){
608 Assert( d_equality_types
.find( n
)!=d_equality_types
.end() );
609 tnnc
= getOrCreateTypeForId( d_equality_types
[n
], n
[0].getType() );
610 Assert( !tnnc
.isNull() );
612 Node nc
= simplifyNode( n
[i
], var_bound
, tnnc
, use_new_visited
? new_visited
: visited
);
613 Trace("sort-inference-debug2") << "Simplify " << i
<< " " << n
[i
] << " returned " << nc
<< std::endl
;
614 children
.push_back( nc
);
615 childChanged
= childChanged
|| nc
!=n
[i
];
619 //remove from variable bindings
621 if( n
.getKind()==kind::FORALL
|| n
.getKind()==kind::EXISTS
){
622 //erase from variable bound
623 for( size_t i
=0; i
<n
[0].getNumChildren(); i
++ ){
624 Trace("sort-inference-debug2") << "Remove bound for " << n
[0][i
] << std::endl
;
625 var_bound
.erase( n
[0][i
] );
627 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
628 }else if( n
.getKind()==kind::EQUAL
){
629 TypeNode tn1
= children
[0].getType();
630 TypeNode tn2
= children
[1].getType();
631 if( !tn1
.isSubtypeOf( tn2
) && !tn2
.isSubtypeOf( tn1
) ){
632 Trace("sort-inference-warn") << "Sort inference created bad equality: " << children
[0] << " = " << children
[1] << std::endl
;
633 Trace("sort-inference-warn") << " Types : " << children
[0].getType() << " " << children
[1].getType() << std::endl
;
636 ret
= NodeManager::currentNM()->mkNode( kind::EQUAL
, children
);
637 }else if( n
.getKind()==kind::APPLY_UF
){
638 if( d_symbol_map
.find( op
)==d_symbol_map
.end() ){
639 //make the new operator if necessary
640 bool opChanged
= false;
641 std::vector
< TypeNode
> argTypes
;
642 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
643 TypeNode tn
= getOrCreateTypeForId( d_op_arg_types
[op
][i
], n
[i
].getType() );
644 argTypes
.push_back( tn
);
645 if( tn
!=n
[i
].getType() ){
649 TypeNode retType
= getOrCreateTypeForId( d_op_return_types
[op
], n
.getType() );
650 if( retType
!=n
.getType() ){
654 std::stringstream ss
;
656 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( argTypes
, retType
);
657 d_symbol_map
[op
] = NodeManager::currentNM()->mkSkolem( ss
.str(), typ
, "op created during sort inference" );
658 Trace("setp-model") << "Function " << op
<< " is replaced with " << d_symbol_map
[op
] << std::endl
;
659 d_model_replace_f
[op
] = d_symbol_map
[op
];
661 d_symbol_map
[op
] = op
;
664 children
[0] = d_symbol_map
[op
];
665 //make sure all children have been taken care of
666 for( size_t i
=0; i
<n
.getNumChildren(); i
++ ){
667 TypeNode tn
= children
[i
+1].getType();
668 TypeNode tna
= getTypeForId( d_op_arg_types
[op
][i
] );
670 Trace("sort-inference-warn") << "Sort inference created bad child: " << n
<< " " << n
[i
] << " " << tn
<< " " << tna
<< std::endl
;
674 ret
= NodeManager::currentNM()->mkNode( kind::APPLY_UF
, children
);
676 std::map
< Node
, Node
>::iterator it
= var_bound
.find( n
);
677 if( it
!=var_bound
.end() ){
679 }else if( n
.getKind() == kind::VARIABLE
|| n
.getKind() == kind::SKOLEM
){
680 if( d_symbol_map
.find( n
)==d_symbol_map
.end() ){
681 TypeNode tn
= getOrCreateTypeForId( d_op_return_types
[n
], n
.getType() );
682 d_symbol_map
[n
] = getNewSymbol( n
, tn
);
684 ret
= d_symbol_map
[n
];
685 }else if( n
.isConst() ){
686 //type is determined by context
687 ret
= getNewSymbol( n
, tnn
);
688 }else if( childChanged
){
689 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
694 visited
[n
][tnn
] = ret
;
699 Node
SortInference::mkInjection( TypeNode tn1
, TypeNode tn2
) {
700 std::vector
< TypeNode
> tns
;
701 tns
.push_back( tn1
);
702 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( tns
, tn2
);
703 Node f
= NodeManager::currentNM()->mkSkolem( "inj", typ
, "injection for monotonicity constraint" );
704 Trace("sort-inference") << "-> Make injection " << f
<< " from " << tn1
<< " to " << tn2
<< std::endl
;
705 Node v1
= NodeManager::currentNM()->mkBoundVar( "?x", tn1
);
706 Node v2
= NodeManager::currentNM()->mkBoundVar( "?y", tn1
);
707 Node ret
= NodeManager::currentNM()->mkNode( kind::FORALL
,
708 NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST
, v1
, v2
),
709 NodeManager::currentNM()->mkNode( kind::OR
,
710 NodeManager::currentNM()->mkNode( kind::APPLY_UF
, f
, v1
).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF
, f
, v2
) ).negate(),
712 ret
= theory::Rewriter::rewrite( ret
);
716 int SortInference::getSortId( Node n
) {
717 Node op
= n
.getKind()==kind::APPLY_UF
? n
.getOperator() : n
;
718 if( d_op_return_types
.find( op
)!=d_op_return_types
.end() ){
719 return d_type_union_find
.getRepresentative( d_op_return_types
[op
] );
725 int SortInference::getSortId( Node f
, Node v
) {
726 if( d_var_types
.find( f
)!=d_var_types
.end() ){
727 return d_type_union_find
.getRepresentative( d_var_types
[f
][v
] );
733 void SortInference::setSkolemVar( Node f
, Node v
, Node sk
){
734 Trace("sort-inference-temp") << "Set skolem var for " << f
<< ", variable " << v
<< std::endl
;
735 if( isWellSortedFormula( f
) && d_var_types
.find( f
)==d_var_types
.end() ){
736 //calculate the sort for variables if not done so already
737 std::map
< Node
, Node
> var_bound
;
738 std::map
< Node
, int > visited
;
739 process( f
, var_bound
, visited
);
741 d_op_return_types
[sk
] = getSortId( f
, v
);
742 Trace("sort-inference-temp") << "Set skolem sort id for " << sk
<< " to " << d_op_return_types
[sk
] << std::endl
;
745 bool SortInference::isWellSortedFormula( Node n
) {
746 if( n
.getType().isBoolean() && n
.getKind()!=kind::APPLY_UF
){
747 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
748 if( !isWellSortedFormula( n
[i
] ) ){
754 return isWellSorted( n
);
758 bool SortInference::isWellSorted( Node n
) {
759 if( getSortId( n
)==0 ){
762 if( n
.getKind()==kind::APPLY_UF
){
763 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
764 int s1
= getSortId( n
[i
] );
765 int s2
= d_type_union_find
.getRepresentative( d_op_arg_types
[ n
.getOperator() ][i
] );
769 if( !isWellSorted( n
[i
] ) ){
778 void SortInference::getSortConstraints( Node n
, UnionFind
& uf
) {
779 if( n
.getKind()==kind::APPLY_UF
){
780 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
781 getSortConstraints( n
[i
], uf
);
782 uf
.setEqual( getSortId( n
[i
] ), d_type_union_find
.getRepresentative( d_op_arg_types
[ n
.getOperator() ][i
] ) );
787 bool SortInference::isMonotonic( TypeNode tn
) {
788 Assert( tn
.isSort() );
789 return d_non_monotonic_sorts_orig
.find( tn
)==d_non_monotonic_sorts_orig
.end();
792 }/* CVC4 namespace */