Use EnvObj-based options in preprocessing (#7165)

This PR is the first step in replacing options access via options::foo() to using the environment (via EnvObj and options().module.foo). It replaces all such options accesses in the preprocessing passes.

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 7f3d778fd633720a88f8444c5f5882e9ae4eba39..57469ab11df9809ae276195b950a9ff6fbb7cf77 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -308,7 +308,7 @@ Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult Ackermann::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  AlwaysAssert(!options::incrementalSolving());
+  AlwaysAssert(!options().base.incrementalSolving);
 
   /* collect all function applications and generate consistency lemmas
    * accordingly */

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index f5152f0d22f1ac2fd015ba4b54ba668bbfdcfae3..206f12a3fe0e3740ebc38c074f9e0cef48518e68 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -20,6 +20,7 @@
 
 #include "base/map_util.h"
 #include "expr/node.h"
+#include "options/bv_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
@@ -35,7 +36,7 @@ using namespace cvc5::theory;
 BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
 {
-  d_boolToBVMode = options::boolToBitvector();
+  d_boolToBVMode = options().bv.boolToBitvector;
 };
 
 PreprocessingPassResult BoolToBV::applyInternal(

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index cc631f4bcffcd460ee3fc343ef73435910b54983..f6a65f90a1ea7f494e9b487f2d74c499366d6427 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -424,13 +424,13 @@ Node BVToInt::translateWithChildren(Node original,
       // operators)
       // 3. translating into a sum
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND)
+      if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND)
       {
         Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
         returnNode = d_nm->mkNode(
             kind::IAND, iAndOp, translated_children[0], translated_children[1]);
       }
-      else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV)
+      else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV)
       {
         // translate the children back to BV
         Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
@@ -445,14 +445,14 @@ Node BVToInt::translateWithChildren(Node original,
       }
       else
       {
-        Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
+        Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM);
         // Construct a sum of ites, based on granularity.
         Assert(translated_children.size() == 2);
         returnNode =
             d_iandUtils.createSumNode(translated_children[0],
                                       translated_children[1],
                                       bvsize,
-                                      options::BVAndIntegerGranularity());
+                                      options().smt.BVAndIntegerGranularity);
       }
       break;
     }
@@ -657,7 +657,7 @@ Node BVToInt::translateWithChildren(Node original,
        * of the bounds that were relevant for the original
        * bit-vectors.
        */
-      if (childrenTypesChanged(original) && options::ufHo())
+      if (childrenTypesChanged(original) && options().uf.ufHo)
       {
         throw TypeCheckingExceptionPrivate(
             original,

diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 7242be54c6d21818b701e49dba3490091dd8be05..06b4f0ba11626f9f542fb2f73a5554684476865b 100644 (file)
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -36,7 +36,7 @@ PreprocessingPassResult ExtRewPre::applyInternal(
     assertionsToPreprocess->replace(
         i,
         extendedRewrite((*assertionsToPreprocess)[i],
-                        options::extRewPrepAgg()));
+                        options().smt.extRewPrepAgg));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 515cc4a3266173b499d252e1b1167b7ff94375a0..d3372a28ec8ce0008f5bae36e5f29c15df4d6859 100644 (file)
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -180,7 +180,7 @@ Node HoElim::eliminateHo(Node n)
       if (cur.isVar())
       {
         Node ret = cur;
-        if (options::hoElim())
+        if (options().quantifiers.hoElim)
         {
           if (tn.isFunction())
           {
@@ -203,7 +203,7 @@ Node HoElim::eliminateHo(Node n)
       else
       {
         d_visited[cur] = Node::null();
-        if (cur.getKind() == APPLY_UF && options::hoElim())
+        if (cur.getKind() == APPLY_UF && options().quantifiers.hoElim)
         {
           Node op = cur.getOperator();
           // convert apply uf with variable arguments eagerly to ho apply
@@ -275,7 +275,7 @@ Node HoElim::eliminateHo(Node n)
           children.insert(children.begin(), retOp);
         }
         // process ho apply
-        if (ret.getKind() == HO_APPLY && options::hoElim())
+        if (ret.getKind() == HO_APPLY && options().quantifiers.hoElim)
         {
           TypeNode tnr = ret.getType();
           tnr = getUSort(tnr);
@@ -382,7 +382,7 @@ PreprocessingPassResult HoElim::applyInternal(
   // extensionality: process all function types
   for (const TypeNode& ftn : d_funTypes)
   {
-    if (options::hoElim())
+    if (options().quantifiers.hoElim)
     {
       Node h = getHoApplyUf(ftn);
       Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl;
@@ -406,7 +406,7 @@ PreprocessingPassResult HoElim::applyInternal(
       // exists another function that acts like the "store" operator for
       // arrays, e.g. it is the same function with one I/O pair updated.
       // Without this axiom, the translation is model unsound.
-      if (options::hoElimStoreAx())
+      if (options().quantifiers.hoElimStoreAx)
       {
         Node u = nm->mkBoundVar("u", uf);
         Node v = nm->mkBoundVar("v", uf);
@@ -428,7 +428,7 @@ PreprocessingPassResult HoElim::applyInternal(
         Trace("ho-elim-ax") << "...store axiom : " << store << std::endl;
       }
     }
-    else if (options::hoElimStoreAx())
+    else if (options().quantifiers.hoElimStoreAx)
     {
       Node u = nm->mkBoundVar("u", ftn);
       Node v = nm->mkBoundVar("v", ftn);

diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index 8b8dc08c2bcd829d6a69e2c688f36b6e81654691..80f8cda70df844f8d349decf276e55ff1d7fe9cf 100644 (file)
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -73,10 +73,10 @@ namespace passes {
  *
  * Based on options, this preprocessing pass may apply a subset o the above
  * steps. In particular:
- * * If options::hoElim() is true, then step [2] is taken and extensionality
+ * * If hoElim is true, then step [2] is taken and extensionality
  * axioms are added in step [3].
- * * If options::hoElimStoreAx() is true, then store axioms are added in step 3.
- * The form of these axioms depends on whether options::hoElim() is true. If it
+ * * If hoElimStoreAx is true, then store axioms are added in step 3.
+ * The form of these axioms depends on whether hoElim is true. If it
  * is true, the axiom is given in terms of the uninterpreted functions that
  * encode function sorts. If it is false, then the store axiom is given in terms
  * of the original function sorts.

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 46c75b56036334a8e83065987189e38067015c95..e6b5a4bcab68b19ec95f109cec57348ab6f948c8 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -105,9 +105,9 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
 
 Node IntToBV::intToBV(TNode n, NodeMap& cache)
 {
-  int size = options::solveIntAsBV();
+  int size = options().smt.solveIntAsBV;
   AlwaysAssert(size > 0);
-  AlwaysAssert(!options::incrementalSolving());
+  AlwaysAssert(!options().base.incrementalSolving);
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 434256d280a8f78e21c8dbf7493c43108dd1b9cb..5f9b4fb1d8f2962c76c9a6d06c3363077e3fd3c7 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -97,7 +97,7 @@ Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion)
     Node result = ite_utils->simpITE(assertion);
     Node res_rewritten = rewrite(result);
 
-    if (options::simplifyWithCareEnabled())
+    if (options().smt.simplifyWithCareEnabled)
     {
       Chat() << "starting simplifyWithCare()" << endl;
       Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
@@ -119,7 +119,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
   bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic();
   if (simpDidALotOfWork)
   {
-    if (options::compressItes())
+    if (options().smt.compressItes)
     {
       result = d_iteUtilities.compress(assertionsToPreprocess);
     }
@@ -128,7 +128,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
     {
       // if false, don't bother to reclaim memory here.
       NodeManager* nm = NodeManager::currentNM();
-      if (nm->poolSize() >= options::zombieHuntThreshold())
+      if (nm->poolSize() >= options().smt.zombieHuntThreshold)
       {
         Chat() << "..ite simplifier did quite a bit of work.. "
                << nm->poolSize() << endl;
@@ -136,7 +136,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
                << " nodes before cleanup" << endl;
         d_iteUtilities.clear();
         d_env.getRewriter()->clearCaches();
-        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+        nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold);
         Chat() << "....node manager contains " << nm->poolSize()
                << " nodes after cleanup" << endl;
       }
@@ -145,7 +145,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
 
   // Do theory specific preprocessing passes
   if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH)
-      && !options::incrementalSolving())
+      && !options().base.incrementalSolving)
   {
     if (!simpDidALotOfWork)
     {

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 3ef4b7e9fc2684c9611c42a2be05f7471e2b573e..c40a65bc1e8db0b607f68bbd8c7590999ec4d84c 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -75,7 +75,7 @@ void traceBackToAssertions(booleans::CircuitPropagator* propagator,
 MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "miplib-trick")
 {
-  if (!options::incrementalSolving())
+  if (!options().base.incrementalSolving)
   {
     NodeManager::currentNM()->subscribeEvents(this);
   }
@@ -83,7 +83,7 @@ MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
 
 MipLibTrick::~MipLibTrick()
 {
-  if (!options::incrementalSolving())
+  if (!options().base.incrementalSolving)
   {
     NodeManager::currentNM()->unsubscribeEvents(this);
   }
@@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
 {
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          == assertionsToPreprocess->size());
-  Assert(!options::incrementalSolving());
+  Assert(!options().base.incrementalSolving);
 
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
@@ -586,7 +586,8 @@ PreprocessingPassResult MipLibTrick::applyInternal(
             Assert(top_level_substs.getSubstitution(newAssertion[0])
                    == newAssertion[1]);
           }
-          else if (pos.getNumChildren() <= options::arithMLTrickSubstitutions())
+          else if (pos.getNumChildren()
+                   <= options().arith.arithMLTrickSubstitutions)
           {
             top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]);
             Debug("miplib") << "addSubs: " << newAssertion[0] << " to "
@@ -596,8 +597,8 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           {
             Debug("miplib")
                 << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1]
-                << " (threshold is " << options::arithMLTrickSubstitutions()
-                << ")" << endl;
+                << " (threshold is "
+                << options().arith.arithMLTrickSubstitutions << ")" << endl;
           }
           newAssertion = rewrite(newAssertion);
           Debug("miplib") << "  " << newAssertion << endl;

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index c139f0a86a79d0c5cb2747ede116e0dacd6bacbe..68fb89e1f063274560d3cd6dd934c43888f9a6b7 100644 (file)
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -41,7 +41,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
   theory::SortInference* si =
       d_preprocContext->getTheoryEngine()->getSortInference();
 
-  if (options::sortInference())
+  if (options().smt.sortInference)
   {
     si->initialize(assertionsToPreprocess->ref());
     std::map<Node, Node> model_replace_f;
@@ -80,7 +80,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
   }
   // only need to compute monotonicity on the resulting formula if we are
   // using this option
-  if (options::ufssFairnessMonotone())
+  if (options().uf.ufssFairnessMonotone)
   {
     si->computeMonotonicity(assertionsToPreprocess->ref());
   }

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 81d5cae846c20cb740889d88d44b54594e969e56..a54d220e555e477a8602e3935b4ebfaf97d813c1 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -146,7 +146,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   Trace("srs-input") << "Make synth variables for types..." << std::endl;
   // We will generate a fixed number of variables per type. These are the
   // variables that appear as free variables in the rewrites we generate.
-  unsigned nvars = options::sygusRewSynthInputNVars();
+  unsigned nvars = options().quantifiers.sygusRewSynthInputNVars;
   // must have at least one variable per type
   nvars = nvars < 1 ? 1 : nvars;
   std::map<TypeNode, std::vector<Node> > tvars;
@@ -162,7 +162,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     // our input does not contain a Boolean variable, we need not allocate any
     // Boolean variables here.
     unsigned useNVars =
-        (options::sygusRewSynthInputUseBool() || !tn.isBoolean())
+        (options().quantifiers.sygusRewSynthInputUseBool || !tn.isBoolean())
             ? nvars
             : (hasBoolVar ? 1 : 0);
     for (unsigned i = 0; i < useNVars; i++)
@@ -276,7 +276,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     // we add variable constructors if we are not Boolean, we are interested
     // in purely propositional rewrites (via the option), or this term is
     // a Boolean variable.
-    if (!ctt.isBoolean() || options::sygusRewSynthInputUseBool()
+    if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool
         || ct.getKind() == BOUND_VARIABLE)
     {
       for (const Node& v : tvars[ctt])