api: Rename kind NULL_EXPR to NULL_TERM. (#8402)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 8a269a24157b3de746a4c38f571f740495c98204..4544fd7d2bb2510404142cb18317f307e2221535 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -116,7 +116,7 @@ const static std::unordered_map<Kind, std::pair<cvc5::Kind, std::string>>
     s_kinds{
         KIND_ENUM(INTERNAL_KIND, cvc5::Kind::UNDEFINED_KIND),
         KIND_ENUM(UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND),
-        KIND_ENUM(NULL_EXPR, cvc5::Kind::NULL_EXPR),
+        KIND_ENUM(NULL_TERM, cvc5::Kind::NULL_EXPR),
         /* Builtin ---------------------------------------------------------- */
         KIND_ENUM(UNINTERPRETED_SORT_VALUE,
                   cvc5::Kind::UNINTERPRETED_SORT_VALUE),
@@ -402,7 +402,7 @@ const static std::unordered_map<Kind, std::pair<cvc5::Kind, std::string>>
 const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
     s_kinds_internal{
         {cvc5::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
-        {cvc5::Kind::NULL_EXPR, NULL_EXPR},
+        {cvc5::Kind::NULL_EXPR, NULL_TERM},
         /* Builtin --------------------------------------------------------- */
         {cvc5::Kind::UNINTERPRETED_SORT_VALUE, UNINTERPRETED_SORT_VALUE},
         {cvc5::Kind::EQUAL, EQUAL},
@@ -1800,7 +1800,7 @@ bool Sort::isNullHelper() const { return d_type->isNull(); }
 /* Op                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new cvc5::Node()) {}
+Op::Op() : d_solver(nullptr), d_kind(NULL_TERM), d_node(new cvc5::Node()) {}
 
 Op::Op(const Solver* slv, const Kind k)
     : d_solver(slv), d_kind(k), d_node(new cvc5::Node())
@@ -1851,7 +1851,7 @@ bool Op::operator!=(const Op& t) const
 
 Kind Op::getKind() const
 {
-  CVC5_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind";
+  CVC5_API_CHECK(d_kind != NULL_TERM) << "Expecting a non-null Kind";
   //////// all checks before this line
   return d_kind;
 }
@@ -2121,7 +2121,7 @@ std::ostream& operator<<(std::ostream& out, const Op& t)
 
 bool Op::isNullHelper() const
 {
-  return (d_node->isNull() && (d_kind == NULL_EXPR));
+  return (d_node->isNull() && (d_kind == NULL_TERM));
 }
 
 bool Op::isIndexedHelper() const { return !d_node->isNull(); }

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 57e8133b3e3cb948e4091f291b23dca4dc438543..9beca24ae5db589ed7ea4284561b7fd6cd21a8c7 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -62,7 +62,7 @@ enum Kind : int32_t
    * @note May not be explicitly created via API functions other than
    *       Term::Term().
    */
-  NULL_EXPR,
+  NULL_TERM,
 
   /* Builtin --------------------------------------------------------------- */
 

diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp
index 3471d9fb0d13f63944e6facd2a86060baac4ea88..ef7ddec2e3c268fded94161b96a67c11d5993b3c 100644 (file)
--- a/src/parser/parse_op.cpp
+++ b/src/parser/parse_op.cpp
@@ -29,7 +29,7 @@ std::ostream& operator<<(std::ostream& os, const ParseOp& p)
   {
     out << " :op " << p.d_op;
   }
-  if (p.d_kind != api::NULL_EXPR)
+  if (p.d_kind != api::NULL_TERM)
   {
     out << " :kind " << p.d_kind;
   }

diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h
index 1484c3e90e2f3399e241661d25fa12289998b9c8..c5d2c459b4edfbe9927c01504682b4176f38e977 100644 (file)
--- a/src/parser/parse_op.h
+++ b/src/parser/parse_op.h
@@ -59,7 +59,7 @@ namespace cvc5 {
  */
 struct ParseOp
 {
-  ParseOp(api::Kind k = api::NULL_EXPR) : d_kind(k) {}
+  ParseOp(api::Kind k = api::NULL_TERM) : d_kind(k) {}
   /** The kind associated with the parsed operator, if it exists */
   api::Kind d_kind;
   /** The name associated with the parsed operator, if it exists */

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f1476b94d70aad394bad89bdc751c5eb12709b9b..870831dbe4cf3f36b8f19bf0c24841df9183ed84 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1248,7 +1248,7 @@ symbolicExpr[cvc5::api::Term& sexpr]
  */
 term[cvc5::api::Term& expr, cvc5::api::Term& expr2]
 @init {
-  api::Kind kind = api::NULL_EXPR;
+  api::Kind kind = api::NULL_TERM;
   cvc5::api::Term f;
   std::string name;
   cvc5::api::Sort type;
@@ -1272,7 +1272,7 @@ term[cvc5::api::Term& expr, cvc5::api::Term& expr2]
 termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
 @init {
   Trace("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
-  api::Kind kind = api::NULL_EXPR;
+  api::Kind kind = api::NULL_TERM;
   std::string name;
   std::vector<cvc5::api::Term> args;
   std::vector< std::pair<std::string, cvc5::api::Sort> > sortedVarNames;

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 031210cabd0fd164d35f5561146f9b02ed747a8c..f921b6fb561c2a18798548a6bd46691f59dc6ec9 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -863,7 +863,7 @@ api::Term Smt2::parseOpToExpr(ParseOp& p)
 {
   Trace("parser") << "parseOpToExpr: " << p << std::endl;
   api::Term expr;
-  if (p.d_kind != api::NULL_EXPR || !p.d_type.isNull())
+  if (p.d_kind != api::NULL_TERM || !p.d_type.isNull())
   {
     parseError(
         "Bad syntax for qualified identifier operator in term position.");
@@ -890,7 +890,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
 {
   bool isBuiltinOperator = false;
   // the builtin kind of the overall return expression
-  api::Kind kind = api::NULL_EXPR;
+  api::Kind kind = api::NULL_TERM;
   // First phase: process the operator
   if (TraceIsOn("parser"))
   {
@@ -902,7 +902,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   api::Op op;
-  if (p.d_kind != api::NULL_EXPR)
+  if (p.d_kind != api::NULL_TERM)
   {
     // It is a special case, e.g. tuple_select or array constant specification.
     // We have to wait until the arguments are parsed to resolve it.
@@ -1094,7 +1094,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     Trace("parser") << "applyParseOp: return projection " << ret << std::endl;
     return ret;
   }
-  else if (p.d_kind != api::NULL_EXPR)
+  else if (p.d_kind != api::NULL_TERM)
   {
     // it should not have an expression or type specified at this point
     if (!p.d_expr.isNull() || !p.d_type.isNull())
@@ -1216,7 +1216,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     Trace("parser") << "applyParseOp: return op : " << ret << std::endl;
     return ret;
   }
-  if (kind == api::NULL_EXPR)
+  if (kind == api::NULL_TERM)
   {
     // should never happen in the new API
     parseError("do not know how to process parse op");

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 8681b623a6266e5a8978ad5c1fca339fde5b6bd4..fcbdea9b6dd1bdea91960fd30a5181d5ef0a89c4 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -239,7 +239,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p)
   }
   // if it has a kind, it's a builtin one and this function should not have been
   // called
-  Assert(p.d_kind == api::NULL_EXPR);
+  Assert(p.d_kind == api::NULL_TERM);
   expr = isTptpDeclared(p.d_name);
   if (expr.isNull())
   {
@@ -290,9 +290,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   }
   bool isBuiltinKind = false;
   // the builtin kind of the overall return expression
-  api::Kind kind = api::NULL_EXPR;
+  api::Kind kind = api::NULL_TERM;
   // First phase: piece operator together
-  if (p.d_kind == api::NULL_EXPR)
+  if (p.d_kind == api::NULL_TERM)
   {
     // A non-built-in function application, get the expression
     api::Term v = isTptpDeclared(p.d_name);
@@ -326,7 +326,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     kind = p.d_kind;
     isBuiltinKind = true;
   }
-  Assert(kind != api::NULL_EXPR);
+  Assert(kind != api::NULL_TERM);
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {