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.

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 612722d481c76e99c22a5f375d0f50f0cdeb0c6b..f99f589697e0d184d98605e35ed396238bfc08a6 100644 (file)
--- 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 3f833702c2cd7a9d565b884f0922b86ddb9a01c4..fabb295eb049a25819eca59a0906187aaeeb8441 100644 (file)
--- 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 9f3ed4f4fcd051beb73fbfe5060741fece318a65..882c9ca7703dbda793bc3d5e788fec321d6ac081 100644 (file)
--- 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 989f7b758f07250d849060b6225f63d201ea9e93..81120da28feb697f477e50658cc57cc65f57c1cd 100644 (file)
--- 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())
   {