From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 10 Nov 2019 14:45:39 +0000 (-0600)
Subject: Fix bugs related to sygus higher-order + recursive functions (#3448)
X-Git-Tag: cvc5-1.0.0~3847
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f7c4e5f7bfb5c38611afa3a016f4f767d5b86fd;p=cvc5.git

Fix bugs related to sygus higher-order + recursive functions (#3448)
---

diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 83debe0d9..376d0eb47 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -150,17 +150,10 @@ Node FunDefEvaluator::evaluate(Node n) const
             ret = nm->mkNode(cur.getKind(), children);
             ret = Rewriter::rewrite(ret);
           }
-          if (!ret.isConst())
-          {
-            Trace("fd-eval") << "FunDefEvaluator: non-constant subterm " << ret
-                             << ", FAIL" << std::endl;
-            // failed, possibly due to free variable
-            return Node::null();
-          }
           visited[cur] = ret;
         }
       }
-      else if (!curEval.isConst())
+      else if (cur != curEval && !curEval.isConst())
       {
         Trace("fd-eval-debug") << "from body " << cur << std::endl;
         // we had to evaluate our body, which should have a definition now
@@ -168,7 +161,6 @@ Node FunDefEvaluator::evaluate(Node n) const
         Assert(it != visited.end());
         // our definition is the result of the body
         visited[cur] = it->second;
-        Assert(it->second.isConst());
       }
     }
   } while (!visit.empty());
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 8f935de27..b8bf6c865 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -287,6 +287,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
   std::stack<TNode> visit;
   TNode cur;
   visit.push(n);
+  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   do {
     cur = visit.top();
     visit.pop();
@@ -337,12 +338,38 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
       }
       if (makeEvalFun)
       {
-        // will make into an application of an evaluation function
-        ret = nm->mkNode(DT_SYGUS_EVAL, children);
+        if (!cur.getType().isFunction())
+        {
+          // will make into an application of an evaluation function
+          ret = nm->mkNode(DT_SYGUS_EVAL, children);
+        }
+        else
+        {
+          Assert(children.size() == 1);
+          Node ef = children[0];
+          // Otherwise, we are using the function-to-synthesize itself in a
+          // higher-order setting. We must return the lambda term:
+          //   lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
+          // where ef is the first order variable for the
+          // function-to-synthesize.
+          SygusTypeInfo& ti = tds->getTypeInfo(ef.getType());
+          const std::vector<Node>& vars = ti.getVarList();
+          Assert(!vars.empty());
+          std::vector<Node> vs;
+          for (const Node& v : vars)
+          {
+            vs.push_back(nm->mkBoundVar(v.getType()));
+          }
+          Node lvl = nm->mkNode(BOUND_VAR_LIST, vs);
+          std::vector<Node> eargs;
+          eargs.push_back(ef);
+          eargs.insert(eargs.end(), vs.begin(), vs.end());
+          ret = nm->mkNode(LAMBDA, lvl, nm->mkNode(DT_SYGUS_EVAL, eargs));
+        }
       }
       else if (childChanged)
       {
-        ret = NodeManager::currentNM()->mkNode(ret_k, children);
+        ret = nm->mkNode(ret_k, children);
       }
       visited[cur] = ret;
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c98dd1be2..aa5329e2f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1718,6 +1718,7 @@ set(regress_1_tests
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
+  regress1/sygus/list_recursor.sy
   regress1/sygus/logiccell_help.sy
   regress1/sygus/max.sy
   regress1/sygus/max2-bv.sy
diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy
new file mode 100644
index 000000000..53c55397e
--- /dev/null
+++ b/test/regress/regress1/sygus/list_recursor.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho
+
+(set-logic ALL)
+
+(declare-datatype List ((cons (head Int) (tail List)) (nil)))
+
+(define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int
+  (ite ((_ is nil) l) x 
+                      (y (head l) (tail l) (List_rec x y (tail l)))))
+
+(synth-fun f () Int
+  ((I Int))
+  ((I Int  (0 1 (+ I I)))))
+   
+(synth-fun g ((x Int) (y List) (z Int)) Int
+  ((I Int) (L List))
+  ((I Int  (x z (+ I I) (head L) 0 1))
+   (L List (y (tail y)))))
+   
+
+(constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2))
+(constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2))
+(constraint (= (List_rec f g (cons 5 (cons 3 (cons 3 (cons 0 nil))))) 4))
+(constraint (= (List_rec f g nil) 0))
+(check-synth)