Merge branch 'master' into fix3089fix3089

9 files changed, 112 insertions, 61 deletions

diff --git a/README.md b/README.md
index faef42e66..b22882d57 100644
--- a/README.md
+++ b/README.md
@@ -13,6 +13,11 @@ modulo a first order theory (or a combination of such theories).  It is the
 fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite,
 CVC3) but does not directly incorporate code from any previous version.
 
+If you are using CVC4 in your work, or incorporating it into software of your
+own, we invite you to send us a description and link to your
+project/software, so that we can link it on our [Third Party
+Applications](https://cvc4.github.io/third-party-applications.html) page.
+
 CVC4 is intended to be an open and extensible SMT engine.  It can be used as a
 stand-alone tool or as a library.  It has been designed to increase the
 performance and reduce the memory overhead of its predecessors.  It is written
@@ -22,10 +27,17 @@ entirely in C++ and is released under an open-source software license (see file
 
 Website
 -------------------------------------------------------------------------------
+CVC4's website  is available at:
+http://cvc4.cs.stanford.edu/
 
-More information about CVC4 is available at:
+Documentation
+-------------------------------------------------------------------------------
+Documentation for users of CVC4 is available at:
 http://cvc4.cs.stanford.edu/
 
+Documentation for developers is available at:
+https://github.com/CVC4/CVC4/wiki/Developer-Guide
+
 Download
 -------------------------------------------------------------------------------
 
@@ -47,25 +59,6 @@ For detailed build and installation instructions on these platforms,
 see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md).
 
 
-Getting Started
--------------------------------------------------------------------------------
-
-We recommend that you visit our CVC4 tutorials online at:
-
-  http://cvc4.cs.stanford.edu/wiki/Tutorials
-
-for help getting started using CVC4.
-
-If you need help with using CVC4, please refer to
-[http://cvc4.stanford.edu#technical-support](
-                                    http://cvc4.stanford.edu#technical-support).
-
-If you are using CVC4 in your work, or incorporating it into software of your
-own, we'd like to invite you to leave a description and link to your
-project/software on our [Third Party
-Applications](http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications).
-
-
 Bug Reports
 -------------------------------------------------------------------------------
 
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 219124d8e..60841a5dd 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "expr/type_matcher.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 
 namespace CVC4 {
 
@@ -42,16 +43,17 @@ struct DatatypeConstructorTypeRule {
     TypeNode consType = n.getOperator().getType(check);
     TypeNode t = consType.getConstructorRangeType();
     Assert(t.isDatatype());
-    DatatypeType dt = DatatypeType(t.toType());
     TNode::iterator child_it = n.begin();
     TNode::iterator child_it_end = n.end();
     TypeNode::iterator tchild_it = consType.begin();
-    if ((dt.isParametric() || check) &&
-        n.getNumChildren() != consType.getNumChildren() - 1) {
+    if ((t.isParametricDatatype() || check)
+        && n.getNumChildren() != consType.getNumChildren() - 1)
+    {
       throw TypeCheckingExceptionPrivate(
           n, "number of arguments does not match the constructor type");
     }
-    if (dt.isParametric()) {
+    if (t.isParametricDatatype())
+    {
       Debug("typecheck-idt") << "typecheck parameterized datatype " << n
                              << std::endl;
       TypeMatcher m(t);
@@ -67,7 +69,9 @@ struct DatatypeConstructorTypeRule {
       TypeNode range = t.instantiateParametricDatatype(instTypes);
       Debug("typecheck-idt") << "Return " << range << std::endl;
       return range;
-    } else {
+    }
+    else
+    {
       if (check) {
         Debug("typecheck-idt") << "typecheck cons: " << n << " "
                                << n.getNumChildren() << std::endl;
@@ -128,12 +132,13 @@ struct DatatypeSelectorTypeRule {
     TypeNode selType = n.getOperator().getType(check);
     TypeNode t = selType[0];
     Assert(t.isDatatype());
-    DatatypeType dt = DatatypeType(t.toType());
-    if ((dt.isParametric() || check) && n.getNumChildren() != 1) {
+    if ((t.isParametricDatatype() || check) && n.getNumChildren() != 1)
+    {
       throw TypeCheckingExceptionPrivate(
           n, "number of arguments does not match the selector type");
     }
-    if (dt.isParametric()) {
+    if (t.isParametricDatatype())
+    {
       Debug("typecheck-idt") << "typecheck parameterized sel: " << n
                              << std::endl;
       TypeMatcher m(t);
@@ -155,7 +160,9 @@ struct DatatypeSelectorTypeRule {
           types.begin(), types.end(), matches.begin(), matches.end());
       Debug("typecheck-idt") << "Return " << range << std::endl;
       return range;
-    } else {
+    }
+    else
+    {
       if (check) {
         Debug("typecheck-idt") << "typecheck sel: " << n << std::endl;
         Debug("typecheck-idt") << "sel type: " << selType << std::endl;
@@ -185,8 +192,8 @@ struct DatatypeTesterTypeRule {
       TypeNode childType = n[0].getType(check);
       TypeNode t = testType[0];
       Assert(t.isDatatype());
-      DatatypeType dt = DatatypeType(t.toType());
-      if (dt.isParametric()) {
+      if (t.isParametricDatatype())
+      {
         Debug("typecheck-idt") << "typecheck parameterized tester: " << n
                                << std::endl;
         TypeMatcher m(t);
@@ -195,7 +202,9 @@ struct DatatypeTesterTypeRule {
               n,
               "matching failed for tester argument of parameterized datatype");
         }
-      } else {
+      }
+      else
+      {
         Debug("typecheck-idt") << "typecheck test: " << n << std::endl;
         Debug("typecheck-idt") << "test type: " << testType << std::endl;
         if (!testType[0].isComparableTo(childType)) {
@@ -395,8 +404,7 @@ class DtSyguEvalTypeRule
       throw TypeCheckingExceptionPrivate(
           n, "datatype sygus eval takes a datatype head");
     }
-    const Datatype& dt =
-        static_cast<DatatypeType>(headType.toType()).getDatatype();
+    const Datatype& dt = headType.getDatatype();
     if (!dt.isSygus())
     {
       throw TypeCheckingExceptionPrivate(
@@ -490,7 +498,7 @@ class MatchTypeRule
             }
             bvs.erase(arg);
           }
-          unsigned ci = Datatype::indexOf(nc[pindex].getOperator().toExpr());
+          unsigned ci = utils::indexOf(nc[pindex].getOperator());
           patIndices.insert(ci);
         }
         else if (ncpk == kind::BOUND_VARIABLE)
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/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 6354b59e9..8ce314c94 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -67,7 +67,7 @@ public:
       return tuple[n_th];
     }
     TypeNode tn = tuple.getType();
-    Datatype dt = tn.getDatatype();
+    const Datatype& dt = tn.getDatatype();
     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple);
   } 
   
@@ -77,7 +77,7 @@ public:
     std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
     std::reverse( tuple_types.begin(), tuple_types.end() );
     TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
-    Datatype dt = tn.getDatatype();
+    const Datatype& dt = tn.getDatatype();
     elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
     for(int i = tuple_types.size() - 1; i >= 0; --i) {
       elements.push_back( nthElementOfTuple(tuple, i) );
@@ -85,7 +85,7 @@ public:
     return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
   }
   static Node constructPair(Node rel, Node a, Node b) {
-    Datatype dt = rel.getType().getSetElementType().getDatatype();
+    const Datatype& dt = rel.getType().getSetElementType().getDatatype();
     return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
   }     
     
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 5c24cb088..e8724aa8b 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -299,7 +299,8 @@ void TheorySetsRels::check(Theory::Effort level)
       }
       hasChecked.insert( fst_mem_rep );
 
-      Datatype dt = join_image_term.getType().getSetElementType().getDatatype();
+      const Datatype& dt =
+          join_image_term.getType().getSetElementType().getDatatype();
       Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
                                                              NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
                                                                                                Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
@@ -428,7 +429,8 @@ void TheorySetsRels::check(Theory::Effort level)
     Node reason = exp;
     Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
     Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
-    Datatype dt = iden_term[0].getType().getSetElementType().getDatatype();
+    const Datatype& dt =
+        iden_term[0].getType().getSetElementType().getDatatype();
     Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
 
     if( exp[1] != iden_term ) {
@@ -765,18 +767,18 @@ void TheorySetsRels::check(Theory::Effort level)
     Node mem = exp[0];
     std::vector<Node>   r1_element;
     std::vector<Node>   r2_element;
-    Datatype     dt      = pt_rel[0].getType().getSetElementType().getDatatype();
+    const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype();
     unsigned int s1_len  = pt_rel[0].getType().getSetElementType().getTupleLength();
     unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
 
-    r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+    r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
 
     unsigned int i = 0;
     for(; i < s1_len; ++i) {
       r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
-    dt = pt_rel[1].getType().getSetElementType().getDatatype();
-    r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+    const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype();
+    r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
     for(; i < tup_len; ++i) {
       r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
@@ -823,18 +825,20 @@ void TheorySetsRels::check(Theory::Effort level)
     TypeNode     shared_type    = r2_rep.getType().getSetElementType().getTupleTypes()[0];
     Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached(
         shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
-    Datatype     dt             = join_rel[0].getType().getSetElementType().getDatatype();
+    const Datatype& dt1 =
+        join_rel[0].getType().getSetElementType().getDatatype();
     unsigned int s1_len         = join_rel[0].getType().getSetElementType().getTupleLength();
     unsigned int tup_len        = join_rel.getType().getSetElementType().getTupleLength();
 
     unsigned int i = 0;
-    r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+    r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
     for(; i < s1_len-1; ++i) {
       r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
     r1_element.push_back(shared_x);
-    dt = join_rel[1].getType().getSetElementType().getDatatype();
-    r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
+    const Datatype& dt2 =
+        join_rel[1].getType().getSetElementType().getDatatype();
+    r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
     r2_element.push_back(shared_x);
     for(; i < tup_len; ++i) {
       r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index aa6f4de3f..a7c506582 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -431,7 +431,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
           ++rel_mems_it_snd;
         }
         if( existing_mems.size() >= min_card ) {
-          Datatype dt = node.getType().getSetElementType().getDatatype();
+          const Datatype& dt = node.getType().getSetElementType().getDatatype();
           join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
         }
         ++rel_mems_it;
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)