src/theory/arith/congruence_manager.cpp

   1 /*********************                                                        */
   2 /*! \file congruence_manager.cpp
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): dejan, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "theory/arith/congruence_manager.h"
  19
  20 #include "theory/arith/constraint.h"
  21 #include "theory/arith/arith_utilities.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace arith {
  26
  27 ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict)
  28   : d_inConflict(c),
  29     d_raiseConflict(raiseConflict),
  30     d_notify(*this),
  31     d_keepAlive(c),
  32     d_propagatations(c),
  33     d_explanationMap(c),
  34     d_constraintDatabase(cd),
  35     d_setupLiteral(setup),
  36     d_av2Node(av2Node),
  37     d_ee(d_notify, c, "theory::arith::ArithCongruenceManager")
  38 {}
  39
  40 ArithCongruenceManager::Statistics::Statistics():
  41   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
  42   d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
  43   d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
  44   d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
  45   d_propagations("theory::arith::congruence::propagations", 0),
  46   d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
  47   d_conflicts("theory::arith::congruence::conflicts", 0)
  48 {
  49   StatisticsRegistry::registerStat(&d_watchedVariables);
  50   StatisticsRegistry::registerStat(&d_watchedVariableIsZero);
  51   StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero);
  52   StatisticsRegistry::registerStat(&d_equalsConstantCalls);
  53   StatisticsRegistry::registerStat(&d_propagations);
  54   StatisticsRegistry::registerStat(&d_propagateConstraints);
  55   StatisticsRegistry::registerStat(&d_conflicts);
  56 }
  57
  58 ArithCongruenceManager::Statistics::~Statistics(){
  59   StatisticsRegistry::unregisterStat(&d_watchedVariables);
  60   StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero);
  61   StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero);
  62   StatisticsRegistry::unregisterStat(&d_equalsConstantCalls);
  63   StatisticsRegistry::unregisterStat(&d_propagations);
  64   StatisticsRegistry::unregisterStat(&d_propagateConstraints);
  65   StatisticsRegistry::unregisterStat(&d_conflicts);
  66 }
  67
  68 void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  69   d_ee.setMasterEqualityEngine(eq);
  70 }
  71
  72 void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){
  73   Assert(lb->isLowerBound());
  74   Assert(ub->isUpperBound());
  75   Assert(lb->getVariable() == ub->getVariable());
  76   Assert(lb->getValue().sgn() == 0);
  77   Assert(ub->getValue().sgn() == 0);
  78
  79   ++(d_statistics.d_watchedVariableIsZero);
  80
  81   ArithVar s = lb->getVariable();
  82   Node reason = ConstraintValue::explainConflict(lb,ub);
  83
  84   d_keepAlive.push_back(reason);
  85   assertionToEqualityEngine(true, s, reason);
  86 }
  87
  88 void ArithCongruenceManager::watchedVariableIsZero(Constraint eq){
  89   Assert(eq->isEquality());
  90   Assert(eq->getValue().sgn() == 0);
  91
  92   ++(d_statistics.d_watchedVariableIsZero);
  93
  94   ArithVar s = eq->getVariable();
  95
  96   //Explain for conflict is correct as these proofs are generated
  97   //and stored eagerly
  98   //These will be safe for propagation later as well
  99   Node reason = eq->explainForConflict();
 100
 101   d_keepAlive.push_back(reason);
 102   assertionToEqualityEngine(true, s, reason);
 103 }
 104
 105 void ArithCongruenceManager::watchedVariableCannotBeZero(Constraint c){
 106   ++(d_statistics.d_watchedVariableIsNotZero);
 107
 108   ArithVar s = c->getVariable();
 109
 110   //Explain for conflict is correct as these proofs are generated and stored eagerly
 111   //These will be safe for propagation later as well
 112   Node reason = c->explainForConflict();
 113
 114   d_keepAlive.push_back(reason);
 115   assertionToEqualityEngine(false, s, reason);
 116 }
 117
 118
 119 bool ArithCongruenceManager::propagate(TNode x){
 120   Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
 121   if(inConflict()){
 122     return true;
 123   }
 124
 125   Node rewritten = Rewriter::rewrite(x);
 126
 127   //Need to still propagate this!
 128   if(rewritten.getKind() == kind::CONST_BOOLEAN){
 129     pushBack(x);
 130
 131     if(rewritten.getConst<bool>()){
 132       return true;
 133     }else{
 134       ++(d_statistics.d_conflicts);
 135
 136       Node conf = flattenAnd(explainInternal(x));
 137       raiseConflict(conf);
 138       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
 139       return false;
 140     }
 141   }
 142
 143   Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
 144
 145   Constraint c = d_constraintDatabase.lookup(rewritten);
 146   if(c == NullConstraint){
 147     //using setup as there may not be a corresponding congruence literal yet
 148     d_setupLiteral(rewritten);
 149     c = d_constraintDatabase.lookup(rewritten);
 150     Assert(c != NullConstraint);
 151   }
 152
 153   Debug("arith::congruenceManager")<< "x is "
 154                                    <<  c->hasProof() << " "
 155                                    << (x == rewritten) << " "
 156                                    << c->canBePropagated() << " "
 157                                    << c->negationHasProof() << std::endl;
 158
 159   if(c->negationHasProof()){
 160     Node expC = explainInternal(x);
 161     Node neg = c->getNegation()->explainForConflict();
 162     Node conf = expC.andNode(neg);
 163     Node final = flattenAnd(conf);
 164
 165     ++(d_statistics.d_conflicts);
 166     raiseConflict(final);
 167     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
 168     return false;
 169   }
 170
 171   // Cases for propagation
 172   // C : c has a proof
 173   // S : x == rewritten
 174   // P : c can be propagated
 175   //
 176   // CSP
 177   // 000 : propagate x, and mark C it as being explained
 178   // 001 : propagate x, and propagate c after marking it as being explained
 179   // 01* : propagate x, mark c but do not propagate c
 180   // 10* : propagate x, do not mark c and do not propagate c
 181   // 11* : drop the constraint, do not propagate x or c
 182
 183   if(!c->hasProof() && x != rewritten){
 184     if(c->assertedToTheTheory()){
 185       pushBack(x, rewritten, c->getWitness());
 186     }else{
 187       pushBack(x, rewritten);
 188     }
 189
 190     c->setEqualityEngineProof();
 191     if(c->canBePropagated() && !c->assertedToTheTheory()){
 192
 193       ++(d_statistics.d_propagateConstraints);
 194       c->propagate();
 195     }
 196   }else if(!c->hasProof() && x == rewritten){
 197     if(c->assertedToTheTheory()){
 198       pushBack(x, c->getWitness());
 199     }else{
 200       pushBack(x);
 201     }
 202     c->setEqualityEngineProof();
 203   }else if(c->hasProof() && x != rewritten){
 204     if(c->assertedToTheTheory()){
 205       pushBack(x, rewritten, c->getWitness());
 206     }else{
 207       pushBack(x, rewritten);
 208     }
 209   }else{
 210     Assert(c->hasProof() && x == rewritten);
 211   }
 212   return true;
 213 }
 214
 215 void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
 216   if (literal.getKind() != kind::NOT) {
 217     d_ee.explainEquality(literal[0], literal[1], true, assumptions);
 218   } else {
 219     d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
 220   }
 221 }
 222
 223 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
 224   std::set<TNode>::const_iterator it = s.begin();
 225   std::set<TNode>::const_iterator it_end = s.end();
 226   for(; it != it_end; ++it) {
 227     nb << *it;
 228   }
 229 }
 230
 231 Node ArithCongruenceManager::explainInternal(TNode internal){
 232   std::vector<TNode> assumptions;
 233   explain(internal, assumptions);
 234
 235   std::set<TNode> assumptionSet;
 236   assumptionSet.insert(assumptions.begin(), assumptions.end());
 237
 238   if (assumptionSet.size() == 1) {
 239     // All the same, or just one
 240     return assumptions[0];
 241   }else{
 242     NodeBuilder<> conjunction(kind::AND);
 243     enqueueIntoNB(assumptionSet, conjunction);
 244     return conjunction;
 245   }
 246 }
 247 Node ArithCongruenceManager::explain(TNode external){
 248   Node internal = externalToInternal(external);
 249   return explainInternal(internal);
 250 }
 251
 252 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
 253   Node internal = externalToInternal(external);
 254
 255   std::vector<TNode> assumptions;
 256   explain(internal, assumptions);
 257   std::set<TNode> assumptionSet;
 258   assumptionSet.insert(assumptions.begin(), assumptions.end());
 259
 260   enqueueIntoNB(assumptionSet, out);
 261 }
 262
 263 void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
 264   Assert(!isWatchedVariable(s));
 265
 266   Debug("arith::congruenceManager")
 267     << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
 268
 269
 270   ++(d_statistics.d_watchedVariables);
 271
 272   d_watchedVariables.add(s);
 273
 274   Node eq = x.eqNode(y);
 275   d_watchedEqualities.set(s, eq);
 276 }
 277
 278 void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
 279   Assert(isWatchedVariable(s));
 280
 281   TNode eq = d_watchedEqualities[s];
 282   Assert(eq.getKind() == kind::EQUAL);
 283
 284   if(isEquality){
 285     d_ee.assertEquality(eq, true, reason);
 286   }else{
 287     d_ee.assertEquality(eq, false, reason);
 288   }
 289 }
 290
 291 void ArithCongruenceManager::equalsConstant(Constraint c){
 292   Assert(c->isEquality());
 293
 294   ++(d_statistics.d_equalsConstantCalls);
 295   Debug("equalsConstant") << "equals constant " << c << std::endl;
 296
 297   ArithVar x = c->getVariable();
 298   Node xAsNode = d_av2Node.asNode(x);
 299   Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
 300
 301
 302   //No guarentee this is in normal form!
 303   Node eq = xAsNode.eqNode(asRational);
 304   d_keepAlive.push_back(eq);
 305
 306   Node reason = c->explainForConflict();
 307   d_keepAlive.push_back(reason);
 308
 309   d_ee.assertEquality(eq, true, reason);
 310 }
 311
 312 void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){
 313   Assert(lb->isLowerBound());
 314   Assert(ub->isUpperBound());
 315   Assert(lb->getVariable() == ub->getVariable());
 316
 317   ++(d_statistics.d_equalsConstantCalls);
 318   Debug("equalsConstant") << "equals constant " << lb << std::endl
 319                           << ub << std::endl;
 320
 321   ArithVar x = lb->getVariable();
 322   Node reason = ConstraintValue::explainConflict(lb,ub);
 323
 324   Node xAsNode = d_av2Node.asNode(x);
 325   Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
 326
 327   //No guarentee this is in normal form!
 328   Node eq = xAsNode.eqNode(asRational);
 329   d_keepAlive.push_back(eq);
 330   d_keepAlive.push_back(reason);
 331
 332
 333   d_ee.assertEquality(eq, true, reason);
 334 }
 335
 336 void ArithCongruenceManager::addSharedTerm(Node x){
 337   d_ee.addTriggerTerm(x, THEORY_ARITH);
 338 }
 339
 340 }/* CVC4::theory::arith namespace */
 341 }/* CVC4::theory namespace */
 342 }/* CVC4 namespace */