First part of options refactoring (#6428)

This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular

- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()

The removed methods are only used in few places with are changed to using Options::current().X() instead.

In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.

3 files changed, 4 insertions, 124 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4687922a0..ce8e2393b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2906,10 +2906,10 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   if(d_qflraStatus != Result::UNSAT){
     static const int32_t pass2Limit = 20;
     int16_t oldCap = options::arithStandardCheckVarOrderPivots();
-    options::arithStandardCheckVarOrderPivots.set(pass2Limit);
+    Options::current().set(options::arithStandardCheckVarOrderPivots, pass2Limit);
     SimplexDecisionProcedure& simplex = selectSimplex(false);
     d_qflraStatus = simplex.findModel(false);
-    options::arithStandardCheckVarOrderPivots.set(oldCap);
+    Options::current().set(options::arithStandardCheckVarOrderPivots, oldCap);
   }
 
   if(Debug.isOn("arith::importSolution")){
@@ -3048,126 +3048,6 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   return emmittedConflictOrSplit;
 }
 
-//   LinUnknown,  /* Unknown error */
-//   LinFeasible, /* Relaxation is feasible */
-//   LinInfeasible,   /* Relaxation is infeasible/all integer branches closed */
-//   LinExhausted
-//     // Fancy final tries the following strategy
-//     // At final check, try the preferred simplex solver with a pivot cap
-//     // If that failed, swap the the other simplex solver
-//     // If that failed, check if there are integer variables to cut
-//     // If that failed, do a simplex without a pivot limit
-
-//     int16_t oldCap = options::arithStandardCheckVarOrderPivots();
-
-//     static const int32_t pass2Limit = 10;
-//     static const int32_t relaxationLimit = 10000;
-//     static const int32_t mipLimit = 200000;
-
-//     //cout << "start" << endl;
-//     d_qflraStatus = simplex.findModel(false);
-//     //cout << "end" << endl;
-//     if(d_qflraStatus == Result::SAT_UNKNOWN ||
-//        (d_qflraStatus == Result::SAT && !hasIntegerModel() && !d_likelyIntegerInfeasible)){
-
-//       ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel, *(getTreeLog()), *(getApproxStats()));
-//       approxSolver->setPivotLimit(relaxationLimit);
-
-//       if(!d_guessedCoeffSet){
-//         d_guessedCoeffs = approxSolver->heuristicOptCoeffs();
-//         d_guessedCoeffSet = true;
-//       }
-//       if(!d_guessedCoeffs.empty()){
-//         approxSolver->setOptCoeffs(d_guessedCoeffs);
-//       }
-
-//       MipResult mipRes;
-//       ApproximateSimplex::Solution relaxSolution, mipSolution;
-//       LinResult relaxRes = approxSolver->solveRelaxation();
-//       switch(relaxRes){
-//       case LinFeasible:
-//         {
-//           relaxSolution = approxSolver->extractRelaxation();
-
-//           /* If the approximate solver  known to be integer infeasible
-//            * only redo*/
-//           int maxDepth =
-//             d_likelyIntegerInfeasible ? 1 : options::arithMaxBranchDepth();
-
-//           if(d_likelyIntegerInfeasible){
-//             d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
-//           }else{
-//             approxSolver->setPivotLimit(mipLimit);
-//             mipRes = approxSolver->solveMIP(false);
-//             if(mipRes == ApproximateSimplex::ApproxUnsat){
-//               mipRes = approxSolver->solveMIP(true);
-//             }
-//             d_errorSet.reduceToSignals();
-//             //CVC5Message() << "here" << endl;
-//             if(mipRes == ApproximateSimplex::ApproxSat){
-//               mipSolution = approxSolver->extractMIP();
-//               d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
-//             }else{
-//               if(mipRes == ApproximateSimplex::ApproxUnsat){
-//                 d_likelyIntegerInfeasible = true;
-//               }
-//               vector<Node> lemmas = approxSolver->getValidCuts();
-//               for(size_t i = 0; i < lemmas.size(); ++i){
-//                 d_approxCuts.pushback(lemmas[i]);
-//               }
-//               d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
-//             }
-//           }
-//           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus =
-//           simplex.findModel(false); }
-//           //CVC5Message() << "done" << endl;
-//         }
-//         break;
-//       case ApproximateSimplex::ApproxUnsat:
-//         {
-//           ApproximateSimplex::Solution sol =
-//           approxSolver->extractRelaxation();
-
-//           d_qflraStatus = d_attemptSolSimplex.attempt(sol);
-//           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
-
-//           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
-//         }
-//         break;
-//       default:
-//         break;
-//       }
-//       delete approxSolver;
-//     }
-//   }
-
-//   if(!useFancyFinal){
-//     d_qflraStatus = simplex.findModel(noPivotLimit);
-//   }else{
-
-//     if(d_qflraStatus == Result::SAT_UNKNOWN){
-//       //CVC5Message() << "got sat unknown" << endl;
-//       vector<ArithVar> toCut = cutAllBounded();
-//       if(toCut.size() > 0){
-//         //branchVector(toCut);
-//         emmittedConflictOrSplit = true;
-//       }else{
-//         //CVC5Message() << "splitting" << endl;
-
-//         d_qflraStatus = simplex.findModel(noPivotLimit);
-//       }
-//     }
-//     options::arithStandardCheckVarOrderPivots.set(oldCap);
-//   }
-
-//   // TODO Save zeroes with no conflicts
-//   d_linEq.stopTrackingBoundCounts();
-//   d_partialModel.startQueueingBoundCounts();
-
-//   return emmittedConflictOrSplit;
-// }
-
 bool TheoryArithPrivate::hasFreshArithLiteral(Node n) const{
   switch(n.getKind()){
   case kind::LEQ:
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 0d62481f9..582d67b31 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
-  if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+  if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout))
   {
     initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
   }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 232b9f736..62f362e2b 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -234,7 +234,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   std::unique_ptr<SmtEngine> repcChecker;
   // initialize the subsolver using the standard method
   initializeSubsolver(repcChecker,
-                      options::sygusRepairConstTimeout.wasSetByUser(),
+                      Options::current().wasSetByUser(options::sygusRepairConstTimeout),
                       options::sygusRepairConstTimeout());
   // renable options disabled by sygus
   repcChecker->setOption("miniscope-quant", "true");