Add finishInit for getInterpol and getAbduct. (#5316)

This PR removes d_subSolver from SygusInterpol class. findInterpol function now receives the sub-solver as input (possibly through solveInterpolation function). In addition, finishInit is now called for getAbduct and getInterpol functions in smt_engine.cpp.

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index ffcb09a23ae51f204a58f57bd0102787a3492f5a..c47d999512c00bbcc859333d145fc84d446ac9d7 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -50,7 +50,7 @@ bool InterpolationSolver::getInterpol(const Node& conj,
   std::string name("A");
 
   quantifiers::SygusInterpol interpolSolver;
-  if (interpolSolver.SolveInterpolation(
+  if (interpolSolver.solveInterpolation(
           name, axioms, conjn, grammarType, interpol))
   {
     if (options::checkInterpols())

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 343b79966bc6813bf591e7b8348aa702e32da68c..f345bee2ead800dbdfce50f408b5c418e3acb280 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1593,6 +1593,7 @@ bool SmtEngine::getInterpol(const Node& conj,
                             Node& interpol)
 {
   SmtScope smts(this);
+  finishInit();
   bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
   // notify the state of whether the get-interpol call was successfuly, which
   // impacts the SMT mode.
@@ -1611,6 +1612,7 @@ bool SmtEngine::getAbduct(const Node& conj,
                           Node& abd)
 {
   SmtScope smts(this);
+  finishInit();
   bool success = d_abductSolver->getAbduct(conj, grammarType, abd);
   // notify the state of whether the get-abduct call was successfuly, which
   // impacts the SMT mode.

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index c58d77a9b96ca820994b6cc8dddfed44b6d5998c..e4e7a02c749d3f535b2cb099c2709718767084d4 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -268,11 +268,11 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
-bool SygusInterpol::findInterpol(Node& interpol, Node itp)
+bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp)
 {
   // get the synthesis solution
   std::map<Node, Node> sols;
-  d_subSolver->getSynthSolutions(sols);
+  subSolver->getSynthSolutions(sols);
   Assert(sols.size() == 1);
   std::map<Node, Node>::iterator its = sols.find(itp);
   if (its == sols.end())
@@ -313,43 +313,44 @@ bool SygusInterpol::findInterpol(Node& interpol, Node itp)
   return true;
 }
 
-bool SygusInterpol::SolveInterpolation(const std::string& name,
+bool SygusInterpol::solveInterpolation(const std::string& name,
                                        const std::vector<Node>& axioms,
                                        const Node& conj,
                                        const TypeNode& itpGType,
                                        Node& interpol)
 {
-  initializeSubsolver(d_subSolver);
+  std::unique_ptr<SmtEngine> subSolver;
+  initializeSubsolver(subSolver);
   // get the logic
-  LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
+  LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
   l.enableSygus();
-  d_subSolver->setLogic(l);
+  subSolver->setLogic(l);
 
   collectSymbols(axioms, conj);
   createVariables(itpGType.isNull());
   for (Node var : d_vars)
   {
-    d_subSolver->declareSygusVar(name, var, var.getType());
+    subSolver->declareSygusVar(name, var, var.getType());
   }
   std::vector<Node> vars_empty;
   TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
   Node itp = mkPredicate(name);
-  d_subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty);
+  subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty);
   mkSygusConjecture(itp, axioms, conj);
   Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
                           << d_sygusConj << ", solving for "
                           << d_sygusConj[0][0] << std::endl;
-  d_subSolver->assertSygusConstraint(d_sygusConj);
+  subSolver->assertSygusConstraint(d_sygusConj);
 
   Trace("sygus-interpol") << "  SmtEngine::getInterpol check sat..."
                           << std::endl;
-  Result r = d_subSolver->checkSynth();
+  Result r = subSolver->checkSynth();
   Trace("sygus-interpol") << "  SmtEngine::getInterpol result: " << r
                           << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
-    return findInterpol(interpol, itp);
+    return findInterpol(subSolver.get(), interpol, itp);
   }
   return false;
 }

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 4e126032bca254f847dabca06b225b0f98364bc9..916f2d9b596f5930f5fa82a592f66d59021d2c02 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -40,6 +40,20 @@ namespace quantifiers {
  * shared between Fa and Fc. In other words, A( x ) must be implied by our
  * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem,
  * we just need to synthesis A( x ).
+ *
+ * This class uses a fresh copy of the SMT engine which is used for solving the
+ * interpolation problem. In particular, consider the input: (assert A)
+ *   (get-interpol s B)
+ * In the copy of the SMT engine where these commands are issued, we maintain
+ * A in the assertion stack. In solving the interpolation problem, we will
+ * need to call a SMT engine solver with a different assertion stack, which is
+ * a sygus conjecture build from A and B. Then to solve the interpolation
+ * problem, instead of modifying the assertion stack to remove A and add the
+ * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
+ * and leave the original assertion stack unchanged. This copy of the SMT
+ * engine will have the assertion stack with the sygus conjecture. This copy
+ * of the SMT engine can be further queried for information regarding further
+ * solutions.
  */
 class SygusInterpol
 {
@@ -59,7 +73,7 @@ class SygusInterpol
    * grammar that should be used for solutions of the interpolation conjecture.
    * @interpol the solution to the sygus conjecture.
    */
-  bool SolveInterpolation(const std::string& name,
+  bool solveInterpolation(const std::string& name,
                           const std::vector<Node>& axioms,
                           const Node& conj,
                           const TypeNode& itpGType,
@@ -156,25 +170,7 @@ class SygusInterpol
    * @param interpol the solution to the sygus conjecture.
    * @param itp the interpolation predicate.
    */
-  bool findInterpol(Node& interpol, Node itp);
-
-  /** The SMT engine subSolver
-   *
-   * This is a fresh copy of the SMT engine which is used for solving the
-   * interpolation problem. In particular, consider the input: (assert A)
-   *   (get-interpol s B)
-   * In the copy of the SMT engine where these commands are issued, we maintain
-   * A in the assertion stack. In solving the interpolation problem, we will
-   * need to call a SMT engine solver with a different assertion stack, which is
-   * a sygus conjecture build from A and B. Then to solve the interpolation
-   * problem, instead of modifying the assertion stack to remove A and add the
-   * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
-   * and leave the original assertion stack unchanged. This copy of the SMT
-   * engine will have the assertion stack with the sygus conjecture. This copy
-   * of the SMT engine can be further queried for information regarding further
-   * solutions.
-   */
-  std::unique_ptr<SmtEngine> d_subSolver;
+  bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
 
   /**
    * symbols from axioms and conjecture.