Add support for emptylist

cvc5 · Feb 2, 2024 · e32a2a2 · e32a2a2
1 parent 00598b8
commit e32a2a2
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 2 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -51,6 +51,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_TO_LIST: o << "EVAL_TO_LIST"; break;
     case Kind::EVAL_FROM_LIST: o << "EVAL_FROM_LIST"; break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
@@ -111,6 +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_TO_LIST: ss << "to_list"; break;
         case Kind::EVAL_FROM_LIST: ss << "from_list"; break;
         case Kind::EVAL_CONS: ss << "cons"; break;
@@ -188,6 +190,7 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_HASH:
     case Kind::EVAL_TYPE_OF:
     // lists
+    case Kind::EVAL_EMPTYLIST:
     case Kind::EVAL_TO_LIST:
     case Kind::EVAL_FROM_LIST:
     case Kind::EVAL_CONS:

diff --git a/src/kind.h b/src/kind.h
@@ -61,6 +61,7 @@ enum class Kind
   EVAL_HASH,
   EVAL_TYPE_OF,
   // lists
+  EVAL_EMPTYLIST,
   EVAL_TO_LIST,
   EVAL_FROM_LIST,
   EVAL_CONS,

diff --git a/src/state.cpp b/src/state.cpp
@@ -53,6 +53,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("typeof", Kind::EVAL_TYPE_OF);
   // TODO: compare?
   // lists
+  bindBuiltinEval("emptylist", Kind::EVAL_EMPTYLIST);
   bindBuiltinEval("to_list", Kind::EVAL_TO_LIST);
   bindBuiltinEval("from_list", Kind::EVAL_FROM_LIST);
   bindBuiltinEval("cons", Kind::EVAL_CONS);

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -164,6 +164,8 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_TO_BV:
     case Kind::EVAL_FIND:
     case Kind::EVAL_CONS:
+    case Kind::EVAL_TO_LIST:
+    case Kind::EVAL_FROM_LIST:
       ret = (nargs==2);
       break;
     case Kind::EVAL_ADD:
@@ -184,8 +186,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_TO_LIST:
-    case Kind::EVAL_FROM_LIST:
+    case Kind::EVAL_EMPTYLIST:
       ret = (nargs==1);
       break;
     case Kind::EVAL_REQUIRES:
@@ -1124,6 +1125,11 @@ Expr TypeChecker::evaluateLiteralOpInternal(
   std::vector<ExprValue*> hargs;
   switch (k)
   {
+    case Kind::EVAL_EMPTYLIST:
+    {
+      return ac->d_attrConsTerm;
+    }
+    break;
     case Kind::EVAL_TO_LIST:
     {
       ExprValue* harg = args[1];
@@ -1276,6 +1282,10 @@ ExprValue* TypeChecker::getLiteralOpType(Kind k,
     case Kind::EVAL_MUL:
       // NOTE: mixed arith
       return childTypes[0];
+    case Kind::EVAL_EMPTYLIST:
+      // 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();
     case Kind::EVAL_NEG:
     case Kind::EVAL_AND:
     case Kind::EVAL_OR:

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -100,6 +100,7 @@ set(alfc_test_file_list
     typeof.smt3
     binder-subterm-share.smt3
     or-concat-false.smt3
+    emptylist.smt3
 )
 
 macro(alfc_test file)

diff --git a/user_manual.md b/user_manual.md
@@ -578,6 +578,8 @@ We describe the evaluation for right associative operators; left associative eva
 We say that a term is an `f`-list with children `t1 ... tn` if it is of the form `(f t1 ... tn)` where `n>0` or `nil` if `n=0`.
 
 List operators:
+- `(alf.emptylist f)`
+    - If `f` is a right associative operator, return its nil terminator.
 - `(alf.cons f t1 t2)`
     - If `t2` is an `f`-list, then this returns the term `(f t1 t2)`.
 - `(alf.concat f t1 t2)`
@@ -597,6 +599,9 @@ The terms on both sides of the given evaluation are written in their form prior
 (declare-const a Bool)
 (declare-const b Bool)
 
+(alf.emptylist or)                  == false
+(alf.emptylist a)                   == (alf.emptylist a)                ; since a is not an associative operator
+
 (alf.cons or a (or a b))            == (or a a b)
 (alf.cons or false (or a b))        == (or false a b)
 (alf.cons or (or a b) (or b))       == (or (or a b) b)