From: Gereon Kremer Date: Thu, 3 Feb 2022 19:57:41 +0000 (-0800) Subject: Replace a some more static options (#8042) X-Git-Tag: cvc5-1.0.0~459 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e032de7a66f789cdbe7ae964428ca5207ac89a07;p=cvc5.git Replace a some more static options (#8042) We now have access to the options in a few more places in quantifiers. --- diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 1adf50ddd..8392cd493 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -660,7 +660,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Env& env, Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl; Node x; - if (options::purifyTriggers()) + if (env.getOptions().quantifiers.purifyTriggers) { Node xi = PatternTermSelector::getInversionVariable(n); if (!xi.isNull()) diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 1b9443dc6..a230fa314 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -128,7 +128,7 @@ int InstMatchGeneratorMultiLinear::resetChildren() bool InstMatchGeneratorMultiLinear::reset(Node eqc) { Assert(eqc.isNull()); - if (options::multiTriggerLinear()) + if (options().quantifiers.multiTriggerLinear) { return true; } @@ -139,7 +139,7 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) { Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl; - if (options::multiTriggerLinear()) + if (options().quantifiers.multiTriggerLinear) { // reset everyone int rc_ret = resetChildren(); @@ -158,7 +158,7 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m) { Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl; - if (options::multiTriggerLinear()) + if (options().quantifiers.multiTriggerLinear) { // now, restrict everyone for (size_t i = 0, csize = d_children.size(); i < csize; i++) diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 10dcfe129..82cb4a840 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -55,7 +55,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Env& env, { if (d_match_pattern[i].getKind() == INST_CONSTANT) { - if (!options::cegqi() + if (!options().quantifiers.cegqi || TermUtil::getInstConstAttr(d_match_pattern[i]) == q) { d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute()); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 082f24514..fc2928343 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -76,7 +76,8 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q) is_tsym = true; d_tsym_vars.push_back( j ); } - if( !is_tsym || options::qcfTConstraint() ){ + if (!is_tsym || options().quantifiers.qcfTConstraint) + { d_var_mg[j] = std::make_unique(p, this, d_vars[j], true); } if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){ @@ -97,16 +98,20 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q) Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl; } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; - - if( d_mg->isValid() && options::qcfEagerCheckRd() ){ + + if (d_mg->isValid() && options().quantifiers.qcfEagerCheckRd) + { //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) - if( options::qcfSkipRd() ){ + if (options().quantifiers.qcfSkipRd) + { for( unsigned j=q[0].getNumChildren(); j visited; getPropagateVars(vars, q[1], false, visited); @@ -211,7 +216,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) } registerNode(n[0], false, pol, beneathQuant); } - else if (options::qcfTConstraint()) + else if (options().quantifiers.qcfTConstraint) { // a theory-specific predicate for (unsigned i = 0; i < n.getNumChildren(); i++) @@ -642,7 +647,8 @@ bool QuantInfo::isMatchSpurious() bool QuantInfo::isTConstraintSpurious(const std::vector& terms) { - if( options::qcfEagerTest() ){ + if (options().quantifiers.qcfEagerTest) + { EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck(); //check whether the instantiation evaluates as expected std::map subs; @@ -670,7 +676,7 @@ bool QuantInfo::isTConstraintSpurious(const std::vector& terms) // combination of known terms under the current substitution. We use // the helper method evaluateTerm from the entailment check utility. Node inst_eval = echeck->evaluateTerm( - d_q[1], subs, false, options::qcfTConstraint(), true); + d_q[1], subs, false, options().quantifiers.qcfTConstraint, true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; Trace("qcf-instance-check") << " " << terms << std::endl; @@ -767,7 +773,8 @@ bool QuantInfo::completeMatch(std::vector& assigned, bool doContinue) doFail = true; success = false; }else{ - if( isBaseMatchComplete() && options::qcfEagerTest() ){ + if (isBaseMatchComplete() && options().quantifiers.qcfEagerTest) + { return true; } //solve for interpreted symbol matches @@ -2436,7 +2443,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, // ensure that quantified formulas that are more likely to have // conflicting instances are checked earlier. d_treg.getModel()->markRelevant(q); - if (options::qcfAllConflict()) + if (options().quantifiers.qcfAllConflict) { isConflict = true; } diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index e63947b20..a81abc3a0 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -50,67 +50,69 @@ void QuantifiersModules::initialize(Env& env, std::vector& modules) { // add quantifiers modules - if (options::quantConflictFind()) + const Options& options = env.getOptions(); + if (options.quantifiers.quantConflictFind) { d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr)); modules.push_back(d_qcf.get()); } - if (options::conjectureGen()) + if (options.quantifiers.conjectureGen) { d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr)); modules.push_back(d_sg_gen.get()); } - if (!options::finiteModelFind() || options::fmfInstEngine()) + if (!options.quantifiers.finiteModelFind || options.quantifiers.fmfInstEngine) { d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr)); modules.push_back(d_inst_engine.get()); } - if (options::cegqi()) + if (options.quantifiers.cegqi) { d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr)); modules.push_back(d_i_cbqi.get()); qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } - if (options::sygus()) + if (options.quantifiers.sygus) { d_synth_e.reset(new SynthEngine(env, qs, qim, qr, tr)); modules.push_back(d_synth_e.get()); } // bounded integer instantiation is used when the user requests it via // fmfBound, or if strings are enabled. - if (options::fmfBound() || options::stringExp()) + if (options.quantifiers.fmfBound || options.strings.stringExp) { d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr)); modules.push_back(d_bint.get()); } - if (options::finiteModelFind() || options::fmfBound() || options::stringExp()) + if (options.quantifiers.finiteModelFind || options.quantifiers.fmfBound + || options.strings.stringExp) { d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder)); modules.push_back(d_model_engine.get()); } - if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) + if (options.quantifiers.quantDynamicSplit != options::QuantDSplitMode::NONE) { d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr)); modules.push_back(d_qsplit.get()); } - if (options::quantAlphaEquiv()) + if (options.quantifiers.quantAlphaEquiv) { d_alpha_equiv.reset(new AlphaEquivalence(env)); } // full saturation : instantiate from relevant domain, then arbitrary terms - if (options::enumInst() || options::enumInstInterleave()) + if (options.quantifiers.enumInst || options.quantifiers.enumInstInterleave) { d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr)); d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } - if (options::poolInst()) + if (options.quantifiers.poolInst) { d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr)); modules.push_back(d_ipool.get()); } - if (options::sygusInst()) + if (options.quantifiers.sygusInst) { d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get());