Use alf.nil_of as placeholder for non-ground nil terminators

cvc5 · Apr 4, 2024 · b639495 · b639495
1 parent bc7facb
commit b639495
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 2 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -56,6 +56,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     // lists
     case Kind::EVAL_NIL: o << "EVAL_NIL";break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
+    case Kind::EVAL_NIL_OF: o << "EVAL_NIL_OF"; break;
     // boolean
     case Kind::EVAL_NOT: o << "EVAL_NOT"; break;
     case Kind::EVAL_AND: o << "EVAL_AND"; break;
@@ -117,8 +118,9 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_TYPE_OF: ss << "typeof"; break;
         case Kind::EVAL_NAME_OF: ss << "nameof"; break;
         // lists
-        case Kind::EVAL_NIL: ss << "emptylist"; break;
+        case Kind::EVAL_NIL: ss << "nil"; break;
         case Kind::EVAL_CONS: ss << "cons"; break;
+        case Kind::EVAL_NIL_OF: ss << "nil_of"; break;
         // boolean
         case Kind::EVAL_NOT: ss << "not"; break;
         case Kind::EVAL_AND: ss << "and"; break;
@@ -197,6 +199,7 @@ bool isLiteralOp(Kind k)
     // lists
     case Kind::EVAL_NIL:
     case Kind::EVAL_CONS:
+    case Kind::EVAL_NIL_OF:
     // boolean
     case Kind::EVAL_NOT:
     case Kind::EVAL_AND:

diff --git a/src/kind.h b/src/kind.h
@@ -66,6 +66,9 @@ enum class Kind
   // lists
   EVAL_NIL,
   EVAL_CONS,
+  // internal only, (alf.nil_of f t1 ... tn) is the nil terminator of f
+  // applied to t1 ... tn.
+  EVAL_NIL_OF,
   // boolean
   EVAL_NOT,
   EVAL_AND,

diff --git a/src/state.cpp b/src/state.cpp
@@ -639,7 +639,19 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
                 // if the last term is not marked as a list variable and
                 // we have a null terminator, then we insert the null terminator
                 Trace("state-debug") << "...insert nil terminator " << consTerm << std::endl;
-                curr = consTerm.getValue();
+                if (consTerm.isNull())
+                {
+                  // if we failed to infer a nil terminator (likely due to
+                  // a non-ground parameter), then we insert a placeholder
+                  // (alf.nil f t1 ... tn), which if t1...tn are non-ground
+                  // will evaluate to the proper nil terminator when
+                  // instantiated.
+                  curr = mkExprInternal(Kind::EVAL_NIL_OF, vchildren);
+                }
+                else
+                {
+                  curr = consTerm.getValue();
+                }
                 i--;
               }
             }

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -190,6 +190,9 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
     case Kind::EVAL_NIL:
       ret = (nargs==1);
       break;
+    case Kind::EVAL_NIL_OF:
+      ret = (nargs>=1);
+      break;
     case Kind::EVAL_REQUIRES:
     case Kind::EVAL_IF_THEN_ELSE:
       ret = (nargs==3);
@@ -1198,6 +1201,7 @@ Expr TypeChecker::evaluateLiteralOpInternal(
   switch (k)
   {
     case Kind::EVAL_NIL:
+    case Kind::EVAL_NIL_OF:
     {
       return nilExpr;
     }
@@ -1439,6 +1443,13 @@ bool TypeChecker::computedParameterizedInternal(AppInfo* ai,
             Warning() << "Failed to find context for " << ct[0][i] << " when applying " << hd << " @ " << children[1] << std::endl;
             return false;
           }
+          if (!cv.isGround())
+          {
+            // If the parameter is non-ground, we also wait to construct;
+            // if the nil terminator is used, it will be replaced by a
+            // placeholder involving alf.nil_of.
+            return false;
+          }
           args.emplace_back(cv);
         }
         // the head is now disambiguated