Standardize the interface for SMT engine subsolvers (#3836)

This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.

This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).

Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).

6 files changed, 55 insertions, 124 deletions

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 6b042e294..8645be1a1 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -18,6 +18,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/smt_engine_subsolver.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -76,41 +77,22 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   // Convert bound variables to skolems. This ensures the satisfiability
   // check is ground.
   Node squery = convertToSkolem(query);
-  NodeManager* nm = NodeManager::currentNM();
   if (options::sygusExprMinerCheckUseExport())
   {
-    // To support a separate timeout for the subsolver, we need to create
-    // a separate ExprManager with its own options. This requires that
-    // the expressions sent to the subsolver can be exported from on
-    // ExprManager to another. If the export fails, we throw an
-    // OptionException.
-    try
-    {
-      checker.reset(new SmtEngine(&em));
-      checker->setIsInternalSubsolver();
-      checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
-      checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
-      checker->setOption("sygus-rr-synth-input", false);
-      checker->setOption("input-language", "smt2");
-      Expr equery = squery.toExpr().exportTo(&em, varMap);
-      checker->assertFormula(equery);
-    }
-    catch (const CVC4::ExportUnsupportedException& e)
-    {
-      std::stringstream msg;
-      msg << "Unable to export " << squery
-          << " but exporting expressions is "
-             "required for an expression "
-             "miner check.";
-      throw OptionException(msg.str());
-    }
+    initializeSubsolverWithExport(checker,
+                                  em,
+                                  varMap,
+                                  squery.toExpr(),
+                                  true,
+                                  options::sygusExprMinerCheckTimeout());
+    checker->setOption("sygus-rr-synth-input", false);
+    checker->setOption("input-language", "smt2");
     needExport = true;
   }
   else
   {
+    initializeSubsolver(checker, squery.toExpr());
     needExport = false;
-    checker.reset(new SmtEngine(nm->toExprManager()));
-    checker->assertFormula(squery.toExpr());
   }
 }
 
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 233ef39f7..4625e762a 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -20,8 +20,9 @@
 #include <map>
 #include <memory>
 #include <vector>
+#include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "expr/node.h"
+#include "expr/variable_type_map.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index ad281b009..cae5cd823 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -24,6 +24,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
 #include "util/random.h"
 
 using namespace CVC4::kind;
@@ -626,36 +627,9 @@ bool CegisCoreConnective::getUnsatCore(
 
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
-  Assert(mvs.empty());
-  Assert(n.getType().isBoolean());
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
-  n = Rewriter::rewrite(n);
-  if (n.isConst())
-  {
-    if (n.getConst<bool>())
-    {
-      // default model
-      for (const Node& v : d_vars)
-      {
-        mvs.push_back(v.getType().mkGroundTerm());
-      }
-      return Result(Result::SAT);
-    }
-    else
-    {
-      return Result(Result::UNSAT);
-    }
-  }
-  SmtEngine smt(NodeManager::currentNM()->toExprManager());
-  smt.setIsInternalSubsolver();
-  smt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-  smt.assertFormula(n.toExpr());
-  Result r = smt.checkSat();
+  Result r = checkWithSubsolver(n, d_vars, mvs);
   Trace("sygus-ccore-debug") << "...got " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat() == Result::SAT)
-  {
-    getModel(smt, mvs);
-  }
   return r;
 }
 
@@ -762,9 +736,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    SmtEngine checkSol(nm->toExprManager());
-    checkSol.setIsInternalSubsolver();
-    checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo());
+    std::unique_ptr<SmtEngine> checkSol;
+    initializeSubsolver(checkSol);
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -773,9 +746,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
     for (const Node& a : rasserts)
     {
-      checkSol.assertFormula(a.toExpr());
+      checkSol->assertFormula(a.toExpr());
     }
-    Result r = checkSol.checkSat();
+    Result r = checkSol->checkSat();
     Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
     // In terms of Variant #2, this is the check "if (S ^ D) => B"
     if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -788,7 +761,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
       std::unordered_set<Node, NodeHashFunction> queryAsserts;
       queryAsserts.insert(ccheck.getFormula());
       queryAsserts.insert(d_sc);
-      bool hasQuery = getUnsatCore(checkSol, queryAsserts, uasserts);
+      bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
       // now, check the side condition
       bool falseCore = false;
       if (!d_sc.isNull())
@@ -803,18 +776,17 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
         {
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
-          SmtEngine checkSc(nm->toExprManager());
-          checkSc.setIsInternalSubsolver();
-          checkSc.setLogic(smt::currentSmtEngine()->getLogicInfo());
+          std::unique_ptr<SmtEngine> checkSc;
+          initializeSubsolver(checkSc);
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
           std::shuffle(scasserts.begin(), scasserts.end(), Random::getRandom());
           for (const Node& sca : scasserts)
           {
-            checkSc.assertFormula(sca.toExpr());
+            checkSc->assertFormula(sca.toExpr());
           }
-          Result rsc = checkSc.checkSat();
+          Result rsc = checkSc->checkSat();
           Trace("sygus-ccore")
               << "----- check-sat returned " << rsc << std::endl;
           if (rsc.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -825,7 +797,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
             uasserts.clear();
             std::unordered_set<Node, NodeHashFunction> queryAsserts2;
             queryAsserts2.insert(d_sc);
-            getUnsatCore(checkSc, queryAsserts2, uasserts);
+            getUnsatCore(*checkSc, queryAsserts2, uasserts);
             falseCore = true;
           }
         }
@@ -869,7 +841,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
       // it does not entail the postcondition, add an assertion that blocks
       // the current point
       mvs.clear();
-      getModel(checkSol, mvs);
+      getModel(*checkSol, mvs);
       // should evaluate to true
       Node ean = evaluate(an, Node::null(), mvs);
       Assert(ean.isConst() && ean.getConst<bool>());
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 9ab94d1bc..5874104ce 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;
 
@@ -111,36 +112,22 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
     // To support a separate timeout for the subsolver, we need to create
     // a separate ExprManager with its own options. This requires that
     // the expressions sent to the subsolver can be exported from on
-    // ExprManager to another. If the export fails, we throw an
-    // OptionException.
-    try
-    {
-      checker.reset(new SmtEngine(&em));
-      checker->setIsInternalSubsolver();
-      checker->setTimeLimit(options::sygusRepairConstTimeout(), true);
-      checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
-      // renable options disabled by sygus
-      checker->setOption("miniscope-quant", true);
-      checker->setOption("miniscope-quant-fv", true);
-      checker->setOption("quant-split", true);
-      // export
-      Expr e_query = query.toExpr().exportTo(&em, varMap);
-      checker->assertFormula(e_query);
-    }
-    catch (const CVC4::ExportUnsupportedException& e)
-    {
-      std::stringstream msg;
-      msg << "Unable to export " << query
-          << " but exporting expressions is required for "
-             "--sygus-repair-const-timeout.";
-      throw OptionException(msg.str());
-    }
+    // ExprManager to another.
+    initializeSubsolverWithExport(checker,
+                                  em,
+                                  varMap,
+                                  query.toExpr(),
+                                  true,
+                                  options::sygusRepairConstTimeout());
+    // renable options disabled by sygus
+    checker->setOption("miniscope-quant", true);
+    checker->setOption("miniscope-quant-fv", true);
+    checker->setOption("quant-split", true);
   }
   else
   {
     needExport = false;
-    checker.reset(new SmtEngine(nm->toExprManager()));
-    checker->assertFormula(query.toExpr());
+    initializeSubsolver(checker, query.toExpr());
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index fe0e99a4d..1596c30f0 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -20,8 +20,6 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -34,6 +32,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -592,24 +591,22 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (options::sygusVerifySubcall())
     {
       Trace("cegqi-engine") << "  *** Verify with subcall..." << std::endl;
-      SmtEngine verifySmt(nm->toExprManager());
-      verifySmt.setIsInternalSubsolver();
-      verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-      verifySmt.assertFormula(query.toExpr());
-      Result r = verifySmt.checkSat();
+
+      Result r =
+          checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
       Trace("cegqi-engine") << "  ...got " << r << std::endl;
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
-        Trace("cegqi-engine") << "  * Verification lemma failed for:\n   ";
-        // do not send out
-        for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
+        if (Trace.isOn("cegqi-engine"))
         {
-          Node v = d_ce_sk_vars[i];
-          Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr()));
-          Trace("cegqi-engine") << vars[i] << " -> " << mv << " ";
-          d_ce_sk_var_mvs.push_back(mv);
+          Trace("cegqi-engine") << "  * Verification lemma failed for:\n   ";
+          for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
+          {
+            Trace("cegqi-engine")
+                << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
+          }
+          Trace("cegqi-engine") << std::endl;
         }
-        Trace("cegqi-engine") << std::endl;
 #ifdef CVC4_ASSERTIONS
         // the values for the query should be a complete model
         Node squery = query.substitute(d_ce_sk_vars.begin(),
@@ -661,15 +658,9 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
   {
     Node sc = d_embedSideCondition.substitute(
         d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
-    sc = Rewriter::rewrite(sc);
     Trace("cegqi-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
-    NodeManager* nm = NodeManager::currentNM();
-    SmtEngine scSmt(nm->toExprManager());
-    scSmt.setIsInternalSubsolver();
-    scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-    scSmt.assertFormula(sc.toExpr());
-    Result r = scSmt.checkSat();
+    Result r = checkWithSubsolver(sc);
     Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
     if (r == Result::UNSAT)
     {
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index c9ed16a5f..a77d3681b 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -16,12 +16,11 @@
 #include "theory/quantifiers/sygus/synth_engine.h"
 
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/smt_engine_subsolver.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
@@ -169,9 +168,8 @@ void SynthEngine::assignConjecture(Node q)
     if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
     {
       // create new smt engine to do quantifier elimination
-      SmtEngine smt_qe(nm->toExprManager());
-      smt_qe.setIsInternalSubsolver();
-      smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
+      std::unique_ptr<SmtEngine> smt_qe;
+      initializeSubsolver(smt_qe);
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."
                          << std::endl;
@@ -234,7 +232,7 @@ void SynthEngine::assignConjecture(Node q)
 
       Trace("cegqi-qep") << "Run quantifier elimination on "
                          << conj_se_ngsi_subs << std::endl;
-      Expr qe_res = smt_qe.doQuantifierElimination(
+      Expr qe_res = smt_qe->doQuantifierElimination(
           conj_se_ngsi_subs.toExpr(), true, false);
       Trace("cegqi-qep") << "Result : " << qe_res << std::endl;