Add typeof

cvc5 · Jan 30, 2024 · 97fe9d4 · 97fe9d4
1 parent 50ade27
commit 97fe9d4
Show file tree

Hide file tree

Showing 6 changed files with 39 additions and 0 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -49,6 +49,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_IF_THEN_ELSE: o << "EVAL_IF_THEN_ELSE"; break;
     case Kind::EVAL_REQUIRES: o << "EVAL_REQUIRES"; break;
     case Kind::EVAL_HASH: o << "EVAL_HASH"; break;
+    case Kind::EVAL_TYPE_OF: o << "EVAL_TYPE_OF"; break;
     // lists
     case Kind::EVAL_TO_LIST: o << "EVAL_TO_LIST"; break;
     case Kind::EVAL_FROM_LIST: o << "EVAL_FROM_LIST"; break;
@@ -108,6 +109,7 @@ std::string kindToTerm(Kind k)
         case Kind::EVAL_IF_THEN_ELSE: ss << "ite"; break;
         case Kind::EVAL_REQUIRES: ss << "requires"; break;
         case Kind::EVAL_HASH: ss << "hash"; break;
+        case Kind::EVAL_TYPE_OF: ss << "typeof"; break;
         // lists
         case Kind::EVAL_TO_LIST: ss << "to_list"; break;
         case Kind::EVAL_FROM_LIST: ss << "from_list"; break;
@@ -184,6 +186,7 @@ bool isLiteralOp(Kind k)
     case Kind::EVAL_IF_THEN_ELSE:
     case Kind::EVAL_REQUIRES:
     case Kind::EVAL_HASH:
+    case Kind::EVAL_TYPE_OF:
     // lists
     case Kind::EVAL_TO_LIST:
     case Kind::EVAL_FROM_LIST:

diff --git a/src/kind.h b/src/kind.h
@@ -59,6 +59,7 @@ enum class Kind
   EVAL_IF_THEN_ELSE,
   EVAL_REQUIRES,
   EVAL_HASH,
+  EVAL_TYPE_OF,
   // lists
   EVAL_TO_LIST,
   EVAL_FROM_LIST,

diff --git a/src/state.cpp b/src/state.cpp
@@ -50,6 +50,7 @@ State::State(Options& opts, Stats& stats)
   bindBuiltinEval("ite", Kind::EVAL_IF_THEN_ELSE);
   bindBuiltinEval("requires", Kind::EVAL_REQUIRES);
   bindBuiltinEval("hash", Kind::EVAL_HASH);
+  bindBuiltinEval("typeof", Kind::EVAL_TYPE_OF);
   // TODO: compare?
   // lists
   bindBuiltinEval("to_list", Kind::EVAL_TO_LIST);

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -175,6 +175,7 @@ bool TypeChecker::checkArity(Kind k, size_t nargs, std::ostream* out)
       ret = (nargs>=2);
       break;
     case Kind::PROOF_TYPE:
+    case Kind::EVAL_TYPE_OF:
     case Kind::EVAL_HASH:
     case Kind::EVAL_NOT:
     case Kind::EVAL_NEG:
@@ -246,6 +247,7 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
     case Kind::ABSTRACT_TYPE:
     case Kind::BOOL_TYPE:
     case Kind::FUNCTION_TYPE:
+    case Kind::EVAL_TYPE_OF:
       return d_state.mkType();
     case Kind::PROOF_TYPE:
     {
@@ -1036,6 +1038,7 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       }
       return d_null;
     }
+    break;
     case Kind::EVAL_HASH:
     {
       if (args[0]->isGround())
@@ -1046,6 +1049,18 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       }
       return d_null;
     }
+    break;
+    case Kind::EVAL_TYPE_OF:
+    {
+      // get the type if ground
+      if (isGround(args))
+      {
+        Expr e(args[0]);
+        return getType(e);
+      }
+      return d_null;
+    }
+    break;
     default:
       break;
   }

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -97,6 +97,7 @@ set(alfc_test_file_list
     tiny_oracle.smt3
     arity-overload.smt3
     binder-ex.smt3
+    typeof.smt3
 )
 
 macro(alfc_test file)

diff --git a/tests/typeof.smt3 b/tests/typeof.smt3
@@ -0,0 +1,18 @@
+(declare-const = (-> (! Type :var A :implicit) A A Bool))
+
+(declare-sort Int 0)
+(declare-consts <numeral> Int)
+
+(declare-sort Real 0)
+(declare-consts <rational> Real)
+
+(declare-const to_real (-> Int Real))
+(declare-const not (-> Bool Bool))
+
+(declare-rule not_half ((T Type) (x T))
+  :args (x)
+  :requires (((alf.typeof x) Int))
+  :conclusion (not (= (to_real x) 0.5)))
+
+
+(step @p0 (not (= (to_real 1) 0.5)) :rule not_half :args (1))