src/theory/sort_inference.cpp

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