src/theory/theory_model_builder.cpp

   1 /*********************                                                        */
   2 /*! \file theory_model_builder.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Clark Barrett, Andrew Reynolds, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of theory model buidler class
  13  **/
  14 #include "theory/theory_model_builder.h"
  15
  16 #include "options/quantifiers_options.h"
  17 #include "options/smt_options.h"
  18 #include "options/uf_options.h"
  19 #include "theory/theory_engine.h"
  20 #include "theory/uf/theory_uf_model.h"
  21
  22 using namespace std;
  23 using namespace CVC4::kind;
  24 using namespace CVC4::context;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
  30 {
  31 }
  32
  33 bool TheoryEngineModelBuilder::isAssignable(TNode n)
  34 {
  35   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
  36   {
  37     // selectors are always assignable (where we guarantee that they are not
  38     // evaluatable here)
  39     if (!options::ufHo())
  40     {
  41       Assert(!n.getType().isFunction());
  42       return true;
  43     }
  44     else
  45     {
  46       // might be a function field
  47       return !n.getType().isFunction();
  48     }
  49   }
  50   else
  51   {
  52     // non-function variables, and fully applied functions
  53     if (!options::ufHo())
  54     {
  55       // no functions exist, all functions are fully applied
  56       Assert(n.getKind() != kind::HO_APPLY);
  57       Assert(!n.getType().isFunction());
  58       return n.isVar() || n.getKind() == kind::APPLY_UF;
  59     }
  60     else
  61     {
  62       // Assert( n.getKind() != kind::APPLY_UF );
  63       return (n.isVar() && !n.getType().isFunction())
  64              || n.getKind() == kind::APPLY_UF
  65              || (n.getKind() == kind::HO_APPLY
  66                  && n[0].getType().getNumChildren() == 2);
  67     }
  68   }
  69 }
  70
  71 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
  72                                                      TheoryModel* tm,
  73                                                      NodeSet& cache)
  74 {
  75   if (n.getKind() == FORALL || n.getKind() == EXISTS)
  76   {
  77     return;
  78   }
  79   if (cache.find(n) != cache.end())
  80   {
  81     return;
  82   }
  83   if (isAssignable(n))
  84   {
  85     tm->d_equalityEngine->addTerm(n);
  86   }
  87   for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
  88   {
  89     addAssignableSubterms(*child_it, tm, cache);
  90   }
  91   cache.insert(n);
  92 }
  93
  94 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
  95                                                  Node eqc,
  96                                                  Node const_rep)
  97 {
  98   d_constantReps[eqc] = const_rep;
  99   Trace("model-builder") << "    Assign: Setting constant rep of " << eqc
 100                          << " to " << const_rep << endl;
 101   tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
 102 }
 103
 104 bool TheoryEngineModelBuilder::isExcludedCdtValue(
 105     Node val,
 106     std::set<Node>* repSet,
 107     std::map<Node, Node>& assertedReps,
 108     Node eqc)
 109 {
 110   Trace("model-builder-debug")
 111       << "Is " << val << " and excluded codatatype value for " << eqc << "? "
 112       << std::endl;
 113   for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
 114   {
 115     Assert(assertedReps.find(*i) != assertedReps.end());
 116     Node rep = assertedReps[*i];
 117     Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
 118     // check matching val to rep with eqc as a free variable
 119     Node eqc_m;
 120     if (isCdtValueMatch(val, rep, eqc, eqc_m))
 121     {
 122       Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
 123                                    << eqc_m << std::endl;
 124       if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
 125       {
 126         Trace("model-builder-debug") << "*** " << val
 127                                      << " is excluded datatype for " << eqc
 128                                      << std::endl;
 129         return true;
 130       }
 131     }
 132   }
 133   return false;
 134 }
 135
 136 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
 137                                                Node r,
 138                                                Node eqc,
 139                                                Node& eqc_m)
 140 {
 141   if (r == v)
 142   {
 143     return true;
 144   }
 145   else if (r == eqc)
 146   {
 147     if (eqc_m.isNull())
 148     {
 149       // only if an uninterpreted constant?
 150       eqc_m = v;
 151       return true;
 152     }
 153     else
 154     {
 155       return v == eqc_m;
 156     }
 157   }
 158   else if (v.getKind() == kind::APPLY_CONSTRUCTOR
 159            && r.getKind() == kind::APPLY_CONSTRUCTOR)
 160   {
 161     if (v.getOperator() == r.getOperator())
 162     {
 163       for (unsigned i = 0; i < v.getNumChildren(); i++)
 164       {
 165         if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
 166         {
 167           return false;
 168         }
 169       }
 170       return true;
 171     }
 172   }
 173   return false;
 174 }
 175
 176 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
 177 {
 178   if (tn.isSort())
 179   {
 180     return true;
 181   }
 182   else if (tn.isArray())
 183   {
 184     return involvesUSort(tn.getArrayIndexType())
 185            || involvesUSort(tn.getArrayConstituentType());
 186   }
 187   else if (tn.isSet())
 188   {
 189     return involvesUSort(tn.getSetElementType());
 190   }
 191   else if (tn.isDatatype())
 192   {
 193     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 194     return dt.involvesUninterpretedType();
 195   }
 196   else
 197   {
 198     return false;
 199   }
 200 }
 201
 202 bool TheoryEngineModelBuilder::isExcludedUSortValue(
 203     std::map<TypeNode, unsigned>& eqc_usort_count,
 204     Node v,
 205     std::map<Node, bool>& visited)
 206 {
 207   Assert(v.isConst());
 208   if (visited.find(v) == visited.end())
 209   {
 210     visited[v] = true;
 211     TypeNode tn = v.getType();
 212     if (tn.isSort())
 213     {
 214       Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
 215                                    << tn << std::endl;
 216       unsigned card = eqc_usort_count[tn];
 217       Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
 218       unsigned index =
 219           v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
 220       Trace("model-builder-debug") << "  Index is " << index << std::endl;
 221       return index > 0 && index >= card;
 222     }
 223     for (unsigned i = 0; i < v.getNumChildren(); i++)
 224     {
 225       if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
 226       {
 227         return true;
 228       }
 229     }
 230   }
 231   return false;
 232 }
 233
 234 void TheoryEngineModelBuilder::addToTypeList(
 235     TypeNode tn,
 236     std::vector<TypeNode>& type_list,
 237     std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
 238 {
 239   if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
 240   {
 241     if (visiting.find(tn) == visiting.end())
 242     {
 243       visiting.insert(tn);
 244       /* This must make a recursive call on all types that are subterms of
 245        * values of the current type.
 246        * Note that recursive traversal here is over enumerated expressions
 247        * (very low expression depth). */
 248       if (tn.isArray())
 249       {
 250         addToTypeList(tn.getArrayIndexType(), type_list, visiting);
 251         addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
 252       }
 253       else if (tn.isSet())
 254       {
 255         addToTypeList(tn.getSetElementType(), type_list, visiting);
 256       }
 257       else if (tn.isDatatype())
 258       {
 259         const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 260         for (unsigned i = 0; i < dt.getNumConstructors(); i++)
 261         {
 262           for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
 263           {
 264             TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
 265             addToTypeList(ctn, type_list, visiting);
 266           }
 267         }
 268       }
 269       Assert(std::find(type_list.begin(), type_list.end(), tn)
 270              == type_list.end());
 271       type_list.push_back(tn);
 272     }
 273   }
 274 }
 275
 276 bool TheoryEngineModelBuilder::buildModel(Model* m)
 277 {
 278   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
 279   TheoryModel* tm = (TheoryModel*)m;
 280
 281   // buildModel should only be called once per check
 282   Assert(!tm->isBuilt());
 283
 284   // Reset model
 285   tm->reset();
 286
 287   // mark as built
 288   tm->d_modelBuilt = true;
 289   tm->d_modelBuiltSuccess = false;
 290
 291   // Collect model info from the theories
 292   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
 293                          << std::endl;
 294   if (!d_te->collectModelInfo(tm))
 295   {
 296     return false;
 297   }
 298
 299   // model-builder specific initialization
 300   if (!preProcessBuildModel(tm))
 301   {
 302     return false;
 303   }
 304
 305   // Loop through all terms and make sure that assignable sub-terms are in the
 306   // equality engine
 307   // Also, record #eqc per type (for finite model finding)
 308   std::map<TypeNode, unsigned> eqc_usort_count;
 309   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
 310   {
 311     NodeSet cache;
 312     for (; !eqcs_i.isFinished(); ++eqcs_i)
 313     {
 314       eq::EqClassIterator eqc_i =
 315           eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine);
 316       for (; !eqc_i.isFinished(); ++eqc_i)
 317       {
 318         addAssignableSubterms(*eqc_i, tm, cache);
 319       }
 320       TypeNode tn = (*eqcs_i).getType();
 321       if (tn.isSort())
 322       {
 323         if (eqc_usort_count.find(tn) == eqc_usort_count.end())
 324         {
 325           eqc_usort_count[tn] = 1;
 326         }
 327         else
 328         {
 329           eqc_usort_count[tn]++;
 330         }
 331       }
 332     }
 333   }
 334
 335   Trace("model-builder") << "Collect representatives..." << std::endl;
 336
 337   // Process all terms in the equality engine, store representatives for each EC
 338   d_constantReps.clear();
 339   std::map<Node, Node> assertedReps;
 340   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
 341   TypeEnumeratorProperties tep;
 342   if (options::finiteModelFind())
 343   {
 344     tep.d_fixed_usort_card = true;
 345     for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
 346          it != eqc_usort_count.end();
 347          ++it)
 348     {
 349       Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
 350                              << it->second << std::endl;
 351       tep.d_fixed_card[it->first] = Integer(it->second);
 352     }
 353     typeConstSet.setTypeEnumeratorProperties(&tep);
 354   }
 355   // AJR: build ordered list of types that ensures that base types are
 356   // enumerated first.
 357   // (I think) this is only strictly necessary for finite model finding +
 358   // parametric types instantiated with uninterpreted sorts, but is probably
 359   // a good idea to do in general since it leads to models with smaller term
 360   // sizes.
 361   std::vector<TypeNode> type_list;
 362   eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
 363   for (; !eqcs_i.isFinished(); ++eqcs_i)
 364   {
 365     // eqc is the equivalence class representative
 366     Node eqc = (*eqcs_i);
 367     Trace("model-builder") << "Processing EC: " << eqc << endl;
 368     Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
 369     TypeNode eqct = eqc.getType();
 370     Assert(assertedReps.find(eqc) == assertedReps.end());
 371     Assert(d_constantReps.find(eqc) == d_constantReps.end());
 372
 373     // Loop through terms in this EC
 374     Node rep, const_rep;
 375     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
 376     for (; !eqc_i.isFinished(); ++eqc_i)
 377     {
 378       Node n = *eqc_i;
 379       Trace("model-builder") << "  Processing Term: " << n << endl;
 380       // Record as rep if this node was specified as a representative
 381       if (tm->d_reps.find(n) != tm->d_reps.end())
 382       {
 383         // AJR: I believe this assertion is too strict,
 384         // e.g. datatypes may assert representative for two constructor terms
 385         // that are not in the care graph and are merged during
 386         // collectModelInfo.
 387         // Assert(rep.isNull());
 388         rep = tm->d_reps[n];
 389         Assert(!rep.isNull());
 390         Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep
 391                                << std::endl;
 392       }
 393       // Record as const_rep if this node is constant
 394       if (n.isConst())
 395       {
 396         Assert(const_rep.isNull());
 397         const_rep = n;
 398         Trace("model-builder") << "  ConstRep( " << eqc << " ) = " << const_rep
 399                                << std::endl;
 400       }
 401       // model-specific processing of the term
 402       tm->addTermInternal(n);
 403     }
 404
 405     // Assign representative for this EC
 406     if (!const_rep.isNull())
 407     {
 408       // Theories should not specify a rep if there is already a constant in the
 409       // EC
 410       // AJR: I believe this assertion is too strict, eqc with asserted reps may
 411       // merge with constant eqc
 412       // Assert(rep.isNull() || rep == const_rep);
 413       assignConstantRep(tm, eqc, const_rep);
 414       typeConstSet.add(eqct.getBaseType(), const_rep);
 415     }
 416     else if (!rep.isNull())
 417     {
 418       assertedReps[eqc] = rep;
 419       typeRepSet.add(eqct.getBaseType(), eqc);
 420       std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
 421       addToTypeList(eqct.getBaseType(), type_list, visiting);
 422     }
 423     else
 424     {
 425       typeNoRepSet.add(eqct, eqc);
 426       std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
 427       addToTypeList(eqct, type_list, visiting);
 428     }
 429   }
 430
 431   // Need to ensure that each EC has a constant representative.
 432
 433   Trace("model-builder") << "Processing EC's..." << std::endl;
 434
 435   TypeSet::iterator it;
 436   vector<TypeNode>::iterator type_it;
 437   set<Node>::iterator i, i2;
 438   bool changed, unassignedAssignable, assignOne = false;
 439   set<TypeNode> evaluableSet;
 440
 441   // Double-fixed-point loop
 442   // Outer loop handles a special corner case (see code at end of loop for
 443   // details)
 444   for (;;)
 445   {
 446     // Inner fixed-point loop: we are trying to learn constant values for every
 447     // EC.  Each time through this loop, we process all of the
 448     // types by type and may learn some new EC values.  EC's in one type may
 449     // depend on EC's in another type, so we need a fixed-point loop
 450     // to ensure that we learn as many EC values as possible
 451     do
 452     {
 453       changed = false;
 454       unassignedAssignable = false;
 455       evaluableSet.clear();
 456
 457       // Iterate over all types we've seen
 458       for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
 459       {
 460         TypeNode t = *type_it;
 461         TypeNode tb = t.getBaseType();
 462         set<Node>* noRepSet = typeNoRepSet.getSet(t);
 463
 464         // 1. Try to evaluate the EC's in this type
 465         if (noRepSet != NULL && !noRepSet->empty())
 466         {
 467           Trace("model-builder") << "  Eval phase, working on type: " << t
 468                                  << endl;
 469           bool assignable, evaluable, evaluated;
 470           d_normalizedCache.clear();
 471           for (i = noRepSet->begin(); i != noRepSet->end();)
 472           {
 473             i2 = i;
 474             ++i;
 475             assignable = false;
 476             evaluable = false;
 477             evaluated = false;
 478             Trace("model-builder-debug") << "Look at eqc : " << (*i2)
 479                                          << std::endl;
 480             eq::EqClassIterator eqc_i =
 481                 eq::EqClassIterator(*i2, tm->d_equalityEngine);
 482             for (; !eqc_i.isFinished(); ++eqc_i)
 483             {
 484               Node n = *eqc_i;
 485               Trace("model-builder-debug") << "Look at term : " << n
 486                                            << std::endl;
 487               if (isAssignable(n))
 488               {
 489                 assignable = true;
 490                 Trace("model-builder-debug") << "...assignable" << std::endl;
 491               }
 492               else
 493               {
 494                 evaluable = true;
 495                 Trace("model-builder-debug") << "...try to normalize"
 496                                              << std::endl;
 497                 Node normalized = normalize(tm, n, true);
 498                 if (normalized.isConst())
 499                 {
 500                   typeConstSet.add(tb, normalized);
 501                   assignConstantRep(tm, *i2, normalized);
 502                   Trace("model-builder") << "    Eval: Setting constant rep of "
 503                                          << (*i2) << " to " << normalized
 504                                          << endl;
 505                   changed = true;
 506                   evaluated = true;
 507                   noRepSet->erase(i2);
 508                   break;
 509                 }
 510               }
 511             }
 512             if (!evaluated)
 513             {
 514               if (evaluable)
 515               {
 516                 evaluableSet.insert(tb);
 517               }
 518               if (assignable)
 519               {
 520                 unassignedAssignable = true;
 521               }
 522             }
 523           }
 524         }
 525
 526         // 2. Normalize any non-const representative terms for this type
 527         set<Node>* repSet = typeRepSet.getSet(t);
 528         if (repSet != NULL && !repSet->empty())
 529         {
 530           Trace("model-builder")
 531               << "  Normalization phase, working on type: " << t << endl;
 532           d_normalizedCache.clear();
 533           for (i = repSet->begin(); i != repSet->end();)
 534           {
 535             Assert(assertedReps.find(*i) != assertedReps.end());
 536             Node rep = assertedReps[*i];
 537             Node normalized = normalize(tm, rep, false);
 538             Trace("model-builder") << "    Normalizing rep (" << rep
 539                                    << "), normalized to (" << normalized << ")"
 540                                    << endl;
 541             if (normalized.isConst())
 542             {
 543               changed = true;
 544               typeConstSet.add(tb, normalized);
 545               assignConstantRep(tm, *i, normalized);
 546               assertedReps.erase(*i);
 547               i2 = i;
 548               ++i;
 549               repSet->erase(i2);
 550             }
 551             else
 552             {
 553               if (normalized != rep)
 554               {
 555                 assertedReps[*i] = normalized;
 556                 changed = true;
 557               }
 558               ++i;
 559             }
 560           }
 561         }
 562       }
 563     } while (changed);
 564
 565     if (!unassignedAssignable)
 566     {
 567       break;
 568     }
 569
 570     // 3. Assign unassigned assignable EC's using type enumeration - assign a
 571     // value *different* from all other EC's if the type is infinite
 572     // Assign first value from type enumerator otherwise - for finite types, we
 573     // rely on polite framework to ensure that EC's that have to be
 574     // different are different.
 575
 576     // Only make assignments on a type if:
 577     // 1. there are no terms that share the same base type with un-normalized
 578     // representatives
 579     // 2. there are no terms that share teh same base type that are unevaluated
 580     // evaluable terms
 581     // Alternatively, if 2 or 3 don't hold but we are in a special
 582     // deadlock-breaking mode where assignOne is true, go ahead and make one
 583     // assignment
 584     changed = false;
 585     // must iterate over the ordered type list to ensure that we do not
 586     // enumerate values with subterms
 587     //  having types that we are currently enumerating (when possible)
 588     //  for example, this ensures we enumerate uninterpreted sort U before (List
 589     //  of U) and (Array U U)
 590     //  however, it does not break cyclic type dependencies for mutually
 591     //  recursive datatypes, but this is handled
 592     //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
 593     for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
 594     {
 595       TypeNode t = *type_it;
 596       // continue if there are no more equivalence classes of this type to
 597       // assign
 598       std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
 599       if (noRepSetPtr == NULL)
 600       {
 601         continue;
 602       }
 603       set<Node>& noRepSet = *noRepSetPtr;
 604       if (noRepSet.empty())
 605       {
 606         continue;
 607       }
 608
 609       // get properties of this type
 610       bool isCorecursive = false;
 611       if (t.isDatatype())
 612       {
 613         const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
 614         isCorecursive =
 615             dt.isCodatatype() && (!dt.isFinite(t.toType())
 616                                   || dt.isRecursiveSingleton(t.toType()));
 617       }
 618 #ifdef CVC4_ASSERTIONS
 619       bool isUSortFiniteRestricted = false;
 620       if (options::finiteModelFind())
 621       {
 622         isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
 623       }
 624 #endif
 625
 626       set<Node>* repSet = typeRepSet.getSet(t);
 627       TypeNode tb = t.getBaseType();
 628       if (!assignOne)
 629       {
 630         set<Node>* repSet = typeRepSet.getSet(tb);
 631         if (repSet != NULL && !repSet->empty())
 632         {
 633           continue;
 634         }
 635         if (evaluableSet.find(tb) != evaluableSet.end())
 636         {
 637           continue;
 638         }
 639       }
 640       Trace("model-builder") << "  Assign phase, working on type: " << t
 641                              << endl;
 642       bool assignable, evaluable CVC4_UNUSED;
 643       for (i = noRepSet.begin(); i != noRepSet.end();)
 644       {
 645         i2 = i;
 646         ++i;
 647         eq::EqClassIterator eqc_i =
 648             eq::EqClassIterator(*i2, tm->d_equalityEngine);
 649         assignable = false;
 650         evaluable = false;
 651         for (; !eqc_i.isFinished(); ++eqc_i)
 652         {
 653           Node n = *eqc_i;
 654           if (isAssignable(n))
 655           {
 656             assignable = true;
 657           }
 658           else
 659           {
 660             evaluable = true;
 661           }
 662         }
 663         Trace("model-builder-debug")
 664             << "    eqc " << *i2 << " is assignable=" << assignable
 665             << ", evaluable=" << evaluable << std::endl;
 666         if (assignable)
 667         {
 668           Assert(!evaluable || assignOne);
 669           // this assertion ensures that if we are assigning to a term of
 670           // Boolean type, then the term is either a variable or an APPLY_UF.
 671           // Note we only assign to terms of Boolean type if the term occurs in
 672           // a singleton equivalence class; otherwise the term would have been
 673           // in the equivalence class of true or false and would not need
 674           // assigning.
 675           Assert(!t.isBoolean() || (*i2).isVar()
 676                  || (*i2).getKind() == kind::APPLY_UF);
 677           Node n;
 678           if (t.getCardinality().isInfinite())
 679           {
 680             // if (!t.isInterpretedFinite()) {
 681             bool success;
 682             do
 683             {
 684               Trace("model-builder-debug") << "Enumerate term of type " << t
 685                                            << std::endl;
 686               n = typeConstSet.nextTypeEnum(t, true);
 687               //--- AJR: this code checks whether n is a legal value
 688               Assert(!n.isNull());
 689               success = true;
 690               Trace("model-builder-debug") << "Check if excluded : " << n
 691                                            << std::endl;
 692 #ifdef CVC4_ASSERTIONS
 693               if (isUSortFiniteRestricted)
 694               {
 695                 // must not involve uninterpreted constants beyond cardinality
 696                 // bound (which assumed to coincide with #eqc)
 697                 // this is just an assertion now, since TypeEnumeratorProperties
 698                 // should ensure that only legal values are enumerated wrt this
 699                 // constraint.
 700                 std::map<Node, bool> visited;
 701                 success = !isExcludedUSortValue(eqc_usort_count, n, visited);
 702                 if (!success)
 703                 {
 704                   Trace("model-builder")
 705                       << "Excluded value for " << t << " : " << n
 706                       << " due to out of range uninterpreted constant."
 707                       << std::endl;
 708                 }
 709                 Assert(success);
 710               }
 711 #endif
 712               if (success && isCorecursive)
 713               {
 714                 if (repSet != NULL && !repSet->empty())
 715                 {
 716                   // in the case of codatatypes, check if it is in the set of
 717                   // values that we cannot assign
 718                   success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
 719                   if (!success)
 720                   {
 721                     Trace("model-builder")
 722                         << "Excluded value : " << n
 723                         << " due to alpha-equivalent codatatype expression."
 724                         << std::endl;
 725                   }
 726                 }
 727               }
 728               //---
 729             } while (!success);
 730           }
 731           else
 732           {
 733             TypeEnumerator te(t);
 734             n = *te;
 735           }
 736           Assert(!n.isNull());
 737           assignConstantRep(tm, *i2, n);
 738           changed = true;
 739           noRepSet.erase(i2);
 740           if (assignOne)
 741           {
 742             assignOne = false;
 743             break;
 744           }
 745         }
 746       }
 747     }
 748
 749     // Corner case - I'm not sure this can even happen - but it's theoretically
 750     // possible to have a cyclical dependency
 751     // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In
 752     // this case, neither one will get assigned because we are waiting
 753     // to be able to evaluate.  But we will never be able to evaluate because
 754     // the variables that need to be assigned are in
 755     // these same EC's.  In this case, repeat the whole fixed-point computation
 756     // with the difference that the first EC
 757     // that has both assignable and evaluable expressions will get assigned.
 758     if (!changed)
 759     {
 760       Assert(!assignOne);  // check for infinite loop!
 761       assignOne = true;
 762     }
 763   }
 764
 765 #ifdef CVC4_ASSERTIONS
 766   // Assert that all representatives have been converted to constants
 767   for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
 768   {
 769     set<Node>& repSet = TypeSet::getSet(it);
 770     if (!repSet.empty())
 771     {
 772       Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
 773                              << ", first = " << *(repSet.begin()) << endl;
 774       Assert(false);
 775     }
 776   }
 777 #endif /* CVC4_ASSERTIONS */
 778
 779   Trace("model-builder") << "Copy representatives to model..." << std::endl;
 780   tm->d_reps.clear();
 781   std::map<Node, Node>::iterator itMap;
 782   for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
 783   {
 784     tm->d_reps[itMap->first] = itMap->second;
 785     tm->d_rep_set.add(itMap->second.getType(), itMap->second);
 786   }
 787
 788   Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
 789   // Make sure every EC has a rep
 790   for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
 791   {
 792     tm->d_reps[itMap->first] = itMap->second;
 793     tm->d_rep_set.add(itMap->second.getType(), itMap->second);
 794   }
 795   for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
 796   {
 797     set<Node>& noRepSet = TypeSet::getSet(it);
 798     set<Node>::iterator i;
 799     for (i = noRepSet.begin(); i != noRepSet.end(); ++i)
 800     {
 801       tm->d_reps[*i] = *i;
 802       tm->d_rep_set.add((*i).getType(), *i);
 803     }
 804   }
 805
 806   // modelBuilder-specific initialization
 807   if (!processBuildModel(tm))
 808   {
 809     return false;
 810   }
 811   else
 812   {
 813     tm->d_modelBuiltSuccess = true;
 814     return true;
 815   }
 816 }
 817
 818 void TheoryEngineModelBuilder::debugCheckModel(Model* m)
 819 {
 820   TheoryModel* tm = (TheoryModel*)m;
 821 #ifdef CVC4_ASSERTIONS
 822   Assert(tm->isBuilt());
 823   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
 824   std::map<Node, Node>::iterator itMap;
 825   // Check that every term evaluates to its representative in the model
 826   for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
 827        !eqcs_i.isFinished();
 828        ++eqcs_i)
 829   {
 830     // eqc is the equivalence class representative
 831     Node eqc = (*eqcs_i);
 832     // get the representative
 833     Node rep = tm->getRepresentative(eqc);
 834     if (!rep.isConst() && eqc.getType().isBoolean())
 835     {
 836       // if Boolean, it does not necessarily have a constant representative, use
 837       // get value instead
 838       rep = tm->getValue(eqc);
 839       Assert(rep.isConst());
 840     }
 841     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
 842     for (; !eqc_i.isFinished(); ++eqc_i)
 843     {
 844       Node n = *eqc_i;
 845       static int repCheckInstance = 0;
 846       ++repCheckInstance;
 847
 848       // non-linear mult is not necessarily accurate wrt getValue
 849       if (n.getKind() != kind::NONLINEAR_MULT)
 850       {
 851         Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
 852                                            << "n: " << n << endl
 853                                            << "getValue(n): " << tm->getValue(n)
 854                                            << endl
 855                                            << "rep: " << rep << endl;
 856         Assert(tm->getValue(*eqc_i) == rep,
 857                "run with -d check-model::rep-checking for details");
 858       }
 859     }
 860   }
 861 #endif /* CVC4_ASSERTIONS */
 862
 863   // builder-specific debugging
 864   debugModel(tm);
 865 }
 866
 867 Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
 868 {
 869   std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
 870   if (itMap != d_constantReps.end())
 871   {
 872     return (*itMap).second;
 873   }
 874   NodeMap::iterator it = d_normalizedCache.find(r);
 875   if (it != d_normalizedCache.end())
 876   {
 877     return (*it).second;
 878   }
 879   Trace("model-builder-debug") << "do normalize on " << r << std::endl;
 880   Node retNode = r;
 881   if (r.getNumChildren() > 0)
 882   {
 883     std::vector<Node> children;
 884     if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
 885     {
 886       children.push_back(r.getOperator());
 887     }
 888     bool childrenConst = true;
 889     for (size_t i = 0; i < r.getNumChildren(); ++i)
 890     {
 891       Node ri = r[i];
 892       bool recurse = true;
 893       if (!ri.isConst())
 894       {
 895         if (m->d_equalityEngine->hasTerm(ri))
 896         {
 897           itMap =
 898               d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
 899           if (itMap != d_constantReps.end())
 900           {
 901             ri = (*itMap).second;
 902             recurse = false;
 903           }
 904           else if (!evalOnly)
 905           {
 906             recurse = false;
 907           }
 908         }
 909         if (recurse)
 910         {
 911           ri = normalize(m, ri, evalOnly);
 912         }
 913         if (!ri.isConst())
 914         {
 915           childrenConst = false;
 916         }
 917       }
 918       children.push_back(ri);
 919     }
 920     retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
 921     if (childrenConst)
 922     {
 923       retNode = Rewriter::rewrite(retNode);
 924       Assert(retNode.getKind() == kind::APPLY_UF
 925              || !retNode.getType().isFirstClass()
 926              || retNode.isConst());
 927     }
 928   }
 929   d_normalizedCache[r] = retNode;
 930   return retNode;
 931 }
 932
 933 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
 934 {
 935   return true;
 936 }
 937
 938 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
 939 {
 940   if (m->areFunctionValuesEnabled())
 941   {
 942     assignFunctions(m);
 943   }
 944   return true;
 945 }
 946
 947 void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
 948 {
 949   Assert(!options::ufHo());
 950   uf::UfModelTree ufmt(f);
 951   Node default_v;
 952   for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
 953   {
 954     Node un = m->d_uf_terms[f][i];
 955     vector<TNode> children;
 956     children.push_back(f);
 957     Trace("model-builder-debug") << "  process term : " << un << std::endl;
 958     for (size_t j = 0; j < un.getNumChildren(); ++j)
 959     {
 960       Node rc = m->getRepresentative(un[j]);
 961       Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned "
 962                                     << rc << std::endl;
 963       Assert(rc.isConst());
 964       children.push_back(rc);
 965     }
 966     Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
 967     Node v = m->getRepresentative(un);
 968     Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")"
 969                            << endl;
 970     ufmt.setValue(m, simp, v);
 971     default_v = v;
 972   }
 973   if (default_v.isNull())
 974   {
 975     // choose default value from model if none exists
 976     TypeEnumerator te(f.getType().getRangeType());
 977     default_v = (*te);
 978   }
 979   ufmt.setDefaultValue(m, default_v);
 980   bool condenseFuncValues = options::condenseFunctionValues();
 981   if (condenseFuncValues)
 982   {
 983     ufmt.simplify();
 984   }
 985   std::stringstream ss;
 986   ss << "_arg_" << f << "_";
 987   Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
 988   m->assignFunctionDefinition(f, val);
 989   // ufmt.debugPrint( std::cout, m );
 990 }
 991
 992 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
 993 {
 994   Assert(options::ufHo());
 995   TypeNode type = f.getType();
 996   std::vector<TypeNode> argTypes = type.getArgTypes();
 997   std::vector<Node> args;
 998   std::vector<TNode> apply_args;
 999   for (unsigned i = 0; i < argTypes.size(); i++)
1000   {
1001     Node v = NodeManager::currentNM()->mkBoundVar(argTypes[i]);
1002     args.push_back(v);
1003     if (i > 0)
1004     {
1005       apply_args.push_back(v);
1006     }
1007   }
1008   // start with the base return value (currently we use the same default value
1009   // for all functions)
1010   TypeEnumerator te(type.getRangeType());
1011   Node curr = (*te);
1012   std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
1013   if (itht != m->d_ho_uf_terms.end())
1014   {
1015     for (size_t i = 0; i < itht->second.size(); i++)
1016     {
1017       Node hn = itht->second[i];
1018       Trace("model-builder-debug") << "    process : " << hn << std::endl;
1019       Assert(hn.getKind() == kind::HO_APPLY);
1020       Assert(m->areEqual(hn[0], f));
1021       Node hni = m->getRepresentative(hn[1]);
1022       Trace("model-builder-debug2") << "      get rep : " << hn[0]
1023                                     << " returned " << hni << std::endl;
1024       Assert(hni.isConst());
1025       Assert(hni.getType().isSubtypeOf(args[0].getType()));
1026       hni = Rewriter::rewrite(args[0].eqNode(hni));
1027       Node hnv = m->getRepresentative(hn);
1028       Trace("model-builder-debug2") << "      get rep val : " << hn
1029                                     << " returned " << hnv << std::endl;
1030       Assert(hnv.isConst());
1031       if (!apply_args.empty())
1032       {
1033         Assert(hnv.getKind() == kind::LAMBDA
1034                && hnv[0].getNumChildren() + 1 == args.size());
1035         std::vector<TNode> largs;
1036         for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
1037         {
1038           largs.push_back(hnv[0][j]);
1039         }
1040         Assert(largs.size() == apply_args.size());
1041         hnv = hnv[1].substitute(
1042             largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
1043         hnv = Rewriter::rewrite(hnv);
1044       }
1045       Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
1046                   .isNull());
1047       curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
1048     }
1049   }
1050   Node val = NodeManager::currentNM()->mkNode(
1051       kind::LAMBDA,
1052       NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args),
1053       curr);
1054   m->assignFunctionDefinition(f, val);
1055 }
1056
1057 // This struct is used to sort terms by the "size" of their type
1058 //   The size of the type is the number of nodes in the type, for example
1059 //  size of Int is 1
1060 //  size of Function( Int, Int ) is 3
1061 //  size of Function( Function( Bool, Int ), Int ) is 5
1062 struct sortTypeSize
1063 {
1064   // stores the size of the type
1065   std::map<TypeNode, unsigned> d_type_size;
1066   // get the size of type tn
1067   unsigned getTypeSize(TypeNode tn)
1068   {
1069     std::map<TypeNode, unsigned>::iterator it = d_type_size.find(tn);
1070     if (it != d_type_size.end())
1071     {
1072       return it->second;
1073     }
1074     else
1075     {
1076       unsigned sum = 1;
1077       for (unsigned i = 0; i < tn.getNumChildren(); i++)
1078       {
1079         sum += getTypeSize(tn[i]);
1080       }
1081       d_type_size[tn] = sum;
1082       return sum;
1083     }
1084   }
1085
1086  public:
1087   // compares the type size of i and j
1088   // returns true iff the size of i is less than that of j
1089   // tiebreaks are determined by node value
1090   bool operator()(Node i, Node j)
1091   {
1092     int si = getTypeSize(i.getType());
1093     int sj = getTypeSize(j.getType());
1094     if (si < sj)
1095     {
1096       return true;
1097     }
1098     else if (si == sj)
1099     {
1100       return i < j;
1101     }
1102     else
1103     {
1104       return false;
1105     }
1106   }
1107 };
1108
1109 void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
1110 {
1111   if (!options::assignFunctionValues())
1112   {
1113     return;
1114   }
1115   Trace("model-builder") << "Assigning function values..." << std::endl;
1116   std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
1117
1118   if (options::ufHo())
1119   {
1120     // sort based on type size if higher-order
1121     Trace("model-builder") << "Sort functions by type..." << std::endl;
1122     sortTypeSize sts;
1123     std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
1124   }
1125
1126   if (Trace.isOn("model-builder"))
1127   {
1128     Trace("model-builder") << "...have " << funcs_to_assign.size()
1129                            << " functions to assign:" << std::endl;
1130     for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1131     {
1132       Node f = funcs_to_assign[k];
1133       Trace("model-builder") << "  [" << k << "] : " << f << " : "
1134                              << f.getType() << std::endl;
1135     }
1136   }
1137
1138   // construct function values
1139   for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1140   {
1141     Node f = funcs_to_assign[k];
1142     Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
1143     // std::map< Node, std::vector< Node > >::iterator itht =
1144     // m->d_ho_uf_terms.find( f );
1145     if (!options::ufHo())
1146     {
1147       Trace("model-builder") << "  Assign function value for " << f
1148                              << " based on APPLY_UF" << std::endl;
1149       assignFunction(m, f);
1150     }
1151     else
1152     {
1153       Trace("model-builder") << "  Assign function value for " << f
1154                              << " based on curried HO_APPLY" << std::endl;
1155       assignHoFunction(m, f);
1156     }
1157   }
1158   Trace("model-builder") << "Finished assigning function values." << std::endl;
1159 }
1160
1161 } /* namespace CVC4::theory */
1162 } /* namespace CVC4 */