Eliminate static options access in BV inverter (#8829)

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 0435874101d4aa4afdfdf82e564fe6e53e631dda..168afe2b6aff5de7aa53a9a00b10fbd713f5f00e 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -31,7 +31,10 @@ namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
-BvInverter::BvInverter(Rewriter* r) : d_rewriter(r) {}
+BvInverter::BvInverter(const Options& opts, Rewriter* r)
+    : d_opts(opts), d_rewriter(r)
+{
+}
 
 /*---------------------------------------------------------------------------*/
 
@@ -342,7 +345,7 @@ Node BvInverter::solveBvLit(Node sv,
     }
     else if (k == BITVECTOR_CONCAT)
     {
-      if (litk == EQUAL && options::cegqiBvConcInv())
+      if (litk == EQUAL && d_opts.quantifiers.cegqiBvConcInv)
       {
         /* Compute inverse for s1 o x, x o s2, s1 o x o s2
          * (while disregarding that invertibility depends on si)

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index d17b58fab330116ea9dcecae09077c000f9e19ed..bd313a4c404baf7c6080cc164d459482f21f0754 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -26,6 +26,9 @@
 #include "expr/node.h"
 
 namespace cvc5::internal {
+
+class Options;
+
 namespace theory {
 
 class Rewriter;
@@ -53,7 +56,7 @@ class BvInverterQuery
 class BvInverter
 {
  public:
-  BvInverter(Rewriter* r = nullptr);
+  BvInverter(const Options& opts, Rewriter* r = nullptr);
   ~BvInverter() {}
   /** get dummy fresh variable of type tn, used as argument for sv */
   Node getSolveVariable(TypeNode tn);
@@ -125,6 +128,8 @@ class BvInverter
    * to this call is null.
    */
   Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
+  /** Reference to options */
+  const Options& d_opts;
   /** (Optional) rewriter used as helper in getInversionNode */
   Rewriter* d_rewriter;
   /** Dummy variables for each type */

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index f0be34902d96566de7e287c93e8a9981616f8e33..5607c04470d194361cd3d07d9cbb8d7201cfd199 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -643,7 +643,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
   // new lemmas
   std::vector<Node> new_lems;
 
-  if (options::cegqiBvRmExtract())
+  if (d_opts.quantifiers.cegqiBvRmExtract)
   {
     NodeManager* nm = NodeManager::currentNM();
     SkolemManager* sm = nm->getSkolemManager();

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index be990899a4d33ec9264aa3884a57875e4115ba77..b116a01b5436238bbce867e7e93ca530c12de2cf 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -167,7 +167,7 @@ class BvInstantiator : public Instantiator
 class BvInstantiatorPreprocess : public InstantiatorPreprocess
 {
  public:
-  BvInstantiatorPreprocess() {}
+  BvInstantiatorPreprocess(const Options& opts) : d_opts(opts) {}
   ~BvInstantiatorPreprocess() override {}
   /** register counterexample lemma
    *
@@ -208,6 +208,8 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
   void collectExtracts(Node lem,
                        std::map<Node, std::vector<Node>>& extract_map,
                        std::unordered_set<TNode>& visited);
+  /** Reference to options */
+  const Options& d_opts;
 };
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 750c07e5db694ab99f12ce436ebee7168a526597..0295d5317e9f4cca6e19d45228cfc4b36a75a31e 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -554,7 +554,7 @@ void CegInstantiator::registerTheoryId(TheoryId tid)
     // setup any theory-specific preprocessors here
     if (tid == THEORY_BV)
     {
-      d_tipp[tid] = new BvInstantiatorPreprocess;
+      d_tipp[tid] = new BvInstantiatorPreprocess(d_env.getOptions());
     }
     d_tids.push_back(tid);
   }

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index e290b0f67ee6d54c59d07745621f36f733d58b8e..1098057023cea59fc78aad0a095f9767c7d4c409 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -66,7 +66,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
   if (options().quantifiers.cegqiBv)
   {
     // if doing instantiation for BV, need the inverter class
-    d_bv_invert.reset(new BvInverter(env.getRewriter()));
+    d_bv_invert.reset(new BvInverter(env.getOptions(), env.getRewriter()));
   }
   if (options().quantifiers.cegqiNestedQE)
   {

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 55ed145cf1b1edf6a25a870f55fc3ef2094112f2..37626015c95dc15fb193071d751ac0b5ea0bbf9c 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -840,7 +840,7 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s)
 
 Node QuantifiersRewriter::getVarElimEq(Node lit,
                                        const std::vector<Node>& args,
-                                       Node& var)
+                                       Node& var) const
 {
   Assert(lit.getKind() == EQUAL);
   Node slv;
@@ -862,7 +862,7 @@ Node QuantifiersRewriter::getVarElimEq(Node lit,
 
 Node QuantifiersRewriter::getVarElimEqReal(Node lit,
                                            const std::vector<Node>& args,
-                                           Node& var)
+                                           Node& var) const
 {
   // for arithmetic, solve the equality
   std::map<Node, Node> msum;
@@ -896,7 +896,7 @@ Node QuantifiersRewriter::getVarElimEqReal(Node lit,
 
 Node QuantifiersRewriter::getVarElimEqBv(Node lit,
                                          const std::vector<Node>& args,
-                                         Node& var)
+                                         Node& var) const
 {
   if (TraceIsOn("quant-velim-bv"))
   {
@@ -914,7 +914,7 @@ Node QuantifiersRewriter::getVarElimEqBv(Node lit,
   std::vector<Node> active_args;
   computeArgVec(args, active_args, lit);
 
-  BvInverter binv;
+  BvInverter binv(d_opts);
   for (const Node& cvar : active_args)
   {
     // solve for the variable on this path using the inverter
@@ -947,7 +947,7 @@ Node QuantifiersRewriter::getVarElimEqBv(Node lit,
 
 Node QuantifiersRewriter::getVarElimEqString(Node lit,
                                              const std::vector<Node>& args,
-                                             Node& var)
+                                             Node& var) const
 {
   Assert(lit.getKind() == EQUAL);
   NodeManager* nm = NodeManager::currentNM();

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7263ece488993ee3cd60be2b06a0024fd64b8f7e..abaebfbaff9bc0ec754372de6a179484d1e083aa 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -101,31 +101,29 @@ class QuantifiersRewriter : public TheoryRewriter
   /**
    * Get variable eliminate for an equality based on theory-specific reasoning.
    */
-  static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var);
+  Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var) const;
   /** variable eliminate for real equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
    * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimEqReal(Node lit,
-                               const std::vector<Node>& args,
-                               Node& var);
+  Node getVarElimEqReal(Node lit,
+                        const std::vector<Node>& args,
+                        Node& var) const;
   /** variable eliminate for bit-vector equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
    * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimEqBv(Node lit,
-                             const std::vector<Node>& args,
-                             Node& var);
+  Node getVarElimEqBv(Node lit, const std::vector<Node>& args, Node& var) const;
   /** variable eliminate for string equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
    * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimEqString(Node lit,
-                                 const std::vector<Node>& args,
-                                 Node& var);
+  Node getVarElimEqString(Node lit,
+                          const std::vector<Node>& args,
+                          Node& var) const;
   /** get variable elimination
    *
    * If there exists an n with some polarity in body, and entails a literal that