Get rid of some static objects in arithmetic theory (#8146)

This PR tackles cvc5/cvc5-projects#17 by removing static variables or making them constexpr.
Most static variables are either compile-time constants (we make them static constexpr) or used to count how often a function is called for debug output (we remove these).

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 5ec46b00c30285fe28af14fa66bb07de0c04ccbf..26f5ed1b40583b9ed80e9bef65073b8c05b91801 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -168,8 +168,6 @@ ApproximateStatistics::ApproximateStatistics()
 {
 }
 
-Integer ApproximateSimplex::s_defaultMaxDenom(1<<26);
-
 ApproximateSimplex::ApproximateSimplex(const ArithVariables& v, TreeLog& l,
                                        ApproximateStatistics& s)
   : d_vars(v)
@@ -195,9 +193,6 @@ void ApproximateSimplex::setBranchOnVariableLimit(int bl){
   d_branchLimit = bl;
 }
 
-const double ApproximateSimplex::SMALL_FIXED_DELTA = .000000001;
-const double ApproximateSimplex::TOLERENCE = 1 + .000000001;
-
 bool ApproximateSimplex::roughlyEqual(double a, double b){
   if (a == 0){
     return -SMALL_FIXED_DELTA <= b && b <= SMALL_FIXED_DELTA;
@@ -320,7 +315,7 @@ std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d,
 
 std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d)
 {
-  return estimateWithCFE(d, s_defaultMaxDenom);
+  return estimateWithCFE(d, Integer(s_defaultMaxDenom));
 }
 
 class ApproxNoOp : public ApproximateSimplex {
@@ -400,8 +395,6 @@ private:
   //DenseMap<ArithVar> d_rowToArithVar;
   DenseMap<ArithVar> d_colToArithVar;
 
-  int d_instanceID;
-
   bool d_solvedRelaxation;
   bool d_solvedMIP;
 
@@ -579,12 +572,9 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var,
       d_solvedRelaxation(false),
       d_solvedMIP(false)
 {
-  static int instance = 0;
-  ++instance;
-  d_instanceID = instance;
 
   d_denomGuesses.push_back(Integer(1<<22));
-  d_denomGuesses.push_back(ApproximateSimplex::s_defaultMaxDenom);
+  d_denomGuesses.push_back(Integer(ApproximateSimplex::s_defaultMaxDenom));
   d_denomGuesses.push_back(Integer(1ul<<29));
   d_denomGuesses.push_back(Integer(1ul<<31));
 
@@ -2142,31 +2132,30 @@ bool ApproxGLPK::attemptMir(int nid, const MirInfo& mir){
 bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound& tmp){
   if(ri <= 0) { return true; }
 
-  static int instance = 0;
-  ++instance;
-  Debug("glpk::loadVB") << "loadVB() " << instance << endl;
+  Debug("glpk::loadVB") << "loadVB()" << endl;
 
   ArithVar rowVar = _getArithVar(nid, M, ri);
   ArithVar contVar = _getArithVar(nid, M, j);
   if(rowVar == ARITHVAR_SENTINEL){
-    Debug("glpk::loadVB") << "loadVB() " << instance
+    Debug("glpk::loadVB") << "loadVB()"
                           << " rowVar is ARITHVAR_SENTINEL " << rowVar << endl;
     return true;
   }
   if(contVar == ARITHVAR_SENTINEL){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " contVar is ARITHVAR_SENTINEL " << contVar << endl;        
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " contVar is ARITHVAR_SENTINEL " << contVar
+                          << endl;
     return true; }
 
   if(!d_vars.isAuxiliary(rowVar)){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " rowVar is not auxilliary " << rowVar << endl;    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " rowVar is not auxilliary " << rowVar << endl;
     return true;
   }
   // is integer is correct here
   if(d_vars.isInteger(contVar)){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " contVar is integer " << contVar << endl;    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " contVar is integer " << contVar << endl;
     return true;
   }
 
@@ -2174,33 +2163,38 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
   ConstraintP ub = d_vars.getUpperBoundConstraint(rowVar);
 
   if(lb != NullConstraint && ub != NullConstraint){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " lb and ub are both NULL " << lb << " " << ub << endl;    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " lb and ub are both NULL " << lb << " " << ub
+                          << endl;
     return true;
   }
 
   ConstraintP rcon = lb == NullConstraint ? ub : lb;
   if(rcon == NullConstraint) {
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " rcon is NULL " << rcon << endl;    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " rcon is NULL " << rcon << endl;
     return true;
   }
 
   if(!rcon->getValue().isZero()){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " rcon value is not 0 " << rcon->getValue() << endl;
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " rcon value is not 0 " << rcon->getValue()
+                          << endl;
     return true;
   }
 
   if(!d_vars.hasNode(rowVar)){
-    Debug("glpk::loadVB") << "loadVB() " << instance
+    Debug("glpk::loadVB") << "loadVB()"
                           << " does not have node " << rowVar << endl;
     return true;
   }
 
   Polynomial p = Polynomial::parsePolynomial(d_vars.asNode(rowVar));
-  if(p.size() != 2) {  
-    Debug("glpk::loadVB") << "loadVB() " << instance << " polynomial is not binary: " << p.getNode() << endl;
+  if (p.size() != 2)
+  {
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " polynomial is not binary: " << p.getNode()
+                          << endl;
     return true;
   }
 
@@ -2211,13 +2205,15 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
   Node nx2 = second.getVarList().getNode();
 
   if(!d_vars.hasArithVar(nx1)) {
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " does not have a variable for nx1: " << nx1 << endl;
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " does not have a variable for nx1: " << nx1
+                          << endl;
     return true;
   }
   if(!d_vars.hasArithVar(nx2)) {
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " does not have a variable for nx2 " << nx2 << endl;
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " does not have a variable for nx2 " << nx2
+                          << endl;
     return true;
   }
   ArithVar x1 = d_vars.asArithVar(nx1), x2 = d_vars.asArithVar(nx2);
@@ -2246,8 +2242,9 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
     << " c2 " << ic << endl;
 
   if(!d_vars.isIntegerInput(iv)){
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " iv is not an integer input variable " << iv << endl;    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " iv is not an integer input variable " << iv
+                          << endl;
     return true;
   }
   // cc * cv + ic * iv <= 0 or
@@ -2272,16 +2269,18 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
   Debug("glpk::loadVB") << d << " " << cc.sgn() << endl;
   bool nowUb = cc.sgn() < 0;
   if(wantUb != nowUb) {
-    Debug("glpk::loadVB") << "loadVB() " << instance
-                          << " wantUb is not nowUb " << wantUb << " " << nowUb << endl;    
-    
+    Debug("glpk::loadVB") << "loadVB()"
+                          << " wantUb is not nowUb " << wantUb << " " << nowUb
+                          << endl;
+
     return true;
   }
 
   Kind rel = wantUb ? kind::LEQ : kind::GEQ;
 
   tmp = VirtualBound(contVar, rel, d, iv, rcon);
-    Debug("glpk::loadVB") << "loadVB() " << instance << " was successful" << endl;    
+  Debug("glpk::loadVB") << "loadVB()"
+                        << " was successful" << endl;
   return false;
 }
 

diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index c0d6990a4a96a63fd681a679c76b09de525e8d03..f2a35f8236c5cb0f45a9c9644e0e3190d70d0804 100644 (file)
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -116,8 +116,8 @@ class ApproximateSimplex{
 
   /** UTILITIES FOR DEALING WITH ESTIMATES */
 
-  static const double SMALL_FIXED_DELTA;
-  static const double TOLERENCE;
+  static constexpr double SMALL_FIXED_DELTA = .000000001;
+  static constexpr double TOLERENCE = 1 + .000000001;
 
   /** Returns true if two doubles are roughly equal based on TOLERENCE and SMALL_FIXED_DELTA.*/
   static bool roughlyEqual(double a, double b);
@@ -160,7 +160,7 @@ class ApproximateSimplex{
   int d_maxDepth;
 
   /* Default denominator for diophatine approximation, 2^{26} .*/
-  static Integer s_defaultMaxDenom;
+  static constexpr uint64_t s_defaultMaxDenom = (1 << 26);
 };/* class ApproximateSimplex */
 
 }  // namespace arith

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index fbd6b33f6c401ae236cbc3201af2539776ac8d6a..be1c103fa116eba94682e0bb142372b32852e75d 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -82,15 +82,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
   d_errorSet.reduceToSignals();
   d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
 
-  static int instance = 0;
-  ++instance;
-
   if(processSignals()){
-    Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl;
+    Debug("arith::findModel") << "attemptSolution() early conflict" << endl;
     d_conflictVariables.purge();
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl;
+    Debug("arith::findModel") << "attemptSolution() fixed itself" << endl;
     return Result::SAT;
   }
 

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index e335b2e55245ba9b41f012e8fe38ef614ff1c9fc..82ee832b7c0abaf629f53a98faf331b3d83e9555 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -158,15 +158,16 @@ typedef context::CDList<ConstraintCP> CDConstraintList;
 typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;
 
 typedef size_t ConstraintRuleID;
-static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
+static constexpr ConstraintRuleID ConstraintRuleIdSentinel =
+    std::numeric_limits<ConstraintRuleID>::max();
 
 typedef size_t AntecedentId;
-static const AntecedentId AntecedentIdSentinel = std::numeric_limits<AntecedentId>::max();
-
+static constexpr AntecedentId AntecedentIdSentinel =
+    std::numeric_limits<AntecedentId>::max();
 
 typedef size_t AssertionOrder;
-static const AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
-
+static constexpr AssertionOrder AssertionOrderSentinel =
+    std::numeric_limits<AssertionOrder>::max();
 
 /**
  * A ValueCollection binds together convex constraints that have the same

diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index 5f0e124fb025156de45a2810f963cdf2098ed42a..e9a64ce196da28ff4c0a31fa8993c222e35ab675 100644 (file)
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -34,7 +34,7 @@ class Constraint;
 typedef Constraint* ConstraintP;
 typedef const Constraint* ConstraintCP;
 
-static const ConstraintP NullConstraint = NULL;
+static constexpr ConstraintP NullConstraint = nullptr;
 
 class ConstraintDatabase;
 
@@ -43,8 +43,8 @@ typedef std::vector<ConstraintCP> ConstraintCPVec;
 typedef std::vector<Rational> RationalVector;
 typedef RationalVector* RationalVectorP;
 typedef const RationalVector* RationalVectorCP;
-static const RationalVectorCP RationalVectorCPSentinel = NULL;
-static const RationalVectorP RationalVectorPSentinel = NULL;
+static constexpr RationalVectorCP RationalVectorCPSentinel = nullptr;
+static constexpr RationalVectorP RationalVectorPSentinel = nullptr;
 
 }  // namespace arith
 }  // namespace theory

diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 054fceb469a947af5a36740ac6701c436943fa65..2e99f04e45980b5f95ceb85fa944b51972ee6452 100644 (file)
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -157,7 +157,7 @@ class DioSolver : protected EnvObj
    * the maximum input constraints length than 2**MAX_GROWTH_RATE.
    */
   context::CDO<uint32_t> d_maxInputCoefficientLength;
-  static const uint32_t MAX_GROWTH_RATE = 3;
+  static constexpr uint32_t MAX_GROWTH_RATE = 3;
 
   /** Returns true if the element on the trail should be dropped.*/
   bool anyCoefficientExceedsMaximum(TrailIndex j) const;

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 147d0a1ffdfa995f7283a2060557acbf54c73dbc..84cd0fe5a07d46fc312a09a7d2460a255e9e7b0c 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -61,12 +61,10 @@ DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
 Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   Assert(d_conflictVariables.empty());
 
-  static thread_local unsigned int instance = 0;
-  instance = instance + 1;
   d_pivots = 0;
 
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
-    Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl;
+    Debug("arith::findModel") << "dualFindModel() trivial" << endl;
     return Result::SAT;
   }
 
@@ -77,15 +75,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   if(processSignals()){
     d_conflictVariables.purge();
 
-    Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl;
+    Debug("arith::findModel") << "dualFindModel() early conflict" << endl;
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl;
+    Debug("arith::findModel") << "dualFindModel() fixed itself" << endl;
     Assert(!d_errorSet.moreSignals());
     return Result::SAT;
   }
 
-  Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl;
+  Debug("arith::findModel") << "dualFindModel() start non-trivial" << endl;
 
   Result::Sat result = Result::SAT_UNKNOWN;
 
@@ -136,7 +134,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
   // ensure that the conflict variable is still in the queue.
   d_conflictVariables.purge();
 
-  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
+  Debug("arith::findModel") << "end findModel() " << result << endl;
 
   return result;
 }

diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index 19d6149f52f73cf4f311bed598ae676d4ff44e92..c7666fff3a2e2f45b79694a0bc304be8d1568c67 100644 (file)
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -446,9 +446,7 @@ DeltaRational ErrorSet::computeDiff(ArithVar v) const{
 }
 
 void ErrorSet::debugPrint(std::ostream& out) const {
-  static int instance = 0;
-  ++instance;
-  out << "error set debugprint " << instance << endl;
+  out << "error set debugprint" << endl;
   for(error_iterator i = errorBegin(), i_end = errorEnd();
       i != i_end; ++i){
     ArithVar e = *i;

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 5b9f37f93b64657ae9742b9e4e014c53bc1f86c1..d3f7e071f573a22ecfefee30e52d8a7181a39b63 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -72,11 +72,9 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static thread_local unsigned int instance = 0;
-  instance = instance + 1;
 
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
-    Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl;
+    Debug("arith::findModel") << "fcFindModel() trivial" << endl;
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
@@ -89,16 +87,16 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
-    Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
+    Debug("arith::findModel") << "fcFindModel() early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
+    Debug("arith::findModel") << "fcFindModel() fixed itself" << endl;
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
 
-  Debug("arith::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
+  Debug("arith::findModel") << "fcFindModel() start non-trivial" << endl;
 
   exactResult |= d_varOrderPivotLimit < 0;
 
@@ -133,7 +131,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   // ensure that the conflict variable is still in the queue.
   d_conflictVariables.purge();
 
-  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
+  Debug("arith::findModel") << "end findModel() " << result << endl;
 
   Assert(d_conflictVariables.empty());
   return result;
@@ -251,15 +249,12 @@ WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){
 UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) {
   UpdateInfo selected;
 
-  static int instance = 0 ;
-  ++instance;
-
   Debug("arith::selectPrimalUpdate")
-    << "selectPrimalUpdate " << instance << endl
-    << basic << " " << d_tableau.basicRowLength(basic)
-    << " " << d_linEq.debugBasicAtBoundCount(basic) << endl;
+      << "selectPrimalUpdate" << endl
+      << basic << " " << d_tableau.basicRowLength(basic) << " "
+      << d_linEq.debugBasicAtBoundCount(basic) << endl;
 
-  static const int s_maxCandidatesAfterImprove = 3;
+  static constexpr int s_maxCandidatesAfterImprove = 3;
   bool isFocus = basic == d_focusErrorVar;
   Assert(isFocus || d_errorSet.inError(basic));
   int basicDir =  isFocus? 1 : d_errorSet.getSgn(basic);
@@ -629,8 +624,12 @@ WitnessImprovement FCSimplexDecisionProcedure::selectFocusImproving() {
   return w;
 }
 
-bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& out, int instance, uint32_t prevFocusSize, uint32_t prevErrorSize ) const{
-  out << "DLV("<<instance<<") ";
+bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w,
+                                               ostream& out,
+                                               uint32_t prevFocusSize,
+                                               uint32_t prevErrorSize) const
+{
+  out << "DLV() ";
   switch(w){
   case ConflictFound:
     out << "found conflict" << endl;
@@ -660,7 +659,6 @@ bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& ou
 }
 
 Result::Sat FCSimplexDecisionProcedure::dualLike(){
-  static int instance = 0;
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer);
 
@@ -678,8 +676,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
 
 
   while(d_pivotBudget != 0  && d_errorSize > 0 && d_conflictVariables.empty()){
-    ++instance;
-    Debug("dualLike") << "dualLike " << instance << endl;
+    Debug("dualLike") << "dualLike " << endl;
 
     Assert(d_errorSet.noSignals());
 
@@ -723,7 +720,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
       // - focus went down
       Assert(d_focusSize > 1);
       ArithVar e = d_errorSet.topFocusVariable();
-      static const unsigned s_sumMetricThreshold = 1;
+      static constexpr unsigned s_sumMetricThreshold = 1;
       if(d_errorSet.sumMetric(e) <= s_sumMetricThreshold){
         Debug("dualLike") << "dualLikeImproveError " << e << endl;
         w = dualLikeImproveError(e);
@@ -736,8 +733,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
     Assert(d_focusSize == d_errorSet.focusSize());
     Assert(d_errorSize == d_errorSet.errorSize());
 
-    Assert(debugDualLike(
-        w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
+    Assert(debugDualLike(w, Debug("dualLike"), prevFocusSize, prevErrorSize));
     Debug("dualLike") << "Focus size " << d_focusSize << " (was " << prevFocusSize << ")" << endl;
     Debug("dualLike") << "Error size " << d_errorSize << " (was " << prevErrorSize << ")" << endl;
   }

diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index ddd868acac3e53be4e1d523da26a210c75c4d989..f3dbccc6eab0925290f0e58c253679b079691cec 100644 (file)
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -86,19 +86,24 @@ public:
  Result::Sat dualLike();
 
 private:
-  static const uint32_t PENALTY = 4;
-  DenseMultiset d_scores;
-  void decreasePenalties(){ d_scores.removeOneOfEverything(); }
-  uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
-  void setPenalty(ArithVar x, WitnessImprovement w){
-    if(improvement(w)){
-      if(d_scores.count(x) > 0){
-        d_scores.removeAll(x);
-      }
-    }else{
-      d_scores.setCount(x, PENALTY);
-    }
-  }
+ static constexpr uint32_t PENALTY = 4;
+ DenseMultiset d_scores;
+ void decreasePenalties() { d_scores.removeOneOfEverything(); }
+ uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
+ void setPenalty(ArithVar x, WitnessImprovement w)
+ {
+   if (improvement(w))
+   {
+     if (d_scores.count(x) > 0)
+     {
+       d_scores.removeAll(x);
+     }
+   }
+   else
+   {
+     d_scores.setCount(x, PENALTY);
+   }
+ }
 
   /** The size of the focus set. */
   uint32_t d_focusSize;
@@ -128,21 +133,15 @@ private:
   const Rational& focusCoefficient(ArithVar nb) const;
 
   int32_t d_pivotBudget;
-  // enum PivotImprovement {
-  //   ErrorDropped,
-  //   NonDegenerate,
-  //   HeuristicDegenerate,
-  //   BlandsDegenerate
-  // };
 
   WitnessImprovement d_prevWitnessImprovement;
   uint32_t d_witnessImprovementInARow;
 
   uint32_t degeneratePivotsInARow() const;
 
-  static const uint32_t s_focusThreshold = 6;
-  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
-  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
+  static constexpr uint32_t s_focusThreshold = 6;
+  static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
+  static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
 
   DenseMap<uint32_t> d_leavingCountSinceImprovement;
   void increaseLeavingCount(ArithVar x){
@@ -163,15 +162,12 @@ private:
   }
 
   bool debugDualLike(WitnessImprovement w, std::ostream& out,
-                     int instance,
                      uint32_t prevFocusSize, uint32_t prevErrorSize) const;
 
   void debugPrintSignal(ArithVar updated) const;
 
   ArithVarVec d_sgnDisagreements;
 
-  //static PivotImprovement pivotImprovement(const UpdateInfo& selected, bool useBlands = false);
-
   void logPivot(WitnessImprovement w);
 
   void updateAndSignal(const UpdateInfo& selected, WitnessImprovement w);

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index a0cc5499de7b53dfa9af3779e0f14d112cf8182a..bc4f11e9d04ea1f0a81e8ad850e094dfa870fdcb 100644 (file)
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -261,11 +261,8 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
 
-  static int instance = 0;
-
   if(Debug.isOn("arith::tracking::pre")){
-    ++instance;
-    Debug("arith::tracking")  << "pre update #" << instance << endl;
+    Debug("arith::tracking") << "pre update" << endl;
     debugCheckTracking();
   }
 
@@ -283,7 +280,7 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt
   updateTracked(x_j, x_j_value);
 
   if(Debug.isOn("arith::tracking::mid")){
-    Debug("arith::tracking")  << "postupdate prepivot #" << instance << endl;
+    Debug("arith::tracking") << "postupdate prepivot" << endl;
     debugCheckTracking();
   }
 
@@ -293,7 +290,7 @@ void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const Delt
   d_tableau.pivot(x_i, x_j, d_trackCallback);
 
   if(Debug.isOn("arith::tracking::post")){
-    Debug("arith::tracking")  << "postpivot #" << instance << endl;
+    Debug("arith::tracking") << "postpivot" << endl;
     debugCheckTracking();
   }
 
@@ -1118,9 +1115,7 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational&
 
   int focusCoeffSgn = focusCoeff.sgn();
 
-  static int instance = 0;
-  ++instance;
-  Debug("speculativeUpdate") << "speculativeUpdate " << instance << endl;
+  Debug("speculativeUpdate") << "speculativeUpdate" << endl;
   Debug("speculativeUpdate") << "nb " << nb << endl;
   Debug("speculativeUpdate") << "focusCoeff " << focusCoeff << endl;
 

diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp
index 032565d3d8c975dd121954d1e95e01e1aa2e8c80..91d775d16dbdce22cdcb6f1a22d33c24b256b5d3 100644 (file)
--- a/src/theory/arith/nl/cad/lazard_evaluation.cpp
+++ b/src/theory/arith/nl/cad/lazard_evaluation.cpp
@@ -106,7 +106,15 @@ std::ostream& operator<<(std::ostream& os, const LazardEvaluationState& state);
 struct LazardEvaluationState
 {
   CoCoA::GlobalManager d_gm;
-  static std::unique_ptr<LazardEvaluationStats> d_stats;
+
+  /**
+   * Statistics about the lazard evaluation.
+   * Although this class is short-lived, there is no need to make the statistics
+   * static or store them persistently: this is handled by the statistics
+   * registry, which recovers statistics from their name.
+   * This member is mutable to allow collecting statistics from const methods.
+   */
+  mutable LazardEvaluationStats d_stats;
 
   /**
    * Maps libpoly variables to indets in J0. Used when constructing the input
@@ -185,14 +193,6 @@ struct LazardEvaluationState
    */
   std::vector<std::optional<CoCoA::RingElem>> d_direct;
 
-  LazardEvaluationState()
-  {
-    if (!d_stats)
-    {
-      d_stats = std::make_unique<LazardEvaluationStats>();
-    }
-  }
-
   /**
    * Converts a libpoly integer to a CoCoA::BigInt.
    */
@@ -595,7 +595,7 @@ struct LazardEvaluationState
    */
   std::vector<poly::Polynomial> reduce(const poly::Polynomial& qpoly) const
   {
-    d_stats->d_evaluations++;
+    d_stats.d_evaluations++;
     std::vector<poly::Polynomial> res;
     Trace("cad::lazard") << "Reducing " << qpoly << std::endl;
     auto input = convertQ(qpoly);
@@ -621,7 +621,7 @@ struct LazardEvaluationState
           while (CoCoA::IsZero(hom(q)))
           {
             q = q / (var - indets[0]);
-            d_stats->d_reductions++;
+            d_stats.d_reductions++;
           }
           // substitute x_i -> a_i
           q = hom(q);
@@ -634,7 +634,7 @@ struct LazardEvaluationState
           while (CoCoA::IsDivisible(q, tmp))
           {
             q /= tmp;
-            d_stats->d_reductions++;
+            d_stats.d_reductions++;
           }
         }
         q = d_qhom[i](q);
@@ -682,7 +682,6 @@ std::ostream& operator<<(std::ostream& os, const LazardEvaluationState& state)
   os << "Done" << std::endl;
   return os;
 }
-std::unique_ptr<LazardEvaluationStats> LazardEvaluationState::d_stats;
 
 LazardEvaluation::LazardEvaluation()
     : d_state(std::make_unique<LazardEvaluationState>())
@@ -747,7 +746,7 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val)
     {
       d_state->addKRational(var,
                             CoCoA::RingElem(d_state->d_K.back(), *rational));
-      d_state->d_stats->d_directAssignments++;
+      d_state->d_stats.d_directAssignments++;
       return;
     }
     Trace("cad::lazard") << "Got mipo " << polymipo << std::endl;
@@ -768,13 +767,13 @@ void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val)
           Trace("cad::lazard") << "Using linear factor " << f << " -> " << var
                                << " = " << rat << std::endl;
           d_state->addKRational(var, rat);
-          d_state->d_stats->d_directAssignments++;
+          d_state->d_stats.d_directAssignments++;
         }
         else
         {
           Trace("cad::lazard") << "Using nonlinear factor " << f << std::endl;
           d_state->addK(var, f);
-          d_state->d_stats->d_ranAssignments++;
+          d_state->d_stats.d_ranAssignments++;
         }
         used_factor = true;
         break;

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 5a834ad424dfdfa2c6bb5a2664a07783d69d3bf9..e8afb64139751d9c7d637e325dd7310bdff91de3 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -78,11 +78,9 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   Assert(d_sgnDisagreements.empty());
 
   d_pivots = 0;
-  static thread_local unsigned int instance = 0;
-  instance = instance + 1;
 
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
-    Debug("soi::findModel") << "soiFindModel("<< instance <<") trivial" << endl;
+    Debug("soi::findModel") << "soiFindModel() trivial" << endl;
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
@@ -95,17 +93,17 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
-    Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
+    Debug("soi::findModel") << "fcFindModel() early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    Debug("soi::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
+    Debug("soi::findModel") << "fcFindModel() fixed itself" << endl;
     Assert(!d_errorSet.moreSignals());
     Assert(d_conflictVariables.empty());
     return Result::SAT;
   }
 
-  Debug("soi::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
+  Debug("soi::findModel") << "fcFindModel() start non-trivial" << endl;
 
   exactResult |= d_varOrderPivotLimit < 0;
 
@@ -140,7 +138,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   // ensure that the conflict variable is still in the queue.
   d_conflictVariables.purge();
 
-  Debug("soi::findModel") << "end findModel() " << instance << " " << result <<  endl;
+  Debug("soi::findModel") << "end findModel() " << result << endl;
 
   Assert(d_conflictVariables.empty());
   return result;
@@ -200,13 +198,10 @@ void SumOfInfeasibilitiesSPD::adjustFocusAndError(const UpdateInfo& up, const AV
 UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) {
   UpdateInfo selected;
 
-  static int instance = 0 ;
-  ++instance;
-
   Debug("soi::selectPrimalUpdate")
-    << "selectPrimalUpdate " << instance << endl
-    << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar)
-    << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
+      << "selectPrimalUpdate " << endl
+      << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar) << " "
+      << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
 
   typedef std::vector<Cand> CandVector;
   CandVector candidates;
@@ -786,11 +781,8 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
 
 
 WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
-  static int instance = 0;
-  instance++;
-  
   Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
-                              << instance << ": |E| = " << d_errorSize << endl;
+                              << ": |E| = " << d_errorSize << endl;
   if(Debug.isOn("arith::SOIConflict")){
     d_errorSet.debugPrint(cout);
   }
@@ -828,8 +820,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   //reportConflict(conf); do not do this. We need a custom explanations!
   d_conflictVariables.add(d_soiVar);
 
-  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
-                              << instance << "end" << endl;
+  Debug("arith::SOIConflict")
+      << "SumOfInfeasibilitiesSPD::SOIConflict() end" << endl;
   return ConflictFound;
 }
 
@@ -865,39 +857,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
   }
 }
 
-bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
-  return true;
-  // out << "DLV("<<instance<<") ";
-  // switch(w){
-  // case ConflictFound:
-  //   out << "found conflict" << endl;
-  //   return !d_conflictVariables.empty();
-  // case ErrorDropped:
-  //   return false;
-  //   // out << "dropped " << prevErrorSize - d_errorSize << endl;
-  //   // return d_errorSize < prevErrorSize;
-  // case FocusImproved:
-  //   out << "focus improved"<< endl;
-  //   return d_errorSize == prevErrorSize;
-  // case FocusShrank:
-  //   Unreachable();
-  //   return false;
-  // case BlandsDegenerate:
-  //   out << "bland degenerate"<< endl;
-  //   return true;
-  // case HeuristicDegenerate:
-  //   out << "heuristic degenerate"<< endl;
-  //   return true;
-  // case AntiProductive:
-  // case Degenerate:
-  //   return false;
-  // }
-  // return false;
-}
-
 Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
-  static int instance = 0;
-  
   TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer);
 
   Assert(d_sgnDisagreements.empty());
@@ -912,8 +872,7 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
 
 
   while(d_pivotBudget != 0  && d_errorSize > 0 && d_conflictVariables.empty()){
-    ++instance;
-    Debug("dualLike") << "dualLike " << instance << endl;
+    Debug("dualLike") << "dualLike" << endl;
 
     Assert(d_errorSet.noSignals());
     // Possible outcomes:
@@ -924,8 +883,6 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
     Debug("dualLike") << "selectFocusImproving -> " << w << endl;
 
     Assert(d_errorSize == d_errorSet.errorSize());
-
-    Assert(debugSOI(w, Debug("dualLike"), instance));
   }
 
 

diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 71b0b36d8d6eaf2744f15ac48deea161c3f36195..96e1de5312c7b7986bf3db8c88501d0281219d38 100644 (file)
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -88,36 +88,16 @@ private:
   // - satisfied error set
   Result::Sat sumOfInfeasibilities();
 
-  // static const uint32_t PENALTY = 4;
-  // DenseMultiset d_scores;
-  // void decreasePenalties(){ d_scores.removeOneOfEverything(); }
-  // uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
-  // void setPenalty(ArithVar x, WitnessImprovement w){
-  //   if(improvement(w)){
-  //     if(d_scores.count(x) > 0){
-  //       d_scores.removeAll(x);
-  //     }
-  //   }else{
-  //     d_scores.setCount(x, PENALTY);
-  //   }
-  // }
-
   int32_t d_pivotBudget;
-  // enum PivotImprovement {
-  //   ErrorDropped,
-  //   NonDegenerate,
-  //   HeuristicDegenerate,
-  //   BlandsDegenerate
-  // };
 
   WitnessImprovement d_prevWitnessImprovement;
   uint32_t d_witnessImprovementInARow;
 
   uint32_t degeneratePivotsInARow() const;
 
-  static const uint32_t s_focusThreshold = 6;
-  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
-  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
+  static constexpr uint32_t s_focusThreshold = 6;
+  static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
+  static constexpr uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
 
   DenseMap<uint32_t> d_leavingCountSinceImprovement;
   void increaseLeavingCount(ArithVar x){
@@ -137,8 +117,6 @@ private:
     }
   }
 
-  bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;
-
   void debugPrintSignal(ArithVar updated) const;
 
   ArithVarVec d_sgnDisagreements;

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c540aa384955f6bda7b151af5bb7704a7aa78db1..ac7acb4be68d8cceaa5bd07d06d05e5ec0ac4378 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1712,7 +1712,6 @@ Node flattenAndSort(Node n){
 void TheoryArithPrivate::outputConflicts(){
   Debug("arith::conflict") << "outputting conflicts" << std::endl;
   Assert(anyConflict());
-  static unsigned int conflicts = 0;
 
   if(!conflictQueueEmpty()){
     Assert(!d_conflicts.empty());
@@ -1737,7 +1736,6 @@ void TheoryArithPrivate::outputConflicts(){
       TrustNode trustedConflict = confConstraint->externalExplainConflict();
       Node conflict = trustedConflict.getNode();
 
-      ++conflicts;
       Debug("arith::conflict")
           << "d_conflicts[" << i << "] " << conflict
           << " has proof: " << hasProof << ", id = " << conf.second << endl;
@@ -1758,9 +1756,7 @@ void TheoryArithPrivate::outputConflicts(){
   }
   if(!d_blackBoxConflict.get().isNull()){
     Node bb = d_blackBoxConflict.get();
-    ++conflicts;
     Debug("arith::conflict") << "black box conflict" << bb
-      //<< "("<<conflicts<<")"
                              << endl;
     if(Debug.isOn("arith::normalize::external")){
       bb = flattenAndSort(bb);
@@ -2702,8 +2698,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   int level = context()->getLevel();
   d_lastContextIntegerAttempted = level;
 
-
-  static const int32_t mipLimit = 200000;
+  static constexpr int32_t mipLimit = 200000;
 
   TreeLog& tl = getTreeLog();
   ApproximateStatistics& stats = getApproxStats();
@@ -2718,7 +2713,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
     if(!d_guessedCoeffs.empty()){
       approx->setOptCoeffs(d_guessedCoeffs);
     }
-    static const int32_t depthForLikelyInfeasible = 10;
+    static constexpr int32_t depthForLikelyInfeasible = 10;
     int maxDepthPass1 = d_likelyIntegerInfeasible
                             ? depthForLikelyInfeasible
                             : options().arith.maxApproxDepth;
@@ -2873,7 +2868,7 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   }
 
   if(d_qflraStatus != Result::UNSAT){
-    static const int64_t pass2Limit = 20;
+    static constexpr int64_t pass2Limit = 20;
     SimplexDecisionProcedure& simplex = selectSimplex(false);
     simplex.setVarOrderPivotLimit(pass2Limit);
     d_qflraStatus = simplex.findModel(false);
@@ -2945,7 +2940,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 
   if(d_qflraStatus == Result::SAT_UNKNOWN && useApprox && safeToCallApprox()){
     // pass2: fancy-final
-    static const int32_t relaxationLimit = 10000;
+    static constexpr int32_t relaxationLimit = 10000;
     Assert(ApproximateSimplex::enabled());
 
     TreeLog& tl = getTreeLog();
@@ -4004,10 +3999,8 @@ void TheoryArithPrivate::presolve(){
 
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
-  static thread_local unsigned callCount = 0;
   if(Debug.isOn("arith::presolve")) {
-    Debug("arith::presolve") << "TheoryArithPrivate::presolve #" << callCount << endl;
-    callCount = callCount + 1;
+    Debug("arith::presolve") << "TheoryArithPrivate::presolve" << endl;
   }
 
   vector<TrustNode> lemmas;
@@ -4520,11 +4513,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   uint32_t rowLength = d_tableau.getRowLength(ridx);
 
   bool success = false;
-  static int instance = 0;
-  ++instance;
 
-  Debug("arith::prop")
-    << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
+  Debug("arith::prop") << "propagateCandidateRow attempt " << rowLength << " "
+                       << hasCount << endl;
 
   if (rowLength >= options().arith.arithPropagateMaxLength
       && Random::getRandom().pickWithProb(

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 7c90352d2b315a65f19ed5ab723cb2523670964d..c10a4ad84dba2242c3ea5cdbc65426c78a33a42d 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -85,7 +85,7 @@ class InferBoundsResult;
 class TheoryArithPrivate : protected EnvObj
 {
  private:
-  static const uint32_t RESET_START = 2;
+  static constexpr uint32_t RESET_START = 2;
 
   TheoryArith& d_containing;
 
@@ -316,8 +316,7 @@ private:
   bool d_tableauSizeHasBeenModified;
   double d_tableauResetDensity;
   uint32_t d_tableauResetPeriod;
-  static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
-
+  static constexpr uint32_t s_TABLEAU_RESET_INCREMENT = 5;
 
   /** This is only used by simplex at the moment. */
   context::CDList<std::pair<ConstraintCP, InferenceId>> d_conflicts;