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