From 932c33baa92bd45377b872eaec91b2c7721ff916 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 8 Nov 2021 17:00:35 -0800 Subject: [PATCH] Remove more static option accesses (#7582) This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers. --- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 26 ++++++++++------ .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 24 ++++++++------ src/theory/quantifiers/first_order_model.cpp | 2 +- .../quantifiers/fmf/bounded_integers.cpp | 9 ++++-- .../quantifiers/fmf/full_model_check.cpp | 11 ++++--- src/theory/quantifiers/fmf/model_builder.cpp | 6 ++-- src/theory/quantifiers/fun_def_evaluator.cpp | 2 +- .../quantifiers/inst_strategy_enumerative.cpp | 18 +++++------ src/theory/quantifiers/inst_strategy_pool.cpp | 2 +- src/theory/quantifiers/quant_split.cpp | 5 +-- .../quantifiers/quantifiers_registry.cpp | 4 +-- src/theory/quantifiers/query_generator.cpp | 6 ++-- src/theory/quantifiers/query_generator.h | 2 +- src/theory/quantifiers/skolemize.cpp | 4 +-- src/theory/quantifiers/solution_filter.cpp | 2 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.cpp | 6 ++-- src/theory/quantifiers/sygus/sygus_interpol.h | 4 +-- src/theory/quantifiers/sygus/sygus_pbe.cpp | 15 +++++---- .../quantifiers/sygus/sygus_repair_const.cpp | 11 +++---- .../quantifiers/sygus/sygus_unif_io.cpp | 2 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 4 +-- src/theory/quantifiers/sygus/synth_engine.cpp | 10 +++--- .../quantifiers/sygus/term_database_sygus.cpp | 16 +++++----- src/theory/quantifiers/sygus_inst.cpp | 10 +++--- src/theory/quantifiers/term_database.cpp | 26 +++++++++------- src/theory/quantifiers/term_database.h | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 4 +-- src/theory/sep/theory_sep.cpp | 22 ++++++++----- src/theory/strings/core_solver.cpp | 14 +++++---- src/theory/strings/extf_solver.cpp | 2 +- src/theory/strings/inference_manager.cpp | 6 ++-- src/theory/strings/regexp_solver.cpp | 8 ++--- src/theory/strings/term_registry.cpp | 6 ++-- src/theory/strings/theory_strings.cpp | 15 +++++---- src/theory/uf/cardinality_extension.cpp | 31 ++++++++++++------- src/theory/uf/cardinality_extension.h | 2 +- src/theory/uf/ho_extension.cpp | 2 +- src/theory/uf/theory_uf.cpp | 16 +++++----- 40 files changed, 205 insertions(+), 156 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 7362e1fba..5a0e8f597 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1794,7 +1794,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) void TheoryArrays::propagateRowLemma(RowLemmaType lem) { Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. " - "options::arraysPropagate() = " + "arraysPropagate = " << options().arrays.arraysPropagate << std::endl; TNode a, b, i, j; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1c6e3f0cb..055b06c47 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -109,7 +109,7 @@ void TheoryDatatypes::finishInit() // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here. // It also could make sense in practice to do congruence for APPLY_UF, but // this is not done. - if (getQuantifiersEngine() && options::sygus()) + if (getQuantifiersEngine() && options().quantifiers.sygus) { quantifiers::TermDbSygus* tds = getQuantifiersEngine()->getTermDatabaseSygus(); @@ -309,7 +309,9 @@ void TheoryDatatypes::postCheck(Effort level) } //if we want to force an assignment of constructors to all ground eqc //d_dtfCounter++; - if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){ + if (!needSplit && options().datatypes.dtForceAssignment + && d_dtfCounter % 2 == 0) + { Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl; needSplit = true; consIndex = fconsIndex!=-1 ? fconsIndex : consIndex; @@ -325,7 +327,8 @@ void TheoryDatatypes::postCheck(Effort level) Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl; }else{ Assert(consIndex != -1 || dt.isSygus()); - if( options::dtBinarySplit() && consIndex!=-1 ){ + if (options().datatypes.dtBinarySplit && consIndex != -1) + { Node test = utils::mkTester(n, consIndex, dt); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; test = rewrite(test); @@ -334,7 +337,9 @@ void TheoryDatatypes::postCheck(Effort level) Node lemma = nb; d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); d_im.requirePhase(test, true); - }else{ + } + else + { Trace("dt-split") << "*************Split for constructors on " << n << endl; Node lemma = utils::mkSplit(n, dt); Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; @@ -342,7 +347,8 @@ void TheoryDatatypes::postCheck(Effort level) InferenceId::DATATYPES_SPLIT, LemmaProperty::SEND_ATOMS); } - if( !options::dtBlastSplits() ){ + if (!options().datatypes.dtBlastSplits) + { break; } } @@ -454,7 +460,7 @@ void TheoryDatatypes::preRegisterTerm(TNode n) throw LogicException(ss.str()); } Trace("dt-expand") << "...well-founded ok" << std::endl; - if (!options::dtNestedRec()) + if (!options().datatypes.dtNestedRec) { if (dt.hasNestedRecursion()) { @@ -1474,7 +1480,7 @@ bool TheoryDatatypes::instantiate(EqcInfo* eqc, Node n) // regress0/datatypes/dt-param-card4-bool-sat.smt2 and // regress0/datatypes/list-bool.smt2). bool forceLemma; - if (options::dtPoliteOptimize()) + if (options().datatypes.dtPoliteOptimize) { forceLemma = dt[index].hasFiniteExternalArgType(ttn); } @@ -1499,7 +1505,8 @@ void TheoryDatatypes::checkCycles() { TypeNode tn = eqc.getType(); if( tn.isDatatype() ) { if( !tn.isCodatatype() ){ - if( options::dtCyclic() ){ + if (options().datatypes.dtCyclic) + { //do cycle checks std::map< TNode, bool > visited; std::map< TNode, bool > proc; @@ -1534,7 +1541,8 @@ void TheoryDatatypes::checkCycles() { } Trace("datatypes-cycle-check") << "Check uniqueness" << std::endl; //process codatatypes - if( cdt_eqc.size()>1 && options::cdtBisimilar() ){ + if (cdt_eqc.size() > 1 && options().datatypes.cdtBisimilar) + { printModelDebug("dt-cdt-debug"); Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl; std::vector< std::vector< Node > > part_out; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index d1ac87626..b5c4a94a0 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -91,8 +91,8 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Node sv = d_inverter->getSolveVariable(pv.getType()); Node pvs = ci->getModelValue(pv); Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl; - Node slit = - d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl()); + Node slit = d_inverter->getPathToPv( + lit, pv, sv, pvs, path, options().quantifiers.cegqiBvSolveNl); if (!slit.isNull()) { CegInstantiatorBvInverterQuery m(ci); @@ -154,7 +154,8 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, { return Node::null(); } - else if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::KEEP + else if (options().quantifiers.cegqiBvIneqMode + == options::CegqiBvIneqMode::KEEP || (pol && k == EQUAL)) { return lit; @@ -173,7 +174,8 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; Node ret; - if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::EQ_SLACK) + if (options().quantifiers.cegqiBvIneqMode + == options::CegqiBvIneqMode::EQ_SLACK) { // if using slack, we convert constraints to a positive equality based on // the current model M, e.g.: @@ -234,7 +236,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, { // if option enabled, use approach for word-level inversion for BV // instantiation - if (options::cegqiBv()) + if (options().quantifiers.cegqiBv) { // get the best rewritten form of lit for solving for pv // this should remove instances of non-invertible operators, and @@ -262,7 +264,7 @@ bool BvInstantiator::useModelValue(CegInstantiator* ci, Node pv, CegInstEffort effort) { - return effort < CEG_INST_EFFORT_FULL || options::cegqiFullEffort(); + return effort < CEG_INST_EFFORT_FULL || options().quantifiers.cegqiFullEffort; } bool BvInstantiator::processAssertions(CegInstantiator* ci, @@ -280,7 +282,8 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; // if interleaving, do not do inversion half the time - if (options::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5)) + if (options().quantifiers.cegqiBvInterleaveValue + && Random::getRandom().pickWithProb(0.5)) { Trace("cegqi-bv") << "...do not do instantiation for " << pv << " (skip, based on heuristic)" << std::endl; @@ -342,7 +345,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, // for constructing instantiations is exponential on the number of // variables in this quantifier prefix. bool ret = false; - bool tryMultipleInst = firstVar && options::cegqiMultiInst(); + bool tryMultipleInst = firstVar && options().quantifiers.cegqiMultiInst; bool revertOnSuccess = tryMultipleInst; for (unsigned j = 0, size = iti->second.size(); j < size; j++) { @@ -557,7 +560,8 @@ Node BvInstantiator::rewriteTermForSolvePv( bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); } - if (options::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) + if (options().quantifiers.cegqiBvLinearize && contains_pv[lhs] + && contains_pv[rhs]) { Node result = utils::normalizePvEqual(pv, children, contains_pv); if (!result.isNull()) @@ -575,7 +579,7 @@ Node BvInstantiator::rewriteTermForSolvePv( } else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_ADD) { - if (options::cegqiBvLinearize() && contains_pv[n]) + if (options().quantifiers.cegqiBvLinearize && contains_pv[n]) { Node result; if (n.getKind() == BITVECTOR_MULT) diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index cfd903646..1ccdd52e7 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -294,7 +294,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn) } else { - if (options::fmfFreshDistConst()) + if (options().quantifiers.fmfFreshDistConst) { mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn); } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 869fbcd21..26b526315 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -43,10 +43,13 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( d_range(r), d_ranges_proxied(userContext()) { - if( options::fmfBoundLazy() ){ + if (options().quantifiers.fmfBoundLazy) + { SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType()); - }else{ + } + else + { d_proxy_range = r; } if( !isProxy ){ @@ -323,7 +326,7 @@ void BoundedIntegers::checkOwnership(Node f) Trace("bound-int") << "check ownership quantifier " << f << std::endl; // determine if we should look at the quantified formula at all - if (!options::fmfBound()) + if (!options().quantifiers.fmfBound) { // only applying it to internal quantifiers QuantAttributes& qattr = d_qreg.getQuantAttributes(); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 94351274a..525db2726 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -626,7 +626,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i FirstOrderModelFmc* fmfmc = static_cast(fm); if (effort == 0) { - if (options::mbqiMode() == options::MbqiMode::NONE) + if (options().quantifiers.mbqiMode == options::MbqiMode::NONE) { // just exhaustive instantiate Node c = mkCondDefault(fmfmc, f); @@ -709,7 +709,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i d_star_insts[f].push_back(i); continue; } - if (options::fmfBound() || options::stringExp()) + if (options().quantifiers.fmfBound || options().strings.stringExp) { std::vector cond; cond.push_back(d_quant_cond[f]); @@ -735,7 +735,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; - if (d_qstate.isInConflict() || options::fmfOneInstPerRound()) + if (d_qstate.isInConflict() || options().quantifiers.fmfOneInstPerRound) { break; } @@ -888,7 +888,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; - if (d_qstate.isInConflict() || options::fmfOneInstPerRound()) + if (d_qstate.isInConflict() + || options().quantifiers.fmfOneInstPerRound) { break; } @@ -1368,7 +1369,7 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const bool FullModelChecker::useSimpleModels() { - return options::fmfFmcSimple(); + return options().quantifiers.fmfFmcSimple; } void FullModelChecker::registerQuantifiedFormula(Node q) { diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index f43b7a6c9..306c0c7ea 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -54,8 +54,8 @@ void QModelBuilder::finishInit() } bool QModelBuilder::optUseModel() { - return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound() - || options::stringExp(); + return options().quantifiers.mbqiMode != options::MbqiMode::NONE + || options().quantifiers.fmfBound || options().strings.stringExp; } bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { @@ -65,7 +65,7 @@ bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { d_addedLemmas = 0; d_triedLemmas = 0; - if (options::fmfFunWellDefinedRelevant()) + if (options().quantifiers.fmfFunWellDefinedRelevant) { //traverse equality engine std::map< TypeNode, bool > eqc_usort; diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 6f31273f0..27c11cca5 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -167,7 +167,7 @@ Node FunDefEvaluator::evaluateDefinitions(Node n) const itCount = funDefCount.find(f); } if (itf == d_funDefMap.end() - || itCount->second > options::sygusRecFunEvalLimit()) + || itCount->second > options().quantifiers.sygusRecFunEvalLimit) { Trace("fd-eval") << "FunDefEvaluator: " diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 6769d8bc2..7b87556a5 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -40,7 +40,7 @@ InstStrategyEnum::InstStrategyEnum(Env& env, } void InstStrategyEnum::presolve() { - d_fullSaturateLimit = options::fullSaturateLimit(); + d_fullSaturateLimit = options().quantifiers.fullSaturateLimit; } bool InstStrategyEnum::needsCheck(Theory::Effort e) { @@ -48,7 +48,7 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e) { return false; } - if (options::fullSaturateInterleave()) + if (options().quantifiers.fullSaturateInterleave) { // if interleaved, we run at the same time as E-matching if (d_qstate.getInstWhenNeedsCheck(e)) @@ -56,7 +56,7 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e) return true; } } - if (options::fullSaturateQuant()) + if (options().quantifiers.fullSaturateQuant) { if (e >= Theory::EFFORT_LAST_CALL) { @@ -73,12 +73,12 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) bool fullEffort = false; if (d_fullSaturateLimit != 0) { - if (options::fullSaturateInterleave()) + if (options().quantifiers.fullSaturateInterleave) { // we only add when interleaved with other strategies doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma(); } - if (options::fullSaturateQuant() && !doCheck) + if (options().quantifiers.fullSaturateQuant && !doCheck) { if (!d_qstate.getValuation().needCheck()) { @@ -99,7 +99,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl; } - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + unsigned rstart = options().quantifiers.fullSaturateQuantRd ? 0 : 1; unsigned rend = fullEffort ? 1 : rstart; unsigned addedLemmas = 0; // First try in relevant domain of all quantified formulas, if no @@ -138,7 +138,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) if (process(q, fullEffort, r == 0)) { // don't need to mark this if we are not stratifying - if (!options::fullSaturateStratify()) + if (!options().quantifiers.fullSaturateStratify) { alreadyProc[q] = true; } @@ -152,7 +152,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } } if (d_qstate.isInConflict() - || (addedLemmas > 0 && options::fullSaturateStratify())) + || (addedLemmas > 0 && options().quantifiers.fullSaturateStratify)) { // we break if we are in conflict, or if we added any lemma at this // effort level and we stratify effort levels. @@ -184,7 +184,7 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) TermTupleEnumeratorEnv ttec; ttec.d_fullEffort = fullEffort; - ttec.d_increaseSum = options::fullSaturateSum(); + ttec.d_increaseSum = options().quantifiers.fullSaturateSum; // make the enumerator, which is either relevant domain or term database // based on the flag isRd. std::unique_ptr enumerator( diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp index cadda033b..16152b50f 100644 --- a/src/theory/quantifiers/inst_strategy_pool.cpp +++ b/src/theory/quantifiers/inst_strategy_pool.cpp @@ -129,7 +129,7 @@ bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas) { TermTupleEnumeratorEnv ttec; ttec.d_fullEffort = true; - ttec.d_increaseSum = options::fullSaturateSum(); + ttec.d_increaseSum = options().quantifiers.fullSaturateSum; TermPools* tp = d_treg.getTermPools(); std::shared_ptr enumerator( mkTermTupleEnumeratorPool(q, &ttec, tp, p)); diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index d8b276ac9..55fa2a1e5 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -62,12 +62,13 @@ void QuantDSplit::checkOwnership(Node q) } else { - if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG) + if (options().quantifiers.quantDynamicSplit + == options::QuantDSplitMode::AGG) { // split if it is a finite datatype doSplit = isFinite; } - else if (options::quantDynamicSplit() + else if (options().quantifiers.quantDynamicSplit == options::QuantDSplitMode::DEFAULT) { if (!qbi.isFiniteBound(q, q[0][i])) diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 487bcc0fe..87a5eff4d 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -26,8 +26,8 @@ namespace quantifiers { QuantifiersRegistry::QuantifiersRegistry(Env& env) : QuantifiersUtil(env), d_quantAttr(), - d_quantBoundInf(options::fmfTypeCompletionThresh(), - options::finiteModelFind()), + d_quantBoundInf(options().quantifiers.fmfTypeCompletionThresh, + options().quantifiers.finiteModelFind), d_quantPreproc(env) { } diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index f7c9aa37b..c7cc6d442 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -147,13 +147,13 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out) void QueryGenerator::checkQuery(Node qy, unsigned spIndex) { // external query - if (options::sygusQueryGenDumpFiles() + if (options().quantifiers.sygusQueryGenDumpFiles == options::SygusQueryDumpFilesMode::ALL) { dumpQuery(qy, spIndex); } - if (options::sygusQueryGenCheck()) + if (options().quantifiers.sygusQueryGenCheck) { Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl; // make the satisfiability query @@ -177,7 +177,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) ss << "but cvc5 answered unsat!" << std::endl; AlwaysAssert(false) << ss.str(); } - if (options::sygusQueryGenDumpFiles() + if (options().quantifiers.sygusQueryGenDumpFiles == options::SygusQueryDumpFilesMode::UNSOLVED) { if (r.asSatisfiabilityResult().isSat() != Result::SAT) diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index 7738a4fe5..952966adc 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -40,7 +40,7 @@ namespace quantifiers { * In detail, given a stream of expressions t_1, ..., t_{n-1}, upon generating * term t_n, we consider a query (not) t_n = t_i to be an interesting query * if it is satisfied by at most D points, where D is a predefined threshold - * given by options::sygusQueryGenThresh(). If t_n has type Bool, we + * given by the sygusQueryGenThresh option. If t_n has type Bool, we * additionally consider the case where t_n is satisfied (or not satisfied) by * fewer than D points. * diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index ccd9afe3e..6dcb318f3 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -59,8 +59,8 @@ TrustNode Skolemize::process(Node q) } Node lem; ProofGenerator* pg = nullptr; - if (isProofEnabled() && !options::dtStcInduction() - && !options::intWfInduction()) + if (isProofEnabled() && !options().quantifiers.dtStcInduction + && !options().quantifiers.intWfInduction) { ProofNodeManager * pnm = d_env.getProofNodeManager(); // if using proofs and not using induction, we use the justified diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 19bfcab66..aead6784f 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -76,7 +76,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) } // check which solutions would have been filtered if the current had come // first - if (options::sygusFilterSolRevSubsume()) + if (options().quantifiers.sygusFilterSolRevSubsume) { std::vector nsubsume; for (const Node& s : d_curr_sols) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 42306383b..b60bc2736 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -416,7 +416,7 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( d_parent(parent) { d_initialized = false; - options::SygusUnifPiMode mode = options::sygusUnifPi(); + options::SygusUnifPiMode mode = options().quantifiers.sygusUnifPi; d_useCondPool = mode == options::SygusUnifPiMode::CENUM || mode == options::SygusUnifPiMode::CENUM_IGAIN; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 7d4434ddd..034f5f23c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -110,7 +110,8 @@ Node CegGrammarConstructor::process(Node q, Trace("cegqi") << "SynthConjecture : convert to deep embedding..." << std::endl; std::map> extra_cons; - if( options::sygusAddConstGrammar() ){ + if (options().quantifiers.sygusAddConstGrammar) + { Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl; collectTerms( q[1], extra_cons ); } @@ -194,7 +195,8 @@ Node CegGrammarConstructor::process(Node q, TNode templ_arg = itta->second; Assert(!templ_arg.isNull()); // if there is a template for this argument, make a sygus type on top of it - if( options::sygusTemplEmbedGrammar() ){ + if (options().quantifiers.sygusTemplEmbedGrammar) + { Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 924426365..4d3ae0219 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -116,7 +116,7 @@ class SygusInterpol : protected EnvObj * Get include_cons for mkSygusDefaultType. * mkSygusDefaultType() is a function to make default grammar. It has an * arguemnt include_cons, which will restrict what operators we want in the - * grammar. The return value depends on options::produceInterpols(). In + * grammar. The return value depends on the produceInterpols option. In * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE * option, it will return the operators from conj. In SHARED option, it will * return the oprators shared by axioms and conj. In ALL option, it will @@ -134,7 +134,7 @@ class SygusInterpol : protected EnvObj * Set up the grammar for the interpol-to-synthesis. * * The user-defined grammar will be encoded by itpGType. The options for - * grammar is given by options::produceInterpols(). In DEFAULT option, it will + * grammar is given by the produceInterpols option. In DEFAULT option, it will * set up the grammar from itpGType. And if itpGType is null, it will set up * the default grammar, which is built according to a policy handled by * getIncludeCons(). diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 453ac5c18..a012bc960 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -51,7 +51,7 @@ bool SygusPbe::initialize(Node conj, Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); - if (!options::sygusUnifPbe()) + if (!options().quantifiers.sygusUnifPbe) { // we are not doing unification return false; @@ -162,7 +162,10 @@ void SygusPbe::getTermList(const std::vector& candidates, } } -bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } +bool SygusPbe::allowPartialModel() +{ + return !options().quantifiers.sygusPbeMultiFair; +} bool SygusPbe::constructCandidates(const std::vector& enums, const std::vector& enum_values, @@ -194,13 +197,13 @@ bool SygusPbe::constructCandidates(const std::vector& enums, } } // Assume two enumerators of types T1 and T2. - // If options::sygusPbeMultiFair() is true, + // If the sygusPbeMultiFair option is true, // we ensure that all values of type T1 and size n are enumerated before // any term of type T2 of size n+d, and vice versa, where d is - // set by options::sygusPbeMultiFairDiff(). If d is zero, then our + // set by the sygusPbeMultiFairDiff option. If d is zero, then our // enumeration is such that all terms of T1 or T2 of size n are considered // before any term of size n+1. - int diffAllow = options::sygusPbeMultiFairDiff(); + int diffAllow = options().quantifiers.sygusPbeMultiFairDiff; std::vector enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { @@ -208,7 +211,7 @@ bool SygusPbe::constructCandidates(const std::vector& enums, { Assert(szs[i] >= min_term_size); int diff = szs[i] - min_term_size; - if (!options::sygusPbeMultiFair() || diff <= diffAllow) + if (!options().quantifiers.sygusPbeMultiFair || diff <= diffAllow) { enum_consider.push_back(i); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 44269eb6f..ddb46aec7 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -230,12 +230,11 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // make the satisfiability query std::unique_ptr repcChecker; // initialize the subsolver using the standard method - initializeSubsolver( - repcChecker, - d_env.getOptions(), - d_env.getLogicInfo(), - Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser, - options::sygusRepairConstTimeout()); + initializeSubsolver(repcChecker, + d_env.getOptions(), + d_env.getLogicInfo(), + options().quantifiers.sygusRepairConstTimeoutWasSetByUser, + options().quantifiers.sygusRepairConstTimeout); // renable options disabled by sygus repcChecker->setOption("miniscope-quant", "true"); repcChecker->setOption("miniscope-quant-fv", "true"); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index e703569d9..7aa952600 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -807,7 +807,7 @@ bool SygusUnifIo::constructSolution(std::vector& sols, Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) { Node c = d_candidate; - if (!d_solution.isNull() && !options::sygusStream()) + if (!d_solution.isNull() && !options().quantifiers.sygusStream) { // already has a solution return d_solution; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index b3033aedb..51804f0ce 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -52,7 +52,7 @@ void SygusUnifRl::initializeCandidate( // based on the strategy inferred for each function, determine if we are // using a unification strategy that is compatible our approach. StrategyRestrictions restrictions; - if (options::sygusBoolIteReturnConst()) + if (options().quantifiers.sygusBoolIteReturnConst) { restrictions.d_iteReturnBoolConst = true; } @@ -67,7 +67,7 @@ void SygusUnifRl::initializeCandidate( d_cand_to_hd_count[f] = 0; } // check whether we are using condition enumeration - options::SygusUnifPiMode mode = options::sygusUnifPi(); + options::SygusUnifPiMode mode = options().quantifiers.sygusUnifPi; d_useCondPool = mode == options::SygusUnifPiMode::CENUM || mode == options::SygusUnifPiMode::CENUM_IGAIN; d_useCondPoolIGain = mode == options::SygusUnifPiMode::CENUM_IGAIN; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 4bee80ab8..a98343bef 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -136,7 +136,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) void SynthEngine::assignConjecture(Node q) { Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl; - if (options::sygusQePreproc()) + if (options().quantifiers.sygusQePreproc) { Node lem = d_sqp.preprocess(q); if (!lem.isNull()) @@ -160,9 +160,9 @@ void SynthEngine::assignConjecture(Node q) void SynthEngine::checkOwnership(Node q) { // take ownership of quantified formulas with sygus attribute, and function - // definitions when options::sygusRecFun is true. + // definitions when the sygusRecFun option is true. QuantAttributes& qa = d_qreg.getQuantAttributes(); - if (qa.isSygus(q) || (qa.isFunDef(q) && options::sygusRecFun())) + if (qa.isSygus(q) || (qa.isFunDef(q) && options().quantifiers.sygusRecFun)) { d_qreg.setOwner(q, this, 2); } @@ -178,7 +178,7 @@ void SynthEngine::registerQuantifier(Node q) } if (d_qreg.getQuantAttributes().isFunDef(q)) { - Assert(options::sygusRecFun()); + Assert(options().quantifiers.sygusRecFun); // If it is a recursive function definition, add it to the function // definition evaluator class. Trace("cegqi") << "Registering function definition : " << q << "\n"; @@ -187,7 +187,7 @@ void SynthEngine::registerQuantifier(Node q) return; } Trace("cegqi") << "Register conjecture : " << q << std::endl; - if (options::sygusQePreproc()) + if (options().quantifiers.sygusQePreproc) { d_waiting_conj.push_back(q); } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 352ce9d88..cf024c59f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -458,7 +458,8 @@ void TermDbSygus::registerEnumerator(Node e, // determine if we are actively-generated bool isActiveGen = false; - if (options::sygusActiveGenMode() != options::SygusActiveGenMode::NONE) + if (options().quantifiers.sygusActiveGenMode + != options::SygusActiveGenMode::NONE) { if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED) { @@ -486,7 +487,8 @@ void TermDbSygus::registerEnumerator(Node e, { // If the enumerator is the single function-to-synthesize, if auto is // enabled, we infer whether it is better to enable active generation. - if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO) + if (options().quantifiers.sygusActiveGenMode + == options::SygusActiveGenMode::AUTO) { // We use active generation if the grammar of the enumerator does not // have ITE and does not have Boolean connectives. Experimentally, it @@ -497,7 +499,7 @@ void TermDbSygus::registerEnumerator(Node e, // sygus stream are to find many solutions to an easy problem, where // the bottleneck often becomes the large number of "exclude the current // solution" clauses. - if (options::sygusStream() + if (options().quantifiers.sygusStream || (!eti.hasIte() && !eti.hasBoolConnective())) { isActiveGen = true; @@ -518,7 +520,7 @@ void TermDbSygus::registerEnumerator(Node e, // Currently, actively-generated enumerators are either basic or variable // agnostic. bool isVarAgnostic = isActiveGen - && options::sygusActiveGenMode() + && options().quantifiers.sygusActiveGenMode == options::SygusActiveGenMode::VAR_AGNOSTIC; d_enum_var_agnostic[e] = isVarAgnostic; if (isVarAgnostic) @@ -752,7 +754,7 @@ Node TermDbSygus::rewriteNode(Node n) const // constant, we are done return res; } - if (options::sygusRecFun()) + if (options().quantifiers.sygusRecFun) { if (d_funDefEval->hasDefinitions()) { @@ -855,7 +857,7 @@ bool TermDbSygus::canConstructKind(TypeNode tn, } return true; } - if (!options::sygusSymBreakAgg()) + if (!options().datatypes.sygusSymBreakAgg) { return false; } @@ -989,7 +991,7 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, Assert(varlist.size() == args.size()); Node res; - if (tryEval && options::sygusEvalOpt()) + if (tryEval && options().quantifiers.sygusEvalOpt) { // Try evaluating, which is much faster than substitution+rewriting. // This may fail if there is a subterm of bn under the diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index d437bde8d..559119dfb 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -250,7 +250,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) TermDbSygus* db = d_treg.getTermDatabaseSygus(); SygusExplain syexplain(db); NodeManager* nm = NodeManager::currentNM(); - options::SygusInstMode mode = options::sygusInstMode(); + options::SygusInstMode mode = options().quantifiers.sygusInstMode; for (const Node& q : d_active_quant) { @@ -346,8 +346,8 @@ void SygusInst::registerQuantifier(Node q) std::unordered_set term_irrelevant; /* Collect relevant local ground terms for each variable type. */ - if (options::sygusInstScope() == options::SygusInstScope::IN - || options::sygusInstScope() == options::SygusInstScope::BOTH) + if (options().quantifiers.sygusInstScope == options::SygusInstScope::IN + || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH) { std::unordered_map> relevant_terms; for (const Node& var : q[0]) @@ -378,8 +378,8 @@ void SygusInst::registerQuantifier(Node q) } /* Collect relevant global ground terms for each variable type. */ - if (options::sygusInstScope() == options::SygusInstScope::OUT - || options::sygusInstScope() == options::SygusInstScope::BOTH) + if (options().quantifiers.sygusInstScope == options::SygusInstScope::OUT + || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH) { for (const Node& var : q[0]) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 225fe0bb1..2a16069f5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -43,7 +43,8 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) d_qim(nullptr), d_qreg(qr), d_termsContext(), - d_termsContextUse(options::termDbCd() ? context() : &d_termsContext), + d_termsContextUse(options().quantifiers.termDbCd ? context() + : &d_termsContext), d_processed(d_termsContextUse), d_typeMap(d_termsContextUse), d_ops(d_termsContextUse), @@ -53,7 +54,7 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) d_consistent_ee = true; d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - if (!options::termDbCd()) + if (!options().quantifiers.termDbCd) { // when not maintaining terms in a context-dependent manner, we clear during // each presolve, which requires maintaining a single outermost level @@ -162,7 +163,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable"); Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn << std::endl; - if (options::instMaxLevel() != -1) + if (options().quantifiers.instMaxLevel != -1) { QuantAttributes::setInstantiationLevelAttr(k, 0); } @@ -469,25 +470,27 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) { return d_has_map.find( n )!=d_has_map.end(); } //some assertions are not sent to EE - if (options::termDbMode() == options::TermDbMode::ALL) + if (options().quantifiers.termDbMode == options::TermDbMode::ALL) { return true; } - else if (options::termDbMode() == options::TermDbMode::RELEVANT) + else if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT) { return d_has_map.find( n )!=d_has_map.end(); } - Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode(); + Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " + << options().quantifiers.termDbMode; return false; } bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) { - if( options::instMaxLevel()!=-1 ){ + if (options().quantifiers.instMaxLevel != -1) + { if( n.hasAttribute(InstLevelAttribute()) ){ int64_t fml = f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f); - unsigned ml = fml>=0 ? fml : options::instMaxLevel(); + unsigned ml = fml >= 0 ? fml : options().quantifiers.instMaxLevel; if( n.getAttribute(InstLevelAttribute())>ml ){ Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute()); @@ -495,7 +498,8 @@ bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f) return false; } }else{ - if( options::instLevelInputOnly() ){ + if (options().quantifiers.instLevelInputOnly) + { Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl; return false; } @@ -566,7 +570,7 @@ void TermDb::setHasTerm( Node n ) { } void TermDb::presolve() { - if (options::incrementalSolving() && !options::termDbCd()) + if (options().base.incrementalSolving && !options().quantifiers.termDbCd) { d_termsContext.pop(); d_termsContext.push(); @@ -591,7 +595,7 @@ bool TermDb::reset( Theory::Effort effort ){ } //compute has map - if (options::termDbMode() == options::TermDbMode::RELEVANT) + if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT) { d_has_map.clear(); d_term_elig_eqc.clear(); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 0e5c7bc01..62b625846 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -198,7 +198,7 @@ class TermDb : public QuantifiersUtil { * It returns whether the term n should be indexed in the current context. * * If the argument useMode is true, then this method returns a value based on - * the option options::termDbMode(). + * the option termDbMode. * Otherwise, it returns the lookup in the map d_has_map. */ bool hasTermCurrent(Node n, bool useMode = true); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index bce827bbd..03e647947 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -54,7 +54,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, // post-construction. d_quantEngine = d_qengine.get(); - if (options::macrosQuant()) + if (options().quantifiers.macrosQuant) { d_qmacros.reset(new QuantifiersMacros(d_qreg)); } @@ -112,7 +112,7 @@ Theory::PPAssertStatus TheoryQuantifiers::ppAssert( if (d_qmacros != nullptr) { bool reqGround = - options::macrosQuantMode() != options::MacrosQuantMode::ALL; + options().quantifiers.macrosQuantMode != options::MacrosQuantMode::ALL; Node eq = d_qmacros->solve(tin.getProven(), reqGround); if (!eq.isNull()) { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 02a368f25..218c09804 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -661,11 +661,11 @@ void TheorySep::postCheck(Effort level) bool addedLemma = false; bool needAddLemma = false; // check negated star / positive wand - if (options::sepCheckNeg()) + if (options().sep.sepCheckNeg) { // get active labels std::map active_lbl; - if (options::sepMinimalRefine()) + if (options().sep.sepMinimalRefine) { for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { Node fact = (*i); @@ -1203,7 +1203,8 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { tn_is_monotonic = tn.getCardinality().isInfinite(); } //add a reference type for maximum occurrences of empty in a constraint - if( options::sepDisequalC() && tn_is_monotonic ){ + if (options().sep.sepDisequalC && tn_is_monotonic) + { for( unsigned r=0; r 1); conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) ); - if( options::sepChildRefine() ){ + if (options().sep.sepChildRefine) + { //child-specific refinements (TODO: use ?) for( unsigned i=0; i tchildren; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 0b7294f2c..3cf08a8d6 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1635,7 +1635,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, int32_t lentTestSuccess = -1; Node lenConstraint; - if (options::stringCheckEntailLen()) + if (options().strings.stringCheckEntailLen) { // If length entailment checks are enabled, we can save the case split by // inferring that `x` has to be longer than `y` or vice-versa. @@ -1784,11 +1784,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, TypeNode stype = veci[loop_index].getType(); - if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT) + if (options().strings.stringProcessLoopMode + == options::ProcessLoopMode::ABORT) { throw LogicException("Looping word equation encountered."); } - else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE + else if (options().strings.stringProcessLoopMode + == options::ProcessLoopMode::NONE || stype.isSequence()) { // note we cannot convert looping word equations into regular expressions if @@ -1932,12 +1934,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } else { - if (options::stringProcessLoopMode() + if (options().strings.stringProcessLoopMode == options::ProcessLoopMode::SIMPLE_ABORT) { throw LogicException("Normal looping word equation encountered."); } - else if (options::stringProcessLoopMode() + else if (options().strings.stringProcessLoopMode == options::ProcessLoopMode::SIMPLE) { d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP); @@ -2081,7 +2083,7 @@ void CoreSolver::processDeq(Node ni, Node nj) return; } - if (options::stringsDeqExt()) + if (options().strings.stringsDeqExt) { processDeqExtensionality(ni, nj); return; diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 6e2f60c6d..cbd67f232 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -325,7 +325,7 @@ void ExtfSolver::checkExtfEval(int effort) << " get symbolic definition..." << std::endl; Node nrs; // only use symbolic definitions if option is set - if (options::stringInferSym()) + if (options().strings.stringInferSym) { nrs = d_termReg.getSymbolicDefinition(sn, exps); } diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index ead18e823..277cc72e1 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -185,13 +185,13 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma) processConflict(ii); return; } - else if (asLemma || options::stringInferAsLemmas() || !ii.isFact()) + else if (asLemma || options().strings.stringInferAsLemmas || !ii.isFact()) { Trace("strings-infer-debug") << "...as lemma" << std::endl; addPendingLemma(std::unique_ptr(new InferInfo(ii))); return; } - if (options::stringInferSym()) + if (options().strings.stringInferSym) { std::vector unproc; for (const Node& ac : ii.d_premises) @@ -325,7 +325,7 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) utils::flattenOp(AND, ec, exp); } std::vector noExplain; - if (!options::stringRExplainLemmas()) + if (!options().strings.stringRExplainLemmas) { // if we aren't regressing the explanation, we add all literals to // noExplain and ignore ii.d_ant. diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 898c0f1b7..050ec594a 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -247,7 +247,7 @@ void RegExpSolver::check(const std::map >& mems) } else { - if (!options::stringExp()) + if (!options().strings.stringExp) { throw LogicException( "Strings Incomplete (due to Negative Membership) by default, " @@ -413,7 +413,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector& mems) bool RegExpSolver::checkEqcIntersect(const std::vector& mems) { // do not compute intersections if the re intersection mode is none - if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE) + if (options().strings.stringRegExpInterMode == options::RegExpInterMode::NONE) { return true; } @@ -436,7 +436,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) } RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]); if (rct == RE_C_VARIABLE - || (options::stringRegExpInterMode() + || (options().strings.stringRegExpInterMode == options::RegExpInterMode::CONSTANT && rct != RE_C_CONRETE_CONSTANT)) { @@ -444,7 +444,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) // on option. continue; } - if (options::stringRegExpInterMode() + if (options().strings.stringRegExpInterMode == options::RegExpInterMode::ONE_CONSTANT) { if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT) diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 61fe786d6..1124be488 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -147,7 +147,7 @@ void TermRegistry::preRegisterTerm(TNode n) << "TheoryString::preregister : " << n << std::endl; // check for logic exceptions Kind k = n.getKind(); - if (!options::stringExp()) + if (!options().strings.stringExp) { if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS || k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR @@ -259,7 +259,7 @@ void TermRegistry::preRegisterTerm(TNode n) { d_functionsTerms.push_back(n); } - if (options::stringFMF()) + if (options().strings.stringFMF) { if (tn.isStringLike()) { @@ -289,7 +289,7 @@ void TermRegistry::registerTerm(Node n, int effort) TypeNode tn = n.getType(); if (!tn.isStringLike()) { - if (options::stringEagerLen()) + if (options().strings.stringEagerLen) { do_register = effort == 0; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e0f0a8dac..799becd29 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -78,7 +78,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_statistics), d_rsolver( env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics), - d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()), + d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()), d_stringsFmf(env, valuation, d_termReg) { d_termReg.finishInit(&d_im); @@ -123,7 +123,7 @@ void TheoryStrings::finishInit() // witness is used to eliminate str.from_code d_valuation.setUnevaluatedKind(WITNESS); - bool eagerEval = options::stringEagerEval(); + bool eagerEval = options().strings.stringEagerEval; // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval); @@ -186,11 +186,13 @@ TrustNode TheoryStrings::explain(TNode literal) } void TheoryStrings::presolve() { - Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl; + Debug("strings-presolve") + << "TheoryStrings::Presolving : get fmf options " + << (options().strings.stringFMF ? "true" : "false") << std::endl; d_strat.initializeStrategy(); // if strings fmf is enabled, register the strategy - if (options::stringFMF()) + if (options().strings.stringFMF) { d_stringsFmf.presolve(); // This strategy is local to a check-sat call, since we refresh the strategy @@ -721,7 +723,8 @@ void TheoryStrings::postCheck(Effort e) } bool TheoryStrings::needsCheckLastEffort() { - if( options::stringGuessModel() ){ + if (options().strings.stringGuessModel) + { return d_esolver.hasExtendedFunctions(); } return false; @@ -1015,7 +1018,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector& lems) } TrustNode ret; Node atomRet = atom; - if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) + if (options().strings.regExpElim && atom.getKind() == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership ret = d_regexp_elim.eliminateTrusted(atomRet); diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index a25a2f470..9fc2915bf 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1243,7 +1243,8 @@ CardinalityExtension::CardinalityExtension(Env& env, d_min_pos_tn_master_card_set(context(), false), d_rel_eqc(context()) { - if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness()) + if (options().uf.ufssMode == options::UfssMode::FULL + && options().uf.ufssFairness) { // Register the strategy with the decision manager of the theory. // We are guaranteed that the decision manager is ready since we @@ -1339,7 +1340,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; - if (options::ufssMode() == options::UfssMode::FULL) + if (options().uf.ufssMode == options::UfssMode::FULL) { if( lit.getKind()==CARDINALITY_CONSTRAINT ){ const CardinalityConstraint& cc = @@ -1350,7 +1351,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) uint32_t nCard = cc.getUpperBound().getUnsignedInt(); Trace("uf-ss-debug") << "...check cardinality constraint : " << tn << std::endl; - if (options::ufssFairnessMonotone()) + if (options().uf.ufssFairnessMonotone) { SortInference* si = d_state.getSortInference(); Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl; @@ -1487,7 +1488,7 @@ void CardinalityExtension::check(Theory::Effort level) } if (!d_state.isInConflict()) { - if (options::ufssMode() == options::UfssMode::FULL) + if (options().uf.ufssMode == options::UfssMode::FULL) { Trace("uf-ss-solver") << "CardinalityExtension: check " << level << std::endl; @@ -1516,7 +1517,7 @@ void CardinalityExtension::check(Theory::Effort level) } } } - else if (options::ufssMode() == options::UfssMode::NO_MINIMAL) + else if (options().uf.ufssMode == options::UfssMode::NO_MINIMAL) { if( level==Theory::EFFORT_FULL ){ // split on an equality between two equivalence classes (at most one per type) @@ -1590,7 +1591,7 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const void CardinalityExtension::preRegisterTerm(TNode n) { - if (options::ufssMode() != options::UfssMode::FULL) + if (options().uf.ufssMode != options::UfssMode::FULL) { return; } @@ -1699,17 +1700,21 @@ void CardinalityExtension::initializeCombinedCardinality() /** check */ void CardinalityExtension::checkCombinedCardinality() { - Assert(options::ufssMode() == options::UfssMode::FULL); - if( options::ufssFairness() ){ + Assert(options().uf.ufssMode == options::UfssMode::FULL); + if (options().uf.ufssFairness) + { Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; uint32_t totalCombinedCard = 0; uint32_t maxMonoSlave = 0; TypeNode maxSlaveType; for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ uint32_t max_neg = it->second->getMaximumNegativeCardinality(); - if( !options::ufssFairnessMonotone() ){ + if (!options().uf.ufssFairnessMonotone) + { totalCombinedCard += max_neg; - }else{ + } + else + { std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first ); if( its==d_tn_mono_slave.end() || !its->second ){ totalCombinedCard += max_neg; @@ -1722,7 +1727,8 @@ void CardinalityExtension::checkCombinedCardinality() } } Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl; - if( options::ufssFairnessMonotone() ){ + if (options().uf.ufssFairnessMonotone) + { Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl; if (!d_min_pos_tn_master_card_set.get() && maxMonoSlave > d_min_pos_tn_master_card.get()) @@ -1751,7 +1757,8 @@ void CardinalityExtension::checkCombinedCardinality() for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ bool doAdd = true; - if( options::ufssFairnessMonotone() ){ + if (options().uf.ufssFairnessMonotone) + { std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first ); if( its!=d_tn_mono_slave.end() && its->second ){ diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 4b989a166..7a6d44ee9 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -426,7 +426,7 @@ class CardinalityExtension : protected EnvObj /** * Decision strategy for combined cardinality constraints. This asserts * the minimal combined cardinality constraint positively in the SAT - * context. It is enabled by options::ufssFairness(). For details, see + * context. It is enabled by the ufssFairness option. For details, see * the extension to multiple sorts in Section 6.3 of Reynolds et al, * "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017. */ diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 2702d6d24..96029eab8 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -231,7 +231,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) } ++eqcs_i; } - if (!options::ufHoExt()) + if (!options().uf.ufHoExt) { // we are not applying extensionality, thus we are incomplete if functions // are present diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a7b8d7ad7..5c9446507 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -71,8 +71,8 @@ bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; esi.d_name = d_instanceName + "theory::uf::ee"; - if (options::finiteModelFind() - && options::ufssMode() != options::UfssMode::NONE) + if (options().quantifiers.finiteModelFind + && options().uf.ufssMode != options::UfssMode::NONE) { // need notifications about sorts esi.d_notifyNewClass = true; @@ -88,9 +88,9 @@ void TheoryUF::finishInit() { d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); // Initialize the cardinality constraints solver if the logic includes UF, // finite model finding is enabled, and it is not disabled by - // options::ufssMode(). - if (options::finiteModelFind() - && options::ufssMode() != options::UfssMode::NONE) + // the ufssMode option. + if (options().quantifiers.finiteModelFind + && options().uf.ufssMode != options::UfssMode::NONE) { d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this)); } @@ -352,7 +352,8 @@ void TheoryUF::presolve() { // TimerStat::CodeTimer codeTimer(d_presolveTimer); Debug("uf") << "uf: begin presolve()" << endl; - if(options::ufSymmetryBreaker()) { + if (options().uf.ufSymmetryBreaker) + { vector newClauses; d_symb.apply(newClauses); for(vector::const_iterator i = newClauses.begin(); @@ -486,7 +487,8 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned) } } - if(options::ufSymmetryBreaker()) { + if (options().uf.ufSymmetryBreaker) + { d_symb.assertFormula(n); } } /* TheoryUF::ppStaticLearn() */ -- 2.30.2