src/theory/uf/theory_uf.cpp

   1 /*********************                                                        */
   2 /*! \file theory_uf.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief This is the interface to TheoryUF implementations
  13  **
  14  ** This is the interface to TheoryUF implementations.  All
  15  ** implementations of TheoryUF should inherit from this class.
  16  **/
  17
  18 #include "theory/uf/theory_uf.h"
  19
  20 #include <memory>
  21
  22 #include "options/quantifiers_options.h"
  23 #include "options/smt_options.h"
  24 #include "options/uf_options.h"
  25 #include "proof/proof_manager.h"
  26 #include "proof/theory_proof.h"
  27 #include "proof/uf_proof.h"
  28 #include "theory/theory_model.h"
  29 #include "theory/type_enumerator.h"
  30 #include "theory/uf/theory_uf_strong_solver.h"
  31 #include "theory/quantifiers/term_database.h"
  32 #include "options/theory_options.h"
  33 #include "theory/uf/theory_uf_rewriter.h"
  34
  35 using namespace std;
  36
  37 namespace CVC4 {
  38 namespace theory {
  39 namespace uf {
  40
  41 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
  42 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
  43                    OutputChannel& out, Valuation valuation,
  44                    const LogicInfo& logicInfo, std::string instanceName)
  45     : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName),
  46       d_notify(*this),
  47       /* The strong theory solver can be notified by EqualityEngine::init(),
  48        * so make sure it's initialized first. */
  49       d_thss(NULL),
  50       d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF",
  51                        true),
  52       d_conflict(c, false),
  53       d_extensionality_deq(u),
  54       d_uf_std_skolem(u),
  55       d_functionsTerms(c),
  56       d_symb(u, instanceName)
  57 {
  58   d_true = NodeManager::currentNM()->mkConst( true );
  59
  60   // The kinds we are treating as function application in congruence
  61   d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo());
  62   if( options::ufHo() ){
  63     d_equalityEngine.addFunctionKind(kind::HO_APPLY);
  64   }
  65 }
  66
  67 TheoryUF::~TheoryUF() {
  68   delete d_thss;
  69 }
  70
  71 void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  72   d_equalityEngine.setMasterEqualityEngine(eq);
  73 }
  74
  75 void TheoryUF::finishInit() {
  76   // initialize the strong solver
  77   if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) {
  78     d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
  79   }
  80 }
  81
  82 static Node mkAnd(const std::vector<TNode>& conjunctions) {
  83   Assert(conjunctions.size() > 0);
  84
  85   std::set<TNode> all;
  86   all.insert(conjunctions.begin(), conjunctions.end());
  87
  88   if (all.size() == 1) {
  89     // All the same, or just one
  90     return conjunctions[0];
  91   }
  92
  93   NodeBuilder<> conjunction(kind::AND);
  94   std::set<TNode>::const_iterator it = all.begin();
  95   std::set<TNode>::const_iterator it_end = all.end();
  96   while (it != it_end) {
  97     conjunction << *it;
  98     ++ it;
  99   }
 100
 101   return conjunction;
 102 }/* mkAnd() */
 103
 104 void TheoryUF::check(Effort level) {
 105   if (done() && !fullEffort(level)) {
 106     return;
 107   }
 108   getOutputChannel().spendResource(options::theoryCheckStep());
 109   TimerStat::CodeTimer checkTimer(d_checkTime);
 110
 111   while (!done() && !d_conflict)
 112   {
 113     // Get all the assertions
 114     Assertion assertion = get();
 115     TNode fact = assertion.assertion;
 116
 117     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
 118     Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;
 119
 120     if (d_thss != NULL) {
 121       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
 122       d_thss->assertNode(fact, isDecision);
 123       if( d_thss->isConflict() ){
 124         d_conflict = true;
 125         return;
 126       }
 127     }
 128
 129     // Do the work
 130     bool polarity = fact.getKind() != kind::NOT;
 131     TNode atom = polarity ? fact : fact[0];
 132     if (atom.getKind() == kind::EQUAL) {
 133       d_equalityEngine.assertEquality(atom, polarity, fact);
 134       if( options::ufHo() && options::ufHoExt() ){
 135         if( !polarity && !d_conflict && atom[0].getType().isFunction() ){
 136           applyExtensionality( fact );
 137         }
 138       }
 139     } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
 140       if( d_thss == NULL ){
 141         if( !getLogicInfo().hasCardinalityConstraints() ){
 142           std::stringstream ss;
 143           ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl;
 144           ss << "Try using a logic containing \"UFC\"." << std::endl;
 145           throw Exception( ss.str() );
 146         }else{
 147           // support for cardinality constraints is not enabled, set incomplete
 148           d_out->setIncomplete();
 149         }
 150       }
 151       //needed for models
 152       if( options::produceModels() ){
 153         d_equalityEngine.assertPredicate(atom, polarity, fact);
 154       }
 155     } else {
 156       d_equalityEngine.assertPredicate(atom, polarity, fact);
 157     }
 158   }
 159
 160   if(! d_conflict ){
 161     if (d_thss != NULL) {
 162       d_thss->check(level);
 163       if( d_thss->isConflict() ){
 164         d_conflict = true;
 165       }
 166     }
 167     if(! d_conflict && fullEffort(level) ){
 168       if( options::ufHo() ){
 169         checkHigherOrder();
 170       }
 171     }
 172   }
 173 }/* TheoryUF::check() */
 174
 175 Node TheoryUF::getApplyUfForHoApply( Node node ) {
 176   Assert( node[0].getType().getNumChildren()==2 );
 177   std::vector< TNode > args;
 178   Node f = TheoryUfRewriter::decomposeHoApply( node, args, true );
 179   Node new_f = f;
 180   if( !TheoryUfRewriter::canUseAsApplyUfOperator( f ) ){
 181     NodeNodeMap::const_iterator itus = d_uf_std_skolem.find( f );
 182     if( itus==d_uf_std_skolem.end() ){
 183       // introduce skolem to make a standard APPLY_UF
 184       new_f = NodeManager::currentNM()->mkSkolem( "app_uf", f.getType() );
 185       Node lem = new_f.eqNode( f );
 186       Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl;
 187       d_out->lemma( lem );
 188       d_uf_std_skolem[f] = new_f;
 189     }else{
 190       new_f = (*itus).second;
 191     }
 192   }
 193   Assert( TheoryUfRewriter::canUseAsApplyUfOperator( new_f ) );
 194   args[0] = new_f;
 195   Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, args );
 196   return ret;
 197 }
 198
 199 Node TheoryUF::getOperatorForApplyTerm( TNode node ) {
 200   Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
 201   if( node.getKind()==kind::APPLY_UF ){
 202     return node.getOperator();
 203   }else{
 204     return d_equalityEngine.getRepresentative( node[0] );
 205   }
 206 }
 207
 208 unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) {
 209   Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY );
 210   return node.getKind()==kind::APPLY_UF ? 0 : 1;
 211 }
 212
 213 Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) {
 214   Trace("uf-ho-debug") << "uf-ho-debug : expanding definition : " << node << std::endl;
 215   if( node.getKind()==kind::HO_APPLY ){
 216     if( !options::ufHo() ){
 217       std::stringstream ss;
 218       ss << "Partial function applications are not supported in default mode, try --uf-ho.";
 219       throw LogicException(ss.str());
 220     }
 221     // convert HO_APPLY to APPLY_UF if fully applied
 222     if( node[0].getType().getNumChildren()==2 ){
 223       Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
 224       Node ret = getApplyUfForHoApply( node );
 225       Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret << std::endl;
 226       return ret;
 227     }
 228   }
 229   return node;
 230 }
 231
 232 void TheoryUF::preRegisterTerm(TNode node) {
 233   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 234
 235   if (d_thss != NULL) {
 236     d_thss->preRegisterTerm(node);
 237   }
 238
 239   // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
 240   //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
 241   Assert( node.getKind()!=kind::HO_APPLY || options::ufHo() );
 242
 243   switch (node.getKind()) {
 244   case kind::EQUAL:
 245     // Add the trigger for equality
 246     d_equalityEngine.addTriggerEquality(node);
 247     break;
 248   case kind::APPLY_UF:
 249   case kind::HO_APPLY:
 250     // Maybe it's a predicate
 251     if (node.getType().isBoolean()) {
 252       // Get triggered for both equal and dis-equal
 253       d_equalityEngine.addTriggerPredicate(node);
 254     } else {
 255       // Function applications/predicates
 256       d_equalityEngine.addTerm(node);
 257     }
 258     // Remember the function and predicate terms
 259     d_functionsTerms.push_back(node);
 260     break;
 261   case kind::CARDINALITY_CONSTRAINT:
 262   case kind::COMBINED_CARDINALITY_CONSTRAINT:
 263     //do nothing
 264     break;
 265   default:
 266     // Variables etc
 267     d_equalityEngine.addTerm(node);
 268     break;
 269   }
 270 }/* TheoryUF::preRegisterTerm() */
 271
 272 bool TheoryUF::propagate(TNode literal) {
 273   Debug("uf::propagate") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
 274   // If already in conflict, no more propagation
 275   if (d_conflict) {
 276     Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
 277     return false;
 278   }
 279   // Propagate out
 280   bool ok = d_out->propagate(literal);
 281   if (!ok) {
 282     d_conflict = true;
 283   }
 284   return ok;
 285 }/* TheoryUF::propagate(TNode) */
 286
 287 void TheoryUF::propagate(Effort effort) {
 288   //if (d_thss != NULL) {
 289   //  return d_thss->propagate(effort);
 290   //}
 291 }
 292
 293 Node TheoryUF::getNextDecisionRequest( unsigned& priority ){
 294   if (d_thss != NULL && !d_conflict) {
 295     return d_thss->getNextDecisionRequest( priority );
 296   }else{
 297     return Node::null();
 298   }
 299 }
 300
 301 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
 302   // Do the work
 303   bool polarity = literal.getKind() != kind::NOT;
 304   TNode atom = polarity ? literal : literal[0];
 305   if (atom.getKind() == kind::EQUAL) {
 306     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
 307   } else {
 308     d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
 309   }
 310   if( pf ){
 311     Debug("pf::uf") << std::endl;
 312     pf->debug_print("pf::uf");
 313   }
 314
 315   Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t";
 316   for (unsigned i = 0; i < assumptions.size(); ++i) {
 317     Debug("pf::uf") << assumptions[i] << " ";
 318   }
 319   Debug("pf::uf") << std::endl;
 320 }
 321
 322 Node TheoryUF::explain(TNode literal) {
 323   return explain(literal, NULL);
 324 }
 325
 326 Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
 327   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
 328   std::vector<TNode> assumptions;
 329   explain(literal, assumptions, pf);
 330   return mkAnd(assumptions);
 331 }
 332
 333 void TheoryUF::collectModelInfo( TheoryModel* m ){
 334   Debug("uf") << "UF : collectModelInfo " << std::endl;
 335   set<Node> termSet;
 336
 337   // Compute terms appearing in assertions and shared terms
 338   computeRelevantTerms(termSet);
 339
 340   m->assertEqualityEngine( &d_equalityEngine, &termSet );
 341
 342   if( options::ufHo() ){
 343     for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){
 344       Node n = *it;
 345       if( n.getKind()==kind::APPLY_UF ){
 346         // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY
 347         Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n );
 348         m->assertEquality( n, hn, true );
 349       }
 350     }
 351   }
 352
 353   Debug("uf") << "UF : finish collectModelInfo " << std::endl;
 354 }
 355
 356 void TheoryUF::presolve() {
 357   // TimerStat::CodeTimer codeTimer(d_presolveTimer);
 358
 359   Debug("uf") << "uf: begin presolve()" << endl;
 360   if(options::ufSymmetryBreaker()) {
 361     vector<Node> newClauses;
 362     d_symb.apply(newClauses);
 363     for(vector<Node>::const_iterator i = newClauses.begin();
 364         i != newClauses.end();
 365         ++i) {
 366       Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
 367       d_out->lemma(*i);
 368     }
 369   }
 370   if( d_thss ){
 371     d_thss->presolve();
 372   }
 373   Debug("uf") << "uf: end presolve()" << endl;
 374 }
 375
 376 void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 377   //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
 378
 379   vector<TNode> workList;
 380   workList.push_back(n);
 381   std::unordered_set<TNode, TNodeHashFunction> processed;
 382
 383   while(!workList.empty()) {
 384     n = workList.back();
 385
 386     if(n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) {
 387       // unsafe to go under quantifiers; we might pull bound vars out of scope!
 388       processed.insert(n);
 389       workList.pop_back();
 390       continue;
 391     }
 392
 393     bool unprocessedChildren = false;
 394     for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
 395       if(processed.find(*i) == processed.end()) {
 396         // unprocessed child
 397         workList.push_back(*i);
 398         unprocessedChildren = true;
 399       }
 400     }
 401
 402     if(unprocessedChildren) {
 403       continue;
 404     }
 405
 406     workList.pop_back();
 407     // has node n been processed in the meantime ?
 408     if(processed.find(n) != processed.end()) {
 409       continue;
 410     }
 411     processed.insert(n);
 412
 413     // == DIAMONDS ==
 414
 415     Debug("diamonds") << "===================== looking at" << endl
 416                       << n << endl;
 417
 418     // binary OR of binary ANDs of EQUALities
 419     if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
 420        n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
 421        n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
 422        (n[0][0].getKind() == kind::EQUAL) &&
 423        (n[0][1].getKind() == kind::EQUAL) &&
 424        (n[1][0].getKind() == kind::EQUAL) &&
 425        (n[1][1].getKind() == kind::EQUAL)) {
 426       // now we have (a = b && c = d) || (e = f && g = h)
 427
 428       Debug("diamonds") << "has form of a diamond!" << endl;
 429
 430       TNode
 431         a = n[0][0][0], b = n[0][0][1],
 432         c = n[0][1][0], d = n[0][1][1],
 433         e = n[1][0][0], f = n[1][0][1],
 434         g = n[1][1][0], h = n[1][1][1];
 435
 436       // test that one of {a, b} = one of {c, d}, and make "b" the
 437       // shared node (i.e. put in the form (a = b && b = d))
 438       // note we don't actually care about the shared ones, so the
 439       // "swaps" below are one-sided, ignoring b and c
 440       if(a == c) {
 441         a = b;
 442       } else if(a == d) {
 443         a = b;
 444         d = c;
 445       } else if(b == c) {
 446         // nothing to do
 447       } else if(b == d) {
 448         d = c;
 449       } else {
 450         // condition not satisfied
 451         Debug("diamonds") << "+ A fails" << endl;
 452         continue;
 453       }
 454
 455       Debug("diamonds") << "+ A holds" << endl;
 456
 457       // same: one of {e, f} = one of {g, h}, and make "f" the
 458       // shared node (i.e. put in the form (e = f && f = h))
 459       if(e == g) {
 460         e = f;
 461       } else if(e == h) {
 462         e = f;
 463         h = g;
 464       } else if(f == g) {
 465         // nothing to do
 466       } else if(f == h) {
 467         h = g;
 468       } else {
 469         // condition not satisfied
 470         Debug("diamonds") << "+ B fails" << endl;
 471         continue;
 472       }
 473
 474       Debug("diamonds") << "+ B holds" << endl;
 475
 476       // now we have (a = b && b = d) || (e = f && f = h)
 477       // test that {a, d} == {e, h}
 478       if( (a == e && d == h) ||
 479           (a == h && d == e) ) {
 480         // learn: n implies a == d
 481         Debug("diamonds") << "+ C holds" << endl;
 482         Node newEquality = a.eqNode(d);
 483         Debug("diamonds") << "  ==> " << newEquality << endl;
 484         learned << n.impNode(newEquality);
 485       } else {
 486         Debug("diamonds") << "+ C fails" << endl;
 487       }
 488     }
 489   }
 490
 491   if(options::ufSymmetryBreaker()) {
 492     d_symb.assertFormula(n);
 493   }
 494 }/* TheoryUF::ppStaticLearn() */
 495
 496 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 497
 498   // Check for equality (simplest)
 499   if (d_equalityEngine.areEqual(a, b)) {
 500     // The terms are implied to be equal
 501     return EQUALITY_TRUE;
 502   }
 503
 504   // Check for disequality
 505   if (d_equalityEngine.areDisequal(a, b, false)) {
 506     // The terms are implied to be dis-equal
 507     return EQUALITY_FALSE;
 508   }
 509
 510   // All other terms we interpret as dis-equal in the model
 511   return EQUALITY_FALSE_IN_MODEL;
 512 }
 513
 514 void TheoryUF::addSharedTerm(TNode t) {
 515   Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
 516   d_equalityEngine.addTriggerTerm(t, THEORY_UF);
 517 }
 518
 519 bool TheoryUF::areCareDisequal(TNode x, TNode y){
 520   Assert( d_equalityEngine.hasTerm(x) );
 521   Assert( d_equalityEngine.hasTerm(y) );
 522   if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
 523     TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
 524     TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
 525     EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
 526     if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
 527       return true;
 528     }
 529   }
 530   return false;
 531 }
 532
 533 //TODO: move quantifiers::TermArgTrie to src/theory/
 534 void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
 535   if( depth==arity ){
 536     if( t2!=NULL ){
 537       Node f1 = t1->getNodeData();
 538       Node f2 = t2->getNodeData();
 539       if( !d_equalityEngine.areEqual( f1, f2 ) ){
 540         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
 541         vector< pair<TNode, TNode> > currentPairs;
 542         unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
 543         for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) {
 544           TNode x = f1[k];
 545           TNode y = f2[k];
 546           Assert( d_equalityEngine.hasTerm(x) );
 547           Assert( d_equalityEngine.hasTerm(y) );
 548           Assert( !d_equalityEngine.areDisequal( x, y, false ) );
 549           Assert( !areCareDisequal( x, y ) );
 550           if( !d_equalityEngine.areEqual( x, y ) ){
 551             if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
 552               TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
 553               TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
 554               currentPairs.push_back(make_pair(x_shared, y_shared));
 555             }
 556           }
 557         }
 558         for (unsigned c = 0; c < currentPairs.size(); ++ c) {
 559           Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
 560           addCarePair(currentPairs[c].first, currentPairs[c].second);
 561         }
 562       }
 563     }
 564   }else{
 565     if( t2==NULL ){
 566       if( depth<(arity-1) ){
 567         //add care pairs internal to each child
 568         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
 569           addCarePairs( &it->second, NULL, arity, depth+1 );
 570         }
 571       }
 572       //add care pairs based on each pair of non-disequal arguments
 573       for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
 574         std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
 575         ++it2;
 576         for( ; it2 != t1->d_data.end(); ++it2 ){
 577           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
 578             if( !areCareDisequal(it->first, it2->first) ){
 579               addCarePairs( &it->second, &it2->second, arity, depth+1 );
 580             }
 581           }
 582         }
 583       }
 584     }else{
 585       //add care pairs based on product of indices, non-disequal arguments
 586       for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
 587         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
 588           if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
 589             if( !areCareDisequal(it->first, it2->first) ){
 590               addCarePairs( &it->second, &it2->second, arity, depth+1 );
 591             }
 592           }
 593         }
 594       }
 595     }
 596   }
 597 }
 598
 599 void TheoryUF::computeCareGraph() {
 600
 601   if (d_sharedTerms.size() > 0) {
 602     //use term indexing
 603     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
 604     std::map< Node, quantifiers::TermArgTrie > index;
 605     std::map< Node, unsigned > arity;
 606     unsigned functionTerms = d_functionsTerms.size();
 607     for (unsigned i = 0; i < functionTerms; ++ i) {
 608       TNode f1 = d_functionsTerms[i];
 609       Node op = getOperatorForApplyTerm( f1 );
 610       unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 );
 611       std::vector< TNode > reps;
 612       bool has_trigger_arg = false;
 613       for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){
 614         reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
 615         if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){
 616           has_trigger_arg = true;
 617         }
 618       }
 619       if( has_trigger_arg ){
 620         index[op].addTerm( f1, reps, arg_start_index );
 621         arity[op] = reps.size();
 622       }
 623     }
 624     //for each index
 625     for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
 626       Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
 627       addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
 628     }
 629     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
 630   }
 631 }/* TheoryUF::computeCareGraph() */
 632
 633 void TheoryUF::conflict(TNode a, TNode b) {
 634   std::shared_ptr<eq::EqProof> pf =
 635       d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
 636   d_conflictNode = explain(a.eqNode(b), pf.get());
 637   ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
 638   d_out->conflict(d_conflictNode, puf);
 639   d_conflict = true;
 640 }
 641
 642 void TheoryUF::eqNotifyNewClass(TNode t) {
 643   if (d_thss != NULL) {
 644     d_thss->newEqClass(t);
 645   }
 646 }
 647
 648 void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
 649   //if (getLogicInfo().isQuantified()) {
 650     //getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
 651   //}
 652 }
 653
 654 void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
 655   if (d_thss != NULL) {
 656     d_thss->merge(t1, t2);
 657   }
 658 }
 659
 660 void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 661   if (d_thss != NULL) {
 662     d_thss->assertDisequal(t1, t2, reason);
 663   }
 664 }
 665
 666 unsigned TheoryUF::applyExtensionality(TNode deq) {
 667   Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL );
 668   Assert( deq[0][0].getType().isFunction() );
 669   // apply extensionality
 670   if( d_extensionality_deq.find( deq )==d_extensionality_deq.end() ){
 671     d_extensionality_deq.insert( deq );
 672     TypeNode tn = deq[0][0].getType();
 673     std::vector< Node > skolems;
 674     for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
 675       Node k = NodeManager::currentNM()->mkSkolem( "k", tn[i], "skolem created for extensionality." );
 676       skolems.push_back( k );
 677     }
 678     Node t[2];
 679     for( unsigned i=0; i<2; i++ ){
 680       std::vector< Node > children;
 681       Node curr = deq[0][i];
 682       while( curr.getKind()==kind::HO_APPLY ){
 683         children.push_back( curr[1] );
 684         curr = curr[0];
 685       }
 686       children.push_back( curr );
 687       std::reverse( children.begin(), children.end() );
 688       children.insert( children.end(), skolems.begin(), skolems.end() );
 689       t[i] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
 690     }
 691     Node conc = t[0].eqNode( t[1] ).negate();
 692     Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc );
 693     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl;
 694     d_out->lemma( lem );
 695     return 1;
 696   }else{
 697     return 0;
 698   }
 699 }
 700
 701 unsigned TheoryUF::checkExtensionality() {
 702   unsigned num_lemmas = 0;
 703   Trace("uf-ho") << "TheoryUF::checkExtensionality..." << std::endl;
 704   // This is bit eager: we should allow functions to be neither equal nor disequal during model construction
 705   // However, doing so would require a function-type enumerator.
 706   std::map< TypeNode, std::vector< Node > > func_eqcs;
 707
 708   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 709   while( !eqcs_i.isFinished() ){
 710     Node eqc = (*eqcs_i);
 711     TypeNode tn = eqc.getType();
 712     if( tn.isFunction() ){
 713       func_eqcs[tn].push_back( eqc );
 714       Trace("uf-ho-debug") << "  func eqc : " << tn << " : " << eqc << std::endl;
 715     }
 716     ++eqcs_i;
 717   }
 718
 719   for( std::map< TypeNode, std::vector< Node > >::iterator itf = func_eqcs.begin();
 720        itf != func_eqcs.end(); ++itf ){
 721     for( unsigned j=0; j<itf->second.size(); j++ ){
 722       for( unsigned k=(j+1); k<itf->second.size(); k++ ){
 723         // if these equivalence classes are not explicitly disequal, do extensionality to ensure distinctness
 724         if( !d_equalityEngine.areDisequal( itf->second[j], itf->second[k], false ) ){
 725           Node deq = Rewriter::rewrite( itf->second[j].eqNode( itf->second[k] ).negate() );
 726           num_lemmas += applyExtensionality( deq );
 727         }
 728       }
 729     }
 730   }
 731   return num_lemmas;
 732 }
 733
 734 unsigned TheoryUF::applyAppCompletion( TNode n ) {
 735   Assert( n.getKind()==kind::APPLY_UF );
 736
 737   //must expand into APPLY_HO version if not there already
 738   Node ret = TheoryUfRewriter::getHoApplyForApplyUf( n );
 739   if( !d_equalityEngine.hasTerm( ret ) || !d_equalityEngine.areEqual( ret, n ) ){
 740     Node eq = ret.eqNode( n );
 741     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl;
 742     d_equalityEngine.assertEquality(eq, true, d_true);
 743     return 1;
 744   }else{
 745     Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "." << std::endl;
 746     return 0;
 747   }
 748 }
 749
 750 unsigned TheoryUF::checkAppCompletion() {
 751   Trace("uf-ho") << "TheoryUF::checkApplyCompletion..." << std::endl;
 752   // compute the operators that are relevant (those for which an HO_APPLY exist)
 753   std::set< TNode > rlvOp;
 754   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 755   std::map< TNode, std::vector< Node > > apply_uf;
 756   while( !eqcs_i.isFinished() ){
 757     Node eqc = (*eqcs_i);
 758     Trace("uf-ho-debug") << "  apply completion : visit eqc " << eqc << std::endl;
 759     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
 760     while( !eqc_i.isFinished() ){
 761       Node n = *eqc_i;
 762       if( n.getKind()==kind::APPLY_UF || n.getKind()==kind::HO_APPLY ){
 763         int curr_sum = 0;
 764         std::map< TNode, bool > curr_rops;
 765         if( n.getKind()==kind::APPLY_UF ){
 766           TNode rop = d_equalityEngine.getRepresentative( n.getOperator() );
 767           if( rlvOp.find( rop )!=rlvOp.end() ){
 768             // try if its operator is relevant
 769             curr_sum = applyAppCompletion( n );
 770             if( curr_sum>0 ){
 771               return curr_sum;
 772             }
 773           }else{
 774             // add to pending list
 775             apply_uf[rop].push_back( n );
 776           }
 777           //arguments are also relevant operators  FIXME (github issue #1115)
 778           for( unsigned k=0; k<n.getNumChildren(); k++ ){
 779             if( n[k].getType().isFunction() ){
 780               TNode rop = d_equalityEngine.getRepresentative( n[k] );
 781               curr_rops[rop] = true;
 782             }
 783           }
 784         }else{
 785           Assert( n.getKind()==kind::HO_APPLY );
 786           TNode rop = d_equalityEngine.getRepresentative( n[0] );
 787           curr_rops[rop] = true;
 788         }
 789         for( std::map< TNode, bool >::iterator itc = curr_rops.begin(); itc != curr_rops.end(); ++itc ){
 790           TNode rop = itc->first;
 791           if( rlvOp.find( rop )==rlvOp.end() ){
 792             rlvOp.insert( rop );
 793             // now, try each pending APPLY_UF for this operator
 794             std::map< TNode, std::vector< Node > >::iterator itu = apply_uf.find( rop );
 795             if( itu!=apply_uf.end() ){
 796               for( unsigned j=0; j<itu->second.size(); j++ ){
 797                 curr_sum = applyAppCompletion( itu->second[j] );
 798                 if( curr_sum>0 ){
 799                   return curr_sum;
 800                 }
 801               }
 802             }
 803           }
 804         }
 805       }
 806       ++eqc_i;
 807     }
 808     ++eqcs_i;
 809   }
 810   return 0;
 811 }
 812
 813 unsigned TheoryUF::checkHigherOrder() {
 814   Trace("uf-ho") << "TheoryUF::checkHigherOrder..." << std::endl;
 815
 816   // infer new facts based on apply completion until fixed point
 817   unsigned num_facts;
 818   do{
 819     num_facts = checkAppCompletion();
 820     if( d_conflict ){
 821       Trace("uf-ho") << "...conflict during app-completion." << std::endl;
 822       return 1;
 823     }
 824   }while( num_facts>0 );
 825
 826   if( options::ufHoExt() ){
 827     unsigned num_lemmas = 0;
 828
 829     num_lemmas = checkExtensionality();
 830     if( num_lemmas>0 ){
 831       Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." << std::endl;
 832       return num_lemmas;
 833     }
 834   }
 835
 836   Trace("uf-ho") << "...finished check higher order." << std::endl;
 837
 838   return 0;
 839 }
 840
 841 } /* namespace CVC4::theory::uf */
 842 } /* namespace CVC4::theory */
 843 } /* namespace CVC4 */