src/theory/arith/congruence_manager.cpp

   1 /*********************                                                        */
   2 /*! \file congruence_manager.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andrew Reynolds, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 "options/arith_options.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace arith {
  29
  30 ArithCongruenceManager::ArithCongruenceManager(
  31     context::Context* c,
  32     context::UserContext* u,
  33     ConstraintDatabase& cd,
  34     SetupLiteralCallBack setup,
  35     const ArithVariables& avars,
  36     RaiseEqualityEngineConflict raiseConflict,
  37     ProofNodeManager* pnm)
  38     : d_inConflict(c),
  39       d_raiseConflict(raiseConflict),
  40       d_notify(*this),
  41       d_keepAlive(c),
  42       d_propagatations(c),
  43       d_explanationMap(c),
  44       d_constraintDatabase(cd),
  45       d_setupLiteral(setup),
  46       d_avariables(avars),
  47       d_ee(nullptr),
  48       d_satContext(c),
  49       d_userContext(u),
  50       d_pnm(pnm),
  51       // Construct d_pfGenEe with the SAT context, since its proof include
  52       // unclosed assumptions of theory literals.
  53       d_pfGenEe(
  54           new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")),
  55       // Construct d_pfGenEe with the USER context, since its proofs are closed.
  56       d_pfGenExplain(new EagerProofGenerator(
  57           pnm, u, "ArithCongruenceManager::pfGenExplain")),
  58       d_pfee(nullptr)
  59 {
  60 }
  61
  62 ArithCongruenceManager::~ArithCongruenceManager() {}
  63
  64 bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
  65 {
  66   esi.d_notify = &d_notify;
  67   esi.d_name = "theory::arith::ArithCongruenceManager";
  68   return true;
  69 }
  70
  71 void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
  72                                         eq::ProofEqEngine* pfee)
  73 {
  74   Assert(ee != nullptr);
  75   d_ee = ee;
  76   d_ee->addFunctionKind(kind::NONLINEAR_MULT);
  77   d_ee->addFunctionKind(kind::EXPONENTIAL);
  78   d_ee->addFunctionKind(kind::SINE);
  79   d_ee->addFunctionKind(kind::IAND);
  80   // have proof equality engine only if proofs are enabled
  81   Assert(isProofEnabled() == (pfee != nullptr));
  82   d_pfee = pfee;
  83 }
  84
  85 ArithCongruenceManager::Statistics::Statistics():
  86   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
  87   d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
  88   d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
  89   d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
  90   d_propagations("theory::arith::congruence::propagations", 0),
  91   d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
  92   d_conflicts("theory::arith::congruence::conflicts", 0)
  93 {
  94   smtStatisticsRegistry()->registerStat(&d_watchedVariables);
  95   smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
  96   smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
  97   smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
  98   smtStatisticsRegistry()->registerStat(&d_propagations);
  99   smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
 100   smtStatisticsRegistry()->registerStat(&d_conflicts);
 101 }
 102
 103 ArithCongruenceManager::Statistics::~Statistics(){
 104   smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
 105   smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
 106   smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
 107   smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
 108   smtStatisticsRegistry()->unregisterStat(&d_propagations);
 109   smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
 110   smtStatisticsRegistry()->unregisterStat(&d_conflicts);
 111 }
 112
 113 ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
 114   : d_acm(acm)
 115 {}
 116
 117 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerPredicate(
 118     TNode predicate, bool value)
 119 {
 120   Assert(predicate.getKind() == kind::EQUAL);
 121   Debug("arith::congruences")
 122       << "ArithCongruenceNotify::eqNotifyTriggerPredicate(" << predicate << ", "
 123       << (value ? "true" : "false") << ")" << std::endl;
 124   if (value) {
 125     return d_acm.propagate(predicate);
 126   }
 127   return d_acm.propagate(predicate.notNode());
 128 }
 129
 130 bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
 131   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
 132   if (value) {
 133     return d_acm.propagate(t1.eqNode(t2));
 134   } else {
 135     return d_acm.propagate(t1.eqNode(t2).notNode());
 136   }
 137 }
 138 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 139   Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
 140   d_acm.propagate(t1.eqNode(t2));
 141 }
 142 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
 143 }
 144 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
 145                                                                   TNode t2)
 146 {
 147 }
 148 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 149 }
 150
 151 void ArithCongruenceManager::raiseConflict(Node conflict){
 152   Assert(!inConflict());
 153   Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
 154   d_inConflict.raise();
 155   d_raiseConflict.raiseEEConflict(conflict);
 156 }
 157 bool ArithCongruenceManager::inConflict() const{
 158   return d_inConflict.isRaised();
 159 }
 160
 161 bool ArithCongruenceManager::hasMorePropagations() const {
 162   return !d_propagatations.empty();
 163 }
 164 const Node ArithCongruenceManager::getNextPropagation() {
 165   Assert(hasMorePropagations());
 166   Node prop = d_propagatations.front();
 167   d_propagatations.dequeue();
 168   return prop;
 169 }
 170
 171 bool ArithCongruenceManager::canExplain(TNode n) const {
 172   return d_explanationMap.find(n) != d_explanationMap.end();
 173 }
 174
 175 Node ArithCongruenceManager::externalToInternal(TNode n) const{
 176   Assert(canExplain(n));
 177   ExplainMap::const_iterator iter = d_explanationMap.find(n);
 178   size_t pos = (*iter).second;
 179   return d_propagatations[pos];
 180 }
 181
 182 void ArithCongruenceManager::pushBack(TNode n){
 183   d_explanationMap.insert(n, d_propagatations.size());
 184   d_propagatations.enqueue(n);
 185
 186   ++(d_statistics.d_propagations);
 187 }
 188 void ArithCongruenceManager::pushBack(TNode n, TNode r){
 189   d_explanationMap.insert(r, d_propagatations.size());
 190   d_explanationMap.insert(n, d_propagatations.size());
 191   d_propagatations.enqueue(n);
 192
 193   ++(d_statistics.d_propagations);
 194 }
 195 void ArithCongruenceManager::pushBack(TNode n, TNode r, TNode w){
 196   d_explanationMap.insert(w, d_propagatations.size());
 197   d_explanationMap.insert(r, d_propagatations.size());
 198   d_explanationMap.insert(n, d_propagatations.size());
 199   d_propagatations.enqueue(n);
 200
 201   ++(d_statistics.d_propagations);
 202 }
 203
 204 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub){
 205   Assert(lb->isLowerBound());
 206   Assert(ub->isUpperBound());
 207   Assert(lb->getVariable() == ub->getVariable());
 208   Assert(lb->getValue().sgn() == 0);
 209   Assert(ub->getValue().sgn() == 0);
 210
 211   ++(d_statistics.d_watchedVariableIsZero);
 212
 213   ArithVar s = lb->getVariable();
 214   TNode eq = d_watchedEqualities[s];
 215   ConstraintCP eqC = d_constraintDatabase.getConstraint(
 216       s, ConstraintType::Equality, lb->getValue());
 217   NodeBuilder<> reasonBuilder(Kind::AND);
 218   auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
 219   auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
 220   Node reason = safeConstructNary(reasonBuilder);
 221   std::shared_ptr<ProofNode> pf{};
 222   if (isProofEnabled())
 223   {
 224     pf = d_pnm->mkNode(
 225         PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()});
 226     pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq});
 227   }
 228
 229   d_keepAlive.push_back(reason);
 230   Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy"
 231                     << std::endl;
 232   Trace("arith-ee") << "  based on " << lb << std::endl;
 233   Trace("arith-ee") << "  based on " << ub << std::endl;
 234   assertionToEqualityEngine(true, s, reason, pf);
 235 }
 236
 237 void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
 238   Debug("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl;
 239
 240   Assert(eq->isEquality());
 241   Assert(eq->getValue().sgn() == 0);
 242
 243   ++(d_statistics.d_watchedVariableIsZero);
 244
 245   ArithVar s = eq->getVariable();
 246
 247   //Explain for conflict is correct as these proofs are generated
 248   //and stored eagerly
 249   //These will be safe for propagation later as well
 250   NodeBuilder<> nb(Kind::AND);
 251   // An open proof of eq from literals now in reason.
 252   if (Debug.isOn("arith::cong"))
 253   {
 254     eq->printProofTree(Debug("arith::cong"));
 255   }
 256   auto pf = eq->externalExplainByAssertions(nb);
 257   if (isProofEnabled())
 258   {
 259     pf = d_pnm->mkNode(
 260         PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {d_watchedEqualities[s]});
 261   }
 262   Node reason = safeConstructNary(nb);
 263
 264   d_keepAlive.push_back(reason);
 265   assertionToEqualityEngine(true, s, reason, pf);
 266 }
 267
 268 void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
 269   Debug("arith::cong::notzero")
 270       << "Cong::watchedVariableCannotBeZero " << *c << std::endl;
 271   ++(d_statistics.d_watchedVariableIsNotZero);
 272
 273   ArithVar s = c->getVariable();
 274   Node disEq = d_watchedEqualities[s].negate();
 275
 276   //Explain for conflict is correct as these proofs are generated and stored eagerly
 277   //These will be safe for propagation later as well
 278   NodeBuilder<> nb(Kind::AND);
 279   // An open proof of eq from literals now in reason.
 280   auto pf = c->externalExplainByAssertions(nb);
 281   if (Debug.isOn("arith::cong::notzero"))
 282   {
 283     Debug("arith::cong::notzero") << "  original proof ";
 284     pf->printDebug(Debug("arith::cong::notzero"));
 285     Debug("arith::cong::notzero") << std::endl;
 286   }
 287   Node reason = safeConstructNary(nb);
 288   if (isProofEnabled())
 289   {
 290     if (c->getType() == ConstraintType::Disequality)
 291     {
 292       Assert(c->getLiteral() == d_watchedEqualities[s].negate());
 293       // We have to prove equivalence to the watched disequality.
 294       pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {disEq});
 295     }
 296     else
 297     {
 298       Debug("arith::cong::notzero")
 299           << "  proof modification needed" << std::endl;
 300
 301       // Four cases:
 302       //   c has form x_i = d, d > 0     => multiply c by -1 in Farkas proof
 303       //   c has form x_i = d, d > 0     => multiply c by 1 in Farkas proof
 304       //   c has form x_i <= d, d < 0     => multiply c by 1 in Farkas proof
 305       //   c has form x_i >= d, d > 0     => multiply c by -1 in Farkas proof
 306       const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound
 307                                     || (c->getType() == ConstraintType::Equality
 308                                         && c->getValue().sgn() > 0);
 309       const int cSign = scaleCNegatively ? -1 : 1;
 310       TNode isZero = d_watchedEqualities[s];
 311       const auto isZeroPf = d_pnm->mkAssume(isZero);
 312       const auto nm = NodeManager::currentNM();
 313       const auto sumPf = d_pnm->mkNode(
 314           PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
 315           {isZeroPf, pf},
 316           // Trick for getting correct, opposing signs.
 317           {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});
 318       const auto botPf = d_pnm->mkNode(
 319           PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
 320       std::vector<Node> assumption = {isZero};
 321       pf = d_pnm->mkScope(botPf, assumption, false);
 322       Debug("arith::cong::notzero") << "  new proof ";
 323       pf->printDebug(Debug("arith::cong::notzero"));
 324       Debug("arith::cong::notzero") << std::endl;
 325     }
 326     Assert(pf->getResult() == disEq);
 327   }
 328   d_keepAlive.push_back(reason);
 329   assertionToEqualityEngine(false, s, reason, pf);
 330 }
 331
 332
 333 bool ArithCongruenceManager::propagate(TNode x){
 334   Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
 335   if(inConflict()){
 336     return true;
 337   }
 338
 339   Node rewritten = Rewriter::rewrite(x);
 340
 341   //Need to still propagate this!
 342   if(rewritten.getKind() == kind::CONST_BOOLEAN){
 343     pushBack(x);
 344
 345     if(rewritten.getConst<bool>()){
 346       return true;
 347     }else{
 348       ++(d_statistics.d_conflicts);
 349
 350       Node conf = flattenAnd(explainInternal(x));
 351       raiseConflict(conf);
 352       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
 353       return false;
 354     }
 355   }
 356
 357   Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
 358
 359   ConstraintP c = d_constraintDatabase.lookup(rewritten);
 360   if(c == NullConstraint){
 361     //using setup as there may not be a corresponding congruence literal yet
 362     d_setupLiteral(rewritten);
 363     c = d_constraintDatabase.lookup(rewritten);
 364     Assert(c != NullConstraint);
 365   }
 366
 367   Debug("arith::congruenceManager")<< "x is "
 368                                    <<  c->hasProof() << " "
 369                                    << (x == rewritten) << " "
 370                                    << c->canBePropagated() << " "
 371                                    << c->negationHasProof() << std::endl;
 372
 373   if(c->negationHasProof()){
 374     Node expC = explainInternal(x);
 375     ConstraintCP negC = c->getNegation();
 376     Node neg = negC->externalExplainByAssertions();
 377     Node conf = expC.andNode(neg);
 378     Node final = flattenAnd(conf);
 379
 380     ++(d_statistics.d_conflicts);
 381     raiseConflict(final);
 382     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
 383     return false;
 384   }
 385
 386   // Cases for propagation
 387   // C : c has a proof
 388   // S : x == rewritten
 389   // P : c can be propagated
 390   //
 391   // CSP
 392   // 000 : propagate x, and mark C it as being explained
 393   // 001 : propagate x, and propagate c after marking it as being explained
 394   // 01* : propagate x, mark c but do not propagate c
 395   // 10* : propagate x, do not mark c and do not propagate c
 396   // 11* : drop the constraint, do not propagate x or c
 397
 398   if(!c->hasProof() && x != rewritten){
 399     if(c->assertedToTheTheory()){
 400       pushBack(x, rewritten, c->getWitness());
 401     }else{
 402       pushBack(x, rewritten);
 403     }
 404
 405     c->setEqualityEngineProof();
 406     if(c->canBePropagated() && !c->assertedToTheTheory()){
 407
 408       ++(d_statistics.d_propagateConstraints);
 409       c->propagate();
 410     }
 411   }else if(!c->hasProof() && x == rewritten){
 412     if(c->assertedToTheTheory()){
 413       pushBack(x, c->getWitness());
 414     }else{
 415       pushBack(x);
 416     }
 417     c->setEqualityEngineProof();
 418   }else if(c->hasProof() && x != rewritten){
 419     if(c->assertedToTheTheory()){
 420       pushBack(x);
 421     }else{
 422       pushBack(x);
 423     }
 424   }else{
 425     Assert(c->hasProof() && x == rewritten);
 426   }
 427   return true;
 428 }
 429
 430 void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
 431   if (literal.getKind() != kind::NOT) {
 432     d_ee->explainEquality(literal[0], literal[1], true, assumptions);
 433   } else {
 434     d_ee->explainEquality(literal[0][0], literal[0][1], false, assumptions);
 435   }
 436 }
 437
 438 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
 439   std::set<TNode>::const_iterator it = s.begin();
 440   std::set<TNode>::const_iterator it_end = s.end();
 441   for(; it != it_end; ++it) {
 442     nb << *it;
 443   }
 444 }
 445
 446 Node ArithCongruenceManager::explainInternal(TNode internal){
 447   std::vector<TNode> assumptions;
 448   explain(internal, assumptions);
 449
 450   std::set<TNode> assumptionSet;
 451   assumptionSet.insert(assumptions.begin(), assumptions.end());
 452
 453   if (assumptionSet.size() == 1) {
 454     // All the same, or just one
 455     return assumptions[0];
 456   }else{
 457     NodeBuilder<> conjunction(kind::AND);
 458     enqueueIntoNB(assumptionSet, conjunction);
 459     return conjunction;
 460   }
 461 }
 462
 463 TrustNode ArithCongruenceManager::explain(TNode external)
 464 {
 465   Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
 466   Node internal = externalToInternal(external);
 467   Trace("arith-ee") << "...internal = " << internal << std::endl;
 468   Node exp = explainInternal(internal);
 469   if (isProofEnabled())
 470   {
 471     Node impl = NodeManager::currentNM()->mkNode(Kind::IMPLIES, exp, external);
 472     // For now, we just trust
 473     auto pfOfImpl = d_pnm->mkNode(PfRule::INT_TRUST, {}, {impl});
 474     return d_pfGenExplain->mkTrustNode(impl, pfOfImpl);
 475   }
 476   return TrustNode::mkTrustPropExp(external, exp, nullptr);
 477 }
 478
 479 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
 480   Node internal = externalToInternal(external);
 481
 482   std::vector<TNode> assumptions;
 483   explain(internal, assumptions);
 484   std::set<TNode> assumptionSet;
 485   assumptionSet.insert(assumptions.begin(), assumptions.end());
 486
 487   enqueueIntoNB(assumptionSet, out);
 488 }
 489
 490 void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
 491   Assert(!isWatchedVariable(s));
 492
 493   Debug("arith::congruenceManager")
 494     << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
 495
 496
 497   ++(d_statistics.d_watchedVariables);
 498
 499   d_watchedVariables.add(s);
 500
 501   Node eq = x.eqNode(y);
 502   d_watchedEqualities.set(s, eq);
 503 }
 504
 505 void ArithCongruenceManager::assertLitToEqualityEngine(
 506     Node lit, TNode reason, std::shared_ptr<ProofNode> pf)
 507 {
 508   bool isEquality = lit.getKind() != Kind::NOT;
 509   Node eq = isEquality ? lit : lit[0];
 510   Assert(eq.getKind() == Kind::EQUAL);
 511
 512   Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason
 513                     << std::endl;
 514   if (isProofEnabled())
 515   {
 516     if (CDProof::isSame(lit, reason))
 517     {
 518       Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl;
 519       // The equality engine doesn't ref-count for us...
 520       d_keepAlive.push_back(eq);
 521       d_keepAlive.push_back(reason);
 522       d_ee->assertEquality(eq, isEquality, reason);
 523     }
 524     else if (hasProofFor(lit))
 525     {
 526       Trace("arith-pfee") << "Skipping b/c already done" << std::endl;
 527     }
 528     else
 529     {
 530       setProofFor(lit, pf);
 531       Trace("arith-pfee") << "Actually asserting" << std::endl;
 532       if (Debug.isOn("arith-pfee"))
 533       {
 534         Trace("arith-pfee") << "Proof: ";
 535         pf->printDebug(Trace("arith-pfee"));
 536         Trace("arith-pfee") << std::endl;
 537       }
 538       // The proof equality engine *does* ref-count for us...
 539       d_pfee->assertFact(lit, reason, d_pfGenEe.get());
 540     }
 541   }
 542   else
 543   {
 544     // The equality engine doesn't ref-count for us...
 545     d_keepAlive.push_back(eq);
 546     d_keepAlive.push_back(reason);
 547     d_ee->assertEquality(eq, isEquality, reason);
 548   }
 549 }
 550
 551 void ArithCongruenceManager::assertionToEqualityEngine(
 552     bool isEquality, ArithVar s, TNode reason, std::shared_ptr<ProofNode> pf)
 553 {
 554   Assert(isWatchedVariable(s));
 555
 556   TNode eq = d_watchedEqualities[s];
 557   Assert(eq.getKind() == kind::EQUAL);
 558
 559   Node lit = isEquality ? Node(eq) : eq.notNode();
 560   Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality
 561                     << ", reason " << reason << std::endl;
 562   assertLitToEqualityEngine(lit, reason, pf);
 563 }
 564
 565 bool ArithCongruenceManager::hasProofFor(TNode f) const
 566 {
 567   Assert(isProofEnabled());
 568   if (d_pfGenEe->hasProofFor(f))
 569   {
 570     return true;
 571   }
 572   Node sym = CDProof::getSymmFact(f);
 573   Assert(!sym.isNull());
 574   return d_pfGenEe->hasProofFor(sym);
 575 }
 576
 577 void ArithCongruenceManager::setProofFor(TNode f,
 578                                          std::shared_ptr<ProofNode> pf) const
 579 {
 580   Assert(!hasProofFor(f));
 581   d_pfGenEe->mkTrustNode(f, pf);
 582   Node symF = CDProof::getSymmFact(f);
 583   auto symPf = d_pnm->mkNode(PfRule::SYMM, {pf}, {});
 584   d_pfGenEe->mkTrustNode(symF, symPf);
 585 }
 586
 587 void ArithCongruenceManager::equalsConstant(ConstraintCP c){
 588   Assert(c->isEquality());
 589
 590   ++(d_statistics.d_equalsConstantCalls);
 591   Debug("equalsConstant") << "equals constant " << c << std::endl;
 592
 593   ArithVar x = c->getVariable();
 594   Node xAsNode = d_avariables.asNode(x);
 595   Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
 596
 597   // No guarentee this is in normal form!
 598   // Note though, that it happens to be in proof normal form!
 599   Node eq = xAsNode.eqNode(asRational);
 600   d_keepAlive.push_back(eq);
 601
 602   NodeBuilder<> nb(Kind::AND);
 603   auto pf = c->externalExplainByAssertions(nb);
 604   Node reason = safeConstructNary(nb);
 605   d_keepAlive.push_back(reason);
 606
 607   Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
 608   assertLitToEqualityEngine(eq, reason, pf);
 609 }
 610
 611 void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
 612   Assert(lb->isLowerBound());
 613   Assert(ub->isUpperBound());
 614   Assert(lb->getVariable() == ub->getVariable());
 615
 616   ++(d_statistics.d_equalsConstantCalls);
 617   Debug("equalsConstant") << "equals constant " << lb << std::endl
 618                           << ub << std::endl;
 619
 620   ArithVar x = lb->getVariable();
 621   NodeBuilder<> nb(Kind::AND);
 622   auto pfLb = lb->externalExplainByAssertions(nb);
 623   auto pfUb = ub->externalExplainByAssertions(nb);
 624   Node reason = safeConstructNary(nb);
 625
 626   Node xAsNode = d_avariables.asNode(x);
 627   Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
 628
 629   // No guarentee this is in normal form!
 630   // Note though, that it happens to be in proof normal form!
 631   Node eq = xAsNode.eqNode(asRational);
 632   std::shared_ptr<ProofNode> pf;
 633   if (isProofEnabled())
 634   {
 635     pf = d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq});
 636   }
 637   d_keepAlive.push_back(eq);
 638   d_keepAlive.push_back(reason);
 639
 640   Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
 641
 642   assertLitToEqualityEngine(eq, reason, pf);
 643 }
 644
 645 bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
 646
 647 std::vector<Node> andComponents(TNode an)
 648 {
 649   auto nm = NodeManager::currentNM();
 650   if (an == nm->mkConst(true))
 651   {
 652     return {};
 653   }
 654   else if (an.getKind() != Kind::AND)
 655   {
 656     return {an};
 657   }
 658   std::vector<Node> a{};
 659   a.reserve(an.getNumChildren());
 660   a.insert(a.end(), an.begin(), an.end());
 661   return a;
 662 }
 663
 664 }/* CVC4::theory::arith namespace */
 665 }/* CVC4::theory namespace */
 666 }/* CVC4 namespace */