Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)

Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

9 files changed, 300 insertions, 44 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 65ccabd89..9753f86a7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -202,6 +202,8 @@ libcvc4_add_sources(
   smt/logic_exception.h
   smt/logic_request.cpp
   smt/logic_request.h
+  smt/interpolation_solver.cpp
+  smt/interpolation_solver.h
   smt/managed_ostreams.cpp
   smt/managed_ostreams.h
   smt/model.cpp
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
new file mode 100644
index 000000000..d2193d226
--- /dev/null
+++ b/src/smt/interpolation_solver.cpp
@@ -0,0 +1,142 @@
+/*********************                                                        */
+/*! \file interpolation_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "smt/interpolation_solver.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_interpol.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
+{
+}
+
+InterpolationSolver::~InterpolationSolver() {}
+
+bool InterpolationSolver::getInterpol(const Node& conj,
+                                      const TypeNode& grammarType,
+                                      Node& interpol)
+{
+  if (options::produceInterpols() == options::ProduceInterpols::NONE)
+  {
+    const char* msg =
+        "Cannot get interpolation when produce-interpol options is off.";
+    throw ModalException(msg);
+  }
+  Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
+                          << std::endl;
+  std::vector<Expr> easserts = d_parent->getExpandedAssertions();
+  std::vector<Node> axioms;
+  for (unsigned i = 0, size = easserts.size(); i < size; i++)
+  {
+    axioms.push_back(Node::fromExpr(easserts[i]));
+  }
+  // must expand definitions
+  Node conjn = d_parent->expandDefinitions(conj);
+  std::string name("A");
+
+  quantifiers::SygusInterpol interpolSolver;
+  if (interpolSolver.SolveInterpolation(
+          name, axioms, conjn, grammarType, interpol))
+  {
+    if (options::checkInterpols())
+    {
+      checkInterpol(interpol.toExpr(), easserts, conj);
+    }
+    return true;
+  }
+  return false;
+}
+
+bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
+{
+  TypeNode grammarType;
+  return getInterpol(conj, grammarType, interpol);
+}
+
+void InterpolationSolver::checkInterpol(Expr interpol,
+                                        const std::vector<Expr>& easserts,
+                                        const Node& conj)
+{
+  Assert(interpol.getType().isBoolean());
+  Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions"
+                          << std::endl;
+
+  // two checks: first, axioms imply interpol, second, interpol implies conj.
+  for (unsigned j = 0; j < 2; j++)
+  {
+    if (j == 1)
+    {
+      Trace("check-interpol") << "SmtEngine::checkInterpol: conjecture is "
+                              << conj.toExpr() << std::endl;
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": make new SMT engine" << std::endl;
+    // Start new SMT engine to check solution
+    std::unique_ptr<SmtEngine> itpChecker;
+    initializeSubsolver(itpChecker);
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": asserting formulas" << std::endl;
+    if (j == 0)
+    {
+      for (const Expr& e : easserts)
+      {
+        itpChecker->assertFormula(e);
+      }
+      Expr negitp = interpol.notExpr();
+      itpChecker->assertFormula(negitp);
+    }
+    else
+    {
+      itpChecker->assertFormula(interpol);
+      Assert(!conj.isNull());
+      itpChecker->assertFormula(conj.toExpr().notExpr());
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": check the assertions" << std::endl;
+    Result r = itpChecker->checkSat();
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": result is " << r << std::endl;
+    std::stringstream serr;
+    if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+    {
+      if (j == 0)
+      {
+        serr << "SmtEngine::checkInterpol(): negated produced solution cannot "
+                "be shown "
+                "satisfiable with assertions, result was "
+             << r;
+      }
+      else
+      {
+        serr
+            << "SmtEngine::checkInterpol(): negated conjecture cannot be shown "
+               "satisfiable with produced solution, result was "
+            << r;
+      }
+      InternalError() << serr.str();
+    }
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
new file mode 100644
index 000000000..8e6d2cd14
--- /dev/null
+++ b/src/smt/interpolation_solver.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file interpolation_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
+#define CVC4__SMT__INTERPOLATION_SOLVER_H
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * A solver for interpolation queries.
+ *
+ * This class is responsible for responding to get-interpol commands. It spawns
+ * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
+ * query, and implements supporting utility methods such as checkInterpol.
+ */
+class InterpolationSolver
+{
+ public:
+  InterpolationSolver(SmtEngine* parent);
+  ~InterpolationSolver();
+
+  /**
+   * This method asks this SMT engine to find an interpolant with respect to
+   * the current assertion stack (call it A) and the conjecture (call it B). If
+   * this method returns true, then interpolant is set to a formula I such that
+   * A ^ ~I and I ^ ~B are both unsatisfiable.
+   *
+   * @param conj The conjecture of the interpolation problem.
+   * @param grammarType A sygus datatype type that encodes the syntax
+   * restrictions on the shape of possible solutions.
+   * @param interpol This argument is updated to contain the solution to the
+   * interpolation problem.
+   *
+   * This method invokes a separate copy of the SMT engine for solving the
+   * corresponding sygus problem for generating such a solution.
+   */
+  bool getInterpol(const Node& conj,
+                   const TypeNode& grammarType,
+                   Node& interpol);
+
+  /**
+   * Same as above, but without user-provided grammar restrictions. A default
+   * grammar is chosen internally using the sygus grammar constructor utility.
+   */
+  bool getInterpol(const Node& conj, Node& interpol);
+
+  /**
+   * Check that a solution to an interpolation problem is indeed a solution.
+   *
+   * The check is made by determining that the assertions imply the solution of
+   * the interpolation problem (interpol), and the solution implies the goal
+   * (conj). If these criteria are not met, an internal error is thrown.
+   */
+  void checkInterpol(Expr interpol,
+                     const std::vector<Expr>& easserts,
+                     const Node& conj);
+
+ private:
+  /** The parent SMT engine */
+  SmtEngine* d_parent;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7f824bff3..d271ca05d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
+#include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
@@ -134,6 +135,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
       d_abductSolver(nullptr),
+      d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
       d_assignments(nullptr),
       d_logic(),
@@ -299,6 +301,10 @@ void SmtEngine::finishInit()
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
+  if (options::produceInterpols() != options::ProduceInterpols::NONE)
+  {
+    d_interpolSolver.reset(new InterpolationSolver(this));
+  }
 
   d_pp->finishInit();
 
@@ -1755,12 +1761,6 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-void SmtEngine::checkInterpol(Expr interpol,
-                              const std::vector<Expr>& easserts,
-                              const Node& conj)
-{
-}
-
 // TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
@@ -1818,7 +1818,11 @@ bool SmtEngine::getInterpol(const Node& conj,
                             const TypeNode& grammarType,
                             Node& interpol)
 {
-  return false;
+  bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
+  // notify the state of whether the get-interpol call was successfuly, which
+  // impacts the SMT mode.
+  d_state->notifyGetInterpol(success);
+  return success;
 }
 
 bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e95e36c3d..eec17a5f8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -105,6 +105,7 @@ class Preprocessor;
 class SmtSolver;
 class SygusSolver;
 class AbductionSolver;
+class InterpolationSolver;
 class QuantElimSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -1101,6 +1102,8 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+  /** The solver for interpolation queries */
+  std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
   /**
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 07f1d3321..4f3782e2a 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -122,6 +122,20 @@ void SmtEngineState::notifyGetAbduct(bool success)
   }
 }
 
+void SmtEngineState::notifyGetInterpol(bool success)
+{
+  if (success)
+  {
+    // successfully generated an interpolant, update to interpol state
+    d_smtMode = SmtMode::INTERPOL;
+  }
+  else
+  {
+    // failed, we revert to the assert state
+    d_smtMode = SmtMode::ASSERT;
+  }
+}
+
 void SmtEngineState::setup()
 {
   // push a context
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index efb86ca88..1a2ae7ee8 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -96,6 +96,18 @@ class SmtEngineState
    */
   void notifyGetAbduct(bool success);
   /**
+   * Notify that we finished an interpolation query, where success is whether
+   * the command was successful. This is managed independently of the above
+   * calls for notifying check-sat. In other words, if a get-interpol command
+   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+   * to solve the interpolation query. This method is called *in addition* to
+   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
+   * In particular, it is called after these two methods are completed.
+   * This overwrites the SMT mode to the "INTERPOL" mode if the call to
+   * interpolation was successful.
+   */
+  void notifyGetInterpol(bool success);
+  /**
    * Setup the context, which makes a single push to maintain a global
    * context around everything.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index c2ca83e41..4d18c850b 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,8 +31,6 @@ namespace quantifiers {
 
 SygusInterpol::SygusInterpol() {}
 
-SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {}
-
 void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
 {
@@ -75,6 +74,9 @@ void SygusInterpol::createVariables(bool needsShared)
     Node var = nm->mkBoundVar(tn);
     d_vars.push_back(var);
     Node vlv = nm->mkBoundVar(ss.str(), tn);
+    // set that this variable encodes the term s
+    SygusVarToTermAttribute sta;
+    vlv.setAttribute(sta, s);
     d_vlvs.push_back(vlv);
     if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
     {
@@ -266,7 +268,7 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
-bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
+bool SygusInterpol::findInterpol(Node& interpol, Node itp)
 {
   // get the synthesis solution
   std::map<Node, Node> sols;
@@ -283,31 +285,31 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
   }
   Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
                           << its->second << std::endl;
-  Node interpoln = its->second;
+  interpol = its->second;
   // replace back the created variables to original symbols.
-  Node interpoln_reduced;
-  if (interpoln.getKind() == kind::LAMBDA)
+  if (interpol.getKind() == kind::LAMBDA)
   {
-    interpoln_reduced = interpoln[1];
+    interpol = interpol[1];
   }
-  else
+
+  // get the grammar type for the interpolant
+  Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute());
+  Assert(!igdtbv.isNull());
+  Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST);
+  // convert back to original
+  // must replace formal arguments of itp with the free variables in the
+  // input problem that they correspond to.
+  std::vector<Node> vars;
+  std::vector<Node> syms;
+  SygusVarToTermAttribute sta;
+  for (const Node& bv : igdtbv)
   {
-    interpoln_reduced = interpoln;
+    vars.push_back(bv);
+    syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
   }
-  if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0)
-  {
-    std::vector<Node> formals;
-    for (const Node& n : interpoln[0])
-    {
-      formals.push_back(n);
-    }
-    interpoln_reduced = interpoln_reduced.substitute(formals.begin(),
-                                                     formals.end(),
-                                                     d_symSetShared.begin(),
-                                                     d_symSetShared.end());
-  }
-  // convert to expression
-  interpol = interpoln_reduced.toExpr();
+  interpol =
+      interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
+
   return true;
 }
 
@@ -315,14 +317,11 @@ bool SygusInterpol::SolveInterpolation(const std::string& name,
                                        const std::vector<Node>& axioms,
                                        const Node& conj,
                                        const TypeNode& itpGType,
-                                       Expr& interpol)
+                                       Node& interpol)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  // we generate a new smt engine to do the interpolation query
-  d_subSolver.reset(new SmtEngine(nm->toExprManager()));
-  d_subSolver->setIsInternalSubsolver();
+  initializeSubsolver(d_subSolver);
   // get the logic
-  LogicInfo l = d_logic.getUnlockedCopy();
+  LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
   l.enableSygus();
   d_subSolver->setLogic(l);
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 0fe66694f..4abe94f15 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -46,8 +46,6 @@ class SygusInterpol
  public:
   SygusInterpol();
 
-  SygusInterpol(LogicInfo logic);
-
   /**
    * Returns the sygus conjecture in interpol corresponding to the interpolation
    * problem for input problem (F above) given by axioms (Fa above), and conj
@@ -65,7 +63,7 @@ class SygusInterpol
                           const std::vector<Node>& axioms,
                           const Node& conj,
                           const TypeNode& itpGType,
-                          Expr& interpol);
+                          Node& interpol);
 
  private:
   /**
@@ -158,7 +156,7 @@ class SygusInterpol
    * @param interpol the solution to the sygus conjecture.
    * @param itp the interpolation predicate.
    */
-  bool findInterpol(Expr& interpol, Node itp);
+  bool findInterpol(Node& interpol, Node itp);
 
   /** The SMT engine subSolver
    *
@@ -179,10 +177,6 @@ class SygusInterpol
   std::unique_ptr<SmtEngine> d_subSolver;
 
   /**
-   * The logic for the local copy of SMT engine (d_subSolver).
-   */
-  LogicInfo d_logic;
-  /**
    * symbols from axioms and conjecture.
    */
   std::vector<Node> d_syms;