From e91077d81183c6c54ff0fdad5c6eb160f16c4205 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 20 Oct 2020 20:28:35 -0500
Subject: 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.
---
 src/theory/quantifiers/sygus/sygus_interpol.h | 36 ++++++++++++---------------
 1 file changed, 16 insertions(+), 20 deletions(-)

(limited to 'src/theory/quantifiers/sygus/sygus_interpol.h')

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 4e126032b..916f2d9b5 100644
--- 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.
-- 
cgit v1.2.3