Eliminate static options access in skolemize (#8831)

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index e8515d370d24f6d5c52236598905da21a1682a25..980233a208d65d25d76dfad8814b3a756dbc06a1 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -439,7 +439,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
             std::vector< TNode > args;
             Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl;
             Node n;
-            if (Skolemize::isInductionTerm(r))
+            if (Skolemize::isInductionTerm(options(), r))
             {
               n = d_op_arg_index[r].getGroundTerm( this, args );
             }else{

diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp
index 2c823c7caea4b5904f1506e8a72c2809d8c28aaf..140ad432f7609afed991c1e8ffe57beb8fe1dee3 100644 (file)
--- a/src/theory/quantifiers/quantifiers_preprocess.cpp
+++ b/src/theory/quantifiers/quantifiers_preprocess.cpp
@@ -176,7 +176,8 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers(
       Node sub;
       std::vector<unsigned> sub_vars;
       // return skolemized body
-      ret = Skolemize::mkSkolemizedBody(n, nn, fvs, sk, sub, sub_vars);
+      ret =
+          Skolemize::mkSkolemizedBody(options(), n, nn, fvs, sk, sub, sub_vars);
     }
     visited[key] = ret;
     return ret;

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 8e5c63d5f02bc416bdd3193c04fcadabccfb41c1..8de2085137aebd6bfca11c3e667659b92982137a 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -174,7 +174,8 @@ void Skolemize::getSelfSel(const DType& dt,
   }
 }
 
-Node Skolemize::mkSkolemizedBody(Node f,
+Node Skolemize::mkSkolemizedBody(const Options& opts,
+                                 Node f,
                                  Node n,
                                  std::vector<TNode>& fvs,
                                  std::vector<Node>& sk,
@@ -197,7 +198,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
   std::vector<unsigned> var_indicies;
   for (unsigned i = 0; i < f[0].getNumChildren(); i++)
   {
-    if (isInductionTerm(f[0][i]))
+    if (isInductionTerm(opts, f[0][i]))
     {
       ind_vars.push_back(f[0][i]);
       ind_var_indicies.push_back(i);
@@ -260,7 +261,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
     Node nret = ret.substitute(ind_vars[0], k);
     // note : everything is under a negation
     // the following constructs ~( R( x, k ) => ~P( x ) )
-    if (options::dtStcInduction() && tn.isDatatype())
+    if (opts.quantifiers.dtStcInduction && tn.isDatatype())
     {
       const DType& dt = tn.getDType();
       std::vector<Node> disj;
@@ -279,7 +280,7 @@ Node Skolemize::mkSkolemizedBody(Node f,
       Assert(!disj.empty());
       n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj);
     }
-    else if (options::intWfInduction() && tn.isInteger())
+    else if (opts.quantifiers.intWfInduction && tn.isInteger())
     {
       Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0)));
       Node iret =
@@ -335,8 +336,8 @@ Node Skolemize::getSkolemizedBody(Node f)
     std::vector<TNode> fvs;
     Node sub;
     std::vector<unsigned> sub_vars;
-    Node ret =
-        mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars);
+    Node ret = mkSkolemizedBody(
+        options(), f, f[1], fvs, d_skolem_constants[f], sub, sub_vars);
     d_skolem_body[f] = ret;
     // store sub quantifier information
     if (!sub.isNull())
@@ -364,15 +365,15 @@ Node Skolemize::getSkolemizedBody(Node f)
   return it->second;
 }
 
-bool Skolemize::isInductionTerm(Node n)
+bool Skolemize::isInductionTerm(const Options& opts, Node n)
 {
   TypeNode tn = n.getType();
-  if (options::dtStcInduction() && tn.isDatatype())
+  if (opts.quantifiers.dtStcInduction && tn.isDatatype())
   {
     const DType& dt = tn.getDType();
     return !dt.isCodatatype();
   }
-  if (options::intWfInduction() && tn.isInteger())
+  if (opts.quantifiers.intWfInduction && tn.isInteger())
   {
     return true;
   }

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 123fe0d95c7d338faa191ac032e28c173176cbed..74f180049d3d62648b0ca11156e414c7a3dedf47 100644 (file)
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -102,7 +102,8 @@ class Skolemize : protected EnvObj
    * has multiple induction variables. See page 5
    * of Reynolds et al., VMCAI 2015.
    */
-  static Node mkSkolemizedBody(Node q,
+  static Node mkSkolemizedBody(const Options& opts,
+                               Node q,
                                Node n,
                                std::vector<TNode>& fvs,
                                std::vector<Node>& sk,
@@ -115,7 +116,7 @@ class Skolemize : protected EnvObj
    */
   Node getSkolemizedBody(Node q);
   /** is n a variable that we can apply inductive strenghtening to? */
-  static bool isInductionTerm(Node n);
+  static bool isInductionTerm(const Options& opts, Node n);
   /**
    * Get skolemization vectors, where for each quantified formula that was
    * skolemized, this is the list of skolems that were used to witness the