src/theory/sort_inference.cpp

   1 /*********************                                                        */
   2 /*! \file sort_inference.cpp
   3  ** \verbatim
   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
  11  **
  12  ** \brief Sort inference module
  13  **
  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.
  18  **/
  19
  20 #include "theory/sort_inference.h"
  21
  22 #include <vector>
  23
  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"
  30
  31 using namespace CVC4;
  32 using namespace std;
  33
  34 namespace CVC4 {
  35
  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 << ", ";
  39   }
  40   for( unsigned i=0; i<d_deq.size(); i++ ){
  41     Trace(c) << "s_" << d_deq[i].first << " != s_" << d_deq[i].second << ", ";
  42   }
  43   Trace(c) << std::endl;
  44 }
  45 void SortInference::UnionFind::set( UnionFind& c ) {
  46   clear();
  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;
  49   }
  50   d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() );
  51 }
  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 ){
  55     return t;
  56   }else{
  57     int rt = getRepresentative( it->second );
  58     d_eqc[t] = rt;
  59     return rt;
  60   }
  61 }
  62 void SortInference::UnionFind::setEqual( int t1, int t2 ){
  63   if( t1!=t2 ){
  64     int rt1 = getRepresentative( t1 );
  65     int rt2 = getRepresentative( t2 );
  66     if( rt1>rt2 ){
  67       d_eqc[rt1] = rt2;
  68     }else{
  69       d_eqc[rt2] = rt1;
  70     }
  71   }
  72 }
  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 ) ){
  76       return false;
  77     }
  78   }
  79   return true;
  80 }
  81
  82
  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 );
  88   }
  89 }
  90
  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];
  95   }else{
  96     Trace(c) << "s_" << rt;
  97   }
  98 }
  99
 100 void SortInference::reset() {
 101   d_sub_sorts.clear();
 102   d_non_monotonic_sorts.clear();
 103   d_type_sub_sorts.clear();
 104   //reset info
 105   sortCount = 1;
 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();
 111   d_var_types.clear();
 112   //for rewriting
 113   d_symbol_map.clear();
 114   d_const_map.clear();
 115 }
 116
 117 void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){
 118   if( doSortInference ){
 119     Trace("sort-inference") << "Calculating sort inference..." << std::endl;
 120     //process all assertions
 121     for( unsigned i=0; i<assertions.size(); i++ ){
 122       Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
 123       std::map< Node, Node > var_bound;
 124       process( assertions[i], var_bound );
 125     }
 126     for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
 127       Trace("sort-inference") << it->first << " : ";
 128       TypeNode retTn = it->first.getType();
 129       if( !d_op_arg_types[ it->first ].empty() ){
 130         Trace("sort-inference") << "( ";
 131         for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){
 132           recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] );
 133           printSort( "sort-inference", d_op_arg_types[ it->first ][i] );
 134           Trace("sort-inference") << " ";
 135         }
 136         Trace("sort-inference") << ") -> ";
 137         retTn = retTn[(int)retTn.getNumChildren()-1];
 138       }
 139       recordSubsort( retTn, it->second );
 140       printSort( "sort-inference", it->second );
 141       Trace("sort-inference") << std::endl;
 142     }
 143     for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
 144       Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl;
 145       for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){
 146         recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] );
 147         printSort( "sort-inference", it->second[it->first[0][i]] );
 148         Trace("sort-inference") << std::endl;
 149       }
 150       Trace("sort-inference") << std::endl;
 151     }
 152
 153     if( !options::ufssSymBreak() ){
 154       bool rewritten = false;
 155       //determine monotonicity of sorts
 156       for( unsigned i=0; i<assertions.size(); i++ ){
 157         Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
 158         std::map< Node, Node > var_bound;
 159         processMonotonic( assertions[i], true, true, var_bound );
 160       }
 161       //doMonotonicyInference = false;
 162
 163       Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl;
 164       for( unsigned i=0; i<d_sub_sorts.size(); i++ ){
 165         printSort( "sort-inference", d_sub_sorts[i] );
 166         if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
 167           Trace("sort-inference") << " is interpreted." << std::endl;
 168         }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
 169           Trace("sort-inference") << " is monotonic." << std::endl;
 170         }else{
 171           Trace("sort-inference") << " is not monotonic." << std::endl;
 172         }
 173       }
 174
 175       //simplify all assertions by introducing new symbols wherever necessary
 176       for( unsigned i=0; i<assertions.size(); i++ ){
 177         Node prev = assertions[i];
 178         std::map< Node, Node > var_bound;
 179         Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl;
 180         Node curr = simplify( assertions[i], var_bound );
 181         Trace("sort-inference-debug") << "Done." << std::endl;
 182         if( curr!=assertions[i] ){
 183           curr = theory::Rewriter::rewrite( curr );
 184           rewritten = true;
 185           Trace("sort-inference-rewrite") << assertions << std::endl;
 186           Trace("sort-inference-rewrite") << " --> " << curr << std::endl;
 187           PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
 188           assertions[i] = curr;
 189         }
 190       }
 191       //now, ensure constants are distinct
 192       for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){
 193         std::vector< Node > consts;
 194         for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 195           consts.push_back( it2->second );
 196         }
 197         //TODO: add lemma enforcing introduced constants to be distinct
 198       }
 199
 200       //enforce constraints based on monotonicity
 201       for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){
 202         int nmonSort = -1;
 203         for( unsigned i=0; i<it->second.size(); i++ ){
 204           if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
 205             nmonSort = it->second[i];
 206             break;
 207           }
 208         }
 209         if( nmonSort!=-1 ){
 210           std::vector< Node > injections;
 211           TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
 212           for( unsigned i=0; i<it->second.size(); i++ ){
 213             if( it->second[i]!=nmonSort ){
 214               TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first );
 215               //make injection to nmonSort
 216               Node a1 = mkInjection( new_tn, base_tn );
 217               injections.push_back( a1 );
 218               if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){
 219                 //also must make injection from nmonSort to this
 220                 Node a2 = mkInjection( base_tn, new_tn );
 221                 injections.push_back( a2 );
 222               }
 223             }
 224           }
 225           Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
 226           for( unsigned j=0; j<injections.size(); j++ ){
 227             Trace("sort-inference-rewrite") << "   " << injections[j] << std::endl;
 228           }
 229           assertions.insert( assertions.end(), injections.begin(), injections.end() );
 230           if( !injections.empty() ){
 231             rewritten = true;
 232           }
 233         }
 234       }
 235       //no sub-sort information is stored
 236       reset();
 237       Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten << std::endl;
 238     }
 239     /*
 240     else if( !options::ufssSymBreak() ){
 241       //just add the unit lemmas between constants
 242       std::map< TypeNode, std::map< int, Node > > constants;
 243       for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){
 244         int rt = d_type_union_find.getRepresentative( it->second );
 245         if( d_op_arg_types[ it->first ].empty() ){
 246           TypeNode tn = it->first.getType();
 247           if( constants[ tn ].find( rt )==constants[ tn ].end() ){
 248             constants[ tn ][ rt ] = it->first;
 249           }
 250         }
 251       }
 252       //add unit lemmas for each constant
 253       for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){
 254         Node first_const;
 255         for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 256           if( first_const.isNull() ){
 257             first_const = it2->second;
 258           }else{
 259             Node eq = first_const.eqNode( it2->second );
 260             //eq = Rewriter::rewrite( eq );
 261             Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl;
 262             assertions.push_back( eq );
 263           }
 264         }
 265       }
 266     }
 267     */
 268     initialSortCount = sortCount;
 269   }
 270   if( doMonotonicyInference ){
 271     for( unsigned i=0; i<assertions.size(); i++ ){
 272       Trace("sort-inference-debug") << "Process type monotonicity for " << assertions[i] << std::endl;
 273       std::map< Node, Node > var_bound;
 274       processMonotonic( assertions[i], true, true, var_bound, true );
 275     }
 276   }
 277 }
 278
 279 void SortInference::setEqual( int t1, int t2 ){
 280   if( t1!=t2 ){
 281     int rt1 = d_type_union_find.getRepresentative( t1 );
 282     int rt2 = d_type_union_find.getRepresentative( t2 );
 283     if( rt1!=rt2 ){
 284       Trace("sort-inference-debug") << "Set equal : ";
 285       printSort( "sort-inference-debug", rt1 );
 286       Trace("sort-inference-debug") << " ";
 287       printSort( "sort-inference-debug", rt2 );
 288       Trace("sort-inference-debug") << std::endl;
 289       /*
 290       d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
 291       d_type_eq_class[rt2].clear();
 292       Trace("sort-inference-debug") << "EqClass : { ";
 293       for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
 294         Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
 295       }
 296       Trace("sort-inference-debug") << "}" << std::endl;
 297       */
 298       if( rt2>rt1 ){
 299         //swap
 300         int swap = rt1;
 301         rt1 = rt2;
 302         rt2 = swap;
 303       }
 304       std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
 305       if( it1!=d_type_types.end() ){
 306         if( d_type_types.find( rt2 )==d_type_types.end() ){
 307           d_type_types[rt2] = it1->second;
 308           d_type_types.erase( rt1 );
 309         }else{
 310           Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl;
 311           return;
 312         }
 313       }
 314       d_type_union_find.d_eqc[rt1] = rt2;
 315     }
 316   }
 317 }
 318
 319 int SortInference::getIdForType( TypeNode tn ){
 320   //register the return type
 321   std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );
 322   if( it==d_id_for_types.end() ){
 323     int sc = sortCount;
 324     d_type_types[ sortCount ] = tn;
 325     d_id_for_types[ tn ] = sortCount;
 326     sortCount++;
 327     return sc;
 328   }else{
 329     return it->second;
 330   }
 331 }
 332
 333 int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
 334   //add to variable bindings
 335   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
 336     if( d_var_types.find( n )!=d_var_types.end() ){
 337       return getIdForType( n.getType() );
 338     }else{
 339       for( size_t i=0; i<n[0].getNumChildren(); i++ ){
 340         //apply sort inference to quantified variables
 341         d_var_types[n][ n[0][i] ] = sortCount;
 342         sortCount++;
 343
 344         //type of the quantified variable must be the same
 345         var_bound[ n[0][i] ] = n;
 346       }
 347     }
 348   }
 349
 350   //process children
 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;
 357     }
 358     if( processChild ){
 359       children.push_back( n[i] );
 360       child_types.push_back( process( n[i], var_bound ) );
 361     }
 362   }
 363
 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] );
 369     }
 370   }
 371   Trace("sort-inference-debug") << "...Process " << n << std::endl;
 372
 373   int retType;
 374   if( n.getKind()==kind::EQUAL ){
 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 );
 382       }
 383     }else{
 384       //we only require that the left and right hand side must be equal
 385       setEqual( child_types[0], child_types[1] );
 386     }
 387     //int eqType = getIdForType( n[0].getType() );
 388     //setEqual( child_types[0], eqType );
 389     //setEqual( child_types[1], eqType );
 390     retType = getIdForType( n.getType() );
 391   }else if( n.getKind()==kind::APPLY_UF ){
 392     Node op = n.getOperator();
 393     TypeNode tn_op = op.getType();
 394     if( d_op_return_types.find( op )==d_op_return_types.end() ){
 395       if( n.getType().isBoolean() ){
 396         //use booleans
 397         d_op_return_types[op] = getIdForType( n.getType() );
 398       }else{
 399         //assign arbitrary sort for return type
 400         d_op_return_types[op] = sortCount;
 401         sortCount++;
 402       }
 403       //d_type_eq_class[sortCount].push_back( op );
 404       //assign arbitrary sort for argument types
 405       for( size_t i=0; i<n.getNumChildren(); i++ ){
 406         d_op_arg_types[op].push_back( sortCount );
 407         sortCount++;
 408       }
 409     }
 410     for( size_t i=0; i<n.getNumChildren(); i++ ){
 411       //the argument of the operator must match the return type of the subterm
 412       if( n[i].getType()!=tn_op[i] ){
 413         //if type mismatch, assume original types
 414         Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType();
 415         Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl;
 416         int ct1 = getIdForType( n[i].getType() );
 417         setEqual( child_types[i], ct1 );
 418         int ct2 = getIdForType( tn_op[i] );
 419         setEqual( d_op_arg_types[op][i], ct2 );
 420       }else{
 421         setEqual( child_types[i], d_op_arg_types[op][i] );
 422       }
 423     }
 424     //return type is the return type
 425     retType = d_op_return_types[op];
 426   }else{
 427     std::map< Node, Node >::iterator it = var_bound.find( n );
 428     if( it!=var_bound.end() ){
 429       Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
 430       //the return type was specified while binding
 431       retType = d_var_types[it->second][n];
 432     }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){
 433       Trace("sort-inference-debug") << n << " is a variable." << std::endl;
 434       if( d_op_return_types.find( n )==d_op_return_types.end() ){
 435         //assign arbitrary sort
 436         d_op_return_types[n] = sortCount;
 437         sortCount++;
 438         //d_type_eq_class[sortCount].push_back( n );
 439       }
 440       retType = d_op_return_types[n];
 441     //}else if( n.isConst() ){
 442     //  Trace("sort-inference-debug") << n << " is a constant." << std::endl;
 443       //can be any type we want
 444     //  retType = sortCount;
 445     //  sortCount++;
 446     }else{
 447       Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
 448       //it is an interpretted term
 449       for( size_t i=0; i<children.size(); i++ ){
 450         Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;
 451         //must enforce the actual type of the operator on the children
 452         int ct = getIdForType( children[i].getType() );
 453         setEqual( child_types[i], ct );
 454       }
 455       //return type must be the actual return type
 456       retType = getIdForType( n.getType() );
 457     }
 458   }
 459   Trace("sort-inference-debug") << "...Type( " << n << " ) = ";
 460   printSort("sort-inference-debug", retType );
 461   Trace("sort-inference-debug") << std::endl;
 462   return retType;
 463 }
 464
 465 void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, bool typeMode ) {
 466   Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl;
 467   if( n.getKind()==kind::FORALL ){
 468     //only consider variables universally if it is possible this quantified formula is asserted positively
 469     if( !hasPol || pol ){
 470       for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
 471         var_bound[n[0][i]] = n;
 472       }
 473     }
 474     processMonotonic( n[1], pol, hasPol, var_bound, typeMode );
 475     if( !hasPol || pol ){
 476       for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
 477         var_bound.erase( n[0][i] );
 478       }
 479     }
 480     return;
 481   }else if( n.getKind()==kind::EQUAL ){
 482     if( !hasPol || pol ){
 483       for( unsigned i=0; i<2; i++ ){
 484         if( var_bound.find( n[i] )!=var_bound.end() ){
 485           if( !typeMode ){
 486             int sid = getSortId( var_bound[n[i]], n[i] );
 487             d_non_monotonic_sorts[sid] = true;
 488           }else{
 489             d_non_monotonic_sorts_orig[n[i].getType()] = true;
 490           }
 491           break;
 492         }
 493       }
 494     }
 495   }
 496   for( unsigned i=0; i<n.getNumChildren(); i++ ){
 497     bool npol;
 498     bool nhasPol;
 499     theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol );
 500     processMonotonic( n[i], npol, nhasPol, var_bound, typeMode );
 501   }
 502 }
 503
 504
 505 TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
 506   int rt = d_type_union_find.getRepresentative( t );
 507   if( d_type_types.find( rt )!=d_type_types.end() ){
 508     return d_type_types[rt];
 509   }else{
 510     TypeNode retType;
 511     //see if we can assign pref
 512     if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){
 513       retType = pref;
 514     }else{
 515       //must create new type
 516       std::stringstream ss;
 517       ss << "it_" << t << "_" << pref;
 518       retType = NodeManager::currentNM()->mkSort( ss.str() );
 519     }
 520     Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
 521     printSort("sort-inference", t );
 522     Trace("sort-inference") << std::endl;
 523     d_id_for_types[ retType ] = rt;
 524     d_type_types[ rt ] = retType;
 525     return retType;
 526   }
 527 }
 528
 529 TypeNode SortInference::getTypeForId( int t ){
 530   int rt = d_type_union_find.getRepresentative( t );
 531   if( d_type_types.find( rt )!=d_type_types.end() ){
 532     return d_type_types[rt];
 533   }else{
 534     return TypeNode::null();
 535   }
 536 }
 537
 538 Node SortInference::getNewSymbol( Node old, TypeNode tn ){
 539   if( tn==old.getType() ){
 540     return old;
 541   }else if( old.isConst() ){
 542     //must make constant of type tn
 543     if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
 544       std::stringstream ss;
 545       ss << "ic_" << tn << "_" << old;
 546       d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" );  //use mkConst???
 547     }
 548     return d_const_map[tn][ old ];
 549   }else if( old.getKind()==kind::BOUND_VARIABLE ){
 550     std::stringstream ss;
 551     ss << "b_" << old;
 552     return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
 553   }else{
 554     std::stringstream ss;
 555     ss << "i_" << old;
 556     return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
 557   }
 558 }
 559
 560 Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
 561   Trace("sort-inference-debug2") << "Simplify " << n << std::endl;
 562   std::vector< Node > children;
 563   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
 564     //recreate based on types of variables
 565     std::vector< Node > new_children;
 566     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
 567       TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
 568       Node v = getNewSymbol( n[0][i], tn );
 569       Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl;
 570       new_children.push_back( v );
 571       var_bound[ n[0][i] ] = v;
 572     }
 573     children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
 574   }
 575
 576   //process children
 577   if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 578     children.push_back( n.getOperator() );
 579   }
 580   bool childChanged = false;
 581   for( size_t i=0; i<n.getNumChildren(); i++ ){
 582     bool processChild = true;
 583     if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
 584       processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
 585     }
 586     if( processChild ){
 587       Node nc = simplify( n[i], var_bound );
 588       Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl;
 589       children.push_back( nc );
 590       childChanged = childChanged || nc!=n[i];
 591     }
 592   }
 593
 594   //remove from variable bindings
 595   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
 596     //erase from variable bound
 597     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
 598       Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
 599       var_bound.erase( n[0][i] );
 600     }
 601     return NodeManager::currentNM()->mkNode( n.getKind(), children );
 602   }else if( n.getKind()==kind::EQUAL ){
 603     TypeNode tn1 = children[0].getType();
 604     TypeNode tn2 = children[1].getType();
 605     if( !tn1.isSubtypeOf( tn2 ) && !tn2.isSubtypeOf( tn1 ) ){
 606       if( children[0].isConst() ){
 607         children[0] = getNewSymbol( children[0], children[1].getType() );
 608       }else if( children[1].isConst() ){
 609         children[1] = getNewSymbol( children[1], children[0].getType() );
 610       }else{
 611         Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
 612         Trace("sort-inference-warn") << "  Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
 613         Assert( false );
 614       }
 615     }
 616     return NodeManager::currentNM()->mkNode( kind::EQUAL, children );
 617   }else if( n.getKind()==kind::APPLY_UF ){
 618     Node op = n.getOperator();
 619     if( d_symbol_map.find( op )==d_symbol_map.end() ){
 620       //make the new operator if necessary
 621       bool opChanged = false;
 622       std::vector< TypeNode > argTypes;
 623       for( size_t i=0; i<n.getNumChildren(); i++ ){
 624         TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
 625         argTypes.push_back( tn );
 626         if( tn!=n[i].getType() ){
 627           opChanged = true;
 628         }
 629       }
 630       TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );
 631       if( retType!=n.getType() ){
 632         opChanged = true;
 633       }
 634       if( opChanged ){
 635         std::stringstream ss;
 636         ss << "io_" << op;
 637         TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
 638         d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
 639         Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl;
 640         d_model_replace_f[op] = d_symbol_map[op];
 641       }else{
 642         d_symbol_map[op] = op;
 643       }
 644     }
 645     children[0] = d_symbol_map[op];
 646     //make sure all children have been taken care of
 647     for( size_t i=0; i<n.getNumChildren(); i++ ){
 648       TypeNode tn = children[i+1].getType();
 649       TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
 650       if( tn!=tna ){
 651         if( n[i].isConst() ){
 652           children[i+1] = getNewSymbol( n[i], tna );
 653         }else{
 654           Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
 655           Assert( false );
 656         }
 657       }
 658     }
 659     return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
 660   }else{
 661     std::map< Node, Node >::iterator it = var_bound.find( n );
 662     if( it!=var_bound.end() ){
 663       return it->second;
 664     }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){
 665       if( d_symbol_map.find( n )==d_symbol_map.end() ){
 666         TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );
 667         d_symbol_map[n] = getNewSymbol( n, tn );
 668       }
 669       return d_symbol_map[n];
 670     }else if( n.isConst() ){
 671       //just return n, we will fix at higher scope
 672       return n;
 673     }else{
 674       if( childChanged ){
 675         return NodeManager::currentNM()->mkNode( n.getKind(), children );
 676       }else{
 677         return n;
 678       }
 679     }
 680   }
 681
 682 }
 683
 684 Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
 685   std::vector< TypeNode > tns;
 686   tns.push_back( tn1 );
 687   TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
 688   Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" );
 689   Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
 690   Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
 691   Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
 692   Node ret = NodeManager::currentNM()->mkNode( kind::FORALL,
 693                NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
 694                NodeManager::currentNM()->mkNode( kind::OR,
 695                  NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(),
 696                  v1.eqNode( v2 ) ) );
 697   ret = theory::Rewriter::rewrite( ret );
 698   return ret;
 699 }
 700
 701 int SortInference::getSortId( Node n ) {
 702   Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
 703   if( d_op_return_types.find( op )!=d_op_return_types.end() ){
 704     return d_type_union_find.getRepresentative( d_op_return_types[op] );
 705   }else{
 706     return 0;
 707   }
 708 }
 709
 710 int SortInference::getSortId( Node f, Node v ) {
 711   if( d_var_types.find( f )!=d_var_types.end() ){
 712     return d_type_union_find.getRepresentative( d_var_types[f][v] );
 713   }else{
 714     return 0;
 715   }
 716 }
 717
 718 void SortInference::setSkolemVar( Node f, Node v, Node sk ){
 719   Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl;
 720   if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){
 721     //calculate the sort for variables if not done so already
 722     std::map< Node, Node > var_bound;
 723     process( f, var_bound );
 724   }
 725   d_op_return_types[sk] = getSortId( f, v );
 726   Trace("sort-inference-temp") << "Set skolem sort id for " << sk << " to " << d_op_return_types[sk] << std::endl;
 727 }
 728
 729 bool SortInference::isWellSortedFormula( Node n ) {
 730   if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){
 731     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 732       if( !isWellSortedFormula( n[i] ) ){
 733         return false;
 734       }
 735     }
 736     return true;
 737   }else{
 738     return isWellSorted( n );
 739   }
 740 }
 741
 742 bool SortInference::isWellSorted( Node n ) {
 743   if( getSortId( n )==0 ){
 744     return false;
 745   }else{
 746     if( n.getKind()==kind::APPLY_UF ){
 747       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 748         int s1 = getSortId( n[i] );
 749         int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] );
 750         if( s1!=s2 ){
 751           return false;
 752         }
 753         if( !isWellSorted( n[i] ) ){
 754           return false;
 755         }
 756       }
 757     }
 758     return true;
 759   }
 760 }
 761
 762 void SortInference::getSortConstraints( Node n, UnionFind& uf ) {
 763   if( n.getKind()==kind::APPLY_UF ){
 764     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 765       getSortConstraints( n[i], uf );
 766       uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) );
 767     }
 768   }
 769 }
 770
 771 bool SortInference::isMonotonic( TypeNode tn ) {
 772   Assert( tn.isSort() );
 773   return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
 774 }
 775
 776 }/* CVC4 namespace */