Merge pull request #30 from cvc5/updateNilSyntax2

This is a more more consistent naming, since it now we have alf.nil / alf.cons as operators on list terms.

alf.null may disappear if we find a good solution to non-ground nil terminators.

src/compiler.cpp

@@ -460,7 +460,7 @@ size_t Compiler::writeExprInternal(const Expr& e, CompilerScope& s)
       {
         os << "  " << cs.d_prefix << ret << " = d_boolType;" << std::endl;
       }
-      else if (ck==Kind::NIL)
+      else if (ck==Kind::NULL_EXPR)
       {
         os << "  " << cs.d_prefix << ret << " = d_nil;" << std::endl;
       }

src/kind.cpp

@@ -33,7 +33,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::VARIABLE: o << "VARIABLE"; break;
     case Kind::ORACLE: o << "ORACLE"; break;
     case Kind::TUPLE: o << "TUPLE"; break;
-    case Kind::NIL: o << "NIL"; break;
+    case Kind::NULL_EXPR: o << "NIL"; break;
     case Kind::PROGRAM: o << "PROGRAM"; break;
     case Kind::COLLECT: o << "COLLECT"; break;
     case Kind::AS: o << "AS"; break;
@@ -52,7 +52,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_HASH: o << "EVAL_HASH"; break;
     case Kind::EVAL_TYPE_OF: o << "EVAL_TYPE_OF"; break;
     // lists
-    case Kind::EVAL_EMPTYLIST: o << "EVAL_EMPTYLIST";break;
+    case Kind::EVAL_NIL: o << "EVAL_EMPTYLIST";break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
     // boolean
     case Kind::EVAL_NOT: o << "EVAL_NOT"; break;
@@ -93,7 +93,7 @@ std::string kindToTerm(Kind k)
     case Kind::ABSTRACT_TYPE: ss << "?"; break;
     case Kind::BOOL_TYPE: ss << "Bool"; break;
     case Kind::QUOTE_TYPE: ss << "Quote"; break;
-    case Kind::NIL: ss << "alf.nil"; break;
+    case Kind::NULL_EXPR: ss << "alf.nil"; break;
     // terms
     case Kind::APPLY: ss << "@"; break;
     case Kind::LAMBDA: ss << "lambda"; break;
@@ -112,7 +112,7 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_HASH: ss << "hash"; break;
         case Kind::EVAL_TYPE_OF: ss << "typeof"; break;
         // lists
-        case Kind::EVAL_EMPTYLIST: ss << "emptylist"; break;
+        case Kind::EVAL_NIL: ss << "emptylist"; break;
         case Kind::EVAL_CONS: ss << "cons"; break;
         // boolean
         case Kind::EVAL_NOT: ss << "not"; break;
@@ -188,7 +188,7 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_HASH:
     case Kind::EVAL_TYPE_OF:
     // lists
-    case Kind::EVAL_EMPTYLIST:
+    case Kind::EVAL_NIL:
     case Kind::EVAL_CONS:
     // boolean
     case Kind::EVAL_NOT:

src/kind.h

@@ -32,7 +32,7 @@ enum class Kind
   APPLY,
   LAMBDA,
   TUPLE,
-  NIL,
+  NULL_EXPR,
   PROGRAM,
   COLLECT,
   AS,
@@ -62,7 +62,7 @@ enum class Kind
   EVAL_HASH,
   EVAL_TYPE_OF,
   // lists
-  EVAL_EMPTYLIST,
+  EVAL_NIL,
   EVAL_CONS,
   // boolean
   EVAL_NOT,

src/state.cpp

@@ -53,7 +53,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("typeof", Kind::EVAL_TYPE_OF);
   // TODO: compare?
   // lists
-  bindBuiltinEval("emptylist", Kind::EVAL_EMPTYLIST);
+  bindBuiltinEval("nil", Kind::EVAL_NIL);
   bindBuiltinEval("cons", Kind::EVAL_CONS);
   // boolean
   bindBuiltinEval("not", Kind::EVAL_NOT);
@@ -81,8 +81,8 @@ State::State(Options& opts, Stats& stats)
   // as
   bindBuiltinEval("as", Kind::AS);
 
-  d_nil = Expr(mkExprInternal(Kind::NIL, {}));
-  bind("alf.nil", d_nil);
+  d_nullExpr = Expr(mkExprInternal(Kind::NULL_EXPR, {}));
+  bind("alf.null", d_nullExpr);
   // self is a distinguished parameter
   d_self = Expr(mkSymbolInternal(Kind::PARAM, "alf.self", mkAbstractType()));
   bind("alf.self", d_self);
@@ -493,7 +493,7 @@ Expr State::mkAnnotatedType(const Expr& t, Attr ck, const Expr& cons)
   {
     return t;
   }
-  if (cons.getKind() != Kind::NIL)
+  if (cons.getKind() != Kind::NULL_EXPR)
   {
     return t;
   }
@@ -542,7 +542,7 @@ Expr State::mkAnnotatedType(const Expr& t, Attr ck, const Expr& cons)
   std::stringstream ss;
   ss << nilArg << "_or_nil";
   Expr u = mkSymbol(Kind::PARAM, ss.str(), d_type);
-  Expr cond = mkExpr(Kind::EVAL_IS_EQ, {u, d_nil});
+  Expr cond = mkExpr(Kind::EVAL_IS_EQ, {u, d_nullExpr});
   if (isRight)
   {
     // (-> t1 (-> t2 t3)) :right-assoc-nil
@@ -584,7 +584,7 @@ Expr State::mkConclusion()
 
 Expr State::mkNil()
 {
-  return d_nil;
+  return d_nullExpr;
 }
 
 Expr State::mkPair(const Expr& t1, const Expr& t2)
@@ -682,7 +682,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
             size_t nextIndex = isLeft ? 2 : 1;
             size_t prevIndex = isLeft ? 1 : 2;
             // note the nil element is always treated as a list
-            if (curr->getKind()!=Kind::NIL && isNil)
+            if (curr->getKind()!=Kind::NULL_EXPR && isNil)
             {
               if (getConstructorKind(curr) != Attr::LIST)
               {

src/state.h

@@ -178,7 +178,7 @@ class State
   Expr d_false;
   Expr d_self;
   Expr d_conclusion;
-  Expr d_nil;
+  Expr d_nullExpr;
   Expr d_fail;
   /** Get the constructor kind for symbol v */
   Attr getConstructorKind(const ExprValue* v) const;

src/type_checker.cpp

@@ -154,7 +154,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
   // check arities
   switch(k)
   {
-    case Kind::NIL:
+    case Kind::NULL_EXPR:
       ret = (nargs==0);
       break;
     case Kind::EVAL_IS_EQ:
@@ -184,7 +184,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_TO_INT:
     case Kind::EVAL_TO_RAT:
     case Kind::EVAL_TO_STRING:
-    case Kind::EVAL_EMPTYLIST:
+    case Kind::EVAL_NIL:
       ret = (nargs==1);
       break;
     case Kind::EVAL_REQUIRES:
@@ -235,7 +235,7 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
       Assert(!ret.isNull());
       return d_state.mkFunctionType(args, ret);
     }
-    case Kind::NIL:
+    case Kind::NULL_EXPR:
       if (!checkArity(k, e->getNumChildren(), out))
       {
         return d_null;
@@ -1133,7 +1133,7 @@ Expr TypeChecker::evaluateLiteralOpInternal(
   std::vector<ExprValue*> hargs;
   switch (k)
   {
-    case Kind::EVAL_EMPTYLIST:
+    case Kind::EVAL_NIL:
     {
       return ac->d_attrConsTerm;
     }
@@ -1248,7 +1248,7 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
     case Kind::EVAL_MUL:
       // NOTE: mixed arith
       return childTypes[0];
-    case Kind::EVAL_EMPTYLIST:
+    case Kind::EVAL_NIL:
       // type is not computable here, since it is the return type of function
       // applications of the argument. just use abstract.
       return d_state.mkAbstractType().getValue();

tests/Quantifiers-rules.smt3

@@ -15,7 +15,7 @@
   (@List @List U) U
   (
     ((substitute_list (@list x xs) (@list t ts) F) (substitute_list xs ts (substitute x t F)))
-    ((substitute_list alf.nil alf.nil F)           F)
+    ((substitute_list alf.null alf.null F)           F)
   )
 )
 
@@ -30,7 +30,7 @@
   (@List Bool) @List
   (
     ((mk_skolems (@list x xs) F) (alf.cons @list (skolem (@k.QUANTIFIERS_SKOLEMIZE F x)) (mk_skolems xs F)))
-    ((mk_skolems alf.nil F)      alf.nil)
+    ((mk_skolems alf.null F)      alf.null)
   )
 )
 

tests/Strings-programs.smt3

@@ -66,7 +66,7 @@
 )
 
 ; Return reverse of t if rev = tt, return t unchanged otherwise.
-(define string_rev ((U Type) (rev Bool) (t U)) (alf.ite rev (nary.reverse str.++ alf.nil t) t))
+(define string_rev ((U Type) (rev Bool) (t U)) (alf.ite rev (nary.reverse str.++ alf.null t) t))
 
 ; Returns true if the length of s evaluates to one, false otherwise.
 (define check_length_one ((s String)) (check_true (alf.is_eq (alf.len s) 1)))
@@ -76,12 +76,12 @@
 
 ; Get first character or empty string from term t.
 ; If t is of the form (str.++ t ...), return t.
-; If t is of the form alf.nil, return alf.nil.
+; If t is of the form alf.null, return alf.null.
 (program string_head_or_empty ((U Type) (T Type) (t U) (tail U :list) (s T))
   (U) U
   (
     ((string_head_or_empty (str.++ t tail)) t)
-    ((string_head_or_empty alf.nil)         alf.nil)
+    ((string_head_or_empty alf.null)         alf.null)
   )
 )
 
@@ -99,29 +99,29 @@
 ; str.++ application corresponding to a string term in cvc5 rewritten form.
 ; It returns the flattened form such that there are no nested applications of
 ; str.++. For example, given input:
-;    (str.++ "AB" (str.++ x alf.nil))
+;    (str.++ "AB" (str.++ x alf.null))
 ; we return:
-;    (str.++ "A" (str.++ "B" (str.++ x alf.nil)))
+;    (str.++ "A" (str.++ "B" (str.++ x alf.null)))
 ; Notice that this is done for all word constants in the chain recursively.
 ; It does not insist that the nested concatenations are over characters only.
 ; This rule may fail if s is not a str.++ application corresponding to a term
 ; in cvc5 rewritten form.
 
 ; Helper for below, assumes t is a non-empty word constant.
-; For example, given "AB", this returns (str.++ "A" (str.++ "B" alf.nil)).
+; For example, given "AB", this returns (str.++ "A" (str.++ "B" alf.null)).
 (program string_flatten_word ((t String))
   (String) String
   (
     ((string_flatten_word t) 
       (alf.ite (check_length_one t) 
-        (alf.cons str.++ t alf.nil)
+        (alf.cons str.++ t alf.null)
         (alf.cons str.++ (alf.extract t 0 0) (string_flatten_word (alf.extract t 1 (alf.len t))))))
   )
 )
 (program string_flatten ((U Type) (t U) (tail U :list) (tail2 U :list))
   (U) U
   (
-    ((string_flatten alf.nil) alf.nil)
+    ((string_flatten alf.null) alf.null)
     ; required for sequences
     ((string_flatten (str.++ (str.++ t tail2) tail)) 
         (alf.concat str.++ (str.++ t tail2) (string_flatten tail)))
@@ -140,9 +140,9 @@
 ; whose first component corresponds to a word constant, and whose second
 ; component is a str.++ application whose first element is not a character.
 ; For example, for:
-;   (str.++ "A" (str.++ "B" (str.++ x alf.nil)))
+;   (str.++ "A" (str.++ "B" (str.++ x alf.null)))
 ; We return:
-;   (@pair "AB" (str.++ x alf.nil))
+;   (@pair "AB" (str.++ x alf.null))
 (program string_collect_acc ((U Type) (t U) (tail String :list))
   (U) (@Pair U U)
   (
@@ -153,32 +153,32 @@
         (alf.match ((s1 U) (s2 U)) 
           (string_collect_acc tail)
           (
-            ((@pair alf.nil s2)  (@pair t s2))
+            ((@pair alf.null s2)  (@pair t s2))
             ((@pair s1 s2)       (@pair (alf.concat t s1) s2))    ; concatentate the constant
           )
         )
-        (@pair alf.nil (str.++ t tail))))
-    ((string_collect_acc alf.nil)            (@pair alf.nil alf.nil))
+        (@pair alf.null (str.++ t tail))))
+    ((string_collect_acc alf.null)            (@pair alf.null alf.null))
   )
 )
 
 ; Collect adjacent constants for the prefix of string s. For example:
-;    (str.++ "A" (str.++ "B" (str.++ x alf.nil)))
+;    (str.++ "A" (str.++ "B" (str.++ x alf.null)))
 ; we return:
-;    (str.++ (str.++ "A" (str.++ "B" alf.nil)) (str.++ x alf.nil))
+;    (str.++ (str.++ "A" (str.++ "B" alf.null)) (str.++ x alf.null))
 ; This side condition may fail if s is not a str.++ application.
 ; Notice that the collection of constants is done for all word constants in the
 ; term s recursively.
 (program string_collect ((U Type) (t U) (s U :list))
   (U) U
   (
-    ((string_collect alf.nil)       alf.nil)
+    ((string_collect alf.null)       alf.null)
     ((string_collect (str.++ t s))
       (alf.match ((s1 U) (s2 U))
         (string_collect_acc (str.++ t s))
         (
           ; did not strip a constant prefix, just append t to the result of processing s
-          ((@pair alf.nil s2)
+          ((@pair alf.null s2)
             (alf.cons str.++ t (string_collect s)))
           ; stripped a constant prefix, append it to second term in the pair
           ((@pair s1 s2)
@@ -211,7 +211,7 @@
 ; (3) (optionally) reverse.
 (define string_to_flat_form ((U Type) (s U) (rev Bool))
   ; intro, flatten, reverse
-  (string_rev U rev (string_flatten (nary.intro str.++ (mk_emptystr U) alf.nil s))))
+  (string_rev U rev (string_flatten (nary.intro str.++ (mk_emptystr U) alf.null s))))
 
 ; Converts a term in "flat form" to a term that is in a form that corresponds
 ; to one in cvc5 rewritten form. This is the dual method to
@@ -221,4 +221,4 @@
 ; (3) eliminate n-ary form to its element if the term is a singleton list.
 (define string_from_flat_form ((U Type) (s U) (rev Bool))
   ; reverse, collect, elim
-  (nary.elim str.++ alf.nil (mk_emptystr U) (string_collect (string_rev U rev s))))
+  (nary.elim str.++ alf.null (mk_emptystr U) (string_collect (string_rev U rev s))))

tests/and-intro-old.smt3

@@ -2,7 +2,7 @@
     (T T) T
     (
       ((maybe_nil t t)       t)
-      ((maybe_nil t alf.nil) t)
+      ((maybe_nil t alf.null) t)
     )
 )
 (declare-const and (-> (! Type :var U :implicit) Bool U (maybe_nil Bool U)) :right-assoc-nil)

tests/emptylist.smt3

@@ -9,14 +9,14 @@
     ((-> U U) Bool) Bool
     (
         ((mk_nary_cong_lhs f (and (= s1 s2) tail)) (f s1 (mk_nary_cong_lhs f tail)))
-        ((mk_nary_cong_lhs f true)                 (alf.emptylist f))
+        ((mk_nary_cong_lhs f true)                 (alf.nil f))
     )
 )
 (program mk_nary_cong_rhs ((U Type) (f (-> U U)) (t1 U) (t2 U) (s1 U) (s2 U)  (tail Bool :list))
     ((-> U U) Bool) Bool
     (
         ((mk_nary_cong_rhs f (and (= s1 s2) tail)) (f s2 (mk_nary_cong_rhs f tail)))
-        ((mk_nary_cong_rhs f true)                 (alf.emptylist f))
+        ((mk_nary_cong_rhs f true)                 (alf.nil f))
     )
 )