src/theory/theory_model_builder.cpp

   1 /*********************                                                        */
   2 /*! \file theory_model_builder.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Clark Barrett, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 "expr/dtype.h"
  17 #include "options/quantifiers_options.h"
  18 #include "options/smt_options.h"
  19 #include "options/uf_options.h"
  20 #include "theory/theory_engine.h"
  21 #include "theory/uf/theory_uf_model.h"
  22
  23 using namespace std;
  24 using namespace CVC4::kind;
  25 using namespace CVC4::context;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 void TheoryEngineModelBuilder::Assigner::initialize(
  31     TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
  32 {
  33   d_te.reset(new TypeEnumerator(tn, tep));
  34   d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
  35 }
  36
  37 Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
  38 {
  39   Assert(d_te != nullptr);
  40   Node n;
  41   bool success = false;
  42   TypeEnumerator& te = *d_te;
  43   // Check if we have run out of elements. This should never happen; if it
  44   // does we assert false and return null.
  45   if (te.isFinished())
  46   {
  47     Assert(false);
  48     return Node::null();
  49   }
  50   // must increment until we find one that is not in the assignment
  51   // exclusion set
  52   do
  53   {
  54     n = *te;
  55     success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
  56               == d_assignExcSet.end();
  57     // increment regardless of fail or succeed, to set up the next value
  58     ++te;
  59   } while (!success);
  60   return n;
  61 }
  62
  63 TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
  64 {
  65 }
  66
  67 Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
  68 {
  69   eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
  70   for (; !eqc_i.isFinished(); ++eqc_i)
  71   {
  72     Node n = *eqc_i;
  73     Trace("model-builder-debug") << "Look at term : " << n << std::endl;
  74     if (!isAssignable(n))
  75     {
  76       Trace("model-builder-debug") << "...try to normalize" << std::endl;
  77       Node normalized = normalize(m, n, true);
  78       if (normalized.isConst())
  79       {
  80         return normalized;
  81       }
  82     }
  83   }
  84   return Node::null();
  85 }
  86
  87 bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
  88 {
  89   if (a.d_isActive)
  90   {
  91     return true;
  92   }
  93   std::vector<Node>& eset = a.d_assignExcSet;
  94   std::map<Node, Node>::iterator it;
  95   for (unsigned i = 0, size = eset.size(); i < size; i++)
  96   {
  97     // Members of exclusion set must have values, otherwise we are not yet
  98     // assignable.
  99     Node er = eset[i];
 100     if (er.isConst())
 101     {
 102       // already processed
 103       continue;
 104     }
 105     // Assignable members of assignment exclusion set should be representatives
 106     // of their equivalence classes. This ensures we look up the constant
 107     // representatives for assignable members of assignment exclusion sets.
 108     Assert(er == tm->getRepresentative(er));
 109     it = d_constantReps.find(er);
 110     if (it == d_constantReps.end())
 111     {
 112       Trace("model-build-aes")
 113           << "isAssignerActive: not active due to " << er << std::endl;
 114       return false;
 115     }
 116     // update
 117     eset[i] = it->second;
 118   }
 119   Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
 120   a.d_isActive = true;
 121   return true;
 122 }
 123
 124 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 125 {
 126   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
 127   {
 128     // selectors are always assignable (where we guarantee that they are not
 129     // evaluatable here)
 130     if (!options::ufHo())
 131     {
 132       Assert(!n.getType().isFunction());
 133       return true;
 134     }
 135     else
 136     {
 137       // might be a function field
 138       return !n.getType().isFunction();
 139     }
 140   }
 141   else if (n.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGN)
 142   {
 143     // Extracting the sign of a floating-point number acts similar to a
 144     // selector on a datatype, i.e. if `(sign x)` wasn't assigned a value, we
 145     // can pick an arbitrary one. Note that the other components of a
 146     // floating-point number should always be assigned a value.
 147     return true;
 148   }
 149   else
 150   {
 151     // non-function variables, and fully applied functions
 152     if (!options::ufHo())
 153     {
 154       // no functions exist, all functions are fully applied
 155       Assert(n.getKind() != kind::HO_APPLY);
 156       Assert(!n.getType().isFunction());
 157       return n.isVar() || n.getKind() == kind::APPLY_UF;
 158     }
 159     else
 160     {
 161       // Assert( n.getKind() != kind::APPLY_UF );
 162       return (n.isVar() && !n.getType().isFunction())
 163              || n.getKind() == kind::APPLY_UF
 164              || (n.getKind() == kind::HO_APPLY
 165                  && n[0].getType().getNumChildren() == 2);
 166     }
 167   }
 168 }
 169
 170 void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
 171                                                      TheoryModel* tm,
 172                                                      NodeSet& cache)
 173 {
 174   if (n.isClosure())
 175   {
 176     return;
 177   }
 178   if (cache.find(n) != cache.end())
 179   {
 180     return;
 181   }
 182   if (isAssignable(n))
 183   {
 184     tm->d_equalityEngine->addTerm(n);
 185   }
 186   for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
 187   {
 188     addAssignableSubterms(*child_it, tm, cache);
 189   }
 190   cache.insert(n);
 191 }
 192
 193 void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
 194                                                  Node eqc,
 195                                                  Node const_rep)
 196 {
 197   d_constantReps[eqc] = const_rep;
 198   Trace("model-builder") << "    Assign: Setting constant rep of " << eqc
 199                          << " to " << const_rep << endl;
 200   tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
 201 }
 202
 203 bool TheoryEngineModelBuilder::isExcludedCdtValue(
 204     Node val,
 205     std::set<Node>* repSet,
 206     std::map<Node, Node>& assertedReps,
 207     Node eqc)
 208 {
 209   Trace("model-builder-debug")
 210       << "Is " << val << " and excluded codatatype value for " << eqc << "? "
 211       << std::endl;
 212   for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
 213   {
 214     Assert(assertedReps.find(*i) != assertedReps.end());
 215     Node rep = assertedReps[*i];
 216     Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
 217     // check matching val to rep with eqc as a free variable
 218     Node eqc_m;
 219     if (isCdtValueMatch(val, rep, eqc, eqc_m))
 220     {
 221       Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
 222                                    << eqc_m << std::endl;
 223       if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
 224       {
 225         Trace("model-builder-debug") << "*** " << val
 226                                      << " is excluded datatype for " << eqc
 227                                      << std::endl;
 228         return true;
 229       }
 230     }
 231   }
 232   return false;
 233 }
 234
 235 bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
 236                                                Node r,
 237                                                Node eqc,
 238                                                Node& eqc_m)
 239 {
 240   if (r == v)
 241   {
 242     return true;
 243   }
 244   else if (r == eqc)
 245   {
 246     if (eqc_m.isNull())
 247     {
 248       // only if an uninterpreted constant?
 249       eqc_m = v;
 250       return true;
 251     }
 252     else
 253     {
 254       return v == eqc_m;
 255     }
 256   }
 257   else if (v.getKind() == kind::APPLY_CONSTRUCTOR
 258            && r.getKind() == kind::APPLY_CONSTRUCTOR)
 259   {
 260     if (v.getOperator() == r.getOperator())
 261     {
 262       for (unsigned i = 0; i < v.getNumChildren(); i++)
 263       {
 264         if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
 265         {
 266           return false;
 267         }
 268       }
 269       return true;
 270     }
 271   }
 272   return false;
 273 }
 274
 275 bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
 276 {
 277   if (tn.isSort())
 278   {
 279     return true;
 280   }
 281   else if (tn.isArray())
 282   {
 283     return involvesUSort(tn.getArrayIndexType())
 284            || involvesUSort(tn.getArrayConstituentType());
 285   }
 286   else if (tn.isSet())
 287   {
 288     return involvesUSort(tn.getSetElementType());
 289   }
 290   else if (tn.isDatatype())
 291   {
 292     const DType& dt = tn.getDType();
 293     return dt.involvesUninterpretedType();
 294   }
 295   else
 296   {
 297     return false;
 298   }
 299 }
 300
 301 bool TheoryEngineModelBuilder::isExcludedUSortValue(
 302     std::map<TypeNode, unsigned>& eqc_usort_count,
 303     Node v,
 304     std::map<Node, bool>& visited)
 305 {
 306   Assert(v.isConst());
 307   if (visited.find(v) == visited.end())
 308   {
 309     visited[v] = true;
 310     TypeNode tn = v.getType();
 311     if (tn.isSort())
 312     {
 313       Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
 314                                    << tn << std::endl;
 315       unsigned card = eqc_usort_count[tn];
 316       Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
 317       unsigned index =
 318           v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
 319       Trace("model-builder-debug") << "  Index is " << index << std::endl;
 320       return index > 0 && index >= card;
 321     }
 322     for (unsigned i = 0; i < v.getNumChildren(); i++)
 323     {
 324       if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
 325       {
 326         return true;
 327       }
 328     }
 329   }
 330   return false;
 331 }
 332
 333 void TheoryEngineModelBuilder::addToTypeList(
 334     TypeNode tn,
 335     std::vector<TypeNode>& type_list,
 336     std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
 337 {
 338   if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
 339   {
 340     if (visiting.find(tn) == visiting.end())
 341     {
 342       visiting.insert(tn);
 343       /* This must make a recursive call on all types that are subterms of
 344        * values of the current type.
 345        * Note that recursive traversal here is over enumerated expressions
 346        * (very low expression depth). */
 347       if (tn.isArray())
 348       {
 349         addToTypeList(tn.getArrayIndexType(), type_list, visiting);
 350         addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
 351       }
 352       else if (tn.isSet())
 353       {
 354         addToTypeList(tn.getSetElementType(), type_list, visiting);
 355       }
 356       else if (tn.isDatatype())
 357       {
 358         const DType& dt = tn.getDType();
 359         for (unsigned i = 0; i < dt.getNumConstructors(); i++)
 360         {
 361           for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
 362           {
 363             TypeNode ctn = dt[i][j].getRangeType();
 364             addToTypeList(ctn, type_list, visiting);
 365           }
 366         }
 367       }
 368       Assert(std::find(type_list.begin(), type_list.end(), tn)
 369              == type_list.end());
 370       type_list.push_back(tn);
 371     }
 372   }
 373 }
 374
 375 bool TheoryEngineModelBuilder::buildModel(Model* m)
 376 {
 377   Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
 378   TheoryModel* tm = (TheoryModel*)m;
 379   eq::EqualityEngine* ee = tm->d_equalityEngine;
 380
 381   // buildModel should only be called once per check
 382   Assert(!tm->isBuilt());
 383
 384   // Reset model
 385   tm->reset();
 386
 387   // mark as built
 388   tm->d_modelBuilt = true;
 389   tm->d_modelBuiltSuccess = false;
 390
 391   // Collect model info from the theories
 392   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
 393                          << std::endl;
 394   if (!d_te->collectModelInfo(tm))
 395   {
 396     Trace("model-builder")
 397         << "TheoryEngineModelBuilder: fail collect model info" << std::endl;
 398     return false;
 399   }
 400
 401   Trace("model-builder")
 402       << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl;
 403   // model-builder specific initialization
 404   if (!preProcessBuildModel(tm))
 405   {
 406     Trace("model-builder")
 407         << "TheoryEngineModelBuilder: fail preprocess build model."
 408         << std::endl;
 409     return false;
 410   }
 411
 412   Trace("model-builder")
 413       << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl;
 414   // Loop through all terms and make sure that assignable sub-terms are in the
 415   // equality engine
 416   // Also, record #eqc per type (for finite model finding)
 417   std::map<TypeNode, unsigned> eqc_usort_count;
 418   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
 419   {
 420     NodeSet cache;
 421     for (; !eqcs_i.isFinished(); ++eqcs_i)
 422     {
 423       eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), ee);
 424       for (; !eqc_i.isFinished(); ++eqc_i)
 425       {
 426         addAssignableSubterms(*eqc_i, tm, cache);
 427       }
 428       TypeNode tn = (*eqcs_i).getType();
 429       if (tn.isSort())
 430       {
 431         if (eqc_usort_count.find(tn) == eqc_usort_count.end())
 432         {
 433           eqc_usort_count[tn] = 1;
 434         }
 435         else
 436         {
 437           eqc_usort_count[tn]++;
 438         }
 439       }
 440     }
 441   }
 442
 443   Trace("model-builder") << "Collect representatives..." << std::endl;
 444
 445   // Process all terms in the equality engine, store representatives for each EC
 446   d_constantReps.clear();
 447   std::map<Node, Node> assertedReps;
 448   TypeSet typeConstSet, typeRepSet, typeNoRepSet;
 449   // Compute type enumerator properties. This code ensures we do not
 450   // enumerate terms that have uninterpreted constants that violate the
 451   // bounds imposed by finite model finding. For example, if finite
 452   // model finding insists that there are only 2 values { U1, U2 } of type U,
 453   // then the type enumerator for list of U should enumerate:
 454   //   nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
 455   // instead of enumerating (cons U3 nil).
 456   TypeEnumeratorProperties tep;
 457   if (options::finiteModelFind())
 458   {
 459     tep.d_fixed_usort_card = true;
 460     for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
 461          it != eqc_usort_count.end();
 462          ++it)
 463     {
 464       Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
 465                              << it->second << std::endl;
 466       tep.d_fixed_card[it->first] = Integer(it->second);
 467     }
 468     typeConstSet.setTypeEnumeratorProperties(&tep);
 469   }
 470
 471   // AJR: build ordered list of types that ensures that base types are
 472   // enumerated first.
 473   // (I think) this is only strictly necessary for finite model finding +
 474   // parametric types instantiated with uninterpreted sorts, but is probably
 475   // a good idea to do in general since it leads to models with smaller term
 476   // sizes.
 477   std::vector<TypeNode> type_list;
 478   eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
 479   for (; !eqcs_i.isFinished(); ++eqcs_i)
 480   {
 481     // eqc is the equivalence class representative
 482     Node eqc = (*eqcs_i);
 483     Trace("model-builder") << "Processing EC: " << eqc << endl;
 484     Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
 485     TypeNode eqct = eqc.getType();
 486     Assert(assertedReps.find(eqc) == assertedReps.end());
 487     Assert(d_constantReps.find(eqc) == d_constantReps.end());
 488
 489     // Loop through terms in this EC
 490     Node rep, const_rep;
 491     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
 492     for (; !eqc_i.isFinished(); ++eqc_i)
 493     {
 494       Node n = *eqc_i;
 495       Trace("model-builder") << "  Processing Term: " << n << endl;
 496       // Record as rep if this node was specified as a representative
 497       if (tm->d_reps.find(n) != tm->d_reps.end())
 498       {
 499         // AJR: I believe this assertion is too strict,
 500         // e.g. datatypes may assert representative for two constructor terms
 501         // that are not in the care graph and are merged during
 502         // collectModelInfo.
 503         // Assert(rep.isNull());
 504         rep = tm->d_reps[n];
 505         Assert(!rep.isNull());
 506         Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep
 507                                << std::endl;
 508       }
 509       // Record as const_rep if this node is constant
 510       if (n.isConst())
 511       {
 512         Assert(const_rep.isNull());
 513         const_rep = n;
 514         Trace("model-builder") << "  ConstRep( " << eqc << " ) = " << const_rep
 515                                << std::endl;
 516       }
 517       // model-specific processing of the term
 518       tm->addTermInternal(n);
 519     }
 520
 521     // Assign representative for this EC
 522     if (!const_rep.isNull())
 523     {
 524       // Theories should not specify a rep if there is already a constant in the
 525       // EC
 526       // AJR: I believe this assertion is too strict, eqc with asserted reps may
 527       // merge with constant eqc
 528       // Assert(rep.isNull() || rep == const_rep);
 529       assignConstantRep(tm, eqc, const_rep);
 530       typeConstSet.add(eqct.getBaseType(), const_rep);
 531     }
 532     else if (!rep.isNull())
 533     {
 534       assertedReps[eqc] = rep;
 535       typeRepSet.add(eqct.getBaseType(), eqc);
 536       std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
 537       addToTypeList(eqct.getBaseType(), type_list, visiting);
 538     }
 539     else
 540     {
 541       typeNoRepSet.add(eqct, eqc);
 542       std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
 543       addToTypeList(eqct, type_list, visiting);
 544     }
 545   }
 546
 547   Trace("model-builder") << "Compute assignable information..." << std::endl;
 548   // The set of equivalence classes that are "assignable"
 549   std::unordered_set<Node, NodeHashFunction> assignableEqc;
 550   // The set of equivalence classes that are "evaluable"
 551   std::unordered_set<Node, NodeHashFunction> evaluableEqc;
 552   // Assigner objects for relevant equivalence classes
 553   std::map<Node, Assigner> eqcToAssigner;
 554   // Maps equivalence classes to the equivalence class that maps to its assigner
 555   // object in the above map.
 556   std::map<Node, Node> eqcToAssignerMaster;
 557   // Compute the above information
 558   computeAssignableInfo(
 559       tm, tep, assignableEqc, evaluableEqc, eqcToAssigner, eqcToAssignerMaster);
 560
 561   // Need to ensure that each EC has a constant representative.
 562
 563   Trace("model-builder") << "Processing EC's..." << std::endl;
 564
 565   TypeSet::iterator it;
 566   vector<TypeNode>::iterator type_it;
 567   set<Node>::iterator i, i2;
 568   bool changed, unassignedAssignable, assignOne = false;
 569   set<TypeNode> evaluableSet;
 570
 571   // Double-fixed-point loop
 572   // Outer loop handles a special corner case (see code at end of loop for
 573   // details)
 574   for (;;)
 575   {
 576     // Inner fixed-point loop: we are trying to learn constant values for every
 577     // EC.  Each time through this loop, we process all of the
 578     // types by type and may learn some new EC values.  EC's in one type may
 579     // depend on EC's in another type, so we need a fixed-point loop
 580     // to ensure that we learn as many EC values as possible
 581     do
 582     {
 583       changed = false;
 584       unassignedAssignable = false;
 585       evaluableSet.clear();
 586
 587       // Iterate over all types we've seen
 588       for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
 589       {
 590         TypeNode t = *type_it;
 591         TypeNode tb = t.getBaseType();
 592         set<Node>* noRepSet = typeNoRepSet.getSet(t);
 593
 594         // 1. Try to evaluate the EC's in this type
 595         if (noRepSet != NULL && !noRepSet->empty())
 596         {
 597           Trace("model-builder") << "  Eval phase, working on type: " << t
 598                                  << endl;
 599           bool evaluable;
 600           d_normalizedCache.clear();
 601           for (i = noRepSet->begin(); i != noRepSet->end();)
 602           {
 603             i2 = i;
 604             ++i;
 605             Trace("model-builder-debug") << "Look at eqc : " << (*i2)
 606                                          << std::endl;
 607             Node normalized;
 608             // only possible to normalize if we are evaluable
 609             evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
 610             if (evaluable)
 611             {
 612               normalized = evaluateEqc(tm, *i2);
 613             }
 614             if (!normalized.isNull())
 615             {
 616               Assert(normalized.isConst());
 617               typeConstSet.add(tb, normalized);
 618               assignConstantRep(tm, *i2, normalized);
 619               Trace("model-builder") << "    Eval: Setting constant rep of "
 620                                      << (*i2) << " to " << normalized << endl;
 621               changed = true;
 622               noRepSet->erase(i2);
 623             }
 624             else
 625             {
 626               if (evaluable)
 627               {
 628                 evaluableSet.insert(tb);
 629               }
 630               // If assignable, remember there is an equivalence class that is
 631               // not assigned and assignable.
 632               if (assignableEqc.find(*i2) != assignableEqc.end())
 633               {
 634                 unassignedAssignable = true;
 635               }
 636             }
 637           }
 638         }
 639
 640         // 2. Normalize any non-const representative terms for this type
 641         set<Node>* repSet = typeRepSet.getSet(t);
 642         if (repSet != NULL && !repSet->empty())
 643         {
 644           Trace("model-builder")
 645               << "  Normalization phase, working on type: " << t << endl;
 646           d_normalizedCache.clear();
 647           for (i = repSet->begin(); i != repSet->end();)
 648           {
 649             Assert(assertedReps.find(*i) != assertedReps.end());
 650             Node rep = assertedReps[*i];
 651             Node normalized = normalize(tm, rep, false);
 652             Trace("model-builder") << "    Normalizing rep (" << rep
 653                                    << "), normalized to (" << normalized << ")"
 654                                    << endl;
 655             if (normalized.isConst())
 656             {
 657               changed = true;
 658               typeConstSet.add(tb, normalized);
 659               assignConstantRep(tm, *i, normalized);
 660               assertedReps.erase(*i);
 661               i2 = i;
 662               ++i;
 663               repSet->erase(i2);
 664             }
 665             else
 666             {
 667               if (normalized != rep)
 668               {
 669                 assertedReps[*i] = normalized;
 670                 changed = true;
 671               }
 672               ++i;
 673             }
 674           }
 675         }
 676       }
 677     } while (changed);
 678
 679     if (!unassignedAssignable)
 680     {
 681       break;
 682     }
 683
 684     // 3. Assign unassigned assignable EC's using type enumeration - assign a
 685     // value *different* from all other EC's if the type is infinite
 686     // Assign first value from type enumerator otherwise - for finite types, we
 687     // rely on polite framework to ensure that EC's that have to be
 688     // different are different.
 689
 690     // Only make assignments on a type if:
 691     // 1. there are no terms that share the same base type with un-normalized
 692     // representatives
 693     // 2. there are no terms that share teh same base type that are unevaluated
 694     // evaluable terms
 695     // Alternatively, if 2 or 3 don't hold but we are in a special
 696     // deadlock-breaking mode where assignOne is true, go ahead and make one
 697     // assignment
 698     changed = false;
 699     // must iterate over the ordered type list to ensure that we do not
 700     // enumerate values with subterms
 701     //  having types that we are currently enumerating (when possible)
 702     //  for example, this ensures we enumerate uninterpreted sort U before (List
 703     //  of U) and (Array U U)
 704     //  however, it does not break cyclic type dependencies for mutually
 705     //  recursive datatypes, but this is handled
 706     //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
 707     for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
 708     {
 709       TypeNode t = *type_it;
 710       // continue if there are no more equivalence classes of this type to
 711       // assign
 712       std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
 713       if (noRepSetPtr == NULL)
 714       {
 715         continue;
 716       }
 717       set<Node>& noRepSet = *noRepSetPtr;
 718       if (noRepSet.empty())
 719       {
 720         continue;
 721       }
 722
 723       // get properties of this type
 724       bool isCorecursive = false;
 725       if (t.isDatatype())
 726       {
 727         const DType& dt = t.getDType();
 728         isCorecursive = dt.isCodatatype()
 729                         && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
 730       }
 731 #ifdef CVC4_ASSERTIONS
 732       bool isUSortFiniteRestricted = false;
 733       if (options::finiteModelFind())
 734       {
 735         isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
 736       }
 737 #endif
 738
 739       set<Node>* repSet = typeRepSet.getSet(t);
 740       TypeNode tb = t.getBaseType();
 741       if (!assignOne)
 742       {
 743         set<Node>* repSet = typeRepSet.getSet(tb);
 744         if (repSet != NULL && !repSet->empty())
 745         {
 746           continue;
 747         }
 748         if (evaluableSet.find(tb) != evaluableSet.end())
 749         {
 750           continue;
 751         }
 752       }
 753       Trace("model-builder") << "  Assign phase, working on type: " << t
 754                              << endl;
 755       bool assignable, evaluable CVC4_UNUSED;
 756       std::map<Node, Assigner>::iterator itAssigner;
 757       std::map<Node, Node>::iterator itAssignerM;
 758       for (i = noRepSet.begin(); i != noRepSet.end();)
 759       {
 760         i2 = i;
 761         ++i;
 762         // check whether it has an assigner object
 763         itAssignerM = eqcToAssignerMaster.find(*i2);
 764         if (itAssignerM != eqcToAssignerMaster.end())
 765         {
 766           // Take the master's assigner. Notice we don't care which order
 767           // equivalence classes are assigned. For instance, the master can
 768           // be assigned after one of its slaves.
 769           itAssigner = eqcToAssigner.find(itAssignerM->second);
 770         }
 771         else
 772         {
 773           itAssigner = eqcToAssigner.find(*i2);
 774         }
 775         if (itAssigner != eqcToAssigner.end())
 776         {
 777           assignable = isAssignerActive(tm, itAssigner->second);
 778         }
 779         else
 780         {
 781           assignable = assignableEqc.find(*i2) != assignableEqc.end();
 782         }
 783         evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
 784         Trace("model-builder-debug")
 785             << "    eqc " << *i2 << " is assignable=" << assignable
 786             << ", evaluable=" << evaluable << std::endl;
 787         if (assignable)
 788         {
 789           Assert(!evaluable || assignOne);
 790           // this assertion ensures that if we are assigning to a term of
 791           // Boolean type, then the term is either a variable or an APPLY_UF.
 792           // Note we only assign to terms of Boolean type if the term occurs in
 793           // a singleton equivalence class; otherwise the term would have been
 794           // in the equivalence class of true or false and would not need
 795           // assigning.
 796           Assert(!t.isBoolean() || (*i2).isVar()
 797                  || (*i2).getKind() == kind::APPLY_UF);
 798           Node n;
 799           if (itAssigner != eqcToAssigner.end())
 800           {
 801             Trace("model-builder-debug")
 802                 << "Get value from assigner for finite type..." << std::endl;
 803             // if it has an assigner, get the value from the assigner.
 804             n = itAssigner->second.getNextAssignment();
 805             Assert(!n.isNull());
 806           }
 807           else if (!t.isFinite())
 808           {
 809             // if its infinite, we get a fresh value that does not occur in
 810             // the model.
 811             bool success;
 812             do
 813             {
 814               Trace("model-builder-debug") << "Enumerate term of type " << t
 815                                            << std::endl;
 816               n = typeConstSet.nextTypeEnum(t, true);
 817               //--- AJR: this code checks whether n is a legal value
 818               Assert(!n.isNull());
 819               success = true;
 820               Trace("model-builder-debug") << "Check if excluded : " << n
 821                                            << std::endl;
 822 #ifdef CVC4_ASSERTIONS
 823               if (isUSortFiniteRestricted)
 824               {
 825                 // must not involve uninterpreted constants beyond cardinality
 826                 // bound (which assumed to coincide with #eqc)
 827                 // this is just an assertion now, since TypeEnumeratorProperties
 828                 // should ensure that only legal values are enumerated wrt this
 829                 // constraint.
 830                 std::map<Node, bool> visited;
 831                 success = !isExcludedUSortValue(eqc_usort_count, n, visited);
 832                 if (!success)
 833                 {
 834                   Trace("model-builder")
 835                       << "Excluded value for " << t << " : " << n
 836                       << " due to out of range uninterpreted constant."
 837                       << std::endl;
 838                 }
 839                 Assert(success);
 840               }
 841 #endif
 842               if (success && isCorecursive)
 843               {
 844                 if (repSet != NULL && !repSet->empty())
 845                 {
 846                   // in the case of codatatypes, check if it is in the set of
 847                   // values that we cannot assign
 848                   success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
 849                   if (!success)
 850                   {
 851                     Trace("model-builder")
 852                         << "Excluded value : " << n
 853                         << " due to alpha-equivalent codatatype expression."
 854                         << std::endl;
 855                   }
 856                 }
 857               }
 858               //---
 859             } while (!success);
 860             Assert(!n.isNull());
 861           }
 862           else
 863           {
 864             Trace("model-builder-debug")
 865                 << "Get first value from finite type..." << std::endl;
 866             // Otherwise, we get the first value from the type enumerator.
 867             TypeEnumerator te(t);
 868             n = *te;
 869           }
 870           Trace("model-builder-debug") << "...got " << n << std::endl;
 871           assignConstantRep(tm, *i2, n);
 872           changed = true;
 873           noRepSet.erase(i2);
 874           if (assignOne)
 875           {
 876             assignOne = false;
 877             break;
 878           }
 879         }
 880       }
 881     }
 882
 883     // Corner case - I'm not sure this can even happen - but it's theoretically
 884     // possible to have a cyclical dependency
 885     // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In
 886     // this case, neither one will get assigned because we are waiting
 887     // to be able to evaluate.  But we will never be able to evaluate because
 888     // the variables that need to be assigned are in
 889     // these same EC's.  In this case, repeat the whole fixed-point computation
 890     // with the difference that the first EC
 891     // that has both assignable and evaluable expressions will get assigned.
 892     if (!changed)
 893     {
 894       Assert(!assignOne);  // check for infinite loop!
 895       assignOne = true;
 896     }
 897   }
 898
 899 #ifdef CVC4_ASSERTIONS
 900   // Assert that all representatives have been converted to constants
 901   for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
 902   {
 903     set<Node>& repSet = TypeSet::getSet(it);
 904     if (!repSet.empty())
 905     {
 906       Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
 907                              << ", first = " << *(repSet.begin()) << endl;
 908       Assert(false);
 909     }
 910   }
 911 #endif /* CVC4_ASSERTIONS */
 912
 913   Trace("model-builder") << "Copy representatives to model..." << std::endl;
 914   tm->d_reps.clear();
 915   std::map<Node, Node>::iterator itMap;
 916   for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
 917   {
 918     tm->d_reps[itMap->first] = itMap->second;
 919     tm->d_rep_set.add(itMap->second.getType(), itMap->second);
 920   }
 921
 922   Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
 923   // Make sure every EC has a rep
 924   for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
 925   {
 926     tm->d_reps[itMap->first] = itMap->second;
 927     tm->d_rep_set.add(itMap->second.getType(), itMap->second);
 928   }
 929   for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
 930   {
 931     set<Node>& noRepSet = TypeSet::getSet(it);
 932     set<Node>::iterator i;
 933     for (i = noRepSet.begin(); i != noRepSet.end(); ++i)
 934     {
 935       tm->d_reps[*i] = *i;
 936       tm->d_rep_set.add((*i).getType(), *i);
 937     }
 938   }
 939
 940   // modelBuilder-specific initialization
 941   if (!processBuildModel(tm))
 942   {
 943     Trace("model-builder")
 944         << "TheoryEngineModelBuilder: fail process build model." << std::endl;
 945     return false;
 946   }
 947   Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
 948   tm->d_modelBuiltSuccess = true;
 949   return true;
 950 }
 951 void TheoryEngineModelBuilder::computeAssignableInfo(
 952     TheoryModel* tm,
 953     TypeEnumeratorProperties& tep,
 954     std::unordered_set<Node, NodeHashFunction>& assignableEqc,
 955     std::unordered_set<Node, NodeHashFunction>& evaluableEqc,
 956     std::map<Node, Assigner>& eqcToAssigner,
 957     std::map<Node, Node>& eqcToAssignerMaster)
 958 {
 959   eq::EqualityEngine* ee = tm->d_equalityEngine;
 960   bool computeAssigners = tm->hasAssignmentExclusionSets();
 961   std::unordered_set<Node, NodeHashFunction> processed;
 962   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
 963   // A flag set to true if the current equivalence class is assignable (see
 964   // assignableEqc).
 965   bool assignable = false;
 966   // Set to true if the current equivalence class is evaluatable (see
 967   // evaluableEqc).
 968   bool evaluable = false;
 969   // Set to true if a term in the current equivalence class has been given an
 970   // assignment exclusion set.
 971   bool hasESet = false;
 972   // Set to true if we found that a term in the current equivalence class has
 973   // been given an assignment exclusion set, and we have not seen this term
 974   // as part of a previous assignment exclusion group. In other words, when
 975   // this flag is true we construct a new assigner object with the current
 976   // equivalence class as its master.
 977   bool foundESet = false;
 978   // Look at all equivalence classes in the model
 979   for (; !eqcs_i.isFinished(); ++eqcs_i)
 980   {
 981     Node eqc = *eqcs_i;
 982     if (d_constantReps.find(eqc) != d_constantReps.end())
 983     {
 984       // already assigned above, skip
 985       continue;
 986     }
 987     // reset information for the current equivalence classe
 988     assignable = false;
 989     evaluable = false;
 990     hasESet = false;
 991     foundESet = false;
 992     // the assignment exclusion set for the current equivalence class
 993     std::vector<Node> eset;
 994     // the group to which this equivalence class belongs when exclusion sets
 995     // were assigned (see the argument group of
 996     // TheoryModel::getAssignmentExclusionSet).
 997     std::vector<Node> group;
 998     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
 999     // For each term in the current equivalence class, we update the above
1000     // information. We may terminate this loop before looking at all terms if we
1001     // have inferred the value of all of the information above.
1002     for (; !eqc_i.isFinished(); ++eqc_i)
1003     {
1004       Node n = *eqc_i;
1005       if (!isAssignable(n))
1006       {
1007         evaluable = true;
1008         if (!computeAssigners)
1009         {
1010           if (assignable)
1011           {
1012             // both flags set, we are done
1013             break;
1014           }
1015         }
1016         // expressions that are not assignable should not be given assignment
1017         // exclusion sets
1018         Assert(!tm->getAssignmentExclusionSet(n, group, eset));
1019         continue;
1020       }
1021       else
1022       {
1023         assignable = true;
1024         if (!computeAssigners)
1025         {
1026           if (evaluable)
1027           {
1028             // both flags set, we are done
1029             break;
1030           }
1031           // we don't compute assigners, skip
1032           continue;
1033         }
1034       }
1035       // process the assignment exclusion set for term n
1036       // was it processed as a slave of a group?
1037       if (processed.find(n) != processed.end())
1038       {
1039         // Should not have two assignment exclusion sets for the same
1040         // equivalence class
1041         Assert(!hasESet);
1042         Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
1043         // already processed as a slave term
1044         hasESet = true;
1045         continue;
1046       }
1047       // was it assigned one?
1048       if (tm->getAssignmentExclusionSet(n, group, eset))
1049       {
1050         // Should not have two assignment exclusion sets for the same
1051         // equivalence class
1052         Assert(!hasESet);
1053         foundESet = true;
1054         hasESet = true;
1055       }
1056     }
1057     if (assignable)
1058     {
1059       assignableEqc.insert(eqc);
1060     }
1061     if (evaluable)
1062     {
1063       evaluableEqc.insert(eqc);
1064     }
1065     // If we found an assignment exclusion set, we construct a new assigner
1066     // object.
1067     if (foundESet)
1068     {
1069       // we don't accept assignment exclusion sets for evaluable eqc
1070       Assert(!evaluable);
1071       // construct the assigner
1072       Assigner& a = eqcToAssigner[eqc];
1073       // Take the representatives of each term in the assignment exclusion
1074       // set, which ensures we can look up their value in d_constReps later.
1075       std::vector<Node> aes;
1076       for (const Node& e : eset)
1077       {
1078         // Should only supply terms that occur in the model or constants
1079         // in assignment exclusion sets.
1080         Assert(tm->hasTerm(e) || e.isConst());
1081         Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
1082         aes.push_back(er);
1083       }
1084       // initialize
1085       a.initialize(eqc.getType(), &tep, aes);
1086       // all others in the group are slaves of this
1087       for (const Node& g : group)
1088       {
1089         Assert(isAssignable(g));
1090         if (!tm->hasTerm(g))
1091         {
1092           // Ignore those that aren't in the model, in the case the user
1093           // has supplied an assignment exclusion set to a variable not in
1094           // the model.
1095           continue;
1096         }
1097         Node gr = tm->getRepresentative(g);
1098         if (gr != eqc)
1099         {
1100           eqcToAssignerMaster[gr] = eqc;
1101           // remember that this term has been processed
1102           processed.insert(g);
1103         }
1104       }
1105     }
1106   }
1107 }
1108
1109 void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
1110 {
1111   // if we are incomplete, there is no guarantee on the model.
1112   // thus, we do not check the model here.
1113   if (incomplete)
1114   {
1115     return;
1116   }
1117   TheoryModel* tm = static_cast<TheoryModel*>(m);
1118   Assert(tm != nullptr);
1119   // debug-check the model if the checkModels() is enabled.
1120   if (options::checkModels())
1121   {
1122     debugCheckModel(tm);
1123   }
1124 }
1125
1126 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
1127 {
1128 #ifdef CVC4_ASSERTIONS
1129   Assert(tm->isBuilt());
1130   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1131   std::map<Node, Node>::iterator itMap;
1132   // Check that every term evaluates to its representative in the model
1133   for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
1134        !eqcs_i.isFinished();
1135        ++eqcs_i)
1136   {
1137     // eqc is the equivalence class representative
1138     Node eqc = (*eqcs_i);
1139     // get the representative
1140     Node rep = tm->getRepresentative(eqc);
1141     if (!rep.isConst() && eqc.getType().isBoolean())
1142     {
1143       // if Boolean, it does not necessarily have a constant representative, use
1144       // get value instead
1145       rep = tm->getValue(eqc);
1146       Assert(rep.isConst());
1147     }
1148     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
1149     for (; !eqc_i.isFinished(); ++eqc_i)
1150     {
1151       Node n = *eqc_i;
1152       static int repCheckInstance = 0;
1153       ++repCheckInstance;
1154
1155       // non-linear mult is not necessarily accurate wrt getValue
1156       if (n.getKind() != kind::NONLINEAR_MULT)
1157       {
1158         Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
1159                                            << "n: " << n << endl
1160                                            << "getValue(n): " << tm->getValue(n)
1161                                            << endl
1162                                            << "rep: " << rep << endl;
1163         Assert(tm->getValue(*eqc_i) == rep)
1164             << "run with -d check-model::rep-checking for details";
1165       }
1166     }
1167   }
1168 #endif /* CVC4_ASSERTIONS */
1169
1170   // builder-specific debugging
1171   debugModel(tm);
1172 }
1173
1174 Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
1175 {
1176   std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
1177   if (itMap != d_constantReps.end())
1178   {
1179     return (*itMap).second;
1180   }
1181   NodeMap::iterator it = d_normalizedCache.find(r);
1182   if (it != d_normalizedCache.end())
1183   {
1184     return (*it).second;
1185   }
1186   Trace("model-builder-debug") << "do normalize on " << r << std::endl;
1187   Node retNode = r;
1188   if (r.getNumChildren() > 0)
1189   {
1190     std::vector<Node> children;
1191     if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
1192     {
1193       children.push_back(r.getOperator());
1194     }
1195     bool childrenConst = true;
1196     for (size_t i = 0; i < r.getNumChildren(); ++i)
1197     {
1198       Node ri = r[i];
1199       bool recurse = true;
1200       if (!ri.isConst())
1201       {
1202         if (m->d_equalityEngine->hasTerm(ri))
1203         {
1204           itMap =
1205               d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
1206           if (itMap != d_constantReps.end())
1207           {
1208             ri = (*itMap).second;
1209             recurse = false;
1210           }
1211           else if (!evalOnly)
1212           {
1213             recurse = false;
1214           }
1215         }
1216         if (recurse)
1217         {
1218           ri = normalize(m, ri, evalOnly);
1219         }
1220         if (!ri.isConst())
1221         {
1222           childrenConst = false;
1223         }
1224       }
1225       children.push_back(ri);
1226     }
1227     retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
1228     if (childrenConst)
1229     {
1230       retNode = Rewriter::rewrite(retNode);
1231       Assert(retNode.getKind() == kind::APPLY_UF
1232              || !retNode.getType().isFirstClass() || retNode.isConst());
1233     }
1234   }
1235   d_normalizedCache[r] = retNode;
1236   return retNode;
1237 }
1238
1239 bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
1240 {
1241   return true;
1242 }
1243
1244 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
1245 {
1246   if (m->areFunctionValuesEnabled())
1247   {
1248     assignFunctions(m);
1249   }
1250   return true;
1251 }
1252
1253 void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
1254 {
1255   Assert(!options::ufHo());
1256   uf::UfModelTree ufmt(f);
1257   Node default_v;
1258   for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
1259   {
1260     Node un = m->d_uf_terms[f][i];
1261     vector<TNode> children;
1262     children.push_back(f);
1263     Trace("model-builder-debug") << "  process term : " << un << std::endl;
1264     for (size_t j = 0; j < un.getNumChildren(); ++j)
1265     {
1266       Node rc = m->getRepresentative(un[j]);
1267       Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned "
1268                                     << rc << std::endl;
1269       Assert(rc.isConst());
1270       children.push_back(rc);
1271     }
1272     Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
1273     Node v = m->getRepresentative(un);
1274     Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")"
1275                            << endl;
1276     ufmt.setValue(m, simp, v);
1277     default_v = v;
1278   }
1279   if (default_v.isNull())
1280   {
1281     // choose default value from model if none exists
1282     TypeEnumerator te(f.getType().getRangeType());
1283     default_v = (*te);
1284   }
1285   ufmt.setDefaultValue(m, default_v);
1286   bool condenseFuncValues = options::condenseFunctionValues();
1287   if (condenseFuncValues)
1288   {
1289     ufmt.simplify();
1290   }
1291   std::stringstream ss;
1292   ss << "_arg_";
1293   Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
1294   m->assignFunctionDefinition(f, val);
1295   // ufmt.debugPrint( std::cout, m );
1296 }
1297
1298 void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
1299 {
1300   Assert(options::ufHo());
1301   TypeNode type = f.getType();
1302   std::vector<TypeNode> argTypes = type.getArgTypes();
1303   std::vector<Node> args;
1304   std::vector<TNode> apply_args;
1305   for (unsigned i = 0; i < argTypes.size(); i++)
1306   {
1307     Node v = NodeManager::currentNM()->mkBoundVar(argTypes[i]);
1308     args.push_back(v);
1309     if (i > 0)
1310     {
1311       apply_args.push_back(v);
1312     }
1313   }
1314   // start with the base return value (currently we use the same default value
1315   // for all functions)
1316   TypeEnumerator te(type.getRangeType());
1317   Node curr = (*te);
1318   std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
1319   if (itht != m->d_ho_uf_terms.end())
1320   {
1321     for (size_t i = 0; i < itht->second.size(); i++)
1322     {
1323       Node hn = itht->second[i];
1324       Trace("model-builder-debug") << "    process : " << hn << std::endl;
1325       Assert(hn.getKind() == kind::HO_APPLY);
1326       Assert(m->areEqual(hn[0], f));
1327       Node hni = m->getRepresentative(hn[1]);
1328       Trace("model-builder-debug2") << "      get rep : " << hn[0]
1329                                     << " returned " << hni << std::endl;
1330       Assert(hni.isConst());
1331       Assert(hni.getType().isSubtypeOf(args[0].getType()));
1332       hni = Rewriter::rewrite(args[0].eqNode(hni));
1333       Node hnv = m->getRepresentative(hn);
1334       Trace("model-builder-debug2") << "      get rep val : " << hn
1335                                     << " returned " << hnv << std::endl;
1336       Assert(hnv.isConst());
1337       if (!apply_args.empty())
1338       {
1339         Assert(hnv.getKind() == kind::LAMBDA
1340                && hnv[0].getNumChildren() + 1 == args.size());
1341         std::vector<TNode> largs;
1342         for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
1343         {
1344           largs.push_back(hnv[0][j]);
1345         }
1346         Assert(largs.size() == apply_args.size());
1347         hnv = hnv[1].substitute(
1348             largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
1349         hnv = Rewriter::rewrite(hnv);
1350       }
1351       Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
1352                   .isNull());
1353       curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
1354     }
1355   }
1356   Node val = NodeManager::currentNM()->mkNode(
1357       kind::LAMBDA,
1358       NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args),
1359       curr);
1360   m->assignFunctionDefinition(f, val);
1361 }
1362
1363 // This struct is used to sort terms by the "size" of their type
1364 //   The size of the type is the number of nodes in the type, for example
1365 //  size of Int is 1
1366 //  size of Function( Int, Int ) is 3
1367 //  size of Function( Function( Bool, Int ), Int ) is 5
1368 struct sortTypeSize
1369 {
1370   // stores the size of the type
1371   std::map<TypeNode, unsigned> d_type_size;
1372   // get the size of type tn
1373   unsigned getTypeSize(TypeNode tn)
1374   {
1375     std::map<TypeNode, unsigned>::iterator it = d_type_size.find(tn);
1376     if (it != d_type_size.end())
1377     {
1378       return it->second;
1379     }
1380     else
1381     {
1382       unsigned sum = 1;
1383       for (unsigned i = 0; i < tn.getNumChildren(); i++)
1384       {
1385         sum += getTypeSize(tn[i]);
1386       }
1387       d_type_size[tn] = sum;
1388       return sum;
1389     }
1390   }
1391
1392  public:
1393   // compares the type size of i and j
1394   // returns true iff the size of i is less than that of j
1395   // tiebreaks are determined by node value
1396   bool operator()(Node i, Node j)
1397   {
1398     int si = getTypeSize(i.getType());
1399     int sj = getTypeSize(j.getType());
1400     if (si < sj)
1401     {
1402       return true;
1403     }
1404     else if (si == sj)
1405     {
1406       return i < j;
1407     }
1408     else
1409     {
1410       return false;
1411     }
1412   }
1413 };
1414
1415 void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
1416 {
1417   if (!options::assignFunctionValues())
1418   {
1419     return;
1420   }
1421   Trace("model-builder") << "Assigning function values..." << std::endl;
1422   std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
1423
1424   if (options::ufHo())
1425   {
1426     // sort based on type size if higher-order
1427     Trace("model-builder") << "Sort functions by type..." << std::endl;
1428     sortTypeSize sts;
1429     std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
1430   }
1431
1432   if (Trace.isOn("model-builder"))
1433   {
1434     Trace("model-builder") << "...have " << funcs_to_assign.size()
1435                            << " functions to assign:" << std::endl;
1436     for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1437     {
1438       Node f = funcs_to_assign[k];
1439       Trace("model-builder") << "  [" << k << "] : " << f << " : "
1440                              << f.getType() << std::endl;
1441     }
1442   }
1443
1444   // construct function values
1445   for (unsigned k = 0; k < funcs_to_assign.size(); k++)
1446   {
1447     Node f = funcs_to_assign[k];
1448     Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
1449     // std::map< Node, std::vector< Node > >::iterator itht =
1450     // m->d_ho_uf_terms.find( f );
1451     if (!options::ufHo())
1452     {
1453       Trace("model-builder") << "  Assign function value for " << f
1454                              << " based on APPLY_UF" << std::endl;
1455       assignFunction(m, f);
1456     }
1457     else
1458     {
1459       Trace("model-builder") << "  Assign function value for " << f
1460                              << " based on curried HO_APPLY" << std::endl;
1461       assignHoFunction(m, f);
1462     }
1463   }
1464   Trace("model-builder") << "Finished assigning function values." << std::endl;
1465 }
1466
1467 } /* namespace CVC4::theory */
1468 } /* namespace CVC4 */