Generalize sygus stream solution filtering to logical strength (#2697)

1 files changed, 23 insertions, 0 deletions

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 16e59c119..b65d1c522 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -113,6 +113,29 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   }
 }
 
+Result ExprMiner::doCheck(Node query)
+{
+  Node queryr = Rewriter::rewrite(query);
+  if (queryr.isConst())
+  {
+    if (!queryr.getConst<bool>())
+    {
+      return Result(Result::UNSAT);
+    }
+    else
+    {
+      return Result(Result::SAT);
+    }
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  bool needExport = false;
+  ExprManagerMapCollection varMap;
+  ExprManager em(nm->getOptions());
+  std::unique_ptr<SmtEngine> smte;
+  initializeChecker(smte, em, varMap, queryr, needExport);
+  return smte->checkSat();
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4