From c8887627fab0a7f8395bb6434b624df028b8ef46 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 1 Nov 2021 05:08:09 -0700 Subject: Replace more static options accesses (#7531) This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method. --- src/smt/interpolation_solver.cpp | 4 +- src/theory/combination_engine.cpp | 6 +-- src/theory/datatypes/sygus_extension.cpp | 55 +++++++++++--------- src/theory/model_manager.cpp | 4 +- .../quantifiers/candidate_rewrite_filter.cpp | 28 +++++----- .../quantifiers/cegqi/ceg_arith_instantiator.cpp | 37 ++++++------- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 18 ++++--- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 15 ++++-- src/theory/quantifiers/conjecture_generator.cpp | 60 +++++++++++++++------- src/theory/quantifiers/ematching/ho_trigger.cpp | 4 +- src/theory/quantifiers/equality_query.cpp | 22 +++++--- src/theory/quantifiers/instantiate.cpp | 23 ++++----- src/theory/quantifiers/sygus/sygus_interpol.cpp | 11 ++-- src/theory/quantifiers/sygus/synth_conjecture.cpp | 25 ++++----- src/theory/quantifiers/term_registry.cpp | 16 +++--- src/theory/quantifiers_engine.cpp | 24 +++++---- src/theory/theory.cpp | 2 +- src/theory/theory_engine.cpp | 10 ++-- src/theory/theory_model.cpp | 2 +- src/theory/theory_model_builder.cpp | 12 ++--- 20 files changed, 215 insertions(+), 163 deletions(-) diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 51be8db51..36f8e2a8d 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -41,7 +41,7 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, const TypeNode& grammarType, Node& interpol) { - if (options::produceInterpols() == options::ProduceInterpols::NONE) + if (options().smt.produceInterpols == options::ProduceInterpols::NONE) { const char* msg = "Cannot get interpolation when produce-interpol options is off."; @@ -57,7 +57,7 @@ bool InterpolationSolver::getInterpol(const std::vector& axioms, if (interpolSolver.solveInterpolation( name, axioms, conjn, grammarType, interpol)) { - if (options::checkInterpols()) + if (options().smt.checkInterpols) { checkInterpol(interpol, axioms, conj); } diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index dfa6d5da4..16f43966e 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -44,7 +44,7 @@ CombinationEngine::CombinationEngine(Env& env, : nullptr) { // create the equality engine, model manager, and shared solver - if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) + if (options().theory.eeMode == options::EqEngineMode::DISTRIBUTED) { // use the distributed shared solver d_sharedSolver.reset(new SharedSolverDistributed(env, d_te)); @@ -55,7 +55,7 @@ CombinationEngine::CombinationEngine(Env& env, d_mmanager.reset( new ModelManagerDistributed(env, d_te, *d_eemanager.get())); } - else if (options::eeMode() == options::EqEngineMode::CENTRAL) + else if (options().theory.eeMode == options::EqEngineMode::CENTRAL) { // for now, the shared solver is the same in both approaches; use the // distributed one for now @@ -70,7 +70,7 @@ CombinationEngine::CombinationEngine(Env& env, else { Unhandled() << "CombinationEngine::finishInit: equality engine mode " - << options::eeMode() << " not supported"; + << options().theory.eeMode << " not supported"; } } diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index d3e711c32..bacbf8c47 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -79,7 +79,8 @@ void SygusExtension::assertTester(int tindex, TNode n, Node exp) // check if parent is active bool do_add = true; - if( options::sygusSymBreakLazy() ){ + if (options().datatypes.sygusSymBreakLazy) + { if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){ NodeSet::const_iterator it = d_active_terms.find( n[0] ); if( it==d_active_terms.end() ){ @@ -120,7 +121,7 @@ void SygusExtension::assertFact(Node n, bool polarity) Node m = n[0]; Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl; registerMeasureTerm( m ); - if (options::sygusFair() == options::SygusFairMode::DT_SIZE) + if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE) { std::map>::iterator its = d_szinfo.find(m); @@ -231,7 +232,7 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) Assert(itsz != d_szinfo.end()); unsigned ssz = itsz->second->d_curr_search_size; - if (options::sygusFair() == options::SygusFairMode::DIRECT) + if (options().datatypes.sygusFair == options::SygusFairMode::DIRECT) { if( dt[tindex].getNumArgs()>0 ){ quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn); @@ -282,7 +283,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) unsigned d = d_term_to_depth[n]; Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl; //Assert( d<=ssz ); - if( options::sygusSymBreakLazy() ){ + if (options().datatypes.sygusSymBreakLazy) + { // dynamic symmetry breaking addSymBreakLemmasFor(ntn, n, d); } @@ -361,7 +363,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) // now activate the children those testers were previously asserted in this // context and are awaiting activation, if they exist. - if( options::sygusSymBreakLazy() ){ + if (options().datatypes.sygusSymBreakLazy) + { Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n"; for( unsigned j=0; jmkNode( @@ -379,7 +382,7 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp) } Node SygusExtension::getRelevancyCondition( Node n ) { - if (!options::sygusSymBreakRlv()) + if (!options().datatypes.sygusSymBreakRlv) { return Node::null(); } @@ -391,7 +394,8 @@ Node SygusExtension::getRelevancyCondition( Node n ) { TypeNode ntn = n[0].getType(); const DType& dt = ntn.getDType(); Node sel = n.getOperator(); - if( options::dtSharedSelectors() ){ + if (options().datatypes.dtSharedSelectors) + { std::vector< Node > disj; bool excl = false; for( unsigned i=0; imkNode( kind::AND, disj); } - }else{ + } + else + { int sindex = utils::cindexOf(sel); Assert(sindex != -1); cond = utils::mkTester(n[0], sindex, dt).negate(); @@ -597,7 +603,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, { Trace("sygus-sb-simple-debug") << " Size..." << std::endl; // fairness - if (options::sygusFair() == options::SygusFairMode::DT_SIZE + if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE && !isAnyConstant) { Node szl = nm->mkNode(DT_SIZE, n); @@ -685,7 +691,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, // if we are the "any constant" constructor, we do no symmetry breaking // only do simple symmetry breaking up to depth 2 - bool doSymBreak = options::sygusSymBreak(); + bool doSymBreak = options().datatypes.sygusSymBreak; if (isAnyConstant || depth > 2) { doSymBreak = false; @@ -961,7 +967,8 @@ void SygusExtension::registerSearchTerm(TypeNode tn, { Trace("sygus-sb-debug") << " register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl; sca.d_search_terms[tn][d].push_back(n); - if( !options::sygusSymBreakLazy() ){ + if (!options().datatypes.sygusSymBreakLazy) + { addSymBreakLemmasFor(tn, n, d); } } @@ -1060,7 +1067,7 @@ Node SygusExtension::registerSearchValue(Node a, { // Is it equivalent under examples? Node bvr_equiv; - if (aconj != nullptr && options::sygusSymBreakPbe()) + if (aconj != nullptr && options().datatypes.sygusSymBreakPbe) { // If the enumerator has examples, see if it is equivalent up to its // examples with a previous term. @@ -1097,7 +1104,7 @@ Node SygusExtension::registerSearchValue(Node a, } } - if (options::sygusRewVerify()) + if (options().quantifiers.sygusRewVerify) { if (bv != bvr) { @@ -1111,7 +1118,7 @@ Node SygusExtension::registerSearchValue(Node a, { smap[tn].reset(new quantifiers::SygusSampler(d_env)); smap[tn]->initializeSygus( - d_tds, nv, options::sygusSamples(), false); + d_tds, nv, options().quantifiers.sygusSamples, false); its = d_sampler[a].find(tn); } // check equivalent @@ -1220,7 +1227,7 @@ void SygusExtension::registerSymBreakLemma(TypeNode tn, { for (const Node& t : itt->second) { - if (!options::sygusSymBreakLazy() + if (!options().datatypes.sygusSymBreakLazy || d_active_terms.find(t) != d_active_terms.end()) { Node slem = lem.substitute(x, t); @@ -1360,11 +1367,11 @@ void SygusExtension::registerSizeTerm(Node e) d_szinfo[m]->d_anchors.push_back(e); d_anchor_to_measure_term[e] = m; NodeManager* nm = NodeManager::currentNM(); - if (options::sygusFair() == options::SygusFairMode::DT_SIZE) + if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE) { // update constraints on the measure term Node slem; - if (options::sygusFairMax()) + if (options().datatypes.sygusFairMax) { Node ds = nm->mkNode(DT_SIZE, e); slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue()); @@ -1490,7 +1497,7 @@ void SygusExtension::incrementCurrentSearchSize(TNode m) if( itt!=itc->second.d_search_terms[tn].end() ){ for (const Node& t : itt->second) { - if (!options::sygusSymBreakLazy() + if (!options().datatypes.sygusSymBreakLazy || (d_active_terms.find(t) != d_active_terms.end() && !s.second.empty())) { @@ -1598,7 +1605,7 @@ void SygusExtension::check() { isExc = false; //debugging : ensure fairness was properly handled - if (options::sygusFair() == options::SygusFairMode::DT_SIZE) + if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE) { Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog ); Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz); @@ -1617,7 +1624,7 @@ void SygusExtension::check() // register the search value ( prog -> progv ), this may invoke symmetry // breaking - if (!isExc && options::sygusSymBreakDynamic()) + if (!isExc && options().datatypes.sygusSymBreakDynamic) { bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); // check that it is unique up to theory-specific rewriting and @@ -1793,15 +1800,15 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s) { - if (options::sygusFair() == options::SygusFairMode::NONE) + if (options().datatypes.sygusFair == options::SygusFairMode::NONE) { return Node::null(); } - if (options::sygusAbortSize() != -1 - && static_cast(s) > options::sygusAbortSize()) + if (options().datatypes.sygusAbortSize != -1 + && static_cast(s) > options().datatypes.sygusAbortSize) { std::stringstream ss; - ss << "Maximum term size (" << options::sygusAbortSize() + ss << "Maximum term size (" << options().datatypes.sygusAbortSize << ") for enumerative SyGuS exceeded."; throw LogicException(ss.str()); } diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 23cd6430f..8c8d63231 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -34,7 +34,7 @@ ModelManager::ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem) d_modelEqualityEngine(nullptr), d_modelEqualityEngineAlloc(nullptr), d_model(new TheoryModel( - env, "DefaultModel", options::assignFunctionValues())), + env, "DefaultModel", options().theory.assignFunctionValues)), d_modelBuilder(nullptr), d_modelBuilt(false), d_modelBuiltSuccess(false) @@ -118,7 +118,7 @@ void ModelManager::postProcessModel(bool incomplete) Trace("model-builder") << "ModelManager: post-process model..." << std::endl; // model construction should always succeed unless lemmas were added AlwaysAssert(d_modelBuiltSuccess); - if (!options::produceModels()) + if (!options().smt.produceModels) { return; } diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index e856f1519..4f9a46181 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -73,15 +73,17 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) bool keep = true; // ----- check redundancy based on variables - if (options::sygusRewSynthFilterOrder() - || options::sygusRewSynthFilterNonLinear()) + if (options().quantifiers.sygusRewSynthFilterOrder + || options().quantifiers.sygusRewSynthFilterNonLinear) { - bool nor = d_ss->checkVariables(bn, - options::sygusRewSynthFilterOrder(), - options::sygusRewSynthFilterNonLinear()); - bool eqor = d_ss->checkVariables(beq_n, - options::sygusRewSynthFilterOrder(), - options::sygusRewSynthFilterNonLinear()); + bool nor = d_ss->checkVariables( + bn, + options().quantifiers.sygusRewSynthFilterOrder, + options().quantifiers.sygusRewSynthFilterNonLinear); + bool eqor = d_ss->checkVariables( + beq_n, + options().quantifiers.sygusRewSynthFilterOrder, + options().quantifiers.sygusRewSynthFilterNonLinear); Trace("cr-filter-debug") << "Variables ok? : " << nor << " " << eqor << std::endl; if (eqor || nor) @@ -118,7 +120,7 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) } // ----- check rewriting redundancy - if (keep && options::sygusRewSynthFilterCong()) + if (keep && options().quantifiers.sygusRewSynthFilterCong) { // When using sygus types, this filtering applies to the builtin versions // of n and eq_n. This means that we may filter out a rewrite rule for one @@ -135,7 +137,7 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) } } - if (keep && options::sygusRewSynthFilterMatch()) + if (keep && options().quantifiers.sygusRewSynthFilterMatch) { // ----- check matchable // check whether the pair is matchable with a previous one @@ -186,13 +188,13 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) beq_n = d_tds->sygusToBuiltin(eq_n); } // ----- check rewriting redundancy - if (options::sygusRewSynthFilterCong()) + if (options().quantifiers.sygusRewSynthFilterCong) { Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl; Assert(!d_drewrite->areEqual(bn, beq_n)); d_drewrite->addRewrite(bn, beq_n); } - if (options::sygusRewSynthFilterMatch()) + if (options().quantifiers.sygusRewSynthFilterMatch) { // cache based on the builtin type TypeNode tn = bn.getType(); @@ -258,7 +260,7 @@ bool CandidateRewriteFilter::notify(Node s, Node nrs = nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end()); bool areEqual = (nrs == d_curr_pair_rhs); - if (!areEqual && options::sygusRewSynthFilterCong()) + if (!areEqual && options().quantifiers.sygusRewSynthFilterCong) { // if dynamic rewriter is available, consult it areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs); diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 85e91fee3..163a49b8c 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -166,7 +166,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } // compute how many bounds we will consider unsigned rmax = 1; - if (atom.getKind() == EQUAL && (pol || !options::cegqiModel())) + if (atom.getKind() == EQUAL && (pol || !options().quantifiers.cegqiModel)) { rmax = 2; } @@ -205,7 +205,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { // disequalities are either strict upper or lower bounds bool is_upper; - if (options::cegqiModel()) + if (options().quantifiers.cegqiModel) { // disequality is a disjunction : only consider the bound in the // direction of the model @@ -272,7 +272,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, // take into account delta if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT) { - if (options::cegqiModel()) + if (options().quantifiers.cegqiModel) { Node delta_coeff = nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)); @@ -294,7 +294,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, uval = rewrite(uval); } } - if (options::cegqiModel()) + if (options().quantifiers.cegqiModel) { // just store bounds, will choose based on tighest bound unsigned index = isUpperBoundCTT(uires) ? 0 : 1; @@ -329,15 +329,15 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Node pv, CegInstEffort effort) { - if (!options::cegqiModel()) + if (!options().quantifiers.cegqiModel) { return false; } NodeManager* nm = NodeManager::currentNM(); - bool use_inf = - d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal(); + bool use_inf = d_type.isInteger() ? options().quantifiers.cegqiUseInfInt + : options().quantifiers.cegqiUseInfReal; bool upper_first = Random::getRandom().pickWithProb(0.5); - if (options::cegqiMinBounds()) + if (options().quantifiers.cegqiMinBounds) { upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size(); } @@ -369,7 +369,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cegqiMultiInst()) + else if (!options().quantifiers.cegqiMultiInst) { return false; } @@ -508,7 +508,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, best_used[rr] = best; // if using cbqiMidpoint, only add the instance based on one bound if // the bound is non-strict - if (!options::cegqiMidpoint() || d_type.isInteger() + if (!options().quantifiers.cegqiMidpoint || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull()) { Node val = d_mbp_bounds[rr][best]; @@ -531,7 +531,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cegqiMultiInst()) + else if (!options().quantifiers.cegqiMultiInst) { return false; } @@ -562,13 +562,13 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cegqiMultiInst()) + else if (!options().quantifiers.cegqiMultiInst) { return false; } } } - if (options::cegqiMidpoint() && !d_type.isInteger()) + if (options().quantifiers.cegqiMidpoint && !d_type.isInteger()) { Node vals[2]; bool bothBounds = true; @@ -633,7 +633,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cegqiMultiInst()) + else if (!options().quantifiers.cegqiMultiInst) { return false; } @@ -642,7 +642,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, // generally should not make it to this point, unless we are using a // non-monotonic selection function - if (!options::cegqiNopt()) + if (!options().quantifiers.cegqiNopt) { // if not trying non-optimal bounds, return return false; @@ -655,7 +655,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++) { if ((int)j != best_used[rr] - && (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull())) + && (!options().quantifiers.cegqiMidpoint + || d_mbp_vts_coeff[rr][1][j].isNull())) { Node val = getModelBasedProjectionValue(ci, pv, @@ -676,7 +677,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { return true; } - else if (!options::cegqiMultiInst()) + else if (!options().quantifiers.cegqiMultiInst) { return false; } @@ -748,7 +749,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( << "...bound type is : " << sf.d_props[index].d_type << std::endl; // intger division rounding up if from a lower bound if (sf.d_props[index].d_type == CEG_TT_UPPER - && options::cegqiRoundUpLowerLia()) + && options().quantifiers.cegqiRoundUpLowerLia) { sf.d_subs[index] = nm->mkNode( PLUS, diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index d61dd2bd2..28314c730 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -629,7 +629,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) // - the instantiator uses model values at this effort or // if we are solving for a subfield of a datatype (is_sv), and // - the instantiator allows model values. - if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv)) + if ((options().quantifiers.cegqiMultiInst || !hasTriedInstantiation(pv)) && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv) && vinst->allowModelValue(this, sf, pv, d_effort)) { @@ -677,7 +677,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl; Node pv_value; - if (options::cegqiModel()) + if (options().quantifiers.cegqiModel) { pv_value = getModelValue(pv); Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; @@ -730,7 +730,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options().quantifiers.cegqiMultiInst + && hasTriedInstantiation(pv)) { return false; } @@ -746,7 +747,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options().quantifiers.cegqiMultiInst + && hasTriedInstantiation(pv)) { return false; } @@ -817,7 +819,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options().quantifiers.cegqiMultiInst + && hasTriedInstantiation(pv)) { return false; } @@ -866,7 +869,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { lits.insert(lit); Node plit; - if (options::cegqiRepeatLit() || !isSolvedAssertion(lit)) + if (options().quantifiers.cegqiRepeatLit || !isSolvedAssertion(lit)) { plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort); } @@ -892,7 +895,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, { return true; } - else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv)) + else if (!options().quantifiers.cegqiMultiInst + && hasTriedInstantiation(pv)) { return false; } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 339524d94..6340e2a2a 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -63,12 +63,12 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, d_small_const(d_small_const_multiplier) { d_check_vts_lemma_lc = false; - if (options::cegqiBv()) + if (options().quantifiers.cegqiBv) { // if doing instantiation for BV, need the inverter class d_bv_invert.reset(new BvInverter); } - if (options::cegqiNestedQE()) + if (options().quantifiers.cegqiNestedQE) { d_nestedQe.reset(new NestedQe(d_env)); } @@ -225,7 +225,8 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) } //refinement: only consider innermost active quantified formulas - if( options::cegqiInnermost() ){ + if (options().quantifiers.cegqiInnermost) + { if( !d_children_quant.empty() && !d_active_quant.empty() ){ Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl; std::vector< Node > ninner; @@ -297,10 +298,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) bool InstStrategyCegqi::checkComplete(IncompleteId& incId) { - if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ + if ((!options().quantifiers.cegqiSat && d_cbqi_set_quant_inactive) + || d_incomplete_check) + { incId = IncompleteId::QUANTIFIERS_CEGQI; return false; - }else{ + } + else + { return true; } } diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index d778a679e..2c6419de1 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -279,7 +279,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) Assert(eqt.getType() == tn); registerPattern(eqt, tn); if (isUniversalLessThan(eqt, t) - || (options::conjectureUeeIntro() + || (options().quantifiers.conjectureUeeIntro && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt])) { setUniversalRelevant(eqt); @@ -344,12 +344,13 @@ bool ConjectureGenerator::needsCheck( Theory::Effort e ) { } bool ConjectureGenerator::hasEnumeratedUf( Node n ) { - if( options::conjectureGenGtEnum()>0 ){ + if (options().quantifiers.conjectureGenGtEnum > 0) + { std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() ); if( it==d_uf_enum.end() ){ d_uf_enum[n.getOperator()] = true; std::vector< Node > lem; - getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem ); + getEnumeratePredUfTerm(n, options().quantifiers.conjectureGenGtEnum, lem); if( !lem.empty() ){ for (const Node& l : lem) { @@ -665,7 +666,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) std::vector< TypeNode > rt_types; std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs; unsigned addedLemmas = 0; - unsigned maxDepth = options::conjectureGenMaxDepth(); + unsigned maxDepth = options().quantifiers.conjectureGenMaxDepth; for( unsigned depth=1; depth<=maxDepth; depth++ ){ Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl; Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl; @@ -676,7 +677,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) while( d_tge.getNextTerm() ){ //construct term Node nn = d_tge.getTerm(); - if( !options::conjectureFilterCanonical() || considerTermCanon( nn, true ) ){ + if (!options().quantifiers.conjectureFilterCanonical + || considerTermCanon(nn, true)) + { rel_term_count++; Trace("sg-rel-term") << "*** Relevant term : "; d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" ); @@ -771,7 +774,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) } } Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl; - }else{ + } + else + { Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl; } } @@ -827,7 +832,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) //consider against all LHS up to depth if( rdepth==depth ){ for( unsigned lhs_depth = 1; lhs_depth<=depth; lhs_depth++ ){ - if( (int)addedLemmas >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){ for( unsigned j=0; jsecond.size(); j++ ){ @@ -840,11 +847,13 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) } } } - if( (int)addedLemmas>=options::conjectureGenPerRound() ){ + if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound) + { break; } } - if( (int)addedLemmas>=options::conjectureGenPerRound() ){ + if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound) + { break; } } @@ -887,7 +896,8 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) { if( !d_waiting_conjectures_lhs.empty() ){ Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl; - if( (int)addedLemmas indices; for( unsigned i=0; i=options::conjectureGenPerRound() ){ + if ((int)addedLemmas + >= options().quantifiers.conjectureGenPerRound) + { break; } } @@ -1304,10 +1321,12 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { return -1; } } - //check if canonical representation (should be, but for efficiency this is not guarenteed) - //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){ - // Trace("sg-cconj") << " -> after processing, not canonical." << std::endl; - // return -1; + // check if canonical representation (should be, but for efficiency this is + // not guarenteed) if( options().quantifiers.conjectureFilterCanonical && ( + // getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs + // )!=rhs ) ){ + // Trace("sg-cconj") << " -> after processing, not canonical." << + // std::endl; return -1; //} int score; @@ -1315,7 +1334,8 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl; //find witness for counterexample, if possible - if( options::conjectureFilterModel() ){ + if (options().quantifiers.conjectureFilterModel) + { Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end()); Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl; std::map< TNode, TNode > subs; @@ -1342,7 +1362,9 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) { for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){ Trace("sg-cconj") << " #witnesses for " << it->first << " : " << it->second.size() << std::endl; } - }else{ + } + else + { score = 1; } diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index d2b0b0542..f6d245fd9 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -205,7 +205,7 @@ uint64_t HigherOrderTrigger::addInstantiations() bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) { - if (options::hoMatching()) + if (options().quantifiers.hoMatching) { // get substitution corresponding to m std::vector vars; @@ -342,7 +342,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) // value at this argument position d_arg_vector[vnum][index].push_back(bv_at_index); d_arg_vector[vnum][index].push_back(itf->second); - if (!options::hoMatchingVarArgPriority()) + if (!options().quantifiers.hoMatchingVarArgPriority) { std::reverse(d_arg_vector[vnum][index].begin(), d_arg_vector[vnum][index].end()); diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 30d223b2a..2c5dd73d1 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -51,7 +51,8 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) { Assert(q.isNull() || q.getKind() == FORALL); Node r = d_qstate.getRepresentative(a); - if( options::finiteModelFind() ){ + if (options().quantifiers.finiteModelFind) + { if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any if (d_model != nullptr) @@ -72,7 +73,7 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index) } } TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); - if (options::quantRepMode() == options::QuantRepMode::EE) + if (options().quantifiers.quantRepMode == options::QuantRepMode::EE) { int32_t score = getRepScore(r, q, index, v_tn); if (score >= 0) @@ -166,23 +167,28 @@ Node EqualityQuery::getInstance(Node n, //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) { - if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject + if (options().quantifiers.cegqi && quantifiers::TermUtil::hasInstConstAttr(n)) + { // reject return -2; - }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type + } + else if (!n.getType().isSubtypeOf(v_tn)) + { // reject if incorrect type return -2; - }else if( options::instMaxLevel()!=-1 ){ + } + else if (options().quantifiers.instMaxLevel != -1) + { //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ return n.getAttribute(InstLevelAttribute()); } - return options::instLevelInputOnly() ? -1 : 0; + return options().quantifiers.instLevelInputOnly ? -1 : 0; } - else if (options::quantRepMode() == options::QuantRepMode::FIRST) + else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST) { // score prefers earliest use of this term as a representative return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n]; } - Assert(options::quantRepMode() == options::QuantRepMode::DEPTH); + Assert(options().quantifiers.quantRepMode == options::QuantRepMode::DEPTH); return quantifiers::TermUtil::getTermDepth(n); } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f47a71926..23f789f4e 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -152,7 +152,7 @@ bool Instantiate::addInstantiation(Node q, << std::endl; bad_inst = true; } - else if (options::cegqi()) + else if (options().quantifiers.cegqi) { Node icf = TermUtil::getInstConstAttr(terms[i]); if (!icf.isNull()) @@ -198,7 +198,7 @@ bool Instantiate::addInstantiation(Node q, // lead to very small gains). // check for positive entailment - if (options::instNoEntail()) + if (options().quantifiers.instNoEntail) { // should check consistency of equality engine // (if not aborting on utility's reset) @@ -216,7 +216,7 @@ bool Instantiate::addInstantiation(Node q, } // check based on instantiation level - if (options::instMaxLevel() != -1) + if (options().quantifiers.instMaxLevel != -1) { TermDb* tdb = d_treg.getTermDatabase(); for (Node& t : terms) @@ -362,7 +362,7 @@ bool Instantiate::addInstantiation(Node q, } } } - if (options::instMaxLevel() != -1) + if (options().quantifiers.instMaxLevel != -1) { if (doVts) { @@ -447,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // check whether we are still redundant bool success = false; // check entailment, only if option is set - if (options::instNoEntail()) + if (options().quantifiers.instNoEntail) { Trace("inst-exp-fail") << " check entailment" << std::endl; success = echeck->isEntailed(q[1], subs, false, true); @@ -505,7 +505,7 @@ bool Instantiate::existsInstantiation(Node q, const std::vector& terms, bool modEq) { - if (options::incrementalSolving()) + if (options().base.incrementalSolving) { std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) @@ -593,7 +593,7 @@ Node Instantiate::getInstantiation(Node q, bool Instantiate::recordInstantiationInternal(Node q, const std::vector& terms) { - if (options::incrementalSolving()) + if (options().base.incrementalSolving) { Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl; @@ -612,7 +612,7 @@ bool Instantiate::recordInstantiationInternal(Node q, bool Instantiate::removeInstantiationInternal(Node q, const std::vector& terms) { - if (options::incrementalSolving()) + if (options().base.incrementalSolving) { std::map::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) @@ -637,8 +637,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector& qs) const void Instantiate::getInstantiationTermVectors( Node q, std::vector >& tvecs) { - - if (options::incrementalSolving()) + if (options().base.incrementalSolving) { std::map::const_iterator it = d_c_inst_match_trie.find(q); @@ -661,7 +660,7 @@ void Instantiate::getInstantiationTermVectors( void Instantiate::getInstantiationTermVectors( std::map > >& insts) { - if (options::incrementalSolving()) + if (options().base.incrementalSolving) { for (const auto& t : d_c_inst_match_trie) { @@ -709,7 +708,7 @@ void Instantiate::notifyEndRound() } if (d_env.isOutputOn(options::OutputTag::INST)) { - bool req = !options::printInstFull(); + bool req = !options().printer.printInstFull; for (std::pair& i : d_instDebugTemp) { Node name; diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 1a42ec337..3e1a5b34c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -99,21 +99,22 @@ void SygusInterpol::getIncludeCons( std::map>& result) { NodeManager* nm = NodeManager::currentNM(); - Assert(options::produceInterpols() != options::ProduceInterpols::NONE); + Assert(options().smt.produceInterpols != options::ProduceInterpols::NONE); // ASSUMPTIONS - if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS) + if (options().smt.produceInterpols == options::ProduceInterpols::ASSUMPTIONS) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); expr::getOperatorsMap(tmpAssumptions, result); } // CONJECTURE - else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE) + else if (options().smt.produceInterpols + == options::ProduceInterpols::CONJECTURE) { expr::getOperatorsMap(conj, result); } // SHARED - else if (options::produceInterpols() == options::ProduceInterpols::SHARED) + else if (options().smt.produceInterpols == options::ProduceInterpols::SHARED) { // Get operators from axioms std::map> include_cons_axioms; @@ -153,7 +154,7 @@ void SygusInterpol::getIncludeCons( } } // ALL - else if (options::produceInterpols() == options::ProduceInterpols::ALL) + else if (options().smt.produceInterpols == options::ProduceInterpols::ALL) { Node tmpAssumptions = (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms)); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 805f19b34..6c3f5e70b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -73,15 +73,16 @@ SynthConjecture::SynthConjecture(Env& env, d_repair_index(0), d_guarded_stream_exc(false) { - if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) + if (options().datatypes.sygusSymBreakPbe + || options().quantifiers.sygusUnifPbe) { d_modules.push_back(d_ceg_pbe.get()); } - if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE) + if (options().quantifiers.sygusUnifPi != options::SygusUnifPiMode::NONE) { d_modules.push_back(d_ceg_cegisUnif.get()); } - if (options::sygusCoreConnective()) + if (options().quantifiers.sygusCoreConnective) { d_modules.push_back(d_sygus_ccore.get()); } @@ -202,10 +203,10 @@ void SynthConjecture::assign(Node q) Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; // initialize the sygus constant repair utility - if (options::sygusRepairConst()) + if (options().quantifiers.sygusRepairConst) { d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); - if (options::sygusConstRepairAbort()) + if (options().quantifiers.sygusConstRepairAbort) { if (!d_sygus_rconst->isActive()) { @@ -337,7 +338,7 @@ bool SynthConjecture::doCheck() // sygusRepairConst is true, we use a default scheme for trying to repair // constants here. bool doRepairConst = - options::sygusRepairConst() && !d_master->usingRepairConst(); + options().quantifiers.sygusRepairConst && !d_master->usingRepairConst(); if (doRepairConst) { // have we tried to repair the previous solution? @@ -502,7 +503,7 @@ bool SynthConjecture::doCheck() } // if we trust the sampling we ran, we terminate now - if (options::cegisSample() == options::CegisSampleMode::TRUST) + if (options().quantifiers.cegisSample == options::CegisSampleMode::TRUST) { // we have that the current candidate passed a sample test // since we trust sampling in this mode, we assert there is no @@ -565,7 +566,7 @@ bool SynthConjecture::doCheck() // now mark that we have a solution d_hasSolution = true; - if (options::sygusStream()) + if (options().quantifiers.sygusStream) { // immediately print the current solution printAndContinueStream(terms, candidate_values); @@ -805,10 +806,10 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) bool is_unique_term = true; if (status != 0 - && (options::sygusRewSynth() + && (options().quantifiers.sygusRewSynth || options().quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE - || options::sygusFilterSolMode() + || options().quantifiers.sygusFilterSolMode != options::SygusFilterSolMode::NONE)) { Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; @@ -819,7 +820,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) d_exprm[prog].reset(new ExpressionMinerManager(d_env)); ExpressionMinerManager* emm = d_exprm[prog].get(); emm->initializeSygus( - d_tds, d_candidates[i], options::sygusSamples(), true); + d_tds, d_candidates[i], options().quantifiers.sygusSamples, true); emm->initializeMinersForOptions(); its = d_exprm.find(prog); } @@ -989,7 +990,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl; // if it was not embedded into the grammar - if (!options::sygusTemplEmbedGrammar()) + if (!options().quantifiers.sygusTemplEmbedGrammar) { TNode templa = d_templInfer->getTemplateArg(sf); // make the builtin version of the full solution diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index d11fb0b8d..5cefb4275 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -44,14 +44,15 @@ TermRegistry::TermRegistry(Env& env, d_sygusTdb(nullptr), d_qmodel(nullptr) { - if (options::sygus() || options::sygusInst()) + if (options().quantifiers.sygus || options().quantifiers.sygusInst) { // must be constructed here since it is required for datatypes finistInit d_sygusTdb.reset(new TermDbSygus(env, qs)); } Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") - << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; + << "Initialize model, mbqi : " << options().quantifiers.mbqiMode + << std::endl; } void TermRegistry::finishInit(FirstOrderModel* fm, @@ -69,7 +70,7 @@ void TermRegistry::presolve() { d_presolve = false; // add all terms to database - if (options::incrementalSolving() && !options::termDbCd()) + if (options().base.incrementalSolving && !options().quantifiers.termDbCd) { Trace("quant-engine-proc") << "Add presolve cache " << d_presolveCache.size() << std::endl; @@ -84,19 +85,20 @@ void TermRegistry::presolve() void TermRegistry::addTerm(Node n, bool withinQuant) { // don't add terms in quantifier bodies - if (withinQuant && !options::registerQuantBodyTerms()) + if (withinQuant && !options().quantifiers.registerQuantBodyTerms) { return; } - if (options::incrementalSolving() && !options::termDbCd()) + if (options().base.incrementalSolving && !options().quantifiers.termDbCd) { d_presolveCache.insert(n); } // only wait if we are doing incremental solving - if (!d_presolve || !options::incrementalSolving() || options::termDbCd()) + if (!d_presolve || !options().base.incrementalSolving + || options().quantifiers.termDbCd) { d_termDb->addTerm(n); - if (d_sygusTdb.get() && options::sygusEvalUnfold()) + if (d_sygusTdb.get() && options().quantifiers.sygusEvalUnfold) { d_sygusTdb->getEvalUnfold()->registerEvalTerm(n); } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e0863f953..1098cd9fe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -64,15 +64,15 @@ QuantifiersEngine::QuantifiersEngine( d_numInstRoundsLemma(0) { Trace("quant-init-debug") - << "Initialize model engine, mbqi : " << options::mbqiMode() << " " - << options::fmfBound() << std::endl; + << "Initialize model engine, mbqi : " << options().quantifiers.mbqiMode + << " " << options().quantifiers.fmfBound << std::endl; // Finite model finding requires specialized ways of building the model. // We require constructing the model here, since it is required for // initializing the CombinationEngine and the rest of quantifiers engine. - if (options::fmfBound() || options::stringExp() - || (options::finiteModelFind() - && (options::mbqiMode() == options::MbqiMode::FMC - || options::mbqiMode() == options::MbqiMode::TRUST))) + if (options().quantifiers.fmfBound || options().strings.stringExp + || (options().quantifiers.finiteModelFind + && (options().quantifiers.mbqiMode == options::MbqiMode::FMC + || options().quantifiers.mbqiMode == options::MbqiMode::TRUST))) { Trace("quant-init-debug") << "...make fmc builder." << std::endl; d_builder.reset( @@ -168,14 +168,15 @@ void QuantifiersEngine::ppNotifyAssertions( Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << std::endl; - if (options::instLevelInputOnly() && options::instMaxLevel() != -1) + if (options().quantifiers.instLevelInputOnly + && options().quantifiers.instMaxLevel != -1) { for (const Node& a : assertions) { quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0); } } - if (options::sygus()) + if (options().quantifiers.sygus) { quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get(); for (const Node& a : assertions) @@ -186,7 +187,7 @@ void QuantifiersEngine::ppNotifyAssertions( /* The SyGuS instantiation module needs a global view of all available * assertions to collect global terms that get added to each grammar. */ - if (options::sygusInst()) + if (options().quantifiers.sygusInst) { quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get(); si->ppNotifyAssertions(assertions); @@ -250,8 +251,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_qim.reset(); bool setIncomplete = false; IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS; - if (options::instMaxRounds() >= 0 - && d_numInstRoundsLemma >= static_cast(options::instMaxRounds())) + if (options().quantifiers.instMaxRounds >= 0 + && d_numInstRoundsLemma + >= static_cast(options().quantifiers.instMaxRounds)) { needsCheck = false; setIncomplete = true; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9844d13bc..cfa8f82cf 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -339,7 +339,7 @@ bool Theory::isLegalElimination(TNode x, TNode val) { return false; } - if (!options::produceModels() && !logicInfo().isQuantified()) + if (!options().smt.produceModels && !logicInfo().isQuantified()) { // Don't care about the model and logic is not quantified, we can eliminate. return true; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a186c05a0..03880bfbb 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -145,17 +145,17 @@ void TheoryEngine::finishInit() CVC5_FOR_EACH_THEORY; // Initialize the theory combination architecture - if (options::tcMode() == options::TcMode::CARE_GRAPH) + if (options().theory.tcMode == options::TcMode::CARE_GRAPH) { d_tc.reset(new CombinationCareGraph(d_env, *this, paraTheories)); } else { Unimplemented() << "TheoryEngine::finishInit: theory combination mode " - << options::tcMode() << " not supported"; + << options().theory.tcMode << " not supported"; } // create the relevance filter if any option requires it - if (options::relevanceFilter() || options::produceDifficulty()) + if (options().theory.relevanceFilter || options().smt.produceDifficulty) { d_relManager.reset(new RelevanceManager(userContext(), Valuation(this))); } @@ -247,7 +247,7 @@ TheoryEngine::TheoryEngine(Env& env) d_theoryOut[theoryId] = NULL; } - if (options::sortInference()) + if (options().smt.sortInference) { d_sortInfer.reset(new SortInference(env)); } @@ -633,7 +633,7 @@ TheoryModel* TheoryEngine::getBuiltModel() Assert(d_tc != nullptr); // If this method was called, we should be in SAT mode, and produceModels // should be true. - AlwaysAssert(options::produceModels()); + AlwaysAssert(options().smt.produceModels); if (!d_inSatMode) { // not available, perhaps due to interuption. diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a5ec0867a..599e192f8 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -143,7 +143,7 @@ Node TheoryModel::getValue(TNode n) const } else if (nn.getKind() == kind::LAMBDA) { - if (options::condenseFunctionValues()) + if (options().theory.condenseFunctionValues) { // normalize the body. Do not normalize the entire node, which // involves array normalization. diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index f50e7e0ee..71fe48de8 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -567,7 +567,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // finished traversing the equality engine TypeNode eqct = eqc.getType(); // count the number of equivalence classes of sorts in finite model finding - if (options::finiteModelFind()) + if (options().quantifiers.finiteModelFind) { if (eqct.isSort()) { @@ -660,7 +660,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) // then the type enumerator for list of U should enumerate: // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ... // instead of enumerating (cons U3 nil). - if (options::finiteModelFind()) + if (options().quantifiers.finiteModelFind) { tep.d_fixed_usort_card = true; for (std::map::iterator it = eqc_usort_count.begin(); @@ -847,7 +847,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } #ifdef CVC5_ASSERTIONS bool isUSortFiniteRestricted = false; - if (options::finiteModelFind()) + if (options().quantifiers.finiteModelFind) { isUSortFiniteRestricted = !t.isSort() && involvesUSort(t); } @@ -1080,7 +1080,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m) } Assert(m != nullptr); // debug-check the model if the checkModels() is enabled. - if (options::debugCheckModels()) + if (options().smt.debugCheckModels) { debugCheckModel(m); } @@ -1258,7 +1258,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) default_v = (*te); } ufmt.setDefaultValue(m, default_v); - bool condenseFuncValues = options::condenseFunctionValues(); + bool condenseFuncValues = options().theory.condenseFunctionValues; if (condenseFuncValues) { ufmt.simplify(); @@ -1389,7 +1389,7 @@ struct sortTypeSize void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) { - if (!options::assignFunctionValues()) + if (!options().theory.assignFunctionValues) { return; } -- cgit v1.2.3