Track sygus variable to term relationship via attribute (#3182)

6 files changed, 68 insertions, 33 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e9c3f06ae..762b21fd8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5147,16 +5147,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   Node conjn = Node::fromExpr(conj).negate();
   d_abdConj = conjn.toExpr();
   asserts.push_back(conjn);
-  d_sssfVarlist.clear();
-  d_sssfSyms.clear();
   std::string name("A");
   Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture(
-      name,
-      asserts,
-      axioms,
-      TypeNode::fromType(grammarType),
-      d_sssfVarlist,
-      d_sssfSyms);
+      name, asserts, axioms, TypeNode::fromType(grammarType));
   // should be a quantified conjecture with one function-to-synthesize
   Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
   // remember the abduct-to-synthesize
@@ -5207,14 +5200,24 @@ bool SmtEngine::getAbductInternal(Expr& abd)
       {
         abdn = abdn[1];
       }
-      Assert(d_sssfVarlist.size() == d_sssfSyms.size());
+      // get the grammar type for the abduct
+      Node af = Node::fromExpr(d_sssf);
+      Node agdtbv = af.getAttribute(theory::SygusSynthFunVarListAttribute());
+      Assert(!agdtbv.isNull());
+      Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
       // convert back to original
       // must replace formal arguments of abd with the free variables in the
       // input problem that they correspond to.
-      abdn = abdn.substitute(d_sssfVarlist.begin(),
-                             d_sssfVarlist.end(),
-                             d_sssfSyms.begin(),
-                             d_sssfSyms.end());
+      std::vector<Node> vars;
+      std::vector<Node> syms;
+      SygusVarToTermAttribute sta;
+      for (const Node& bv : agdtbv)
+      {
+        vars.push_back(bv);
+        syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
+      }
+      abdn =
+          abdn.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
 
       // convert to expression
       abd = abdn.toExpr();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f783b0a33..f032d202a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -170,12 +170,6 @@ class CVC4_PUBLIC SmtEngine {
    */
   Expr d_sssf;
   /**
-   * The substitution to apply to the solutions from the subsolver, used for
-   * the get-abduct command.
-   */
-  std::vector<Node> d_sssfVarlist;
-  std::vector<Node> d_sssfSyms;
-  /**
    * The conjecture of the current abduction problem. This expression is only
    * valid while we are in mode SMT_MODE_ABDUCT.
    */
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 329f9d08a..827c5e7f4 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -84,6 +84,18 @@ struct SygusSideConditionAttributeId
 typedef expr::Attribute<SygusSideConditionAttributeId, Node>
     SygusSideConditionAttribute;
 
+/** Attribute for indicating that a sygus variable encodes a term
+ *
+ * This is used, e.g., for abduction where the formal argument list of the
+ * abduct-to-synthesize corresponds to the free variables of the sygus
+ * problem.
+ */
+struct SygusVarToTermAttributeId
+{
+};
+typedef expr::Attribute<SygusVarToTermAttributeId, Node>
+    SygusVarToTermAttribute;
+
 namespace quantifiers {
 
 /** Attribute priority for rewrite rules */
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 52fb60c06..4f6219343 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -35,9 +35,7 @@ SygusAbduct::SygusAbduct() {}
 Node SygusAbduct::mkAbductionConjecture(const std::string& name,
                                         const std::vector<Node>& asserts,
                                         const std::vector<Node>& axioms,
-                                        TypeNode abdGType,
-                                        std::vector<Node>& varlist,
-                                        std::vector<Node>& syms)
+                                        TypeNode abdGType)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_set<Node, NodeHashFunction> symset;
@@ -49,7 +47,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
       << "...finish, got " << symset.size() << " symbols." << std::endl;
 
   Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
+  std::vector<Node> syms;
   std::vector<Node> vars;
+  std::vector<Node> varlist;
   std::vector<TypeNode> varlistTypes;
   for (const Node& s : symset)
   {
@@ -64,6 +64,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
       Node vlv = nm->mkBoundVar(ss.str(), tn);
       varlist.push_back(vlv);
       varlistTypes.push_back(tn);
+      // set that this variable encodes the term s
+      SygusVarToTermAttribute sta;
+      vlv.setAttribute(sta, s);
     }
   }
   // make the sygus variable list
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index d6bbd0e3f..2fdce542a 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -68,19 +68,19 @@ class SygusAbduct
    * The type abdGType (if non-null) is a sygus datatype type that encodes the
    * grammar that should be used for solutions of the abduction conjecture.
    *
-   * The arguments varlist and syms specify the relationship between the free
-   * variables of asserts and the formal argument list of the
-   * abduct-to-synthesize. In particular, solutions to the synthesis conjecture
-   * will be in the form of a closed term (lambda varlist. t). The intended
-   * solution, which is a term whose free variables are a subset of asserts,
-   * is the term t { varlist -> syms }.
+   * The relationship between the free variables of asserts and the formal
+   * rgument list of the abduct-to-synthesize are tracked by the attribute
+   * SygusVarToTermAttribute.
+   *
+   * In particular, solutions to the synthesis conjecture will be in the form
+   * of a closed term (lambda varlist. t). The intended solution, which is a
+   * term whose free variables are a subset of asserts, is the term
+   * t * { varlist -> SygusVarToTermAttribute(varlist) }.
    */
   static Node mkAbductionConjecture(const std::string& name,
                                     const std::vector<Node>& asserts,
                                     const std::vector<Node>& axioms,
-                                    TypeNode abdGType,
-                                    std::vector<Node>& varlist,
-                                    std::vector<Node>& syms);
+                                    TypeNode abdGType);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 41caf8c6c..b302c4657 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1017,6 +1017,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
   {
     return;
   }
+  NodeManager* nm = NodeManager::currentNM();
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node sol = sols[i];
@@ -1081,13 +1082,35 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
       if (is_unique_term)
       {
         out << "(define-fun " << f << " ";
-        if (dt.getSygusVarList().isNull())
+        // Only include variables that are truly bound variables of the
+        // function-to-synthesize. This means we exclude variables that encode
+        // external terms. This ensures that --sygus-stream prints
+        // solutions with no arguments on the predicate for responses to
+        // the get-abduct command.
+        // pvs stores the variables that will be printed in the argument list
+        // below.
+        std::vector<Node> pvs;
+        Node vl = Node::fromExpr(dt.getSygusVarList());
+        if (!vl.isNull())
+        {
+          Assert(vl.getKind() == BOUND_VAR_LIST);
+          SygusVarToTermAttribute sta;
+          for (const Node& v : vl)
+          {
+            if (!v.hasAttribute(sta))
+            {
+              pvs.push_back(v);
+            }
+          }
+        }
+        if (pvs.empty())
         {
           out << "() ";
         }
         else
         {
-          out << dt.getSygusVarList() << " ";
+          vl = nm->mkNode(BOUND_VAR_LIST, pvs);
+          out << vl << " ";
         }
         out << dt.getSygusType() << " ";
         if (status == 0)