src/theory/theory_model.cpp

   1 /*********************                                                        */
   2 /*! \file theory_model.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Clark Barrett, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of model class
  13  **/
  14 #include "theory/theory_model.h"
  15
  16 #include "expr/node_algorithm.h"
  17 #include "options/quantifiers_options.h"
  18 #include "options/smt_options.h"
  19 #include "options/theory_options.h"
  20 #include "options/uf_options.h"
  21 #include "smt/smt_engine.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 TheoryModel::TheoryModel(context::Context* c,
  31                          std::string name,
  32                          bool enableFuncModels)
  33     : d_name(name),
  34       d_substitutions(c, false),
  35       d_equalityEngine(nullptr),
  36       d_using_model_core(false),
  37       d_enableFuncModels(enableFuncModels)
  38 {
  39   // must use function models when ufHo is enabled
  40   Assert(d_enableFuncModels || !options::ufHo());
  41   d_true = NodeManager::currentNM()->mkConst( true );
  42   d_false = NodeManager::currentNM()->mkConst( false );
  43 }
  44
  45 TheoryModel::~TheoryModel() {}
  46
  47 void TheoryModel::finishInit(eq::EqualityEngine* ee)
  48 {
  49   Assert(ee != nullptr);
  50   d_equalityEngine = ee;
  51   // The kinds we are treating as function application in congruence
  52   d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
  53   d_equalityEngine->addFunctionKind(kind::HO_APPLY);
  54   d_equalityEngine->addFunctionKind(kind::SELECT);
  55   // d_equalityEngine->addFunctionKind(kind::STORE);
  56   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
  57   d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
  58   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
  59   // do not interpret APPLY_UF if we are not assigning function values
  60   if (!d_enableFuncModels)
  61   {
  62     setSemiEvaluatedKind(kind::APPLY_UF);
  63   }
  64   // Equal and not terms are not relevant terms. In other words, asserted
  65   // equalities and negations of predicates (as terms) do not need to be sent
  66   // to the model. Regardless, theories should send information to the model
  67   // that ensures that all assertions are satisfied.
  68   setIrrelevantKind(EQUAL);
  69   setIrrelevantKind(NOT);
  70 }
  71
  72 void TheoryModel::reset(){
  73   d_modelCache.clear();
  74   d_comment_str.clear();
  75   d_sep_heap = Node::null();
  76   d_sep_nil_eq = Node::null();
  77   d_approximations.clear();
  78   d_approx_list.clear();
  79   d_reps.clear();
  80   d_assignExcSet.clear();
  81   d_aesMaster.clear();
  82   d_aesSlaves.clear();
  83   d_rep_set.clear();
  84   d_uf_terms.clear();
  85   d_ho_uf_terms.clear();
  86   d_uf_models.clear();
  87   d_using_model_core = false;
  88   d_model_core.clear();
  89 }
  90
  91 void TheoryModel::getComments(std::ostream& out) const {
  92   Trace("model-builder") << "get comments..." << std::endl;
  93   out << d_comment_str.str();
  94 }
  95
  96 void TheoryModel::setHeapModel( Node h, Node neq ) {
  97   d_sep_heap = h;
  98   d_sep_nil_eq = neq;
  99 }
 100
 101 bool TheoryModel::getHeapModel(Node& h, Node& neq) const
 102 {
 103   if (d_sep_heap.isNull() || d_sep_nil_eq.isNull())
 104   {
 105     return false;
 106   }
 107   h = d_sep_heap;
 108   neq = d_sep_nil_eq;
 109   return true;
 110 }
 111
 112 bool TheoryModel::hasApproximations() const { return !d_approx_list.empty(); }
 113
 114 std::vector<std::pair<Node, Node> > TheoryModel::getApproximations() const
 115 {
 116   return d_approx_list;
 117 }
 118
 119 std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const
 120 {
 121   // must be an uninterpreted sort
 122   Assert(tn.isSort());
 123   std::vector<Node> elements;
 124   const std::vector<Node>* type_refs = d_rep_set.getTypeRepsOrNull(tn);
 125   if (type_refs == nullptr || type_refs->empty())
 126   {
 127     // This is called when t is a sort that does not occur in this model.
 128     // Sorts are always interpreted as non-empty, thus we add a single element.
 129     elements.push_back(tn.mkGroundTerm());
 130     return elements;
 131   }
 132   return *type_refs;
 133 }
 134
 135 Node TheoryModel::getValue(TNode n) const
 136 {
 137   //apply substitutions
 138   Node nn = d_substitutions.apply(n);
 139   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
 140   //get value in model
 141   nn = getModelValue(nn);
 142   if (nn.isNull()) return nn;
 143   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
 144     //normalize
 145     nn = Rewriter::rewrite(nn);
 146   }
 147   Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
 148                           << "[model-getvalue] returning " << nn << std::endl;
 149   return nn;
 150 }
 151
 152 bool TheoryModel::isModelCoreSymbol(Node s) const
 153 {
 154   if (!d_using_model_core)
 155   {
 156     return true;
 157   }
 158   Assert(s.isVar() && s.getKind() != BOUND_VARIABLE);
 159   return d_model_core.find(s) != d_model_core.end();
 160 }
 161
 162 Cardinality TheoryModel::getCardinality(TypeNode tn) const
 163 {
 164   //for now, we only handle cardinalities for uninterpreted sorts
 165   if (!tn.isSort())
 166   {
 167     Debug("model-getvalue-debug")
 168         << "Get cardinality other sort, unknown." << std::endl;
 169     return Cardinality( CardinalityUnknown() );
 170   }
 171   if (d_rep_set.hasType(tn))
 172   {
 173     Debug("model-getvalue-debug")
 174         << "Get cardinality sort, #rep : "
 175         << d_rep_set.getNumRepresentatives(tn) << std::endl;
 176     return Cardinality(d_rep_set.getNumRepresentatives(tn));
 177   }
 178   Debug("model-getvalue-debug")
 179       << "Get cardinality sort, unconstrained, return 1." << std::endl;
 180   return Cardinality(1);
 181 }
 182
 183 Node TheoryModel::getModelValue(TNode n) const
 184 {
 185   std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
 186   if (it != d_modelCache.end()) {
 187     return (*it).second;
 188   }
 189   Debug("model-getvalue-debug") << "Get model value " << n << " ... ";
 190   Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl;
 191   Kind nk = n.getKind();
 192   if (n.isConst() || nk == BOUND_VARIABLE)
 193   {
 194     d_modelCache[n] = n;
 195     return n;
 196   }
 197
 198   Node ret = n;
 199   NodeManager* nm = NodeManager::currentNM();
 200
 201   // if it is an evaluated kind, compute model values for children and evaluate
 202   if (n.getNumChildren() > 0
 203       && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
 204       && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end())
 205   {
 206     Debug("model-getvalue-debug")
 207         << "Get model value children " << n << std::endl;
 208     std::vector<Node> children;
 209     if (n.getKind() == APPLY_UF)
 210     {
 211       Node op = getModelValue(n.getOperator());
 212       Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
 213       children.push_back(op);
 214     }
 215     else if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
 216     {
 217       children.push_back(n.getOperator());
 218     }
 219     // evaluate the children
 220     for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
 221     {
 222       ret = getModelValue(n[i]);
 223       Debug("model-getvalue-debug")
 224           << "  " << n << "[" << i << "] is " << ret << std::endl;
 225       children.push_back(ret);
 226     }
 227     ret = nm->mkNode(n.getKind(), children);
 228     Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
 229     ret = Rewriter::rewrite(ret);
 230     Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
 231     // special cases
 232     if (ret.getKind() == kind::CARDINALITY_CONSTRAINT)
 233     {
 234       Debug("model-getvalue-debug")
 235           << "get cardinality constraint " << ret[0].getType() << std::endl;
 236       ret = nm->mkConst(getCardinality(ret[0].getType()).getFiniteCardinality()
 237                         <= ret[1].getConst<Rational>().getNumerator());
 238     }
 239     else if (ret.getKind() == kind::CARDINALITY_VALUE)
 240     {
 241       Debug("model-getvalue-debug")
 242           << "get cardinality value " << ret[0].getType() << std::endl;
 243       ret = nm->mkConst(
 244           Rational(getCardinality(ret[0].getType()).getFiniteCardinality()));
 245     }
 246     d_modelCache[n] = ret;
 247     return ret;
 248   }
 249   // it might be approximate
 250   std::map<Node, Node>::const_iterator ita = d_approximations.find(n);
 251   if (ita != d_approximations.end())
 252   {
 253     // If the value of n is approximate based on predicate P(n), we return
 254     // witness z. P(z).
 255     Node v = nm->mkBoundVar(n.getType());
 256     Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
 257     Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v));
 258     d_modelCache[n] = answer;
 259     return answer;
 260   }
 261   // must rewrite the term at this point
 262   ret = Rewriter::rewrite(n);
 263   // return the representative of the term in the equality engine, if it exists
 264   TypeNode t = ret.getType();
 265   bool eeHasTerm;
 266   if (!options::ufHo() && (t.isFunction() || t.isPredicate()))
 267   {
 268     // functions are in the equality engine, but *not* as first-class members
 269     // when higher-order is disabled. In this case, we cannot query
 270     // representatives for functions since they are "internal" nodes according
 271     // to the equality engine despite hasTerm returning true. However, they are
 272     // first class members when higher-order is enabled. Hence, the special
 273     // case here.
 274     eeHasTerm = false;
 275   }
 276   else
 277   {
 278     eeHasTerm = d_equalityEngine->hasTerm(ret);
 279   }
 280   if (eeHasTerm)
 281   {
 282     Debug("model-getvalue-debug")
 283         << "get value from representative " << ret << "..." << std::endl;
 284     ret = d_equalityEngine->getRepresentative(ret);
 285     Assert(d_reps.find(ret) != d_reps.end());
 286     std::map<Node, Node>::const_iterator it2 = d_reps.find(ret);
 287     if (it2 != d_reps.end())
 288     {
 289       ret = it2->second;
 290       d_modelCache[n] = ret;
 291       return ret;
 292     }
 293   }
 294
 295   // if we are a evaluated or semi-evaluated kind, return an arbitrary value
 296   // if we are not in the d_unevaluated_kinds map, we are evaluated
 297   if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end())
 298   {
 299     if (t.isFunction() || t.isPredicate())
 300     {
 301       if (d_enableFuncModels)
 302       {
 303         std::map<Node, Node>::const_iterator entry = d_uf_models.find(n);
 304         if (entry != d_uf_models.end())
 305         {
 306           // Existing function
 307           ret = entry->second;
 308           d_modelCache[n] = ret;
 309           return ret;
 310         }
 311         // Unknown function symbol: return LAMBDA x. c, where c is the first
 312         // constant in the enumeration of the range type
 313         vector<TypeNode> argTypes = t.getArgTypes();
 314         vector<Node> args;
 315         for (unsigned i = 0, size = argTypes.size(); i < size; ++i)
 316         {
 317           args.push_back(nm->mkBoundVar(argTypes[i]));
 318         }
 319         Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
 320         TypeEnumerator te(t.getRangeType());
 321         ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
 322       }
 323       else
 324       {
 325         // if func models not enabled, throw an error
 326         Unreachable();
 327       }
 328     }
 329     else if (!t.isFirstClass())
 330     {
 331       // this is the class for regular expressions
 332       // we simply invoke the rewriter on them
 333       ret = Rewriter::rewrite(ret);
 334     }
 335     else
 336     {
 337       // Unknown term - return first enumerated value for this type
 338       TypeEnumerator te(n.getType());
 339       ret = *te;
 340     }
 341     d_modelCache[n] = ret;
 342     return ret;
 343   }
 344
 345   d_modelCache[n] = n;
 346   return n;
 347 }
 348
 349 /** add substitution */
 350 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
 351   if( !d_substitutions.hasSubstitution( x ) ){
 352     Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl;
 353     d_substitutions.addSubstitution( x, t, invalidateCache );
 354   } else {
 355 #ifdef CVC4_ASSERTIONS
 356     Node oldX = d_substitutions.getSubstitution(x);
 357     // check that either the old substitution is the same, or it now maps to the new substitution
 358     if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) {
 359       InternalError()
 360           << "Two incompatible substitutions added to TheoryModel:\n"
 361           << "the term:    " << x << "\n"
 362           << "old mapping: " << d_substitutions.apply(oldX) << "\n"
 363           << "new mapping: " << d_substitutions.apply(t);
 364     }
 365 #endif /* CVC4_ASSERTIONS */
 366   }
 367 }
 368
 369 /** add term */
 370 void TheoryModel::addTermInternal(TNode n)
 371 {
 372   Assert(d_equalityEngine->hasTerm(n));
 373   Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n << std::endl;
 374   //must collect UF terms
 375   if (n.getKind()==APPLY_UF) {
 376     Node op = n.getOperator();
 377     if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
 378       d_uf_terms[ op ].push_back( n );
 379       Trace("model-builder-fun") << "Add apply term " << n << std::endl;
 380     }
 381   }else if( n.getKind()==HO_APPLY ){
 382     Node op = n[0];
 383     if( std::find( d_ho_uf_terms[ op ].begin(), d_ho_uf_terms[ op ].end(), n )==d_ho_uf_terms[ op ].end() ){
 384       d_ho_uf_terms[ op ].push_back( n );
 385       Trace("model-builder-fun") << "Add ho apply term " << n << std::endl;
 386     }
 387   }
 388   // all functions must be included, marked as higher-order
 389   if( n.getType().isFunction() ){
 390     Trace("model-builder-fun") << "Add function variable (without term) " << n << std::endl;
 391     if( d_uf_terms.find( n )==d_uf_terms.end() ){
 392       d_uf_terms[n].clear();
 393     }
 394     if( d_ho_uf_terms.find( n )==d_ho_uf_terms.end() ){
 395       d_ho_uf_terms[n].clear();
 396     }
 397   }
 398 }
 399
 400 /** assert equality */
 401 bool TheoryModel::assertEquality(TNode a, TNode b, bool polarity)
 402 {
 403   Assert(d_equalityEngine->consistent());
 404   if (a == b && polarity) {
 405     return true;
 406   }
 407   Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
 408   d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() );
 409   return d_equalityEngine->consistent();
 410 }
 411
 412 /** assert predicate */
 413 bool TheoryModel::assertPredicate(TNode a, bool polarity)
 414 {
 415   Assert(d_equalityEngine->consistent());
 416   if ((a == d_true && polarity) ||
 417       (a == d_false && (!polarity))) {
 418     return true;
 419   }
 420   if (a.getKind() == EQUAL) {
 421     Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
 422     d_equalityEngine->assertEquality( a, polarity, Node::null() );
 423   } else {
 424     Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
 425     d_equalityEngine->assertPredicate( a, polarity, Node::null() );
 426   }
 427   return d_equalityEngine->consistent();
 428 }
 429
 430 /** assert equality engine */
 431 bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
 432                                        const std::set<Node>* termSet)
 433 {
 434   Assert(d_equalityEngine->consistent());
 435   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
 436   for (; !eqcs_i.isFinished(); ++eqcs_i) {
 437     Node eqc = (*eqcs_i);
 438     bool predicate = false;
 439     bool predTrue = false;
 440     bool predFalse = false;
 441     Trace("model-builder-debug") << "...asserting terms in equivalence class " << eqc;
 442     if (eqc.getType().isBoolean()) {
 443       predicate = true;
 444       predTrue = ee->areEqual(eqc, d_true);
 445       predFalse = ee->areEqual(eqc, d_false);
 446       Trace("model-builder-debug") << ", pred = " << predTrue << "/" << predFalse;
 447     }
 448     Trace("model-builder-debug") << std::endl;
 449     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
 450     bool first = true;
 451     Node rep;
 452     for (; !eqc_i.isFinished(); ++eqc_i) {
 453       if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
 454         Trace("model-builder-debug") << "...skip node " << (*eqc_i) << " in eqc " << eqc << std::endl;
 455         continue;
 456       }
 457       if (predicate) {
 458         if (predTrue || predFalse)
 459         {
 460           if (!assertPredicate(*eqc_i, predTrue))
 461           {
 462             return false;
 463           }
 464         }
 465         else {
 466           if (first) {
 467             rep = (*eqc_i);
 468             first = false;
 469           }
 470           else {
 471             Node eq = (*eqc_i).eqNode(rep);
 472             Trace("model-builder-assertions")
 473                 << "(assert " << eq << ");" << std::endl;
 474             d_equalityEngine->assertEquality(eq, true, Node::null());
 475             if (!d_equalityEngine->consistent())
 476             {
 477               return false;
 478             }
 479           }
 480         }
 481       } else {
 482         if (first) {
 483           rep = (*eqc_i);
 484           //add the term (this is specifically for the case of singleton equivalence classes)
 485           if (rep.getType().isFirstClass())
 486           {
 487             d_equalityEngine->addTerm( rep );
 488             Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
 489           }
 490           first = false;
 491         }
 492         else {
 493           if (!assertEquality(*eqc_i, rep, true))
 494           {
 495             return false;
 496           }
 497         }
 498       }
 499     }
 500   }
 501   return true;
 502 }
 503
 504 void TheoryModel::assertSkeleton(TNode n)
 505 {
 506   Trace("model-builder-reps") << "Assert skeleton : " << n << std::endl;
 507   Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n)
 508                               << std::endl;
 509   d_reps[ n ] = n;
 510 }
 511
 512 void TheoryModel::setAssignmentExclusionSet(TNode n,
 513                                             const std::vector<Node>& eset)
 514 {
 515   // should not be assigned yet
 516   Assert(d_assignExcSet.find(n) == d_assignExcSet.end());
 517   Trace("model-builder-debug")
 518       << "Exclude values of " << n << " : " << eset << std::endl;
 519   std::vector<Node>& aes = d_assignExcSet[n];
 520   aes.insert(aes.end(), eset.begin(), eset.end());
 521 }
 522
 523 void TheoryModel::setAssignmentExclusionSetGroup(
 524     const std::vector<TNode>& group, const std::vector<Node>& eset)
 525 {
 526   if (group.empty())
 527   {
 528     return;
 529   }
 530   // for efficiency, we store a single copy of eset and set a slave/master
 531   // relationship
 532   setAssignmentExclusionSet(group[0], eset);
 533   std::vector<Node>& gslaves = d_aesSlaves[group[0]];
 534   for (unsigned i = 1, gsize = group.size(); i < gsize; ++i)
 535   {
 536     Node gs = group[i];
 537     // set master
 538     d_aesMaster[gs] = group[0];
 539     // add to slaves
 540     gslaves.push_back(gs);
 541   }
 542 }
 543
 544 bool TheoryModel::getAssignmentExclusionSet(TNode n,
 545                                             std::vector<Node>& group,
 546                                             std::vector<Node>& eset)
 547 {
 548   // does it have a master?
 549   std::map<Node, Node>::iterator itm = d_aesMaster.find(n);
 550   if (itm != d_aesMaster.end())
 551   {
 552     return getAssignmentExclusionSet(itm->second, group, eset);
 553   }
 554   std::map<Node, std::vector<Node> >::iterator ita = d_assignExcSet.find(n);
 555   if (ita == d_assignExcSet.end())
 556   {
 557     return false;
 558   }
 559   eset.insert(eset.end(), ita->second.begin(), ita->second.end());
 560   group.push_back(n);
 561   // does it have slaves?
 562   ita = d_aesSlaves.find(n);
 563   if (ita != d_aesSlaves.end())
 564   {
 565     group.insert(group.end(), ita->second.begin(), ita->second.end());
 566   }
 567   return true;
 568 }
 569
 570 bool TheoryModel::hasAssignmentExclusionSets() const
 571 {
 572   return !d_assignExcSet.empty();
 573 }
 574
 575 void TheoryModel::recordApproximation(TNode n, TNode pred)
 576 {
 577   Trace("model-builder-debug")
 578       << "Record approximation : " << n << " satisfies the predicate " << pred
 579       << std::endl;
 580   Assert(d_approximations.find(n) == d_approximations.end());
 581   Assert(pred.getType().isBoolean());
 582   d_approximations[n] = pred;
 583   d_approx_list.push_back(std::pair<Node, Node>(n, pred));
 584   // model cache is invalid
 585   d_modelCache.clear();
 586 }
 587 void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness)
 588 {
 589   Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
 590   recordApproximation(n, predDisj);
 591 }
 592 void TheoryModel::setUsingModelCore()
 593 {
 594   d_using_model_core = true;
 595   d_model_core.clear();
 596 }
 597
 598 void TheoryModel::recordModelCoreSymbol(Node sym) { d_model_core.insert(sym); }
 599
 600 void TheoryModel::setUnevaluatedKind(Kind k) { d_unevaluated_kinds.insert(k); }
 601
 602 void TheoryModel::setSemiEvaluatedKind(Kind k)
 603 {
 604   d_semi_evaluated_kinds.insert(k);
 605 }
 606
 607 void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); }
 608
 609 const std::set<Kind>& TheoryModel::getIrrelevantKinds() const
 610 {
 611   return d_irrKinds;
 612 }
 613
 614 bool TheoryModel::isLegalElimination(TNode x, TNode val)
 615 {
 616   return !expr::hasSubtermKinds(d_unevaluated_kinds, val);
 617 }
 618
 619 bool TheoryModel::hasTerm(TNode a)
 620 {
 621   return d_equalityEngine->hasTerm( a );
 622 }
 623
 624 Node TheoryModel::getRepresentative(TNode a)
 625 {
 626   if( d_equalityEngine->hasTerm( a ) ){
 627     Node r = d_equalityEngine->getRepresentative( a );
 628     if( d_reps.find( r )!=d_reps.end() ){
 629       return d_reps[ r ];
 630     }else{
 631       return r;
 632     }
 633   }else{
 634     return a;
 635   }
 636 }
 637
 638 bool TheoryModel::areEqual(TNode a, TNode b)
 639 {
 640   if( a==b ){
 641     return true;
 642   }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
 643     return d_equalityEngine->areEqual( a, b );
 644   }else{
 645     return false;
 646   }
 647 }
 648
 649 bool TheoryModel::areDisequal(TNode a, TNode b)
 650 {
 651   if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){
 652     return d_equalityEngine->areDisequal( a, b, false );
 653   }else{
 654     return false;
 655   }
 656 }
 657
 658 bool TheoryModel::areFunctionValuesEnabled() const
 659 {
 660   return d_enableFuncModels;
 661 }
 662
 663 void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
 664   Trace("model-builder") << "  Assigning function (" << f << ") to (" << f_def << ")" << endl;
 665   Assert(d_uf_models.find(f) == d_uf_models.end());
 666
 667   if( options::ufHo() ){
 668     //we must rewrite the function value since the definition needs to be a constant value
 669     f_def = Rewriter::rewrite( f_def );
 670     Trace("model-builder-debug")
 671         << "Model value (post-rewrite) : " << f_def << std::endl;
 672     Assert(f_def.isConst()) << "Non-constant f_def: " << f_def;
 673   }
 674
 675   // d_uf_models only stores models for variables
 676   if( f.isVar() ){
 677     d_uf_models[f] = f_def;
 678   }
 679
 680   if (options::ufHo() && d_equalityEngine->hasTerm(f))
 681   {
 682     Trace("model-builder-debug") << "  ...function is first-class member of equality engine" << std::endl;
 683     // assign to representative if higher-order
 684     Node r = d_equalityEngine->getRepresentative( f );
 685     //always replace the representative, since it is initially assigned to itself
 686     Trace("model-builder") << "    Assign: Setting function rep " << r << " to " << f_def << endl;
 687     d_reps[r] = f_def;
 688     // also assign to other assignable functions in the same equivalence class
 689     eq::EqClassIterator eqc_i = eq::EqClassIterator(r,d_equalityEngine);
 690     while( !eqc_i.isFinished() ) {
 691       Node n = *eqc_i;
 692       // if an unassigned variable function
 693       if( n.isVar() && d_uf_terms.find( n )!=d_uf_terms.end() && !hasAssignedFunctionDefinition( n ) ){
 694         d_uf_models[n] = f_def;
 695         Trace("model-builder") << "  Assigning function (" << n << ") to function definition of " << f << std::endl;
 696       }
 697       ++eqc_i;
 698     }
 699     Trace("model-builder-debug") << "  ...finished." << std::endl;
 700   }
 701 }
 702
 703 std::vector< Node > TheoryModel::getFunctionsToAssign() {
 704   std::vector< Node > funcs_to_assign;
 705   std::map< Node, Node > func_to_rep;
 706
 707   // collect functions
 708   for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){
 709     Node n = it->first;
 710     Assert(!n.isNull());
 711     if( !hasAssignedFunctionDefinition( n ) ){
 712       Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl;
 713       if( options::ufHo() ){
 714         // if in higher-order mode, assign function definitions modulo equality
 715         Node r = getRepresentative( n );
 716         std::map< Node, Node >::iterator itf = func_to_rep.find( r );
 717         if( itf==func_to_rep.end() ){
 718           func_to_rep[r] = n;
 719           funcs_to_assign.push_back( n );
 720           Trace("model-builder-fun") << "Make function " << n;
 721           Trace("model-builder-fun") << " the assignable function in its equivalence class." << std::endl;
 722         }else{
 723           // must combine uf terms
 724           Trace("model-builder-fun") << "Copy " << it->second.size() << " uf terms";
 725           d_uf_terms[itf->second].insert( d_uf_terms[itf->second].end(), it->second.begin(), it->second.end() );
 726           std::map< Node, std::vector< Node > >::iterator ith = d_ho_uf_terms.find( n );
 727           if( ith!=d_ho_uf_terms.end() ){
 728             d_ho_uf_terms[itf->second].insert( d_ho_uf_terms[itf->second].end(), ith->second.begin(), ith->second.end() );
 729             Trace("model-builder-fun") << " and " << ith->second.size() << " ho uf terms";
 730           }
 731           Trace("model-builder-fun") << " from " << n << " to its assignable representative function " << itf->second << std::endl;
 732           it->second.clear();
 733         }
 734       }else{
 735         Trace("model-builder-fun") << "Function to assign : " << n << std::endl;
 736         funcs_to_assign.push_back( n );
 737       }
 738     }
 739   }
 740
 741   Trace("model-builder-fun") << "return " << funcs_to_assign.size() << " functions to assign..." << std::endl;
 742   return funcs_to_assign;
 743 }
 744
 745 const std::string& TheoryModel::getName() const { return d_name; }
 746
 747 } /* namespace CVC4::theory */
 748 } /* namespace CVC4 */