From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 00:04:21 +0000 (-0500)
Subject: Make expression mining use configurable options and logic (#7426)
X-Git-Tag: cvc5-1.0.0~1010
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=738f38bf6b5f2cf6a5812c056ae6f771bffb42e6;p=cvc5.git

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 d648a7a29..fad95612f 100644
--- 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 3933b9635..702dbf5aa 100644
--- 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).