src/theory/uf/theory_uf.cpp

   1 /*********************                                                        */
   2 /*! \file theory_uf.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief This is the interface to TheoryUF implementations
  15  **
  16  ** This is the interface to TheoryUF implementations.  All
  17  ** implementations of TheoryUF should inherit from this class.
  18  **/
  19
  20 #include "theory/uf/theory_uf.h"
  21 #include "theory/uf/theory_uf_instantiator.h"
  22 #include "theory/uf/theory_uf_strong_solver.h"
  23 #include "theory/model.h"
  24
  25 using namespace std;
  26 using namespace CVC4;
  27 using namespace CVC4::theory;
  28 using namespace CVC4::theory::uf;
  29
  30 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
  31 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
  32   Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe),
  33   d_notify(*this),
  34   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
  35   d_conflict(c, false),
  36   d_literalsToPropagate(c),
  37   d_literalsToPropagateIndex(c, 0),
  38   d_functionsTerms(c)
  39 {
  40   // The kinds we are treating as function application in congruence
  41   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
  42
  43   if (Options::current()->finiteModelFind) {
  44     d_thss = new StrongSolverTheoryUf(c, u, out, this);
  45   } else {
  46     d_thss = NULL;
  47   }
  48 }/* TheoryUF::TheoryUF() */
  49
  50 static Node mkAnd(const std::vector<TNode>& conjunctions) {
  51   Assert(conjunctions.size() > 0);
  52
  53   std::set<TNode> all;
  54   all.insert(conjunctions.begin(), conjunctions.end());
  55
  56   if (all.size() == 1) {
  57     // All the same, or just one
  58     return conjunctions[0];
  59   }
  60
  61   NodeBuilder<> conjunction(kind::AND);
  62   std::set<TNode>::const_iterator it = all.begin();
  63   std::set<TNode>::const_iterator it_end = all.end();
  64   while (it != it_end) {
  65     conjunction << *it;
  66     ++ it;
  67   }
  68
  69   return conjunction;
  70 }/* mkAnd() */
  71
  72 void TheoryUF::check(Effort level) {
  73
  74   while (!done() && !d_conflict)
  75   {
  76     // Get all the assertions
  77     Assertion assertion = get();
  78     TNode fact = assertion.assertion;
  79
  80     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
  81     if (d_thss != NULL) {
  82       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
  83       d_thss->assertNode(fact, isDecision);
  84     }
  85
  86     // Do the work
  87     bool polarity = fact.getKind() != kind::NOT;
  88     TNode atom = polarity ? fact : fact[0];
  89     if (atom.getKind() == kind::EQUAL) {
  90       d_equalityEngine.assertEquality(atom, polarity, fact);
  91     } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) {
  92       // do nothing
  93     } else {
  94       d_equalityEngine.assertPredicate(atom, polarity, fact);
  95     }
  96   }
  97
  98
  99   if (d_thss != NULL) {
 100     if (! d_conflict) {
 101       d_thss->check(level);
 102     }
 103   }
 104
 105 }/* TheoryUF::check() */
 106
 107 void TheoryUF::preRegisterTerm(TNode node) {
 108   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 109
 110   if (d_thss != NULL) {
 111     d_thss->preRegisterTerm(node);
 112   }
 113
 114   switch (node.getKind()) {
 115   case kind::EQUAL:
 116     // Add the trigger for equality
 117     d_equalityEngine.addTriggerEquality(node);
 118     break;
 119   case kind::APPLY_UF:
 120     // Maybe it's a predicate
 121     if (node.getType().isBoolean()) {
 122       // Get triggered for both equal and dis-equal
 123       d_equalityEngine.addTriggerPredicate(node);
 124     } else {
 125       // Function applications/predicates
 126       d_equalityEngine.addTerm(node);
 127     }
 128     // Remember the function and predicate terms
 129     d_functionsTerms.push_back(node);
 130     break;
 131   default:
 132     // Variables etc
 133     d_equalityEngine.addTerm(node);
 134     break;
 135   }
 136 }/* TheoryUF::preRegisterTerm() */
 137
 138 bool TheoryUF::propagate(TNode literal) {
 139   Debug("uf::propagate") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
 140   // If already in conflict, no more propagation
 141   if (d_conflict) {
 142     Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
 143     return false;
 144   }
 145   // Propagate out
 146   bool ok = d_out->propagate(literal);
 147   if (!ok) {
 148     d_conflict = true;
 149   }
 150   return ok;
 151 }/* TheoryUF::propagate(TNode) */
 152
 153 void TheoryUF::propagate(Effort effort) {
 154   if (d_thss != NULL) {
 155     return d_thss->propagate(effort);
 156   }
 157 }
 158
 159 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
 160   // Do the work
 161   bool polarity = literal.getKind() != kind::NOT;
 162   TNode atom = polarity ? literal : literal[0];
 163   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 164     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 165   } else {
 166     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 167   }
 168 }
 169
 170 Node TheoryUF::explain(TNode literal) {
 171   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
 172   std::vector<TNode> assumptions;
 173   explain(literal, assumptions);
 174   return mkAnd(assumptions);
 175 }
 176
 177 void TheoryUF::collectModelInfo( TheoryModel* m ){
 178   m->assertEqualityEngine( &d_equalityEngine );
 179 }
 180
 181 void TheoryUF::presolve() {
 182   // TimerStat::CodeTimer codeTimer(d_presolveTimer);
 183
 184   Debug("uf") << "uf: begin presolve()" << endl;
 185   if(Options::current()->ufSymmetryBreaker) {
 186     vector<Node> newClauses;
 187     d_symb.apply(newClauses);
 188     for(vector<Node>::const_iterator i = newClauses.begin();
 189         i != newClauses.end();
 190         ++i) {
 191       d_out->lemma(*i);
 192     }
 193   }
 194   Debug("uf") << "uf: end presolve()" << endl;
 195 }
 196
 197 void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 198   //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
 199
 200   vector<TNode> workList;
 201   workList.push_back(n);
 202   __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
 203
 204   while(!workList.empty()) {
 205     n = workList.back();
 206
 207     bool unprocessedChildren = false;
 208     for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
 209       if(processed.find(*i) == processed.end()) {
 210         // unprocessed child
 211         workList.push_back(*i);
 212         unprocessedChildren = true;
 213       }
 214     }
 215
 216     if(unprocessedChildren) {
 217       continue;
 218     }
 219
 220     workList.pop_back();
 221     // has node n been processed in the meantime ?
 222     if(processed.find(n) != processed.end()) {
 223       continue;
 224     }
 225     processed.insert(n);
 226
 227     // == DIAMONDS ==
 228
 229     Debug("diamonds") << "===================== looking at" << endl
 230                       << n << endl;
 231
 232     // binary OR of binary ANDs of EQUALities
 233     if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
 234        n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
 235        n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
 236        (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
 237        (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
 238        (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
 239        (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
 240       // now we have (a = b && c = d) || (e = f && g = h)
 241
 242       Debug("diamonds") << "has form of a diamond!" << endl;
 243
 244       TNode
 245         a = n[0][0][0], b = n[0][0][1],
 246         c = n[0][1][0], d = n[0][1][1],
 247         e = n[1][0][0], f = n[1][0][1],
 248         g = n[1][1][0], h = n[1][1][1];
 249
 250       // test that one of {a, b} = one of {c, d}, and make "b" the
 251       // shared node (i.e. put in the form (a = b && b = d))
 252       // note we don't actually care about the shared ones, so the
 253       // "swaps" below are one-sided, ignoring b and c
 254       if(a == c) {
 255         a = b;
 256       } else if(a == d) {
 257         a = b;
 258         d = c;
 259       } else if(b == c) {
 260         // nothing to do
 261       } else if(b == d) {
 262         d = c;
 263       } else {
 264         // condition not satisfied
 265         Debug("diamonds") << "+ A fails" << endl;
 266         continue;
 267       }
 268
 269       Debug("diamonds") << "+ A holds" << endl;
 270
 271       // same: one of {e, f} = one of {g, h}, and make "f" the
 272       // shared node (i.e. put in the form (e = f && f = h))
 273       if(e == g) {
 274         e = f;
 275       } else if(e == h) {
 276         e = f;
 277         h = g;
 278       } else if(f == g) {
 279         // nothing to do
 280       } else if(f == h) {
 281         h = g;
 282       } else {
 283         // condition not satisfied
 284         Debug("diamonds") << "+ B fails" << endl;
 285         continue;
 286       }
 287
 288       Debug("diamonds") << "+ B holds" << endl;
 289
 290       // now we have (a = b && b = d) || (e = f && f = h)
 291       // test that {a, d} == {e, h}
 292       if( (a == e && d == h) ||
 293           (a == h && d == e) ) {
 294         // learn: n implies a == d
 295         Debug("diamonds") << "+ C holds" << endl;
 296         Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
 297         Debug("diamonds") << "  ==> " << newEquality << endl;
 298         learned << n.impNode(newEquality);
 299       } else {
 300         Debug("diamonds") << "+ C fails" << endl;
 301       }
 302     }
 303   }
 304
 305   if(Options::current()->ufSymmetryBreaker) {
 306     d_symb.assertFormula(n);
 307   }
 308 }/* TheoryUF::ppStaticLearn() */
 309
 310 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 311
 312   // Check for equality (simplest)
 313   if (d_equalityEngine.areEqual(a, b)) {
 314     // The terms are implied to be equal
 315     return EQUALITY_TRUE;
 316   }
 317
 318   // Check for disequality
 319   if (d_equalityEngine.areDisequal(a, b, false)) {
 320     // The terms are implied to be dis-equal
 321     return EQUALITY_FALSE;
 322   }
 323
 324   // All other terms we interpret as dis-equal in the model
 325   return EQUALITY_FALSE_IN_MODEL;
 326 }
 327
 328 void TheoryUF::addSharedTerm(TNode t) {
 329   Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
 330   d_equalityEngine.addTriggerTerm(t, THEORY_UF);
 331 }
 332
 333 void TheoryUF::computeCareGraph() {
 334
 335   if (d_sharedTerms.size() > 0) {
 336
 337     vector< pair<TNode, TNode> > currentPairs;
 338
 339     // Go through the function terms and see if there are any to split on
 340     unsigned functionTerms = d_functionsTerms.size();
 341     for (unsigned i = 0; i < functionTerms; ++ i) {
 342
 343       TNode f1 = d_functionsTerms[i];
 344       Node op = f1.getOperator();
 345
 346       for (unsigned j = i + 1; j < functionTerms; ++ j) {
 347
 348         TNode f2 = d_functionsTerms[j];
 349
 350         // If the operators are not the same, we can skip this pair
 351         if (f2.getOperator() != op) {
 352           continue;
 353         }
 354
 355         Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
 356
 357         // If the terms are already known to be equal, we are also in good shape
 358         if (d_equalityEngine.areEqual(f1, f2)) {
 359           Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl;
 360           continue;
 361         }
 362
 363         // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal
 364         // We split on the argument pairs that are are not known, unless there is some
 365         // argument pair that is already dis-equal.
 366         bool somePairIsDisequal = false;
 367         currentPairs.clear();
 368         for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
 369
 370           TNode x = f1[k];
 371           TNode y = f2[k];
 372
 373           Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl;
 374
 375           if (d_equalityEngine.areDisequal(x, y, false)) {
 376             // Mark that there is a dis-equal pair and break
 377             somePairIsDisequal = true;
 378             Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl;
 379             break;
 380           }
 381
 382           if (d_equalityEngine.areEqual(x, y)) {
 383             // We don't need this one
 384             Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
 385             continue;
 386           }
 387
 388           if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) {
 389             // Not connected to shared terms, we don't care
 390             continue;
 391           }
 392
 393           // Get representative trigger terms
 394           TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
 395           TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
 396
 397           EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
 398           switch (eqStatusDomain) {
 399           case EQUALITY_FALSE_AND_PROPAGATED:
 400           case EQUALITY_FALSE:
 401           case EQUALITY_FALSE_IN_MODEL:
 402             somePairIsDisequal = true;
 403             continue;
 404             break;
 405           default:
 406             break;
 407             // nothing
 408           }
 409
 410           // Otherwise, we need to figure it out
 411           Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
 412           currentPairs.push_back(make_pair(x_shared, y_shared));
 413         }
 414
 415         if (!somePairIsDisequal) {
 416           for (unsigned i = 0; i < currentPairs.size(); ++ i) {
 417             addCarePair(currentPairs[i].first, currentPairs[i].second);
 418           }
 419         }
 420       }
 421     }
 422   }
 423 }/* TheoryUF::computeCareGraph() */
 424
 425 void TheoryUF::conflict(TNode a, TNode b) {
 426   if (a.getKind() == kind::CONST_BOOLEAN) {
 427     d_conflictNode = explain(a.iffNode(b));
 428   } else {
 429     d_conflictNode = explain(a.eqNode(b));
 430   }
 431   d_out->conflict(d_conflictNode);
 432   d_conflict = true;
 433 }
 434
 435 void TheoryUF::eqNotifyNewClass(TNode t) {
 436   if (d_thss != NULL) {
 437     d_thss->newEqClass(t);
 438   }
 439   // this can be called very early, during initialization
 440   if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
 441     ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t);
 442   }
 443 }
 444
 445 void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
 446   if (getLogicInfo().isQuantified()) {
 447     ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2);
 448   }
 449 }
 450
 451 void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) {
 452   if (d_thss != NULL) {
 453     d_thss->merge(t1, t2);
 454   }
 455 }
 456
 457 void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 458   if (d_thss != NULL) {
 459     d_thss->assertDisequal(t1, t2, reason);
 460   }
 461   if (getLogicInfo().isQuantified()) {
 462     ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason);
 463   }
 464 }
 465
 466 Node TheoryUF::ppRewrite(TNode node) {
 467
 468   if (node.getKind() != kind::APPLY_UF) {
 469     return node;
 470   }
 471
 472   // perform the callbacks requested by TheoryUF::registerPpRewrite()
 473   RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator());
 474   if (c == d_registeredPpRewrites.end()) {
 475     return node;
 476   } else {
 477     Node res = c->second->ppRewrite(node);
 478     if (res != node) {
 479       return ppRewrite(res);
 480     } else {
 481       return res;
 482     }
 483   }
 484 }