Make expression mining use configurable options and logic (#7426)

Required for doing options-specific internal fuzzing using SyGuS.

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index d648a7a29059756e097d74894c28379656d15dfe..fad95612f2d7b18b1aecdab5c65ad1c93a5a5c4a 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -52,18 +52,24 @@ Node ExprMiner::convertToSkolem(Node n)
 
 void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
                                   Node query)
+{
+  initializeChecker(checker, query, options(), logicInfo());
+}
+
+void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
+                                  Node query,
+                                  const Options& opts,
+                                  const LogicInfo& logicInfo)
 {
   Assert (!query.isNull());
   if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
   {
-    initializeSubsolver(checker,
-                        d_env,
-                        true,
-                        options::sygusExprMinerCheckTimeout());
+    initializeSubsolver(
+        checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout());
   }
   else
   {
-    initializeSubsolver(checker, d_env);
+    initializeSubsolver(checker, opts, logicInfo);
   }
   // also set the options
   checker->setOption("sygus-rr-synth-input", "false");

diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 3933b963577c2740712cb46fd62b24837acab343..702dbf5aa2199ede2515d7bf29258782e64bcddb 100644 (file)
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -85,7 +85,12 @@ class ExprMiner : protected EnvObj
    * of the argument "query", which is a formula whose free variables (of
    * kind BOUND_VARIABLE) are a subset of d_vars.
    */
-  void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query);
+  void initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query);
+  /** Also with configurable options and logic */
+  void initializeChecker(std::unique_ptr<SolverEngine>& checker,
+                         Node query,
+                         const Options& opts,
+                         const LogicInfo& logicInfo);
   /**
    * Run the satisfiability check on query and return the result
    * (sat/unsat/unknown).