From 099043243897f4d216224e7be652a00a81e9bb6c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 7 Dec 2021 15:47:15 -0800 Subject: [PATCH] Remove more static accesses to options (#7764) This PR removes a bunch of the remaining places where options are accessed statically. --- src/proof/unsat_core.cpp | 3 +- src/prop/minisat/core/Solver.cc | 18 ++++++----- src/prop/minisat/core/Solver.h | 10 +++--- src/prop/minisat/minisat.cpp | 3 +- src/prop/minisat/simp/SimpSolver.cc | 31 ++++++++++--------- src/prop/minisat/simp/SimpSolver.h | 3 +- src/prop/prop_engine.cpp | 28 ++++++++--------- src/prop/prop_engine.h | 8 ++--- src/prop/theory_proxy.cpp | 14 ++++----- src/prop/theory_proxy.h | 12 +++---- src/smt/model.cpp | 3 +- src/smt/smt_solver.cpp | 7 +++-- src/theory/bv/int_blaster.cpp | 2 +- .../quantifiers/fmf/full_model_check.cpp | 5 +-- src/theory/quantifiers/instantiation_list.cpp | 7 +++-- .../quantifiers/quant_conflict_find.cpp | 14 ++++++--- .../quantifiers/sygus/sygus_process_conj.cpp | 4 +-- src/theory/quantifiers/sygus/synth_verify.cpp | 2 +- .../quantifiers/sygus/template_infer.cpp | 6 ++-- src/theory/sort_inference.cpp | 16 +++++----- src/theory/uf/cardinality_extension.cpp | 11 +++---- 21 files changed, 109 insertions(+), 98 deletions(-) diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 68e0f9a85..419dda9e2 100644 --- 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 36f31eba9..a82ab5e06 100644 --- 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& 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& 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& 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 d0f5006e1..c5dc807ac 100644 --- 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 a681aa4f1..a8da07753 100644 --- 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 04db5e3cb..32b0b736f 100644 --- 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 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 extra_frozen; diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 5e218419c..3d116d500 100644 --- 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 eeca414e2..df18f9a85 100644 --- 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& core) { - Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); + Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS); std::vector unsat_assumptions; d_satSolver->getUnsatAssumptions(unsat_assumptions); for (const SatLiteral& lit : unsat_assumptions) @@ -684,7 +682,7 @@ void PropEngine::getUnsatCore(std::vector& core) std::shared_ptr PropEngine::getRefutation() { - Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS); + Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS); std::vector core; getUnsatCore(core); CDProof cdp(d_env.getProofNodeManager()); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 2f569ba72..da6a50b9a 100644 --- 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 d_decisionEngine; diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index ff00acc51..269921da2 100644 --- 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 d4f8fb3a2..8e998583d 100644 --- 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 5c427fa46..69dddded8 100644 --- 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 4530df774..d9108a28c 100644 --- 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 0109649f0..692fdc1b3 100644 --- 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 be69617c7..c9e08b7a8 100644 --- 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 f4b52619a..81ef84ae0 100644 --- 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& 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 9f7b270de..9522a4b9b 100644 --- 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 d51cd9ab1..a1f197596 100644 --- 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& 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 5b26efef5..6b4796949 100644 --- 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())); } } diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index ab9d5f845..043e8f5ed 100644 --- 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 83062ce48..d44492259 100644 --- 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= 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= 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 6dcc0f72f..2ebdf5a24 100644 --- 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(options::ufssAbortCardinality())) + if (options().uf.ufssAbortCardinality >= 0 + && c >= static_cast(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()); } -- 2.30.2