Allows SAT checks of repair const to have different options (#2412)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 6e1c7f6b627b5a6454767726f0d950f814b60288..c9d1aefa1905743968c639ff4dd8356f0292017e 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1000,6 +1000,13 @@ header = "options/quantifiers_options.h"
   default    = "true"
   help       = "use approach to repair constants in sygus candidate solutions"
 
+[[option]]
+  name       = "sygusRepairConstTimeout"
+  category   = "regular"
+  long       = "sygus-repair-const-timeout=N"
+  type       = "unsigned long"
+  help       = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
+
 [[option]]
   name       = "sygusMinGrammar"
   category   = "regular"

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 75d595a39b546f49403f1454c375f868aef6670f..89f04ffb69392b1a7ec9729f7b84113fe6bd9ee1 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
 #include "options/base_options.h"
+#include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -97,6 +98,50 @@ bool SygusRepairConst::isActive() const
   return !d_base_inst.isNull() && d_allow_constant_grammar;
 }
 
+void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+                                         ExprManager& em,
+                                         ExprManagerMapCollection& varMap,
+                                         Node query,
+                                         bool& needExport)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (options::sygusRepairConstTimeout.wasSetByUser())
+  {
+    // 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->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());
+    }
+  }
+  else
+  {
+    needExport = false;
+    checker.reset(new SmtEngine(nm->toExprManager()));
+    checker->assertFormula(query.toExpr());
+  }
+}
+
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
                                       std::vector<Node>& repair_cv,
@@ -130,8 +175,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   for (unsigned i = 0, size = candidates.size(); i < size; i++)
   {
     Node cv = candidate_values[i];
-    Node skeleton =
-        getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
+    Node skeleton = getSkeleton(
+        cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
     if (Trace.isOn("sygus-repair-const"))
     {
       Printer* p = Printer::getPrinter(options::outputLanguage());
@@ -206,68 +251,66 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                   << std::endl;
       return false;
     }
-
-    // do miniscoping explicitly
-    if (fo_body[1].getKind() == AND)
-    {
-      Node bvl = fo_body[0];
-      std::vector<Node> children;
-      for (const Node& conj : fo_body[1])
-      {
-        children.push_back(nm->mkNode(FORALL, bvl, conj));
-      }
-      fo_body = nm->mkNode(AND, children);
-    }
   }
 
   Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
-  SmtEngine repcChecker(nm->toExprManager());
-  repcChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
-  repcChecker.assertFormula(fo_body.toExpr());
-  Result r = repcChecker.checkSat();
+  bool needExport = false;
+  ExprManagerMapCollection varMap;
+  ExprManager em(nm->getOptions());
+  std::unique_ptr<SmtEngine> repcChecker;
+  initializeChecker(repcChecker, em, varMap, fo_body, needExport);
+  Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT
-      && !r.asSatisfiabilityResult().isUnknown())
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
+      || r.asSatisfiabilityResult().isUnknown())
   {
-    std::vector<Node> sk_sygus_m;
-    for (const Node& v : sk_vars)
+    Trace("cegqi-engine") << "...failed" << std::endl;
+    return false;
+  }
+  std::vector<Node> sk_sygus_m;
+  for (const Node& v : sk_vars)
+  {
+    Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
+    Node fov = d_sk_to_fo[v];
+    Node fov_m;
+    if (needExport)
     {
-      Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
-      Node fov = d_sk_to_fo[v];
-      Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr()));
-      Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
-      // convert to sygus
-      Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
-      sk_sygus_m.push_back(fov_m_to_sygus);
+      Expr e_fov = fov.toExpr().exportTo(&em, varMap);
+      fov_m = Node::fromExpr(
+          repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
     }
-    std::stringstream ss;
-    // convert back to sygus
-    for (unsigned i = 0, size = candidates.size(); i < size; i++)
+    else
     {
-      Node csk = candidate_skeletons[i];
-      Node scsk = csk.substitute(
-          sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
-      repair_cv.push_back(scsk);
-      if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
-      {
-        std::stringstream sss;
-        Printer::getPrinter(options::outputLanguage())
-            ->toStreamSygus(sss, repair_cv[i]);
-        ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
-      }
+      fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr()));
     }
-    Trace("cegqi-engine") << "...success:" << std::endl;
-    Trace("cegqi-engine") << ss.str();
-    Trace("sygus-repair-const")
-        << "Repaired constants in solution : " << std::endl;
-    Trace("sygus-repair-const") << ss.str();
-    return true;
+    Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
+    // convert to sygus
+    Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
+    sk_sygus_m.push_back(fov_m_to_sygus);
   }
-
-  Trace("cegqi-engine") << "...failed" << std::endl;
-
-  return false;
+  std::stringstream ss;
+  // convert back to sygus
+  for (unsigned i = 0, size = candidates.size(); i < size; i++)
+  {
+    Node csk = candidate_skeletons[i];
+    Node scsk = csk.substitute(
+        sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
+    repair_cv.push_back(scsk);
+    if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
+    {
+      std::stringstream sss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(sss, repair_cv[i]);
+      ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
+    }
+  }
+  Trace("cegqi-engine") << "...success:" << std::endl;
+  Trace("cegqi-engine") << ss.str();
+  Trace("sygus-repair-const") << "Repaired constants in solution : "
+                              << std::endl;
+  Trace("sygus-repair-const") << ss.str();
+  return true;
 }
 
 bool SygusRepairConst::mustRepair(Node n)

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 3e45f9210783a4ad0aee04b59e7ae97fdde048d3..c6bfd2806fd202ec5965b311da039fbaeccacdd7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -189,6 +189,26 @@ class SygusRepairConst
    * If n is in the given logic, this method returns true.
    */
   bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
+  /** initialize checker
+   *
+   * This function initializes the smt engine checker to check the
+   * satisfiability of the argument "query"
+   *
+   * The arguments em and varMap are used for supporting cases where we
+   * want checker to use a different expression manager instead of the current
+   * expression manager. The motivation for this so that different options can
+   * be set for the subcall.
+   *
+   * We update the flag needExport to true if checker is using the expression
+   * manager em. In this case, subsequent expressions extracted from smte
+   * (for instance, model values) must be exported to the current expression
+   * manager.
+   */
+  void initializeChecker(std::unique_ptr<SmtEngine>& checker,
+                         ExprManager& em,
+                         ExprManagerMapCollection& varMap,
+                         Node query,
+                         bool& needExport);
 };
 
 } /* CVC4::theory::quantifiers namespace */