Add new method for enumerating unsat queries with SyGuS (#7459)

[cvc5.git] / src / theory / quantifiers / expr_miner.cpp

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 6069745e0d48966ae1b0b73789b7f2fd822a8206..b0dd61d33ac6445afff62eaf9ebf1eb850e9cb2d 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -17,11 +17,8 @@
 
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
-#include "theory/smt_engine_subsolver.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -38,51 +35,44 @@ void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
 
 Node ExprMiner::convertToSkolem(Node n)
 {
-  std::vector<Node> fvs;
-  TermUtil::computeVarContains(n, fvs);
-  if (fvs.empty())
+  if (d_skolems.empty())
   {
-    return n;
-  }
-  std::vector<Node> sfvs;
-  std::vector<Node> sks;
-  // map to skolems
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  for (unsigned i = 0, size = fvs.size(); i < size; i++)
-  {
-    Node v = fvs[i];
-    // only look at the sampler variables
-    if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    for (const Node& v : d_vars)
     {
-      sfvs.push_back(v);
-      std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
-      if (itf == d_fv_to_skolem.end())
-      {
-        Node sk = sm->mkDummySkolem("rrck", v.getType());
-        d_fv_to_skolem[v] = sk;
-        sks.push_back(sk);
-      }
-      else
-      {
-        sks.push_back(itf->second);
-      }
+      Node sk = sm->mkDummySkolem("rrck", v.getType());
+      d_skolems.push_back(sk);
+      d_fv_to_skolem[v] = sk;
     }
   }
-  return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
+  return n.substitute(
+      d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
 }
 
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+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.sygusExprMinerCheckTimeout__setByUser)
+  if (options().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
   {
-    initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
+    initializeSubsolver(checker,
+                        opts,
+                        logicInfo,
+                        true,
+                        options().quantifiers.sygusExprMinerCheckTimeout);
   }
   else
   {
-    initializeSubsolver(checker);
+    initializeSubsolver(checker, opts, logicInfo);
   }
   // also set the options
   checker->setOption("sygus-rr-synth-input", "false");
@@ -107,7 +97,7 @@ Result ExprMiner::doCheck(Node query)
       return Result(Result::SAT);
     }
   }
-  std::unique_ptr<SmtEngine> smte;
+  std::unique_ptr<SolverEngine> smte;
   initializeChecker(smte, query);
   return smte->checkSat();
 }