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 1adf50ddddb38b6ce76522657ed37a105525f7d7..8392cd493d64c3b1f7467217607d291ae7b58cb4 100644 (file)
--- 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 1b9443dc65560460db0a2618fadd041f8709acf8..a230fa314fae6253c263b8a5a6e247cea90da51d 100644 (file)
--- 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 10dcfe1298a5535a4d031be05bbc6023543576c5..82cb4a84058b7c227c6fec8aab8de228c22da310 100644 (file)
--- 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 082f24514606ac7d3c770b0e6a19aae4924e3c1b..fc292834397a3cef76d2d2ea83915bec2f5602ed 100644 (file)
--- 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<MatchGen>(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<d_vars.size(); j++ ){
         vars.push_back( d_vars[j] );
       }
-    }else{
+    }
+    else
+    {
       //get all variables that are always relevant
       std::map< TNode, bool > 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<Node>& terms)
 {
-  if( options::qcfEagerTest() ){
+  if (options().quantifiers.qcfEagerTest)
+  {
     EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
     //check whether the instantiation evaluates as expected
     std::map<TNode, TNode> subs;
@@ -670,7 +676,7 @@ bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& 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<size_t>& 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 e63947b201a2d65b95abd798259e9fbc50c64641..a81abc3a0347a797f3adfef6c0ec78bc66cc70e5 100644 (file)
--- 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<QuantifiersModule*>& 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());