Fix for sygusToBuiltinEval for non-ground composite terms (#5466)

There was a bug in the method for computing the evaluation of a sygus term applied to arguments.

The case that was wrong was for (DT_SYGUS_EVAL t c1 ... cn) where t contained a subterm (op t1 ... tn) where:
(1) (op t1 ... tn) is a non-ground sygus datatype term
(2) op was an operator of the form (lambda ((z T)) (g z xi)) where xi is a variable from the formal argument list of the function to synthesize.
In this case, xi was not getting replaced by ci.

This bug appears when using sygus repair for grammars with composite term that involve variables from the formal argument list of the synth-fun.

4 files changed, 31 insertions, 15 deletions

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 612722d48..f99f58969 100644
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -37,12 +37,19 @@ Node applySygusArgs(const DType& dt,
                     Node n,
                     const std::vector<Node>& args)
 {
+  // optimization: if n is just a sygus bound variable, return immediately
+  // by replacing with the proper argument, or returning unchanged if it is
+  // a bound variable not corresponding to a formal argument.
   if (n.getKind() == BOUND_VARIABLE)
   {
-    Assert(n.hasAttribute(SygusVarNumAttribute()));
-    int vn = n.getAttribute(SygusVarNumAttribute());
-    Assert(dt.getSygusVarList()[vn] == n);
-    return args[vn];
+    if (n.hasAttribute(SygusVarNumAttribute()))
+    {
+      int vn = n.getAttribute(SygusVarNumAttribute());
+      Assert(dt.getSygusVarList()[vn] == n);
+      return args[vn];
+    }
+    // it is a different bound variable, it is unchanged
+    return n;
   }
   // n is an application of operator op.
   // We must compute the free variables in op to determine if there are
@@ -551,8 +558,10 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
           children.push_back(it->second);
         }
         index = indexOf(cur.getOperator());
-        // apply to arguments
+        // apply to children, which constructs the builtin term
         ret = mkSygusTerm(dt, index, children);
+        // now apply it to arguments in args
+        ret = applySygusArgs(dt, dt[index].getSygusOp(), ret, args);
       }
       visited[cur] = ret;
     }
diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h
index 3f833702c..fabb295eb 100644
--- a/src/theory/datatypes/sygus_datatype_utils.h
+++ b/src/theory/datatypes/sygus_datatype_utils.h
@@ -113,7 +113,7 @@ Node mkSygusTerm(Node op,
                  const std::vector<Node>& children,
                  bool doBetaReduction = true);
 /**
- * n is a builtin term that is an application of operator op.
+ * n is a builtin term that is a (rewritten) application of operator op.
  *
  * This returns an n' such that (eval n args) is n', where n' is a instance of
  * n for the appropriate substitution.
@@ -122,18 +122,18 @@ Node mkSygusTerm(Node op,
  * say we have grammar:
  *   A -> A+A | A+x | A+(x+y) | y
  * These lead to constructors with sygus ops:
- *   C1 / (lambda w1 w2. w1+w2)
- *   C2 / (lambda w1. w1+x)
- *   C3 / (lambda w1. w1+(x+y))
- *   C4 / y
+ *   C1 / L1 where L1 is (lambda w1 w2. w1+w2)
+ *   C2 / L2 where L2 is (lambda w1. w1+x)
+ *   C3 / L3 where L3 is (lambda w1. w1+(x+y))
+ *   C4 / L4 where L4 is y
  * Examples of calling this function:
- *   applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } )
+ *   applySygusArgs( dt, L1, (APPLY_UF L1 t1 t2), { 3, 5 } )
  *     ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
- *   applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } )
+ *   applySygusArgs( dt, L2, (APPLY_UF L2 t1), { 3, 5 } )
  *     ... returns (APPLY_UF (lambda w1. w1+3) t1).
- *   applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } )
+ *   applySygusArgs( dt, L3, (APPLY_UF L3 t1), { 3, 5 } )
  *     ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
- *   applySygusArgs( dt, C4, y, { 3, 5 } )
+ *   applySygusArgs( dt, L4, L4, { 3, 5 } )
  *     ... returns 5.
  * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
  * to cache the results of whether the evaluation of this constructor needs
@@ -185,7 +185,7 @@ Node builtinVarToSygus(Node v);
  * where n' is a variable, then this method returns:
  *   12 + (DT_SYGUS_EVAL n' 3 4)
  * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin
- * equivalent x*y and evaluated under the substition { x -> 3, x -> 4 } giving
+ * equivalent x*y and evaluated under the substition { x -> 3, y -> 4 } giving
  * 12. The subterm n' is non-constant and thus we return its evaluation under
  * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor
  * is C_+, these terms are added together to give the result.
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 9f3ed4f4f..882c9ca77 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -314,8 +314,11 @@ Node SygusEvalUnfold::unfold(Node en,
   Node ret = d_tds->mkGeneric(dt, i, pre);
   // apply the appropriate substitution to ret
   ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
+  Trace("sygus-eval-unfold-debug")
+      << "Applied sygus args : " << ret << std::endl;
   // rewrite
   ret = Rewriter::rewrite(ret);
+  Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
   return ret;
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 989f7b758..81120da28 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
 #include "api/cvc4cpp.h"
+#include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -200,7 +201,10 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
                          candidate_skeletons,
                          sk_vars,
                          sk_vars_to_subs);
+    Trace("sygus-repair-const-debug")
+        << "...after fit-to-logic : " << fo_body << std::endl;
   }
+  Assert(!expr::hasFreeVar(fo_body));
 
   if (fo_body.isNull() || sk_vars.empty())
   {