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