src/theory/arith/congruence_manager.cpp

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