Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)

This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.

This PR also eliminates some unused code in TheoryArithPrivate.

Followup PRs will start formalizing/eliminating calls to mkDummySkolem.

9 files changed, 26 insertions, 451 deletions

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 218fdf179..64309ad16 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -20,6 +20,7 @@
 #include <ostream>
 
 #include "base/output.h"
+#include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "preprocessing/util/ite_utilities.h"
 #include "theory/arith/arith_utilities.h"
@@ -441,10 +442,11 @@ bool ArithIteUtils::solveBinOr(TNode binor){
         // a: (sel = otherL) or (sel = otherR), otherL-otherR = c
 
         NodeManager* nm = NodeManager::currentNM();
+        SkolemManager* sm = nm->getSkolemManager();
 
         Node cnd = findIteCnd(binor[0], binor[1]);
 
-        Node sk = nm->mkSkolem("deor", nm->booleanType());
+        Node sk = sm->mkDummySkolem("deor", nm->booleanType());
         Node ite = sk.iteNode(otherL, otherR);
         d_skolems.insert(sk, cnd);
         addSubstitution(sel, ite);
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index bc35c6941..c9f572364 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -49,20 +49,6 @@ inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }
 
-inline Node mkIntSkolem(const std::string& name){
-  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
-}
-
-inline Node mkRealSkolem(const std::string& name){
-  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
-}
-
-inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
-  NodeManager* currNM = NodeManager::currentNM();
-  TypeNode functionType = currNM->mkFunctionType(dom, range);
-  return currNM->mkSkolem(name, functionType);
-}
-
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index b2c48163f..0043ccae6 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/callbacks.h"
 
 #include "expr/proof_node.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 
@@ -46,7 +47,9 @@ TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
 : d_ta(ta)
 {}
 ArithVar TempVarMalloc::request(){
-  Node skolem = mkRealSkolem("tmpVar");
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
   return d_ta.requestArithVar(skolem, false, true);
 }
 void TempVarMalloc::release(ArithVar v){
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 3825a3a42..6ceab1933 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -18,6 +18,7 @@
 #include <iostream>
 
 #include "base/output.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/partial_model.h"
@@ -29,8 +30,11 @@ namespace theory {
 namespace arith {
 
 inline Node makeIntegerVariable(){
-  NodeManager* curr = NodeManager::currentNM();
-  return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver");
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  return sm->mkDummySkolem("intvar",
+                           nm->integerType(),
+                           "is an integer variable created by the dio solver");
 }
 
 DioSolver::DioSolver(context::Context* ctxt)
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 1cf9cbc54..aa9bce776 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -14,11 +14,12 @@
 
 #include "theory/arith/nl/cad_solver.h"
 
-#include "theory/inference_id.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
+#include "theory/inference_id.h"
 
 namespace cvc5 {
 namespace theory {
@@ -37,11 +38,10 @@ CadSolver::CadSolver(InferenceManager& im,
       d_im(im),
       d_model(model)
 {
-  d_ranVariable =
-      NodeManager::currentNM()->mkSkolem("__z",
-                                         NodeManager::currentNM()->realType(),
-                                         "",
-                                         NodeManager::SKOLEM_EXACT_NAME);
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  d_ranVariable = sm->mkDummySkolem(
+      "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
 #ifdef CVC4_POLY_IMP
   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
   if (pc != nullptr)
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index c8c375096..2a1f2ad91 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -20,6 +20,7 @@
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
 #include "expr/proof.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
@@ -55,10 +56,11 @@ SineSolver::~SineSolver() {}
 void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Assert(a.getKind() == Kind::SINE);
   Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
   Assert(!d_data->d_pi.isNull());
-  Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+  Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts");
   // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based
   // refinement for constant shifts (cvc4-projects #1284)
   Node lem = nm->mkNode(
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ed5ab4255..b3fd40ce7 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
@@ -56,14 +57,15 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   for (const Node& a : needsMaster)
   {
     // should not have processed this already
     Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
     Kind k = a.getKind();
     Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
-    Node y =
-        nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+    Node y = sm->mkDummySkolem(
+        "y", nm->realType(), "phase shifted trigonometric arg");
     Node new_a = nm->mkNode(k, y);
     d_tstate.d_trSlaves[new_a].insert(new_a);
     d_tstate.d_trSlaves[new_a].insert(a);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0a64a4e63..7ad0bbfbb 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4958,16 +4958,6 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith
         setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
       }
       break;
-    case inferbounds::Simplex:
-      {
-        // primDir * diffm * diff < c or primDir * diffm * diff > c
-        tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
-        setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
-
-        tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
-        setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
-      }
-      break;
     default:
       Unhandled();
     }
@@ -5298,419 +5288,11 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t
   tmp.first = nb;
 }
 
-std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){
-
-  if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){
-    return make_pair(Node::null(), DeltaRational());
-  }
-
-  Assert(d_qflraStatus == Result::SAT);
-  Assert(d_errorSet.noSignals());
-  Assert(param.getAlgorithm() == inferbounds::Simplex);
-
-  // TODO Move me into a new file
-
-  enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
-  ResultState finalState = Unset;
-
-  const int maxRounds =
-      param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1;
-
-  Maybe<DeltaRational> threshold;
-  // TODO: get this from the parameters
-
-  // setup term
-  Polynomial p = Polynomial::parsePolynomial(tp);
-  vector<ArithVar> variables;
-  vector<Rational> coefficients;
-  asVectors(p, coefficients, variables);
-  if(sgn < 0){
-    for(size_t i=0, N=coefficients.size(); i < N; ++i){
-      coefficients[i] = -coefficients[i];
-    }
-  }
-  // implicitly an upperbound
-  Node skolem = mkRealSkolem("tmpVar$$");
-  ArithVar optVar = requestArithVar(skolem, false, true);
-  d_tableau.addRow(optVar, coefficients, variables);
-  RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
-  DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
-  d_partialModel.setAssignment(optVar, newAssignment);
-  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
-  // Setup simplex
-  d_partialModel.stopQueueingBoundCounts();
-  UpdateTrackingCallback utcb(&d_linEq);
-  d_partialModel.processBoundsQueue(utcb);
-  d_linEq.startTrackingBoundCounts();
-
-  // maximize optVar via primal Simplex
-  int rounds = 0;
-  while(finalState == Unset){
-    ++rounds;
-    if(maxRounds >= 0 && rounds > maxRounds){
-      finalState = ExhaustedRounds;
-      break;
-    }
-
-    // select entering by bland's rule
-    // TODO improve upon bland's
-    ArithVar entering = ARITHVAR_SENTINEL;
-    const Tableau::Entry* enteringEntry = NULL;
-    for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
-      const Tableau::Entry& entry = *ri;
-      ArithVar v = entry.getColVar();
-      if(v != optVar){
-        int sgn1 = entry.getCoefficient().sgn();
-        Assert(sgn1 != 0);
-        bool candidate = (sgn1 > 0)
-                             ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
-                             : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
-        if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
-          entering = v;
-          enteringEntry = &entry;
-        }
-      }
-    }
-    if(entering == ARITHVAR_SENTINEL){
-      finalState = Inferred;
-      break;
-    }
-    Assert(entering != ARITHVAR_SENTINEL);
-    Assert(enteringEntry != NULL);
-
-    int esgn = enteringEntry->getCoefficient().sgn();
-    Assert(esgn != 0);
-
-    // select leaving and ratio
-    ArithVar leaving = ARITHVAR_SENTINEL;
-    DeltaRational minRatio;
-    const Tableau::Entry* pivotEntry = NULL;
-
-    // Special case check the upper/lowerbound on entering
-    ConstraintP cOnEntering = (esgn > 0)
-      ? d_partialModel.getUpperBoundConstraint(entering)
-      : d_partialModel.getLowerBoundConstraint(entering);
-    if(cOnEntering != NullConstraint){
-      leaving = entering;
-      minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
-    }
-    for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
-      const Tableau::Entry& centry = *ci;
-      ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
-      int csgn = centry.getCoefficient().sgn();
-      int basicDir = csgn * esgn;
-
-      ConstraintP bound = (basicDir > 0)
-        ? d_partialModel.getUpperBoundConstraint(basic)
-        : d_partialModel.getLowerBoundConstraint(basic);
-      if(bound != NullConstraint){
-        DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
-        DeltaRational ratio = diff/(centry.getCoefficient());
-        bool selected = false;
-        if(leaving == ARITHVAR_SENTINEL){
-          selected = true;
-        }else{
-          int cmp = ratio.compare(minRatio);
-          if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
-            selected = (cmp != 0) ||
-              ((leaving != entering) && (basic < leaving));
-          }
-        }
-        if(selected){
-          leaving = basic;
-          minRatio = ratio;
-          pivotEntry = &centry;
-        }
-      }
-    }
-
-
-    if(leaving == ARITHVAR_SENTINEL){
-      finalState = NoBound;
-      break;
-    }else if(leaving == entering){
-      d_linEq.update(entering, minRatio);
-    }else{
-      DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
-      d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
-      // no conflicts clear signals
-      Assert(d_errorSet.noSignals());
-    }
-
-    if(threshold.just()){
-      if (d_partialModel.getAssignment(optVar) >= threshold.value())
-      {
-        finalState = ReachedThreshold;
-        break;
-      }
-    }
-  };
-
-  result = InferBoundsResult(tp, sgn > 0);
-
-  // tear down term
-  switch(finalState){
-  case Inferred:
-    {
-      NodeBuilder nb(kind::AND);
-      for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
-        const Tableau::Entry& e =*ri;
-        ArithVar colVar = e.getColVar();
-        if(colVar != optVar){
-          const Rational& q = e.getCoefficient();
-          Assert(q.sgn() != 0);
-          ConstraintP c = (q.sgn() > 0)
-            ? d_partialModel.getUpperBoundConstraint(colVar)
-            : d_partialModel.getLowerBoundConstraint(colVar);
-          c->externalExplainByAssertions(nb);
-        }
-      }
-      Assert(nb.getNumChildren() >= 1);
-      Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
-      result.setBound(d_partialModel.getAssignment(optVar), exp);
-      result.setIsOptimal();
-      break;
-    }
-  case NoBound:
-    break;
-  case ReachedThreshold:
-    result.setReachedThreshold();
-    break;
-  case ExhaustedRounds:
-    result.setBudgetExhausted();
-    break;
-  case Unset:
-  default:
-    Unreachable();
-    break;
-  };
-
-  d_linEq.stopTrackingRowIndex(ridx);
-  d_tableau.removeBasicRow(optVar);
-  releaseArithVar(optVar);
-
-  d_linEq.stopTrackingBoundCounts();
-  d_partialModel.startQueueingBoundCounts();
-
-  if(result.foundBound()){
-    return make_pair(result.getExplanation(), result.getValue());
-  }else{
-    return make_pair(Node::null(), DeltaRational());
-  }
-}
-
 ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
 {
   return &d_checker;
 }
 
-// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const
-// inferbounds::InferBoundAlgorithm& param){
-//   Assert(param.findUpperBound());
-
-//   if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){
-//     InferBoundsResult inconsistent;
-//     inconsistent.setInconsistent();
-//     return inconsistent;
-//   }
-
-//   Assert(d_qflraStatus == Result::SAT);
-//   Assert(d_errorSet.noSignals());
-
-//   // TODO Move me into a new file
-
-//   enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
-//   ResultState finalState = Unset;
-
-//   int maxRounds = 0;
-//   switch(param.getParamKind()){
-//   case InferBoundsParameters::Unbounded:
-//     maxRounds = -1;
-//     break;
-//   case InferBoundsParameters::NumVars:
-//     maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter();
-//     break;
-//   case InferBoundsParameters::Direct:
-//     maxRounds = param.getSimplexRoundParameter();
-//     break;
-//   default: maxRounds = 0; break;
-//   }
-
-//   // setup term
-//   Polynomial p = Polynomial::parsePolynomial(t);
-//   vector<ArithVar> variables;
-//   vector<Rational> coefficients;
-//   asVectors(p, coefficients, variables);
-
-//   Node skolem = mkRealSkolem("tmpVar$$");
-//   ArithVar optVar = requestArithVar(skolem, false, true);
-//   d_tableau.addRow(optVar, coefficients, variables);
-//   RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
-//   DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
-//   d_partialModel.setAssignment(optVar, newAssignment);
-//   d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
-//   // Setup simplex
-//   d_partialModel.stopQueueingBoundCounts();
-//   UpdateTrackingCallback utcb(&d_linEq);
-//   d_partialModel.processBoundsQueue(utcb);
-//   d_linEq.startTrackingBoundCounts();
-
-//   // maximize optVar via primal Simplex
-//   int rounds = 0;
-//   while(finalState == Unset){
-//     ++rounds;
-//     if(maxRounds >= 0 && rounds > maxRounds){
-//       finalState = ExhaustedRounds;
-//       break;
-//     }
-
-//     // select entering by bland's rule
-//     // TODO improve upon bland's
-//     ArithVar entering = ARITHVAR_SENTINEL;
-//     const Tableau::Entry* enteringEntry = NULL;
-//     for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-//     !ri.atEnd(); ++ri){
-//       const Tableau::Entry& entry = *ri;
-//       ArithVar v = entry.getColVar();
-//       if(v != optVar){
-//         int sgn = entry.getCoefficient().sgn();
-//         Assert(sgn != 0);
-//         bool candidate = (sgn > 0)
-//           ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
-//           : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
-//         if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
-//           entering = v;
-//           enteringEntry = &entry;
-//         }
-//       }
-//     }
-//     if(entering == ARITHVAR_SENTINEL){
-//       finalState = Inferred;
-//       break;
-//     }
-//     Assert(entering != ARITHVAR_SENTINEL);
-//     Assert(enteringEntry != NULL);
-
-//     int esgn = enteringEntry->getCoefficient().sgn();
-//     Assert(esgn != 0);
-
-//     // select leaving and ratio
-//     ArithVar leaving = ARITHVAR_SENTINEL;
-//     DeltaRational minRatio;
-//     const Tableau::Entry* pivotEntry = NULL;
-
-//     // Special case check the upper/lowerbound on entering
-//     ConstraintP cOnEntering = (esgn > 0)
-//       ? d_partialModel.getUpperBoundConstraint(entering)
-//       : d_partialModel.getLowerBoundConstraint(entering);
-//     if(cOnEntering != NullConstraint){
-//       leaving = entering;
-//       minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
-//     }
-//     for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
-//       const Tableau::Entry& centry = *ci;
-//       ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
-//       int csgn = centry.getCoefficient().sgn();
-//       int basicDir = csgn * esgn;
-
-//       ConstraintP bound = (basicDir > 0)
-//         ? d_partialModel.getUpperBoundConstraint(basic)
-//         : d_partialModel.getLowerBoundConstraint(basic);
-//       if(bound != NullConstraint){
-//         DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
-//         DeltaRational ratio = diff/(centry.getCoefficient());
-//         bool selected = false;
-//         if(leaving == ARITHVAR_SENTINEL){
-//           selected = true;
-//         }else{
-//           int cmp = ratio.compare(minRatio);
-//           if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
-//             selected = (cmp != 0) ||
-//               ((leaving != entering) && (basic < leaving));
-//           }
-//         }
-//         if(selected){
-//           leaving = basic;
-//           minRatio = ratio;
-//           pivotEntry = &centry;
-//         }
-//       }
-//     }
-
-//     if(leaving == ARITHVAR_SENTINEL){
-//       finalState = NoBound;
-//       break;
-//     }else if(leaving == entering){
-//       d_linEq.update(entering, minRatio);
-//     }else{
-//       DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
-//       d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
-//       // no conflicts clear signals
-//       Assert(d_errorSet.noSignals());
-//     }
-
-//     if(param.useThreshold()){
-//       if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){
-//         finalState = ReachedThreshold;
-//         break;
-//       }
-//     }
-//   };
-
-//   InferBoundsResult result(t, param.findUpperBound());
-
-//   // tear down term
-//   switch(finalState){
-//   case Inferred:
-//     {
-//       NodeBuilder nb(kind::AND);
-//       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-//       !ri.atEnd(); ++ri){
-//         const Tableau::Entry& e =*ri;
-//         ArithVar colVar = e.getColVar();
-//         if(colVar != optVar){
-//           const Rational& q = e.getCoefficient();
-//           Assert(q.sgn() != 0);
-//           ConstraintP c = (q.sgn() > 0)
-//             ? d_partialModel.getUpperBoundConstraint(colVar)
-//             : d_partialModel.getLowerBoundConstraint(colVar);
-//           c->externalExplainByAssertions(nb);
-//         }
-//       }
-//       Assert(nb.getNumChildren() >= 1);
-//       Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
-//       result.setBound(d_partialModel.getAssignment(optVar), exp);
-//       result.setIsOptimal();
-//       break;
-//     }
-//   case NoBound:
-//     break;
-//   case ReachedThreshold:
-//     result.setReachedThreshold();
-//     break;
-//   case ExhaustedRounds:
-//     result.setBudgetExhausted();
-//     break;
-//   case Unset:
-//   default:
-//     Unreachable();
-//     break;
-//   };
-
-//   d_linEq.stopTrackingRowIndex(ridx);
-//   d_tableau.removeBasicRow(optVar);
-//   releaseArithVar(optVar);
-
-//   d_linEq.stopTrackingBoundCounts();
-//   d_partialModel.startQueueingBoundCounts();
-
-//   return result;
-// }
-
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ba3fdfaf5..50fb89808 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -137,12 +137,6 @@ private:
   void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
   void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
 
-  std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
-
-  //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
-  //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
-  //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
-
   /**
    * Infers either a new upper/lower bound on term in the real relaxation.
    * Either: