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

4 files changed, 52 insertions, 14 deletions

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)