Add implementation for SyGuS interpolation module (step4) (#4811)

This is the 4th step of adding interface for SyGuS Interpolation module. 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 4th step finished the implementation of the interpolation module.

2 files changed, 138 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index cc97bb974..0d08140d3 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -204,7 +204,15 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
 
 Node SygusInterpol::mkPredicate(const std::string& name)
 {
-  Node itp;
+  NodeManager* nm = NodeManager::currentNM();
+  // make the interpolation predicate to synthesize
+  Trace("sygus-interpol-debug")
+      << "Make interpolation predicate..." << std::endl;
+  TypeNode itpType = d_varTypesShared.empty()
+                         ? nm->booleanType()
+                         : nm->mkPredicateType(d_varTypesShared);
+  Node itp = nm->mkBoundVar(name.c_str(), itpType);
+  Trace("sygus-interpol-debug") << "...finish" << std::endl;
   return itp;
 }
 
@@ -212,11 +220,100 @@ void SygusInterpol::mkSygusConjecture(Node itp,
                                       const std::vector<Node>& axioms,
                                       const Node& conj)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  // make the interpolation application to synthesize
+  Trace("sygus-interpol-debug")
+      << "Make interpolation predicate app..." << std::endl;
+  std::vector<Node> ichildren;
+  ichildren.push_back(itp);
+  ichildren.insert(ichildren.end(), d_varsShared.begin(), d_varsShared.end());
+  Node itpApp =
+      d_varsShared.empty() ? itp : nm->mkNode(kind::APPLY_UF, ichildren);
+  Trace("sygus-interpol-debug") << "itpApp: " << itpApp << std::endl
+                                << std::endl;
+  Trace("sygus-interpol-debug") << "...finish" << std::endl;
+
+  // set the sygus bound variable list
+  Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
+  itp.setAttribute(theory::SygusSynthFunVarListAttribute(), d_ibvlShared);
+  // sygus attribute
+  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+  theory::SygusAttribute ca;
+  sygusVar.setAttribute(ca, true);
+  Node instAttr = nm->mkNode(kind::INST_ATTRIBUTE, sygusVar);
+  std::vector<Node> iplc;
+  iplc.push_back(instAttr);
+  Node instAttrList = nm->mkNode(kind::INST_PATTERN_LIST, iplc);
+  Trace("sygus-interpol-debug") << "...finish" << std::endl;
+
+  // Fa( x )
+  Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl;
+  Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms);
+  // Fa( x ) => A( x )
+  Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp);
+  Trace("sygus-interpol-debug")
+      << "first implication: " << firstImplication << std::endl
+      << std::endl;
+  // A( x ) => Fc( x )
+  Node Fc = conj;
+  Node secondImplication = nm->mkNode(kind::IMPLIES, itpApp, Fc);
+  Trace("sygus-interpol-debug")
+      << "second implication: " << secondImplication << std::endl
+      << std::endl;
+  // Fa( x ) => A( x ) ^ A( x ) => Fc( x )
+  Node constraint = nm->mkNode(kind::AND, firstImplication, secondImplication);
+  constraint = constraint.substitute(
+      d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end());
+  Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl;
+  constraint = theory::Rewriter::rewrite(constraint);
+
+  d_sygusConj = constraint;
+  Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
 bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
 {
-  return false;
+  // get the synthesis solution
+  std::map<Expr, Expr> sols;
+  d_subSolver->getSynthSolutions(sols);
+  Assert(sols.size() == 1);
+  std::map<Expr, Expr>::iterator its = sols.find(itp.toExpr());
+  if (its == sols.end())
+  {
+    Trace("sygus-interpol")
+        << "SmtEngine::getInterpol: could not find solution!" << std::endl;
+    throw RecoverableModalException(
+        "Could not find solution for get-interpol.");
+    return false;
+  }
+  Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
+                          << its->second << std::endl;
+  Node interpoln = Node::fromExpr(its->second);
+  // replace back the created variables to original symbols.
+  Node interpoln_reduced;
+  if (interpoln.getKind() == kind::LAMBDA)
+  {
+    interpoln_reduced = interpoln[1];
+  }
+  else
+  {
+    interpoln_reduced = interpoln;
+  }
+  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();
+  return true;
 }
 
 bool SygusInterpol::SolveInterpolation(const std::string& name,
@@ -225,6 +322,42 @@ bool SygusInterpol::SolveInterpolation(const std::string& name,
                                        const TypeNode& itpGType,
                                        Expr& 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();
+  // get the logic
+  LogicInfo l = d_logic.getUnlockedCopy();
+  // enable everything needed for sygus
+  l.enableSygus();
+  d_subSolver->setLogic(l);
+
+  collectSymbols(axioms, conj);
+  createVariables(itpGType.isNull());
+  for (Node var : d_vars)
+  {
+    d_subSolver->declareSygusVar(name, var.toExpr(), var.getType().toType());
+  }
+  std::vector<Expr> vars_empty;
+  TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
+  Node itp = mkPredicate(name);
+  d_subSolver->declareSynthFun(
+      name, itp.toExpr(), grammarType.toType(), false, vars_empty);
+  mkSygusConjecture(itp, axioms, conj);
+  Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
+                          << d_sygusConj << ", solving for "
+                          << d_sygusConj[0][0].toExpr() << std::endl;
+  d_subSolver->assertSygusConstraint(d_sygusConj.toExpr());
+
+  Trace("sygus-interpol") << "  SmtEngine::getInterpol check sat..."
+                          << std::endl;
+  Result r = d_subSolver->checkSynth();
+  Trace("sygus-interpol") << "  SmtEngine::getInterpol result: " << r
+                          << std::endl;
+  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    return findInterpol(interpol, itp);
+  }
   return false;
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index a79d583cd..0fe66694f 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -34,7 +34,7 @@ namespace quantifiers {
  * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc
  * then the sygus conjecture we construct is:
  *
- * exists A. forall x. ( (Fa( x ) => A( x )) ^ (A( x ) => Fc( x )) )
+ * (Fa( x ) => A( x )) ^ (A( x ) => Fc( x ))
  *
  * where A( x ) is a predicate over the free symbols of our input that are
  * shared between Fa and Fc. In other words, A( x ) must be implied by our
@@ -141,6 +141,8 @@ class SygusInterpol
 
   /**
    * Make the sygus conjecture to be synthesis.
+   * The conjecture body is Fa( x ) => A( x ) ^ A( x ) => Fc( x ) as described
+   * above.
    *
    * @param itp the interpolation predicate.
    * @param axioms the assertions (Fa above)