src/theory/arith/congruence_manager.cpp

   1 /*! \file congruence_manager.cpp
   2  ** \verbatim
   3  ** Original author: Tim King
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   8  ** See the file COPYING in the top-level source directory for licensing
   9  ** information.\endverbatim
  10  **
  11  ** \brief [[ Add one-line brief description here ]]
  12  **
  13  ** [[ Add lengthier description here ]]
  14  ** \todo document this file
  15  **/
  16
  17 #include "theory/arith/congruence_manager.h"
  18
  19 #include "theory/arith/constraint.h"
  20 #include "theory/arith/arith_utilities.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace arith {
  25
  26 ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict)
  27   : d_inConflict(c),
  28     d_raiseConflict(raiseConflict),
  29     d_notify(*this),
  30     d_keepAlive(c),
  31     d_propagatations(c),
  32     d_explanationMap(c),
  33     d_constraintDatabase(cd),
  34     d_setupLiteral(setup),
  35     d_avariables(avars),
  36     d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
  37 {}
  38
  39 ArithCongruenceManager::Statistics::Statistics():
  40   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
  41   d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
  42   d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
  43   d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
  44   d_propagations("theory::arith::congruence::propagations", 0),
  45   d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
  46   d_conflicts("theory::arith::congruence::conflicts", 0)
  47 {
  48   StatisticsRegistry::registerStat(&d_watchedVariables);
  49   StatisticsRegistry::registerStat(&d_watchedVariableIsZero);
  50   StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero);
  51   StatisticsRegistry::registerStat(&d_equalsConstantCalls);
  52   StatisticsRegistry::registerStat(&d_propagations);
  53   StatisticsRegistry::registerStat(&d_propagateConstraints);
  54   StatisticsRegistry::registerStat(&d_conflicts);
  55 }
  56
  57 ArithCongruenceManager::Statistics::~Statistics(){
  58   StatisticsRegistry::unregisterStat(&d_watchedVariables);
  59   StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero);
  60   StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero);
  61   StatisticsRegistry::unregisterStat(&d_equalsConstantCalls);
  62   StatisticsRegistry::unregisterStat(&d_propagations);
  63   StatisticsRegistry::unregisterStat(&d_propagateConstraints);
  64   StatisticsRegistry::unregisterStat(&d_conflicts);
  65 }
  66
  67 ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
  68   : d_acm(acm)
  69 {}
  70
  71 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerEquality(TNode equality, bool value) {
  72   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
  73   if (value) {
  74     return d_acm.propagate(equality);
  75   } else {
  76     return d_acm.propagate(equality.notNode());
  77   }
  78 }
  79 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(TNode predicate, bool value) {
  80   Unreachable();
  81 }
  82
  83 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  84   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
  85   if (value) {
  86     return d_acm.propagate(t1.eqNode(t2));
  87   } else {
  88     return d_acm.propagate(t1.eqNode(t2).notNode());
  89   }
  90 }
  91 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  92   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
  93   if (t1.getKind() == kind::CONST_BOOLEAN) {
  94     d_acm.propagate(t1.iffNode(t2));
  95   } else {
  96     d_acm.propagate(t1.eqNode(t2));
  97   }
  98 }
  99 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
 100 }
 101 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPreMerge(TNode t1, TNode t2) {
 102 }
 103 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPostMerge(TNode t1, TNode t2) {
 104 }
 105 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 106 }
 107
 108 void ArithCongruenceManager::raiseConflict(Node conflict){
 109   Assert(!inConflict());
 110   Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
 111   d_inConflict.raise();
 112   d_raiseConflict.raiseEEConflict(conflict);
 113 }
 114 bool ArithCongruenceManager::inConflict() const{
 115   return d_inConflict.isRaised();
 116 }
 117
 118 bool ArithCongruenceManager::hasMorePropagations() const {
 119   return !d_propagatations.empty();
 120 }
 121 const Node ArithCongruenceManager::getNextPropagation() {
 122   Assert(hasMorePropagations());
 123   Node prop = d_propagatations.front();
 124   d_propagatations.dequeue();
 125   return prop;
 126 }
 127
 128 bool ArithCongruenceManager::canExplain(TNode n) const {
 129   return d_explanationMap.find(n) != d_explanationMap.end();
 130 }
 131
 132 void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 133   d_ee.setMasterEqualityEngine(eq);
 134 }
 135
 136 Node ArithCongruenceManager::externalToInternal(TNode n) const{
 137   Assert(canExplain(n));
 138   ExplainMap::const_iterator iter = d_explanationMap.find(n);
 139   size_t pos = (*iter).second;
 140   return d_propagatations[pos];
 141 }
 142
 143 void ArithCongruenceManager::pushBack(TNode n){
 144   d_explanationMap.insert(n, d_propagatations.size());
 145   d_propagatations.enqueue(n);
 146
 147   ++(d_statistics.d_propagations);
 148 }
 149 void ArithCongruenceManager::pushBack(TNode n, TNode r){
 150   d_explanationMap.insert(r, d_propagatations.size());
 151   d_explanationMap.insert(n, d_propagatations.size());
 152   d_propagatations.enqueue(n);
 153
 154   ++(d_statistics.d_propagations);
 155 }
 156 void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w){
 157   d_explanationMap.insert(w, d_propagatations.size());
 158   d_explanationMap.insert(r, d_propagatations.size());
 159   d_explanationMap.insert(n, d_propagatations.size());
 160   d_propagatations.enqueue(n);
 161
 162   ++(d_statistics.d_propagations);
 163 }
 164
 165 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub){
 166   Assert(lb->isLowerBound());
 167   Assert(ub->isUpperBound());
 168   Assert(lb->getVariable() == ub->getVariable());
 169   Assert(lb->getValue().sgn() == 0);
 170   Assert(ub->getValue().sgn() == 0);
 171
 172   ++(d_statistics.d_watchedVariableIsZero);
 173
 174   ArithVar s = lb->getVariable();
 175   Node reason = Constraint::externalExplainByAssertions(lb,ub);
 176
 177   d_keepAlive.push_back(reason);
 178   assertionToEqualityEngine(true, s, reason);
 179 }
 180
 181 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
 182   Assert(eq->isEquality());
 183   Assert(eq->getValue().sgn() == 0);
 184
 185   ++(d_statistics.d_watchedVariableIsZero);
 186
 187   ArithVar s = eq->getVariable();
 188
 189   //Explain for conflict is correct as these proofs are generated
 190   //and stored eagerly
 191   //These will be safe for propagation later as well
 192   Node reason = eq->externalExplainByAssertions();
 193
 194   d_keepAlive.push_back(reason);
 195   assertionToEqualityEngine(true, s, reason);
 196 }
 197
 198 void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
 199   ++(d_statistics.d_watchedVariableIsNotZero);
 200
 201   ArithVar s = c->getVariable();
 202
 203   //Explain for conflict is correct as these proofs are generated and stored eagerly
 204   //These will be safe for propagation later as well
 205   Node reason = c->externalExplainByAssertions();
 206
 207   d_keepAlive.push_back(reason);
 208   assertionToEqualityEngine(false, s, reason);
 209 }
 210
 211
 212 bool ArithCongruenceManager::propagate(TNode x){
 213   Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
 214   if(inConflict()){
 215     return true;
 216   }
 217
 218   Node rewritten = Rewriter::rewrite(x);
 219
 220   //Need to still propagate this!
 221   if(rewritten.getKind() == kind::CONST_BOOLEAN){
 222     pushBack(x);
 223
 224     if(rewritten.getConst<bool>()){
 225       return true;
 226     }else{
 227       ++(d_statistics.d_conflicts);
 228
 229       Node conf = flattenAnd(explainInternal(x));
 230       raiseConflict(conf);
 231       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
 232       return false;
 233     }
 234   }
 235
 236   Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
 237
 238   ConstraintP c = d_constraintDatabase.lookup(rewritten);
 239   if(c == NullConstraint){
 240     //using setup as there may not be a corresponding congruence literal yet
 241     d_setupLiteral(rewritten);
 242     c = d_constraintDatabase.lookup(rewritten);
 243     Assert(c != NullConstraint);
 244   }
 245
 246   Debug("arith::congruenceManager")<< "x is "
 247                                    <<  c->hasProof() << " "
 248                                    << (x == rewritten) << " "
 249                                    << c->canBePropagated() << " "
 250                                    << c->negationHasProof() << std::endl;
 251
 252   if(c->negationHasProof()){
 253     Node expC = explainInternal(x);
 254     ConstraintCP negC = c->getNegation();
 255     Node neg = negC->externalExplainByAssertions();
 256     Node conf = expC.andNode(neg);
 257     Node final = flattenAnd(conf);
 258
 259     ++(d_statistics.d_conflicts);
 260     raiseConflict(final);
 261     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
 262     return false;
 263   }
 264
 265   // Cases for propagation
 266   // C : c has a proof
 267   // S : x == rewritten
 268   // P : c can be propagated
 269   //
 270   // CSP
 271   // 000 : propagate x, and mark C it as being explained
 272   // 001 : propagate x, and propagate c after marking it as being explained
 273   // 01* : propagate x, mark c but do not propagate c
 274   // 10* : propagate x, do not mark c and do not propagate c
 275   // 11* : drop the constraint, do not propagate x or c
 276
 277   if(!c->hasProof() && x != rewritten){
 278     if(c->assertedToTheTheory()){
 279       pushBack(x, rewritten, c->getWitness());
 280     }else{
 281       pushBack(x, rewritten);
 282     }
 283
 284     c->setEqualityEngineProof();
 285     if(c->canBePropagated() && !c->assertedToTheTheory()){
 286
 287       ++(d_statistics.d_propagateConstraints);
 288       c->propagate();
 289     }
 290   }else if(!c->hasProof() && x == rewritten){
 291     if(c->assertedToTheTheory()){
 292       pushBack(x, c->getWitness());
 293     }else{
 294       pushBack(x);
 295     }
 296     c->setEqualityEngineProof();
 297   }else if(c->hasProof() && x != rewritten){
 298     if(c->assertedToTheTheory()){
 299       pushBack(x, rewritten, c->getWitness());
 300     }else{
 301       pushBack(x, rewritten);
 302     }
 303   }else{
 304     Assert(c->hasProof() && x == rewritten);
 305   }
 306   return true;
 307 }
 308
 309 void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
 310   if (literal.getKind() != kind::NOT) {
 311     d_ee.explainEquality(literal[0], literal[1], true, assumptions);
 312   } else {
 313     d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
 314   }
 315 }
 316
 317 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
 318   std::set<TNode>::const_iterator it = s.begin();
 319   std::set<TNode>::const_iterator it_end = s.end();
 320   for(; it != it_end; ++it) {
 321     nb << *it;
 322   }
 323 }
 324
 325 Node ArithCongruenceManager::explainInternal(TNode internal){
 326   std::vector<TNode> assumptions;
 327   explain(internal, assumptions);
 328
 329   std::set<TNode> assumptionSet;
 330   assumptionSet.insert(assumptions.begin(), assumptions.end());
 331
 332   if (assumptionSet.size() == 1) {
 333     // All the same, or just one
 334     return assumptions[0];
 335   }else{
 336     NodeBuilder<> conjunction(kind::AND);
 337     enqueueIntoNB(assumptionSet, conjunction);
 338     return conjunction;
 339   }
 340 }
 341 Node ArithCongruenceManager::explain(TNode external){
 342   Node internal = externalToInternal(external);
 343   return explainInternal(internal);
 344 }
 345
 346 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
 347   Node internal = externalToInternal(external);
 348
 349   std::vector<TNode> assumptions;
 350   explain(internal, assumptions);
 351   std::set<TNode> assumptionSet;
 352   assumptionSet.insert(assumptions.begin(), assumptions.end());
 353
 354   enqueueIntoNB(assumptionSet, out);
 355 }
 356
 357 void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
 358   Assert(!isWatchedVariable(s));
 359
 360   Debug("arith::congruenceManager")
 361     << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
 362
 363
 364   ++(d_statistics.d_watchedVariables);
 365
 366   d_watchedVariables.add(s);
 367
 368   Node eq = x.eqNode(y);
 369   d_watchedEqualities.set(s, eq);
 370 }
 371
 372 void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
 373   Assert(isWatchedVariable(s));
 374
 375   TNode eq = d_watchedEqualities[s];
 376   Assert(eq.getKind() == kind::EQUAL);
 377
 378   if(isEquality){
 379     d_ee.assertEquality(eq, true, reason);
 380   }else{
 381     d_ee.assertEquality(eq, false, reason);
 382   }
 383 }
 384
 385 void ArithCongruenceManager::equalsConstant(ConstraintCP c){
 386   Assert(c->isEquality());
 387
 388   ++(d_statistics.d_equalsConstantCalls);
 389   Debug("equalsConstant") << "equals constant " << c << std::endl;
 390
 391   ArithVar x = c->getVariable();
 392   Node xAsNode = d_avariables.asNode(x);
 393   Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
 394
 395
 396   //No guarentee this is in normal form!
 397   Node eq = xAsNode.eqNode(asRational);
 398   d_keepAlive.push_back(eq);
 399
 400   Node reason = c->externalExplainByAssertions();
 401   d_keepAlive.push_back(reason);
 402
 403   d_ee.assertEquality(eq, true, reason);
 404 }
 405
 406 void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
 407   Assert(lb->isLowerBound());
 408   Assert(ub->isUpperBound());
 409   Assert(lb->getVariable() == ub->getVariable());
 410
 411   ++(d_statistics.d_equalsConstantCalls);
 412   Debug("equalsConstant") << "equals constant " << lb << std::endl
 413                           << ub << std::endl;
 414
 415   ArithVar x = lb->getVariable();
 416   Node reason = Constraint::externalExplainByAssertions(lb,ub);
 417
 418   Node xAsNode = d_avariables.asNode(x);
 419   Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
 420
 421   //No guarentee this is in normal form!
 422   Node eq = xAsNode.eqNode(asRational);
 423   d_keepAlive.push_back(eq);
 424   d_keepAlive.push_back(reason);
 425
 426
 427   d_ee.assertEquality(eq, true, reason);
 428 }
 429
 430 void ArithCongruenceManager::addSharedTerm(Node x){
 431   d_ee.addTriggerTerm(x, THEORY_ARITH);
 432 }
 433
 434 }/* CVC4::theory::arith namespace */
 435 }/* CVC4::theory namespace */
 436 }/* CVC4 namespace */