Interpolation step 1 (#4638)

This is the first step of adding Interpolation. The whole change will be 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.

The first step creates the API framework, while omits the implementation for getting interpolation.

11 files changed, 297 insertions, 4 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0c8de5291..1e14e9b3a 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4744,6 +4744,31 @@ void Solver::pop(uint32_t nscopes) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+bool Solver::getInterpolant(Term conj, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Expr result;
+  bool success = d_smtEngine->getInterpol(*conj.d_expr, result);
+  if (success) {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Expr result;
+  bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result);
+  if (success)
+  {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 void Solver::printModel(std::ostream& out) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 828dc6f65..76306d443 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3023,6 +3023,29 @@ class CVC4_PUBLIC Solver
   void pop(uint32_t nscopes = 1) const;
 
   /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, Term& output) const;
+
+  /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param gtype the grammar for the interpolant I
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, const Type& gtype, Term& output) const;
+
+  /**
    * Print the model of a satisfiable query to the given output stream.
    * Requires to enable option 'produce-models'.
    * @param out the output stream
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 303448d1b..c104cb3e7 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -669,6 +669,34 @@ header = "options/smt_options.h"
   help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
 
 [[option]]
+  name       = "produceInterpols"
+  category   = "undocumented"
+  long       = "produce-interpols=MODE"
+  type       = "ProduceInterpols"
+  default    = "NONE"
+  read_only  = true
+  help       = "support the get-interpol command"
+  help_mode  = "Interpolants grammar mode"
+[[option.mode.NONE]]
+  name = "none"
+  help = "don't compute interpolants"
+[[option.mode.DEFAULT]]
+  name = "default"
+  help = "use the default grammar for the theory or the user-defined grammar if given"
+[[option.mode.ASSUMPTIONS]]
+  name = "assumptions"
+  help = "use only operators that occur in the assumptions"
+[[option.mode.CONJECTURE]]
+  name = "conjecture"
+  help = "use only operators that occur in the conjecture"
+[[option.mode.SHARED]]
+  name = "shared"
+  help = "use only operators that occur both in the assumptions and the conjecture"
+[[option.mode.ALL]]
+  name = "all"
+  help = "use only operators that occur either in the assumptions or the conjecture"
+
+[[option]]
   name       = "produceAbducts"
   category   = "undocumented"
   long       = "produce-abducts"
@@ -678,6 +706,15 @@ header = "options/smt_options.h"
   help       = "support the get-abduct command"
 
 [[option]]
+  name       = "checkInterpols"
+  category   = "regular"
+  long       = "check-interpols"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "checks whether produced solutions to get-interpol are correct"
+
+[[option]]
   name       = "checkAbducts"
   category   = "regular"
   long       = "check-abducts"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3e8234a86..703696cf5 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1136,6 +1136,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     {
       cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
     }
+  | GET_INTERPOL_TOK {
+      PARSER_STATE->checkThatLogicIsSet();
+    }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    term[e,e2]
+    (
+      sygusGrammar[t, terms, name]
+    )?
+    {
+      cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType()));
+    }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
     sortSymbol[t, CHECK_DECLARED]
@@ -2315,6 +2326,7 @@ INCLUDE_TOK : 'include';
 GET_QE_TOK : 'get-qe';
 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
 GET_ABDUCT_TOK : 'get-abduct';
+GET_INTERPOL_TOK : 'get-interpol';
 DECLARE_HEAP : 'declare-heap';
 
 // SyGuS commands
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cbb2076dd..095c59374 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2091,6 +2091,90 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
+GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+                                       const std::string& name,
+                                       api::Term conj)
+    : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+                                       const std::string& name,
+                                       api::Term conj,
+                                       const Type& gtype)
+    : Command(solver),
+      d_name(name),
+      d_conj(conj),
+      d_sygus_grammar_type(gtype),
+      d_resultStatus(false)
+{
+}
+
+api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
+Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; }
+api::Term GetInterpolCommand::getResult() const { return d_result; }
+
+void GetInterpolCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    if (d_sygus_grammar_type.isNull())
+    {
+      d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
+    }
+    else
+    {
+      d_resultStatus =
+          d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result);
+    }
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetInterpolCommand::printResult(std::ostream& out,
+                                     uint32_t verbosity) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out, verbosity);
+  }
+  else
+  {
+    expr::ExprDag::Scope scope(out, false);
+    if (d_resultStatus)
+    {
+      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+          << std::endl;
+    }
+    else
+    {
+      out << "none" << std::endl;
+    }
+  }
+}
+
+Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
+                                      ExprManagerMapCollection& variableMap)
+{
+  Unimplemented();
+}
+
+Command* GetInterpolCommand::clone() const
+{
+  GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj);
+  c->d_result = d_result;
+  c->d_resultStatus = d_resultStatus;
+  return c;
+}
+
+std::string GetInterpolCommand::getCommandName() const
+{
+  return "get-interpol";
+}
+
 GetAbductCommand::GetAbductCommand() {}
 GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
     : d_name(name), d_conj(conj), d_resultStatus(false)
diff --git a/src/smt/command.h b/src/smt/command.h
index efb4f2f4a..a6a0faaae 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -28,6 +28,7 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/type.h"
@@ -1038,6 +1039,58 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
   SmtEngine* d_smtEngine;
 }; /* class GetSynthSolutionCommand */
 
+/** The command (get-interpol s B)
+ *
+ * This command asks for an interpolant from the current set of assertions and
+ * conjecture (goal) B.
+ *
+ * The symbol s is the name for the interpolation predicate. If we successfully
+ * find a predicate P, then the output response of this command is: (define-fun
+ * s () Bool P)
+ */
+class CVC4_PUBLIC GetInterpolCommand : public Command
+{
+ public:
+  GetInterpolCommand(api::Solver* solver,
+                     const std::string& name,
+                     api::Term conj);
+  /** The argument gtype is the grammar of the interpolation query */
+  GetInterpolCommand(api::Solver* solver,
+                     const std::string& name,
+                     api::Term conj,
+                     const Type& gtype);
+
+  /** Get the conjecture of the interpolation query */
+  api::Term getConjecture() const;
+  /** Get the grammar sygus datatype type given for the interpolation query */
+  Type getGrammarType() const;
+  /** Get the result of the query, which is the solution to the interpolation
+   * query. */
+  api::Term getResult() const;
+
+  void invoke(SmtEngine* smtEngine) override;
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ protected:
+  /** The name of the interpolation predicate */
+  std::string d_name;
+  /** The conjecture of the interpolation query */
+  api::Term d_conj;
+  /**
+   * The (optional) grammar of the interpolation query, expressed as a sygus
+   * datatype type.
+   */
+  Type d_sygus_grammar_type;
+  /** the return status of the command */
+  bool d_resultStatus;
+  /** the return expression of the command */
+  api::Term d_result;
+}; /* class GetInterpolCommand */
+
 /** The command (get-abduct s B (G)?)
  *
  * This command asks for an abduct from the current set of assertions and
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d663352f7..a7e8e6212 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -291,8 +291,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   // sygus inference may require datatypes
   if (!smte.isInternalSubsolver())
   {
-    if (options::produceAbducts() || options::sygusInference()
-        || options::sygusRewSynthInput() || options::sygusInst())
+    if (options::produceAbducts()
+        || options::produceInterpols() != options::ProduceInterpols::NONE
+        || options::sygusInference() || options::sygusRewSynthInput()
+        || options::sygusInst())
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
@@ -316,6 +318,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
 
   if ((options::checkModels() || options::checkSynthSol()
        || options::produceAbducts()
+       || options::produceInterpols() != options::ProduceInterpols::NONE
        || options::modelCoresMode() != options::ModelCoresMode::NONE
        || options::blockModelsMode() != options::BlockModelsMode::NONE)
       && !options::produceAssertions())
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a6d89aaf5..bb4d82fe0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2934,6 +2934,12 @@ void SmtEngine::checkSynthSolution()
   }
 }
 
+void SmtEngine::checkInterpol(Expr interpol,
+                              const std::vector<Expr>& easserts,
+                              const Node& conj)
+{
+}
+
 void SmtEngine::checkAbduct(Expr a)
 {
   Assert(a.getType().isBoolean());
@@ -3152,6 +3158,19 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
+bool SmtEngine::getInterpol(const Expr& conj,
+                            const Type& grammarType,
+                            Expr& interpol)
+{
+  return false;
+}
+
+bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol)
+{
+  Type grammarType;
+  return getInterpol(conj, grammarType, interpol);
+}
+
 bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
 {
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8a9a60251..afb39b41b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -166,7 +166,9 @@ class CVC4_PUBLIC SmtEngine
     // immediately after a check-sat returning "unsat"
     SMT_MODE_UNSAT,
     // immediately after a successful call to get-abduct
-    SMT_MODE_ABDUCT
+    SMT_MODE_ABDUCT,
+    // immediately after a successful call to get-interpol
+    SMT_MODE_INTERPOL
   };
 
   /** Construct an SmtEngine with the given expression manager.  */
@@ -619,6 +621,23 @@ class CVC4_PUBLIC SmtEngine
   Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true);
 
   /**
+   * 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.
+   *
+   * The argument grammarType is a sygus datatype type that encodes the syntax
+   * restrictions on the shapes of possible solutions.
+   *
+   * This method invokes a separate copy of the SMT engine for solving the
+   * corresponding sygus problem for generating such a solution.
+   */
+  bool getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol);
+
+  /** Same as above, but without user-provided grammar restrictions */
+  bool getInterpol(const Expr& conj, Expr& interpol);
+
+  /**
    * This method asks this SMT engine to find an abduct with respect to the
    * current assertion stack (call it A) and the conjecture (call it B).
    * If this method returns true, then abd is set to a formula C such that
@@ -935,6 +954,18 @@ class CVC4_PUBLIC SmtEngine
    * unsatisfiable. If not, then the found solutions are wrong.
    */
   void checkSynthSolution();
+
+  /**
+   * 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);
+
   /**
    * Check that a solution to an abduction conjecture is indeed a solution.
    *
@@ -1058,6 +1089,7 @@ class CVC4_PUBLIC SmtEngine
   void debugCheckFunctionBody(Expr formula,
                               const std::vector<Expr>& formals,
                               Expr func);
+
   /**
    * Get abduct internal.
    *
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 49c7461e6..fda08bb0e 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1673,7 +1673,6 @@ bool SygusExtension::checkValue(Node n,
   }
   TypeNode tn = n.getType();
   const DType& dt = tn.getDType();
-  Assert(dt.isSygus());
 
   // ensure that the expected size bound is met
   int cindex = utils::indexOf(vn.getOperator());
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index f080f5348..ddff63352 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -95,6 +95,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testUFIteration();
 
   void testGetInfo();
+  void testGetInterpolant();
   void testGetOp();
   void testGetOption();
   void testGetUnsatAssumptions1();
@@ -1309,6 +1310,11 @@ void SolverBlack::testGetInfo()
   TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&);
 }
 
+void SolverBlack::testGetInterpolant()
+{
+  // TODO
+}
+
 void SolverBlack::testGetOp()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);