src/theory/arith/congruence_manager.cpp

   1 /*********************                                                        */
   2 /*! \file congruence_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Paul Meng, 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 [[ 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 "base/output.h"
  21 #include "smt/smt_statistics_registry.h"
  22 #include "theory/arith/arith_utilities.h"
  23 #include "theory/arith/constraint.h"
  24 #include "theory/quantifiers/equality_infer.h"
  25 #include "options/arith_options.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace arith {
  30
  31 ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict)
  32   : d_inConflict(c),
  33     d_raiseConflict(raiseConflict),
  34     d_notify(*this),
  35     d_eq_infer(NULL),
  36     d_eqi_counter(0,c),
  37     d_keepAlive(c),
  38     d_propagatations(c),
  39     d_explanationMap(c),
  40     d_constraintDatabase(cd),
  41     d_setupLiteral(setup),
  42     d_avariables(avars),
  43     d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
  44 {
  45   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
  46   d_ee.addFunctionKind(kind::EXPONENTIAL);
  47   d_ee.addFunctionKind(kind::SINE);
  48   //module to infer additional equalities based on normalization
  49   if( options::sNormInferEq() ){
  50     d_eq_infer = new quantifiers::EqualityInference(c, true);
  51     d_true = NodeManager::currentNM()->mkConst( true );
  52   }
  53 }
  54
  55 ArithCongruenceManager::~ArithCongruenceManager() {
  56   if( d_eq_infer ){
  57     delete d_eq_infer;
  58   }
  59 }
  60
  61 ArithCongruenceManager::Statistics::Statistics():
  62   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
  63   d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
  64   d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
  65   d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
  66   d_propagations("theory::arith::congruence::propagations", 0),
  67   d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
  68   d_conflicts("theory::arith::congruence::conflicts", 0)
  69 {
  70   smtStatisticsRegistry()->registerStat(&d_watchedVariables);
  71   smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
  72   smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
  73   smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
  74   smtStatisticsRegistry()->registerStat(&d_propagations);
  75   smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
  76   smtStatisticsRegistry()->registerStat(&d_conflicts);
  77 }
  78
  79 ArithCongruenceManager::Statistics::~Statistics(){
  80   smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
  81   smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
  82   smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
  83   smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
  84   smtStatisticsRegistry()->unregisterStat(&d_propagations);
  85   smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
  86   smtStatisticsRegistry()->unregisterStat(&d_conflicts);
  87 }
  88
  89 ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
  90   : d_acm(acm)
  91 {}
  92
  93 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerEquality(TNode equality, bool value) {
  94   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
  95   if (value) {
  96     return d_acm.propagate(equality);
  97   } else {
  98     return d_acm.propagate(equality.notNode());
  99   }
 100 }
 101 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(TNode predicate, bool value) {
 102   Unreachable();
 103 }
 104
 105 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 106   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
 107   if (value) {
 108     return d_acm.propagate(t1.eqNode(t2));
 109   } else {
 110     return d_acm.propagate(t1.eqNode(t2).notNode());
 111   }
 112 }
 113 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 114   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
 115   d_acm.propagate(t1.eqNode(t2));
 116 }
 117 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
 118   d_acm.eqNotifyNewClass(t);
 119 }
 120 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPreMerge(TNode t1, TNode t2) {
 121 }
 122 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPostMerge(TNode t1, TNode t2) {
 123   d_acm.eqNotifyPostMerge(t1,t2);
 124 }
 125 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 126 }
 127
 128 void ArithCongruenceManager::raiseConflict(Node conflict){
 129   Assert(!inConflict());
 130   Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
 131   d_inConflict.raise();
 132   d_raiseConflict.raiseEEConflict(conflict);
 133 }
 134 bool ArithCongruenceManager::inConflict() const{
 135   return d_inConflict.isRaised();
 136 }
 137
 138 bool ArithCongruenceManager::hasMorePropagations() const {
 139   return !d_propagatations.empty();
 140 }
 141 const Node ArithCongruenceManager::getNextPropagation() {
 142   Assert(hasMorePropagations());
 143   Node prop = d_propagatations.front();
 144   d_propagatations.dequeue();
 145   return prop;
 146 }
 147
 148 bool ArithCongruenceManager::canExplain(TNode n) const {
 149   return d_explanationMap.find(n) != d_explanationMap.end();
 150 }
 151
 152 void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 153   d_ee.setMasterEqualityEngine(eq);
 154 }
 155
 156 Node ArithCongruenceManager::externalToInternal(TNode n) const{
 157   Assert(canExplain(n));
 158   ExplainMap::const_iterator iter = d_explanationMap.find(n);
 159   size_t pos = (*iter).second;
 160   return d_propagatations[pos];
 161 }
 162
 163 void ArithCongruenceManager::pushBack(TNode n){
 164   d_explanationMap.insert(n, d_propagatations.size());
 165   d_propagatations.enqueue(n);
 166
 167   ++(d_statistics.d_propagations);
 168 }
 169 void ArithCongruenceManager::pushBack(TNode n, TNode r){
 170   d_explanationMap.insert(r, d_propagatations.size());
 171   d_explanationMap.insert(n, d_propagatations.size());
 172   d_propagatations.enqueue(n);
 173
 174   ++(d_statistics.d_propagations);
 175 }
 176 void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w){
 177   d_explanationMap.insert(w, d_propagatations.size());
 178   d_explanationMap.insert(r, d_propagatations.size());
 179   d_explanationMap.insert(n, d_propagatations.size());
 180   d_propagatations.enqueue(n);
 181
 182   ++(d_statistics.d_propagations);
 183 }
 184
 185 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub){
 186   Assert(lb->isLowerBound());
 187   Assert(ub->isUpperBound());
 188   Assert(lb->getVariable() == ub->getVariable());
 189   Assert(lb->getValue().sgn() == 0);
 190   Assert(ub->getValue().sgn() == 0);
 191
 192   ++(d_statistics.d_watchedVariableIsZero);
 193
 194   ArithVar s = lb->getVariable();
 195   Node reason = Constraint::externalExplainByAssertions(lb,ub);
 196
 197   d_keepAlive.push_back(reason);
 198   assertionToEqualityEngine(true, s, reason);
 199 }
 200
 201 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
 202   Assert(eq->isEquality());
 203   Assert(eq->getValue().sgn() == 0);
 204
 205   ++(d_statistics.d_watchedVariableIsZero);
 206
 207   ArithVar s = eq->getVariable();
 208
 209   //Explain for conflict is correct as these proofs are generated
 210   //and stored eagerly
 211   //These will be safe for propagation later as well
 212   Node reason = eq->externalExplainByAssertions();
 213
 214   d_keepAlive.push_back(reason);
 215   assertionToEqualityEngine(true, s, reason);
 216 }
 217
 218 void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
 219   ++(d_statistics.d_watchedVariableIsNotZero);
 220
 221   ArithVar s = c->getVariable();
 222
 223   //Explain for conflict is correct as these proofs are generated and stored eagerly
 224   //These will be safe for propagation later as well
 225   Node reason = c->externalExplainByAssertions();
 226
 227   d_keepAlive.push_back(reason);
 228   assertionToEqualityEngine(false, s, reason);
 229 }
 230
 231
 232 bool ArithCongruenceManager::propagate(TNode x){
 233   Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
 234   if(inConflict()){
 235     return true;
 236   }
 237
 238   Node rewritten = Rewriter::rewrite(x);
 239
 240   //Need to still propagate this!
 241   if(rewritten.getKind() == kind::CONST_BOOLEAN){
 242     pushBack(x);
 243
 244     if(rewritten.getConst<bool>()){
 245       return true;
 246     }else{
 247       ++(d_statistics.d_conflicts);
 248
 249       Node conf = flattenAnd(explainInternal(x));
 250       raiseConflict(conf);
 251       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
 252       return false;
 253     }
 254   }
 255
 256   Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
 257
 258   ConstraintP c = d_constraintDatabase.lookup(rewritten);
 259   if(c == NullConstraint){
 260     //using setup as there may not be a corresponding congruence literal yet
 261     d_setupLiteral(rewritten);
 262     c = d_constraintDatabase.lookup(rewritten);
 263     Assert(c != NullConstraint);
 264   }
 265
 266   Debug("arith::congruenceManager")<< "x is "
 267                                    <<  c->hasProof() << " "
 268                                    << (x == rewritten) << " "
 269                                    << c->canBePropagated() << " "
 270                                    << c->negationHasProof() << std::endl;
 271
 272   if(c->negationHasProof()){
 273     Node expC = explainInternal(x);
 274     ConstraintCP negC = c->getNegation();
 275     Node neg = negC->externalExplainByAssertions();
 276     Node conf = expC.andNode(neg);
 277     Node final = flattenAnd(conf);
 278
 279     ++(d_statistics.d_conflicts);
 280     raiseConflict(final);
 281     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
 282     return false;
 283   }
 284
 285   // Cases for propagation
 286   // C : c has a proof
 287   // S : x == rewritten
 288   // P : c can be propagated
 289   //
 290   // CSP
 291   // 000 : propagate x, and mark C it as being explained
 292   // 001 : propagate x, and propagate c after marking it as being explained
 293   // 01* : propagate x, mark c but do not propagate c
 294   // 10* : propagate x, do not mark c and do not propagate c
 295   // 11* : drop the constraint, do not propagate x or c
 296
 297   if(!c->hasProof() && x != rewritten){
 298     if(c->assertedToTheTheory()){
 299       pushBack(x, rewritten, c->getWitness());
 300     }else{
 301       pushBack(x, rewritten);
 302     }
 303
 304     c->setEqualityEngineProof();
 305     if(c->canBePropagated() && !c->assertedToTheTheory()){
 306
 307       ++(d_statistics.d_propagateConstraints);
 308       c->propagate();
 309     }
 310   }else if(!c->hasProof() && x == rewritten){
 311     if(c->assertedToTheTheory()){
 312       pushBack(x, c->getWitness());
 313     }else{
 314       pushBack(x);
 315     }
 316     c->setEqualityEngineProof();
 317   }else if(c->hasProof() && x != rewritten){
 318     if(c->assertedToTheTheory()){
 319       pushBack(x);
 320     }else{
 321       pushBack(x);
 322     }
 323   }else{
 324     Assert(c->hasProof() && x == rewritten);
 325   }
 326   return true;
 327 }
 328
 329 void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
 330   if (literal.getKind() != kind::NOT) {
 331     d_ee.explainEquality(literal[0], literal[1], true, assumptions);
 332   } else {
 333     d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
 334   }
 335 }
 336
 337 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
 338   std::set<TNode>::const_iterator it = s.begin();
 339   std::set<TNode>::const_iterator it_end = s.end();
 340   for(; it != it_end; ++it) {
 341     nb << *it;
 342   }
 343 }
 344
 345 Node ArithCongruenceManager::explainInternal(TNode internal){
 346   std::vector<TNode> assumptions;
 347   explain(internal, assumptions);
 348
 349   std::set<TNode> assumptionSet;
 350   assumptionSet.insert(assumptions.begin(), assumptions.end());
 351
 352   if (assumptionSet.size() == 1) {
 353     // All the same, or just one
 354     return assumptions[0];
 355   }else{
 356     NodeBuilder<> conjunction(kind::AND);
 357     enqueueIntoNB(assumptionSet, conjunction);
 358     return conjunction;
 359   }
 360 }
 361
 362 void ArithCongruenceManager::eqNotifyNewClass(TNode t) {
 363   if( d_eq_infer ){
 364     d_eq_infer->eqNotifyNewClass(t);
 365     fixpointInfer();
 366   }
 367 }
 368 void ArithCongruenceManager::eqNotifyPostMerge(TNode t1, TNode t2) {
 369   if( d_eq_infer ){
 370     d_eq_infer->eqNotifyMerge(t1, t2);
 371     fixpointInfer();
 372   }
 373 }
 374
 375 Node ArithCongruenceManager::explain(TNode external){
 376   Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
 377   Node internal = externalToInternal(external);
 378   Trace("arith-ee") << "...internal = " << internal << std::endl;
 379   return explainInternal(internal);
 380 }
 381
 382 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
 383   Node internal = externalToInternal(external);
 384
 385   std::vector<TNode> assumptions;
 386   explain(internal, assumptions);
 387   std::set<TNode> assumptionSet;
 388   assumptionSet.insert(assumptions.begin(), assumptions.end());
 389
 390   enqueueIntoNB(assumptionSet, out);
 391 }
 392
 393 void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
 394   Assert(!isWatchedVariable(s));
 395
 396   Debug("arith::congruenceManager")
 397     << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
 398
 399
 400   ++(d_statistics.d_watchedVariables);
 401
 402   d_watchedVariables.add(s);
 403
 404   Node eq = x.eqNode(y);
 405   d_watchedEqualities.set(s, eq);
 406 }
 407
 408 void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
 409   Assert(isWatchedVariable(s));
 410
 411   TNode eq = d_watchedEqualities[s];
 412   Assert(eq.getKind() == kind::EQUAL);
 413
 414   Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl;
 415   if(isEquality){
 416     d_ee.assertEquality(eq, true, reason);
 417   }else{
 418     d_ee.assertEquality(eq, false, reason);
 419   }
 420 }
 421
 422 void ArithCongruenceManager::equalsConstant(ConstraintCP c){
 423   Assert(c->isEquality());
 424
 425   ++(d_statistics.d_equalsConstantCalls);
 426   Debug("equalsConstant") << "equals constant " << c << std::endl;
 427
 428   ArithVar x = c->getVariable();
 429   Node xAsNode = d_avariables.asNode(x);
 430   Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
 431
 432
 433   //No guarentee this is in normal form!
 434   Node eq = xAsNode.eqNode(asRational);
 435   d_keepAlive.push_back(eq);
 436
 437   Node reason = c->externalExplainByAssertions();
 438   d_keepAlive.push_back(reason);
 439
 440   Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
 441   d_ee.assertEquality(eq, true, reason);
 442 }
 443
 444 void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
 445   Assert(lb->isLowerBound());
 446   Assert(ub->isUpperBound());
 447   Assert(lb->getVariable() == ub->getVariable());
 448
 449   ++(d_statistics.d_equalsConstantCalls);
 450   Debug("equalsConstant") << "equals constant " << lb << std::endl
 451                           << ub << std::endl;
 452
 453   ArithVar x = lb->getVariable();
 454   Node reason = Constraint::externalExplainByAssertions(lb,ub);
 455
 456   Node xAsNode = d_avariables.asNode(x);
 457   Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
 458
 459   //No guarentee this is in normal form!
 460   Node eq = xAsNode.eqNode(asRational);
 461   d_keepAlive.push_back(eq);
 462   d_keepAlive.push_back(reason);
 463
 464   Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
 465   d_ee.assertEquality(eq, true, reason);
 466 }
 467
 468 void ArithCongruenceManager::addSharedTerm(Node x){
 469   d_ee.addTriggerTerm(x, THEORY_ARITH);
 470 }
 471
 472 bool ArithCongruenceManager::fixpointInfer() {
 473   if( d_eq_infer ){
 474     while(! inConflict() && d_eqi_counter.get()<d_eq_infer->getNumPendingMerges() ) {
 475       Trace("snorm-infer-eq-debug") << "Processing " << d_eqi_counter.get() << " / " << d_eq_infer->getNumPendingMerges() << std::endl;
 476       Node eq = d_eq_infer->getPendingMerge( d_eqi_counter.get() );
 477       Trace("snorm-infer-eq") << "ArithCongruenceManager : Infer by normalization : " << eq << std::endl;
 478       if( !d_ee.areEqual( eq[0], eq[1] ) ){
 479         Node eq_exp = d_eq_infer->getPendingMergeExplanation( d_eqi_counter.get() );
 480         Trace("snorm-infer-eq") << "           explanation : " << eq_exp << std::endl;
 481         //regress explanation
 482         std::vector<TNode> assumptions;
 483         if( eq_exp.getKind()==kind::AND ){
 484           for( unsigned i=0; i<eq_exp.getNumChildren(); i++ ){
 485             explain( eq_exp[i], assumptions );
 486           }
 487         }else if( eq_exp.getKind()==kind::EQUAL ){
 488           explain( eq_exp, assumptions );
 489         }else{
 490           //eq_exp should be true
 491           Assert( eq_exp==d_true );
 492         }
 493         Node req_exp;
 494         if( assumptions.empty() ){
 495           req_exp = d_true;
 496         }else{
 497           std::set<TNode> assumptionSet;
 498           assumptionSet.insert(assumptions.begin(), assumptions.end());
 499           if( assumptionSet.size()==1 ){
 500             req_exp = assumptions[0];
 501           }else{
 502             NodeBuilder<> conjunction(kind::AND);
 503             enqueueIntoNB(assumptionSet, conjunction);
 504             req_exp = conjunction;
 505           }
 506         }
 507         Trace("snorm-infer-eq") << " regressed explanation : " << req_exp << std::endl;
 508         d_ee.assertEquality( eq, true, req_exp );
 509         d_keepAlive.push_back( req_exp );
 510       }else{
 511         Trace("snorm-infer-eq") << "...already equal." << std::endl;
 512       }
 513       d_eqi_counter = d_eqi_counter.get() + 1;
 514     }
 515   }
 516   return inConflict();
 517 }
 518
 519 }/* CVC4::theory::arith namespace */
 520 }/* CVC4::theory namespace */
 521 }/* CVC4 namespace */