From bc7d8b4922e37abf128c36136cede86048b420eb Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 25 Mar 2022 13:50:34 -0700 Subject: [PATCH] api: Rename kind NULL_EXPR to NULL_TERM. (#8402) --- src/api/cpp/cvc5.cpp | 10 +++++----- src/api/cpp/cvc5_kind.h | 2 +- src/parser/parse_op.cpp | 2 +- src/parser/parse_op.h | 2 +- src/parser/smt2/Smt2.g | 4 ++-- src/parser/smt2/smt2.cpp | 10 +++++----- src/parser/tptp/tptp.cpp | 8 ++++---- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 8a269a241..4544fd7d2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -116,7 +116,7 @@ const static std::unordered_map> 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> const static std::unordered_map 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 57e8133b3..9beca24ae 100644 --- 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 3471d9fb0..ef7ddec2e 100644 --- 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 1484c3e90..c5d2c459b 100644 --- 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 f1476b94d..870831dbe 100644 --- 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 args; std::vector< std::pair > sortedVarNames; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 031210cab..f921b6fb5 100644 --- 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& 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& 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& 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& 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 8681b623a..fcbdea9b6 100644 --- 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& 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& 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) { -- 2.30.2