pow2 -- final changes (#6800)

[cvc5.git] / src / theory / arith / congruence_manager.cpp

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index ff0b46338cafe73fae5a58c18ead7fc8edef5b6e..9e7202f1dfdb238ba7277d36b5a9d25dee7783f9 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -19,8 +19,9 @@
 #include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
+#include "options/arith_options.h"
+#include "proof/proof_node.h"
+#include "proof/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
@@ -29,7 +30,6 @@
 #include "theory/rewriter.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
-#include "options/arith_options.h"
 
 namespace cvc5 {
 namespace theory {
@@ -85,37 +85,28 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
   d_ee->addFunctionKind(kind::EXPONENTIAL);
   d_ee->addFunctionKind(kind::SINE);
   d_ee->addFunctionKind(kind::IAND);
+  d_ee->addFunctionKind(kind::POW2);
   // have proof equality engine only if proofs are enabled
   Assert(isProofEnabled() == (pfee != nullptr));
   d_pfee = pfee;
 }
 
-ArithCongruenceManager::Statistics::Statistics():
-  d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
-  d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
-  d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
-  d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
-  d_propagations("theory::arith::congruence::propagations", 0),
-  d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
-  d_conflicts("theory::arith::congruence::conflicts", 0)
+ArithCongruenceManager::Statistics::Statistics()
+    : d_watchedVariables(smtStatisticsRegistry().registerInt(
+        "theory::arith::congruence::watchedVariables")),
+      d_watchedVariableIsZero(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::watchedVariableIsZero")),
+      d_watchedVariableIsNotZero(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::watchedVariableIsNotZero")),
+      d_equalsConstantCalls(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::equalsConstantCalls")),
+      d_propagations(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::propagations")),
+      d_propagateConstraints(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::propagateConstraints")),
+      d_conflicts(smtStatisticsRegistry().registerInt(
+          "theory::arith::congruence::conflicts"))
 {
-  smtStatisticsRegistry()->registerStat(&d_watchedVariables);
-  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
-  smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
-  smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
-  smtStatisticsRegistry()->registerStat(&d_propagations);
-  smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
-  smtStatisticsRegistry()->registerStat(&d_conflicts);
-}
-
-ArithCongruenceManager::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
-  smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
-  smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
-  smtStatisticsRegistry()->unregisterStat(&d_propagations);
-  smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
-  smtStatisticsRegistry()->unregisterStat(&d_conflicts);
 }
 
 ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
@@ -321,7 +312,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
       const auto isZeroPf = d_pnm->mkAssume(isZero);
       const auto nm = NodeManager::currentNM();
       const auto sumPf = d_pnm->mkNode(
-          PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+          PfRule::MACRO_ARITH_SCALE_SUM_UB,
           {isZeroPf, pf},
           // Trick for getting correct, opposing signs.
           {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))});