Eliminate some static options access (#8795)

In preparation for eliminating options scopes.

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 350348927cafef3b01768a9f92019a7e8a10a8aa..c5cb6aa229958fa47f9ae33fa3cca9d050a0b58f 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -105,14 +105,6 @@ name   = "Strings Theory"
   default    = "true"
   help       = "regression explanations for string lemmas"
 
-[[option]]
-  name       = "stringMinPrefixExplain"
-  category   = "expert"
-  long       = "strings-min-prefix-explain"
-  type       = "bool"
-  default    = "true"
-  help       = "minimize explanations for prefix of normal forms in strings"
-
 [[option]]
   name       = "stringModelBasedReduction"
   category   = "regular"

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 70544aa8e29f68442cf8b641ecc195bd8a72c0b1..c567c319071af1b3ce23f810fbfcc08d35b20156 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -703,7 +703,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     }
   } while (expanded);
   // now we should be able to close it
-  if (options::proofCheck() == options::ProofCheckMode::EAGER)
+  if (options().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     std::vector<Node> assumptionsVec;
     for (const Node& a : d_assumptions)

diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp
index 76012e5bd76ae664db572ee0ed61853ee4a89d37..57dc93f6bc1c1acac1f82ea37f02968ced23be23 100644 (file)
--- a/src/smt/abstract_values.cpp
+++ b/src/smt/abstract_values.cpp
@@ -22,11 +22,8 @@
 namespace cvc5::internal {
 namespace smt {
 
-AbstractValues::AbstractValues(NodeManager* nm)
-    : d_nm(nm),
-      d_fakeContext(),
-      d_abstractValueMap(&d_fakeContext),
-      d_abstractValues()
+AbstractValues::AbstractValues()
+    : d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues()
 {
 }
 AbstractValues::~AbstractValues() {}
@@ -41,11 +38,10 @@ Node AbstractValues::substituteAbstractValues(TNode n)
 
 Node AbstractValues::mkAbstractValue(TNode n)
 {
-  Assert(options::abstractValues());
   Node& val = d_abstractValues[n];
   if (val.isNull())
   {
-    val = d_nm->getSkolemManager()->mkDummySkolem(
+    val = NodeManager::currentNM()->getSkolemManager()->mkDummySkolem(
         "a",
         n.getType(),
         "an abstract value",

diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h
index 5cf66aa925cb176876d2687e11d2be2f14f6a4db..1d7e6e4cede8bfde85e394cfc1b9f635eb21637a 100644 (file)
--- a/src/smt/abstract_values.h
+++ b/src/smt/abstract_values.h
@@ -37,7 +37,7 @@ class AbstractValues
   typedef std::unordered_map<Node, Node> NodeToNodeHashMap;
 
  public:
-  AbstractValues(NodeManager* nm);
+  AbstractValues();
   ~AbstractValues();
   /**
    * Substitute away all AbstractValues in a node, which replaces all

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index eb37c0c21db8db296cf023480bc22a5da9fc48f1..efd7f18ce53d338d750dcb79e2f0bcf85f66c3db 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -765,9 +765,9 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
     d_commandStatus = CommandSuccess::instance();
     d_solution.clear();
     // check whether we should print the status
-    if (!d_result.hasSolution()
-        || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
-        || options::sygusOut() == options::SygusSolutionOutMode::STATUS)
+    std::string sygusOut = solver->getOption("sygus-out");
+    if (!d_result.hasSolution() || sygusOut == "status-and-def"
+        || sygusOut == "status")
     {
       if (d_result.hasSolution())
       {
@@ -783,8 +783,7 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
       }
     }
     // check whether we should print the solution
-    if (d_result.hasSolution()
-        && options::sygusOut() != options::SygusSolutionOutMode::STATUS)
+    if (d_result.hasSolution() && sygusOut != "status")
     {
       std::vector<cvc5::Term> synthFuns = sm->getFunctionsToSynthesize();
       d_solution << "(" << std::endl;
@@ -2402,12 +2401,13 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
 /* class GetUnsatCoreCommand                                                  */
 /* -------------------------------------------------------------------------- */
 
-GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
+GetUnsatCoreCommand::GetUnsatCoreCommand() : d_solver(nullptr), d_sm(nullptr) {}
 void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 {
   try
   {
     d_sm = sm;
+    d_solver = solver;
     d_result = solver->getUnsatCore();
 
     d_commandStatus = CommandSuccess::instance();
@@ -2430,7 +2430,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out) const
   }
   else
   {
-    if (options::printUnsatCoresFull())
+    if (d_solver->getOption("print-unsat-cores-full") == "true")
     {
       // use the assertions
       UnsatCore ucr(termVectorToNodes(d_result));
@@ -2456,6 +2456,7 @@ const std::vector<cvc5::Term>& GetUnsatCoreCommand::getUnsatCore() const
 Command* GetUnsatCoreCommand::clone() const
 {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
+  c->d_solver = d_solver;
   c->d_sm = d_sm;
   c->d_result = d_result;
   return c;

diff --git a/src/smt/command.h b/src/smt/command.h
index 0af8b4b48511e392c6e5fc23761952cc2b6e165f..d5801eb4bdd112c08cad654e8dbf2c4da9093267 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1288,6 +1288,8 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command
                     internal::Language::LANG_AUTO) const override;
 
  protected:
+  /** The solver we were invoked with */
+  cvc5::Solver* d_solver;
   /** The symbol manager we were invoked with */
   SymbolManager* d_sm;
   /** the result of the unsat core call */

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 2cb2efe39d08ed47e86f314ce30f706d09e61335..2893ccb23cd1cae4548d2a48a17ed27dd144aaee 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -250,7 +250,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
 
 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 {
-  if (options::proofCheck() == options::ProofCheckMode::EAGER)
+  if (options().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation

diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index 2d109da171d11ede9d93f35510bfbd64ff7bf6f2..1ec4a9c8634491781f21f24819050735f47d7f7a 100644 (file)
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -18,6 +18,7 @@
 #include "options/proof_options.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_manager.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/theory_id.h"
@@ -28,22 +29,21 @@ using namespace cvc5::internal::theory;
 namespace cvc5::internal {
 namespace smt {
 
-ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm)
-    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
+ProofFinalCallback::ProofFinalCallback(Env& env)
+    : EnvObj(env),
+      d_ruleCount(statisticsRegistry().registerHistogram<PfRule>(
           "finalProof::ruleCount")),
-      d_instRuleIds(
-          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
-              "finalProof::instRuleId")),
+      d_instRuleIds(statisticsRegistry().registerHistogram<theory::InferenceId>(
+          "finalProof::instRuleId")),
       d_annotationRuleIds(
-          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
+          statisticsRegistry().registerHistogram<theory::InferenceId>(
               "finalProof::annotationRuleId")),
       d_totalRuleCount(
-          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
+          statisticsRegistry().registerInt("finalProof::totalRuleCount")),
       d_minPedanticLevel(
-          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
+          statisticsRegistry().registerInt("finalProof::minPedanticLevel")),
       d_numFinalProofs(
-          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
-      d_pnm(pnm),
+          statisticsRegistry().registerInt("finalProofs::numFinalProofs")),
       d_pedanticFailure(false)
 {
   d_minPedanticLevel += 10;
@@ -61,23 +61,25 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
                                       bool& continueUpdate)
 {
   PfRule r = pn->getRule();
+  ProofNodeManager* pnm = d_env.getProofNodeManager();
+  Assert(pnm != nullptr);
   // if not doing eager pedantic checking, fail if below threshold
-  if (options::proofCheck() != options::ProofCheckMode::EAGER)
+  if (options().proof.proofCheck != options::ProofCheckMode::EAGER)
   {
     if (!d_pedanticFailure)
     {
       Assert(d_pedanticFailureOut.str().empty());
-      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
+      if (pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
       {
         d_pedanticFailure = true;
       }
     }
   }
-  if (options::proofCheck() != options::ProofCheckMode::NONE)
+  if (options().proof.proofCheck != options::ProofCheckMode::NONE)
   {
-    d_pnm->ensureChecked(pn.get());
+    pnm->ensureChecked(pn.get());
   }
-  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
+  uint32_t plevel = pnm->getChecker()->getPedanticLevel(r);
   if (plevel != 0)
   {
     d_minPedanticLevel.minAssign(plevel);

diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h
index 666e25a534987b03302128788119e1eea85a1999..e5b2ff058b29c44cd79453a09ae88e11a8a9f0d5 100644 (file)
--- a/src/smt/proof_final_callback.h
+++ b/src/smt/proof_final_callback.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "proof/proof_node_updater.h"
+#include "smt/env_obj.h"
 #include "theory/inference_id.h"
 #include "util/statistics_stats.h"
 
@@ -30,10 +31,10 @@ namespace cvc5::internal {
 namespace smt {
 
 /** Final callback class, for stats and pedantic checking */
-class ProofFinalCallback : public ProofNodeUpdaterCallback
+class ProofFinalCallback : protected EnvObj, public ProofNodeUpdaterCallback
 {
  public:
-  ProofFinalCallback(ProofNodeManager* pnm);
+  ProofFinalCallback(Env& env);
   /**
    * Initialize, called once for each new ProofNode to process. This initializes
    * static information to be used by successive calls to update.
@@ -65,8 +66,6 @@ class ProofFinalCallback : public ProofNodeUpdaterCallback
   IntStat d_minPedanticLevel;
   /** The total number of final proofs */
   IntStat d_numFinalProofs;
-  /** Proof node manager (used for pedantic checking) */
-  ProofNodeManager* d_pnm;
   /** Was there a pedantic failure? */
   bool d_pedanticFailure;
   /** The pedantic failure string for debugging */

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 7317ed35182c846e67dadffb4a52eac805bc5263..029bfdfcd0450564de4ddf3650e827b993ecd99d 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1267,9 +1267,8 @@ ProofPostproccess::ProofPostproccess(Env& env,
     : EnvObj(env),
       d_cb(env, pppg, rdb, updateScopedAssumptions),
       // the update merges subproofs
-      d_updater(
-          env.getProofNodeManager(), d_cb, options().proof.proofPpMerge),
-      d_finalCb(env.getProofNodeManager()),
+      d_updater(env.getProofNodeManager(), d_cb, options().proof.proofPpMerge),
+      d_finalCb(env),
       d_finalizer(env.getProofNodeManager(), d_finalCb)
 {
 }

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 952db55ffc4b6fc024dc4f5df423f98e0b292394..5ef8257cb95f606cd94f4f76efbf60f78fa78e53 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -86,7 +86,7 @@ namespace cvc5::internal {
 SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
     : d_env(new Env(nm, optr)),
       d_state(new SolverEngineState(*d_env.get(), *this)),
-      d_absValues(new AbstractValues(getNodeManager())),
+      d_absValues(new AbstractValues),
       d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
       d_routListener(new ResourceOutListener(*this)),
       d_smtSolver(nullptr),

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index a2975f694d08773cae2fc8f11fc5490c7aacab6a..a75ccebeb9ddb29dfd841fcf32439c51a248e8ae 100644 (file)
--- a/src/theory/datatypes/inference.cpp
+++ b/src/theory/datatypes/inference.cpp
@@ -39,20 +39,13 @@ DatatypesInference::DatatypesInference(InferenceManager* im,
 bool DatatypesInference::mustCommunicateFact(Node n, Node exp)
 {
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
-  // Force lemmas if option is set
-  if (options::dtInferAsLemmas())
-  {
-    Trace("dt-lemma-debug")
-        << "Communicate " << n << " due to option" << std::endl;
-    return true;
-  }
   // Note that equalities due to instantiate are forced as lemmas if
   // necessary as they are created. This ensures that terms are shared with
   // external theories when necessary. We send the lemma here only if the
   // conclusion has kind LEQ (for datatypes size) or OR. Notice that
   // all equalities are kept internal, apart from those forced as lemmas
   // via instantiate.
-  else if (n.getKind() == LEQ || n.getKind() == OR)
+  if (n.getKind() == LEQ || n.getKind() == OR)
   {
     Trace("dt-lemma-debug")
         << "Communicate " << n << " due to kind" << std::endl;

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 32e86bd68aa9bfeaed551235d8f1ffa39baf1508..755c545f0218da388d7bf0168f98258aee330101 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -53,10 +53,11 @@ void InferenceManager::addPendingInference(Node conc,
                                            Node exp,
                                            bool forceLemma)
 {
-  // if we are forcing the inference to be processed as a lemma, or if the
-  // inference must be sent as a lemma based on the policy in
-  // mustCommunicateFact.
-  if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp))
+  // if we are forcing the inference to be processed as a lemma, if the
+  // dtInferAsLemmas option is set, or if the inference must be sent as a lemma
+  // based on the policy in mustCommunicateFact.
+  if (forceLemma || options().datatypes.dtInferAsLemmas
+      || DatatypesInference::mustCommunicateFact(conc, exp))
   {
     d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id));
   }

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index f49bfc0358d6e7ffcaf934a23e2cda40f3a4cfd9..750c07e5db694ab99f12ce436ebee7168a526597 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -407,7 +407,7 @@ CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q)
   return hmin;
 }
 
-CegHandledStatus CegInstantiator::isCbqiQuant(Node q)
+CegHandledStatus CegInstantiator::isCbqiQuant(Node q, bool cegqiAll)
 {
   Assert(q.getKind() == FORALL);
   // compute attributes
@@ -467,7 +467,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q)
       ret = CEG_PARTIALLY_HANDLED;
     }
   }
-  if (ret == CEG_UNHANDLED && options::cegqiAll())
+  if (ret == CEG_UNHANDLED && cegqiAll)
   {
     // try but not exclusively
     ret = CEG_PARTIALLY_HANDLED;

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index e413e3089412c813a4b46f029ad315c7a2d1545d..12b8d019afadd76f0b863aa1e040e4ec0f3cdff6 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -346,8 +346,11 @@ class CegInstantiator : protected EnvObj
    * returns CEG_PARTIALLY_HANDLED, then it may be worthwhile to handle the
    * quantified formula using cegqi, however other strategies should also be
    * tried.
+   *
+   * @param cegqiAll Whether we apply CEQGI to all quantifiers (option
+   * options::cegqiAll).
    */
-  static CegHandledStatus isCbqiQuant(Node q);
+  static CegHandledStatus isCbqiQuant(Node q, bool cegqiAll);
   //------------------------------------ end static queries
  private:
   /** The quantified formula of this instantiator */

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 7760b9391c7fb5bfed6169003fc4f80c8eb686d5..e290b0f67ee6d54c59d07745621f36f733d58b8e 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -409,7 +409,8 @@ bool InstStrategyCegqi::doCbqi(Node q)
 {
   std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
   if( it==d_do_cbqi.end() ){
-    CegHandledStatus ret = CegInstantiator::isCbqiQuant(q);
+    CegHandledStatus ret =
+        CegInstantiator::isCbqiQuant(q, options().quantifiers.cegqiAll);
     Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
     return ret != CEG_UNHANDLED;

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index d29b5a8883777dca8fb8a920d39c2e80d42b8073..0a7a79af84a2ebeb19b7bc2cad2824e44f3b1d76 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -182,7 +182,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
     }
     else
     {
-      status = CegInstantiator::isCbqiQuant(d_single_inv);
+      status = CegInstantiator::isCbqiQuant(d_single_inv,
+                                            options().quantifiers.cegqiAll);
     }
   }
   Trace("sygus-si") << "CegHandledStatus is " << status << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index c138984fe07b8a6d2b3eda68efb8494dcc55895d..7395a583a1bb97c1313ed1091029a00b1237323f 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -215,7 +215,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   if (fo_body.getKind() == FORALL)
   {
     // must be a CBQI quantifier
-    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body);
+    CegHandledStatus hstatus =
+        CegInstantiator::isCbqiQuant(fo_body, options().quantifiers.cegqiAll);
     if (hstatus < CEG_HANDLED)
     {
       // abort if less than fully handled

diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index e17a9afdf13d073db3815c394edcd5301689dc91..52a1c5493769c17e4ea68a5375161c4fc6ca78bc 100644 (file)
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -116,7 +116,7 @@ void NormalForm::addToExplanation(Node exp,
 
 void NormalForm::getExplanation(int index, std::vector<Node>& curr_exp)
 {
-  if (index == -1 || !options::stringMinPrefixExplain())
+  if (index == -1)
   {
     curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end());
     return;