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