src/theory/arith/congruence_manager.cpp

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