Remove more static accesses to options (#7764)

This PR removes a bunch of the remaining places where options are accessed statically.

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 68e0f9a858b0f5f2e64be1af487f21ef0ddf71d9..419dda9e261985e9b67b01b3d1b500cf05e8f8a4 100644 (file)
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -52,7 +52,8 @@ UnsatCore::const_iterator UnsatCore::end() const {
 void UnsatCore::toStream(std::ostream& out) const {
   options::ioutils::Scope scope(out);
   options::ioutils::applyDagThresh(out, 0);
-  Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
+  auto language = options::ioutils::getOutputLang(out);
+  Printer::getPrinter(language)->toStream(out, *this);
 }
 
 std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 36f31eba9ed3c1f538f8d8bb297fe07f99880836..a82ab5e06d92097f76dd12a8a466136c31d7a4a9 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -145,12 +145,14 @@ class ScopedBool
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(cvc5::prop::TheoryProxy* proxy,
+Solver::Solver(Env& env,
+               cvc5::prop::TheoryProxy* proxy,
                cvc5::context::Context* context,
                cvc5::context::UserContext* userContext,
                ProofNodeManager* pnm,
                bool enableIncremental)
-    : d_proxy(proxy),
+    : EnvObj(env),
+      d_proxy(proxy),
       d_context(context),
       assertionLevel(0),
       d_pfManager(nullptr),
@@ -454,7 +456,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
       // If a literal is false at 0 level (both sat and user level) we also
       // ignore it, unless we are tracking the SAT solver's reasoning
       if (value(ps[i]) == l_False) {
-        if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0
+        if (!options().smt.unsatCores && !needProof() && level(var(ps[i])) == 0
             && user_level(var(ps[i])) == 0)
         {
           continue;
@@ -489,7 +491,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
-        if (options::unsatCores() || needProof())
+        if (options().smt.unsatCores || needProof())
         {
           // Take care of false units here; otherwise, we need to
           // construct the clause below to give to the proof manager
@@ -520,7 +522,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
         clauses_persistent.push(cr);
         attachClause(cr);
 
-        if (options::unsatCores() || needProof())
+        if (options().smt.unsatCores || needProof())
         {
           if (ps.size() == falseLiteralsCount)
           {
@@ -2043,7 +2045,7 @@ CRef Solver::updateLemmas() {
 
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
-        Assert(!options::unsatCores() && !needProof());
+        Assert(!options().smt.unsatCores && !needProof());
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -2189,8 +2191,8 @@ bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
 bool Solver::needProof() const
 {
   return isProofEnabled()
-         && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
-         && options::unsatCoresMode() != options::UnsatCoresMode::PP_ONLY;
+         && options().smt.unsatCoresMode != options::UnsatCoresMode::ASSUMPTIONS
+         && options().smt.unsatCoresMode != options::UnsatCoresMode::PP_ONLY;
 }
 
 }  // namespace Minisat

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index d0f5006e19424d4fa0e1f000faa2b5fc56009736..c5dc807ac4f25286020bcc76de8c73370ded0fbb 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -35,6 +35,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/utils/Options.h"
 #include "prop/sat_proof_manager.h"
+#include "smt/env_obj.h"
 #include "theory/theory.h"
 #include "util/resource_manager.h"
 
@@ -52,7 +53,8 @@ namespace Minisat {
 //=================================================================================================
 // Solver -- the main class:
 
-class Solver {
+class Solver : protected EnvObj
+{
   /** The only two cvc5 entry points to the private solver data */
   friend class cvc5::prop::PropEngine;
   friend class cvc5::prop::TheoryProxy;
@@ -128,7 +130,8 @@ public:
 
     // Constructor/Destructor:
     //
- Solver(cvc5::prop::TheoryProxy* proxy,
+ Solver(Env& env,
+        cvc5::prop::TheoryProxy* proxy,
         cvc5::context::Context* context,
         cvc5::context::UserContext* userContext,
         ProofNodeManager* pnm,
@@ -549,11 +552,8 @@ public:
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
-
 };
 
-
-
 //=================================================================================================
 // Implementation of inline methods:
 

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a681aa4f118a1e80319881f3ef0d368601f201fe..a8da077536d0cb7afa36820f1bfb10b4c67e9d83 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -121,7 +121,8 @@ void MinisatSatSolver::initialize(context::Context* context,
 
   // Create the solver
   d_minisat =
-      new Minisat::SimpSolver(theoryProxy,
+      new Minisat::SimpSolver(d_env,
+                              theoryProxy,
                               d_context,
                               userContext,
                               pnm,

diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 04db5e3cbc3a34431ddaa6c3684e08b50acb454f..32b0b736f340857a48d9d569c158e928f74688a8 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -48,25 +48,26 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
+SimpSolver::SimpSolver(Env& env,
+                       cvc5::prop::TheoryProxy* proxy,
                        cvc5::context::Context* context,
                        cvc5::context::UserContext* userContext,
                        ProofNodeManager* pnm,
                        bool enableIncremental)
-    : Solver(proxy, context, userContext, pnm, enableIncremental),
+    : Solver(env, proxy, context, userContext, pnm, enableIncremental),
       grow(opt_grow),
       clause_lim(opt_clause_lim),
       subsumption_lim(opt_subsumption_lim),
       simp_garbage_frac(opt_simp_garbage_frac),
       use_asymm(opt_use_asymm),
       // make sure this is not enabled if unsat cores or proofs are on
-      use_rcheck(opt_use_rcheck && !options::unsatCores() && !pnm),
-      use_elim(options::minisatUseElim() && !enableIncremental),
+      use_rcheck(opt_use_rcheck && !options().smt.unsatCores && !pnm),
+      use_elim(options().prop.minisatUseElim && !enableIncremental),
       merges(0),
       asymm_lits(0),
       eliminated_vars(0),
       elimorder(1),
-      use_simplification(!enableIncremental && !options::unsatCores()
+      use_simplification(!enableIncremental && !options().smt.unsatCores
                          && !pnm)  // TODO: turn off simplifications if
                                    // proofs are on initially
       ,
@@ -75,11 +76,12 @@ SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
       bwdsub_assigns(0),
       n_touched(0)
 {
-    if(options::minisatUseElim() &&
-       Options::current().prop.minisatUseElimWasSetByUser &&
-       enableIncremental) {
-        WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
-    }
+  if (options().prop.minisatUseElim && options().prop.minisatUseElimWasSetByUser
+      && enableIncremental)
+  {
+    WarningOnce() << "Incremental mode incompatible with --minisat-elim"
+                  << std::endl;
+  }
 
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
@@ -124,10 +126,11 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
 
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
-    if (options::minisatDumpDimacs()) {
-      toDimacs();
-      return l_Undef;
-    }
+  if (options().prop.minisatDumpDimacs)
+  {
+    toDimacs();
+    return l_Undef;
+  }
     Assert(decisionLevel() == 0);
 
     vec<Var> extra_frozen;

diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 5e218419ca872dafb07e7dd1f0d72774ada3a023..3d116d500209261a1c283c9044c664c042e1adca 100644 (file)
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -42,7 +42,8 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(cvc5::prop::TheoryProxy* proxy,
+  SimpSolver(Env& env,
+             cvc5::prop::TheoryProxy* proxy,
              cvc5::context::Context* context,
              cvc5::context::UserContext* userContext,
              ProofNodeManager* pnm,

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index eeca414e2b5d042ab0db9c6990fbb2e4b9e66301..df18f9a851dac4c5300b4b5d91638fbdecd7361c 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -65,10 +65,10 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te, Env& env)
-    : d_inCheckSat(false),
+PropEngine::PropEngine(Env& env, TheoryEngine* te)
+    : EnvObj(env),
+      d_inCheckSat(false),
       d_theoryEngine(te),
-      d_env(env),
       d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
@@ -83,7 +83,7 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
   ProofNodeManager* pnm = d_env.getProofNodeManager();
   ResourceManager* rm = d_env.getResourceManager();
 
-  options::DecisionMode dmode = options::decisionMode();
+  options::DecisionMode dmode = options().decision.decisionMode;
   if (dmode == options::DecisionMode::JUSTIFICATION
       || dmode == options::DecisionMode::STOPONLY)
   {
@@ -105,7 +105,7 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
   // CNF stream and theory proxy required pointers to each other, make the
   // theory proxy first
   d_theoryProxy = new TheoryProxy(
-      this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get(), d_env);
+      d_env, this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get());
   d_cnfStream = new CnfStream(d_satSolver,
                               d_theoryProxy,
                               userContext,
@@ -214,7 +214,7 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
 
   // do final checks on the lemmas we are about to send
   if (isProofEnabled()
-      && options::proofCheck() == options::ProofCheckMode::EAGER)
+      && options().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug
@@ -245,11 +245,8 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
   Node node = trn.getNode();
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
   bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
-  Assert(
-      !isProofEnabled() || trn.getGenerator() != nullptr
-      || options::unsatCores()
-      || (options::unsatCores()
-          && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF));
+  Assert(!isProofEnabled() || trn.getGenerator() != nullptr
+         || options().smt.unsatCores);
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
 }
 
@@ -257,7 +254,7 @@ void PropEngine::assertInternal(
     TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
 {
   // Assert as (possibly) removable
-  if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
+  if (options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS)
   {
     if (input)
     {
@@ -378,7 +375,8 @@ Result PropEngine::checkSat() {
   // Note this currently ignores conflicts (a dangerous practice).
   d_theoryProxy->presolve();
 
-  if(options::preprocessOnly()) {
+  if (options().base.preprocessOnly)
+  {
     return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
   }
 
@@ -673,7 +671,7 @@ bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
 
 void PropEngine::getUnsatCore(std::vector<Node>& core)
 {
-  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS);
   std::vector<SatLiteral> unsat_assumptions;
   d_satSolver->getUnsatAssumptions(unsat_assumptions);
   for (const SatLiteral& lit : unsat_assumptions)
@@ -684,7 +682,7 @@ void PropEngine::getUnsatCore(std::vector<Node>& core)
 
 std::shared_ptr<ProofNode> PropEngine::getRefutation()
 {
-  Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+  Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS);
   std::vector<Node> core;
   getUnsatCore(core);
   CDProof cdp(d_env.getProofNodeManager());

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2f569ba7255f808eda478e38703532637b0dcc35..da6a50b9ac2075be2ddab0144cfb97348a858a76 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "proof/trust_node.h"
 #include "prop/skolem_def_manager.h"
+#include "smt/env_obj.h"
 #include "theory/output_channel.h"
 #include "theory/skolem_lemma.h"
 #include "util/result.h"
@@ -51,13 +52,13 @@ class TheoryProxy;
  * PropEngine is the abstraction of a Sat Solver, providing methods for
  * solving the SAT problem and conversion to CNF (via the CnfStream).
  */
-class PropEngine
+class PropEngine : protected EnvObj
 {
  public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine* te, Env& env);
+  PropEngine(Env& env, TheoryEngine* te);
 
   /**
    * Destructor.
@@ -348,9 +349,6 @@ class PropEngine
   /** The theory engine we will be using */
   TheoryEngine* d_theoryEngine;
 
-  /** Reference to the environment */
-  Env& d_env;
-
   /** The decision engine we will be using */
   std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
 

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index ff00acc517da0cbda61c9781032b8496b270b0ed..269921da274638d1771781226095fb75b1bd22d8 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -33,20 +33,20 @@
 namespace cvc5 {
 namespace prop {
 
-TheoryProxy::TheoryProxy(PropEngine* propEngine,
+TheoryProxy::TheoryProxy(Env& env,
+                         PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          decision::DecisionEngine* decisionEngine,
-                         SkolemDefManager* skdm,
-                         Env& env)
-    : d_propEngine(propEngine),
+                         SkolemDefManager* skdm)
+    : EnvObj(env),
+      d_propEngine(propEngine),
       d_cnfStream(nullptr),
       d_decisionEngine(decisionEngine),
       d_dmNeedsActiveDefs(d_decisionEngine->needsActiveSkolemDefs()),
       d_theoryEngine(theoryEngine),
       d_queue(env.getContext()),
       d_tpp(env, *theoryEngine),
-      d_skdm(skdm),
-      d_env(env)
+      d_skdm(skdm)
 {
 }
 
@@ -120,7 +120,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   Node theoryExplanation = tte.getNode();
   if (d_env.isSatProofProducing())
   {
-    Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
+    Assert(options().smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF
            || tte.getGenerator());
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index d4f8fb3a2df924f1f95636db1311352db0923806..8e998583d06a9a733855e4e867da5ea44469ab68 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -25,6 +25,7 @@
 #include "proof/trust_node.h"
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
 #include "util/resource_manager.h"
@@ -47,14 +48,14 @@ class SkolemDefManager;
 /**
  * The proxy class that allows the SatSolver to communicate with the theories
  */
-class TheoryProxy : public Registrar
+class TheoryProxy : protected EnvObj, public Registrar
 {
  public:
-  TheoryProxy(PropEngine* propEngine,
+  TheoryProxy(Env& env,
+              PropEngine* propEngine,
               TheoryEngine* theoryEngine,
               decision::DecisionEngine* decisionEngine,
-              SkolemDefManager* skdm,
-              Env& env);
+              SkolemDefManager* skdm);
 
   ~TheoryProxy();
 
@@ -167,9 +168,6 @@ class TheoryProxy : public Registrar
 
   /** The skolem definition manager */
   SkolemDefManager* d_skdm;
-
-  /** Reference to the environment */
-  Env& d_env;
 }; /* class TheoryProxy */
 
 }  // namespace prop

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 5c427fa46aabf35e0aca2edc1992e809ceaf568c..69dddded80a811e65d7c69a447049e43d99fd1b4 100644 (file)
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -30,7 +30,8 @@ Model::Model(bool isKnownSat, const std::string& inputName)
 std::ostream& operator<<(std::ostream& out, const Model& m) {
   options::ioutils::Scope scope(out);
   options::ioutils::applyDagThresh(out, 0);
-  Printer::getPrinter(options::outputLanguage())->toStream(out, m);
+  auto language = options::ioutils::getOutputLang(out);
+  Printer::getPrinter(language)->toStream(out, m);
   return out;
 }
 

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 4530df774297ea66e72ec5d36e9a0e62454e7197..d9108a28cdc89ce1d85555ac4ed3bcad5f2321be 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -71,7 +71,7 @@ void SmtSolver::finishInit()
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
+  d_propEngine.reset(new prop::PropEngine(d_env, d_theoryEngine.get()));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -89,7 +89,7 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
+  d_propEngine.reset(new prop::PropEngine(d_env, d_theoryEngine.get()));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
@@ -164,7 +164,8 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
                  << rm->getTimeUsage() << ", resources "
                  << rm->getResourceUsage() << endl;
 
-  if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
+  if ((d_env.getOptions().smt.solveRealAsInt
+       || d_env.getOptions().smt.solveIntAsBV > 0)
       && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
     result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 0109649f00885d18f2471ea2ce4fecfbefcf636e..692fdc1b39bbfb20de1dd32ecf2b343c44cf5945 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -1017,7 +1017,7 @@ Node IntBlaster::createBVAndNode(Node x,
   {
     Assert(d_mode == options::SolveBVAsIntMode::BITWISE);
     // Enforce semantics over individual bits with iextract and ites
-    uint64_t granularity = options::BVAndIntegerGranularity();
+    uint64_t granularity = options().smt.BVAndIntegerGranularity;
 
     Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
     Node iAnd = d_nm->mkNode(kind::IAND, iAndOp, x, y);

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index be69617c79d44dba35b83d84c21fdd56b399bcc4..c9e08b7a8645b9d0d517f5f7af67ad3e4d71223c 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -67,8 +67,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
     }
     if( c[index].getType().isSort() ){
       //for star: check if all children are defined and have generalizations
-      if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
-        //check if all children exist and are complete
+      if (c[index] == st)
+      {  /// option fmfFmcCoverSimplify
+        // check if all children exist and are complete
         unsigned num_child_def =
             d_child.size() - (d_child.find(st) != d_child.end() ? 1 : 0);
         if (num_child_def == m->getRepSet()->getNumRepresentatives(tn))

diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp
index f4b52619a4fea33da4f5415d56e9b1502198c4a0..81ef84ae01a5bb8eafdb5995e6b805663609c1ec 100644 (file)
--- a/src/theory/quantifiers/instantiation_list.cpp
+++ b/src/theory/quantifiers/instantiation_list.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/instantiation_list.h"
 
 #include "options/base_options.h"
+#include "options/io_utils.h"
 #include "printer/printer.h"
 
 namespace cvc5 {
@@ -30,13 +31,15 @@ InstantiationVec::InstantiationVec(const std::vector<Node>& vec,
 void InstantiationList::initialize(Node q) { d_quant = q; }
 std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist)
 {
-  Printer::getPrinter(options::outputLanguage())->toStream(out, ilist);
+  auto language = options::ioutils::getOutputLang(out);
+  Printer::getPrinter(language)->toStream(out, ilist);
   return out;
 }
 
 std::ostream& operator<<(std::ostream& out, const SkolemList& skl)
 {
-  Printer::getPrinter(options::outputLanguage())->toStream(out, skl);
+  auto language = options::ioutils::getOutputLang(out);
+  Printer::getPrinter(language)->toStream(out, skl);
   return out;
 }
 

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9f7b270de0aac5f1820da848734a0578a982c1b9..9522a4b9b5d60c7b0ccecf58b814d74d00b7f17c 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1918,13 +1918,17 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
 
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
   bool performCheck = false;
-  if( options::quantConflictFind() && !d_conflict ){
+  if (options().quantifiers.quantConflictFind && !d_conflict)
+  {
     if( level==Theory::EFFORT_LAST_CALL ){
-      performCheck = options::qcfWhenMode() == options::QcfWhenMode::LAST_CALL;
+      performCheck =
+          options().quantifiers.qcfWhenMode == options::QcfWhenMode::LAST_CALL;
     }else if( level==Theory::EFFORT_FULL ){
-      performCheck = options::qcfWhenMode() == options::QcfWhenMode::DEFAULT;
+      performCheck =
+          options().quantifiers.qcfWhenMode == options::QcfWhenMode::DEFAULT;
     }else if( level==Theory::EFFORT_STANDARD ){
-      performCheck = options::qcfWhenMode() == options::QcfWhenMode::STD;
+      performCheck =
+          options().quantifiers.qcfWhenMode == options::QcfWhenMode::STD;
     }
   }
   return performCheck;
@@ -1943,7 +1947,7 @@ void QuantConflictFind::reset_round( Theory::Effort level ) {
     if (tdb->hasTermCurrent(r))
     {
       TypeNode rtn = r.getType();
-      if (!options::cegqi() || !TermUtil::hasInstConstAttr(r))
+      if (!options().quantifiers.cegqi || !TermUtil::hasInstConstAttr(r))
       {
         d_eqcs[rtn].push_back(r);
       }

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index d51cd9ab11083c73a45a03922cf1e9927cd21728..a1f1975962d9cfc047bd25caac1816db8fa07721 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -526,7 +526,7 @@ Node SynthConjectureProcess::postSimplify(Node q)
   Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl;
   Assert(q.getKind() == FORALL);
 
-  if (options::sygusArgRelevant())
+  if (options().quantifiers.sygusArgRelevant)
   {
     // initialize the information about each function to synthesize
     for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
@@ -586,7 +586,7 @@ void SynthConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
 
 bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i)
 {
-  if (!options::sygusArgRelevant())
+  if (!options().quantifiers.sygusArgRelevant)
   {
     return true;
   }

diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 5b26efef58293fd48d28bf917a7b4a852aa367d1..6b47969495e683b4b9ea18ed90af17022773e3a8 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -124,7 +124,7 @@ Result SynthVerify::verify(Node query,
       Trace("cegqi-debug") << "...squery : " << squery << std::endl;
       squery = rewrite(squery);
       Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
-      Assert(options::sygusRecFun()
+      Assert(options().quantifiers.sygusRecFun
              || (squery.isConst() && squery.getConst<bool>()));
     }
   }

diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index ab9d5f8450cb66531287a255ae1a22b49f5b8c18..043e8f5ed2b666498088e5ce81194c0a165f05db 100644 (file)
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -36,7 +36,7 @@ void SygusTemplateInfer::initialize(Node q)
   // We are processing without single invocation techniques, now check if
   // we should fix an invariant template (post-condition strengthening or
   // pre-condition weakening).
-  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
+  options::SygusInvTemplMode tmode = options().quantifiers.sygusInvTemplMode;
   if (tmode != options::SygusInvTemplMode::NONE)
   {
     // currently only works for single predicate synthesis
@@ -44,7 +44,7 @@ void SygusTemplateInfer::initialize(Node q)
     {
       tmode = options::SygusInvTemplMode::NONE;
     }
-    else if (!options::sygusInvTemplWhenSyntax())
+    else if (!options().quantifiers.sygusInvTemplWhenSyntax)
     {
       // only use invariant templates if no syntactic restrictions
       if (CegGrammarConstructor::hasSyntaxRestrictions(q))
@@ -106,7 +106,7 @@ void SygusTemplateInfer::initialize(Node q)
 
   // construct template
   Node templ;
-  if (options::sygusInvAutoUnfold())
+  if (options().quantifiers.sygusInvAutoUnfold)
   {
     if (d_ti.isComplete())
     {

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 83062ce480a8bdbcf27ca60bc0cd52231d22e11b..d444922597bfc35da501574bae81a4b8f5425627 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -405,10 +405,10 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       bool processChild = true;
       if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-        processChild =
-            options::userPatternsQuant() == options::UserPatMode::IGNORE
-                ? i == 1
-                : i >= 1;
+        processChild = options().quantifiers.userPatternsQuant
+                               == options::UserPatMode::IGNORE
+                           ? i == 1
+                           : i >= 1;
       }
       if( processChild ){
         children.push_back( n[i] );
@@ -672,10 +672,10 @@ Node SortInference::simplifyNode(
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       bool processChild = true;
       if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-        processChild =
-            options::userPatternsQuant() == options::UserPatMode::IGNORE
-                ? i == 1
-                : i >= 1;
+        processChild = options().quantifiers.userPatternsQuant
+                               == options::UserPatMode::IGNORE
+                           ? i == 1
+                           : i >= 1;
       }
       if( processChild ){
         if (isHandledApplyUf(n.getKind()))

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 6dcc0f72f70d325cbc1f878814110768a35d8c7a..2ebdf5a24c546552f7431b06b09dda1cb3f0aaa2 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -486,8 +486,7 @@ SortModel::SortModel(Env& env,
       d_initialized(thss->userContext(), false),
       d_c_dec_strat(nullptr)
 {
-
-  if (options::ufssMode() == options::UfssMode::FULL)
+  if (options().uf.ufssMode == options::UfssMode::FULL)
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
@@ -674,7 +673,7 @@ bool SortModel::areDisequal( Node a, Node b ) {
 
 void SortModel::check(Theory::Effort level)
 {
-  Assert(options::ufssMode() == options::UfssMode::FULL);
+  Assert(options().uf.ufssMode == options::UfssMode::FULL);
   if (!d_hasCard && d_state.isInConflict())
   {
     // not necessary to check
@@ -887,11 +886,11 @@ void SortModel::assertCardinality(uint32_t c, bool val)
         }
       }
       // we assert it positively, if its beyond the bound, abort
-      if (options::ufssAbortCardinality() >= 0
-          && c >= static_cast<uint32_t>(options::ufssAbortCardinality()))
+      if (options().uf.ufssAbortCardinality >= 0
+          && c >= static_cast<uint32_t>(options().uf.ufssAbortCardinality))
       {
         std::stringstream ss;
-        ss << "Maximum cardinality (" << options::ufssAbortCardinality()
+        ss << "Maximum cardinality (" << options().uf.ufssAbortCardinality
            << ")  for finite model finding exceeded." << std::endl;
         throw LogicException(ss.str());
       }