From 3cc0fe4d64cea1bfc155005e7fd7d8bc8f0c6ec3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Feb 2022 18:18:51 -0800 Subject: [PATCH] api: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8034) This renames the arithmetic kinds MINUS and UMINUS on the API level for consistency with our naming scheme for other operators (e.g., BITVECTOR_SUB, FLOATINGPOINT_SUB). --- examples/api/cpp/linear_arith.cpp | 2 +- examples/api/cpp/quickstart.cpp | 2 +- examples/api/cpp/sygus-fun.cpp | 2 +- examples/api/cpp/sygus-grammar.cpp | 2 +- examples/api/java/LinearArith.java | 2 +- examples/api/java/QuickStart.java | 2 +- examples/api/java/SygusFun.java | 2 +- examples/api/java/SygusGrammar.java | 2 +- examples/api/python/linear_arith.py | 2 +- examples/api/python/quickstart.py | 2 +- examples/api/python/sygus-fun.py | 2 +- examples/api/python/sygus-grammar.py | 2 +- src/api/cpp/cvc5.cpp | 12 ++++++------ src/api/cpp/cvc5_kind.h | 4 ++-- src/parser/smt2/smt2.cpp | 10 +++++----- src/parser/smt2/smt2.h | 4 ++-- src/parser/tptp/Tptp.g | 28 ++++++++++++++-------------- src/parser/tptp/tptp.cpp | 4 ++-- test/unit/api/cpp/solver_black.cpp | 6 +++--- test/unit/api/python/test_solver.py | 4 ++-- 20 files changed, 48 insertions(+), 48 deletions(-) diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 979959d21..9b027844a 100644 --- a/examples/api/cpp/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp @@ -44,7 +44,7 @@ int main() // Terms Term three_y = slv.mkTerm(MULT, three, y); - Term diff = slv.mkTerm(MINUS, y, x); + Term diff = slv.mkTerm(SUB, y, x); // Formulas Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp index 7758c5f79..5bcb6bc66 100644 --- a/examples/api/cpp/quickstart.cpp +++ b/examples/api/cpp/quickstart.cpp @@ -102,7 +102,7 @@ int main() // It is also possible to get values for compound terms, // even if those did not appear in the original formula. - Term xMinusY = solver.mkTerm(MINUS, x, y); + Term xMinusY = solver.mkTerm(SUB, x, y); Term xMinusYVal = solver.getValue(xMinusY); // We can now obtain the string representations of the values. diff --git a/examples/api/cpp/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 0f96e72a7..e7a554177 100644 --- a/examples/api/cpp/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp @@ -83,7 +83,7 @@ int main() Term one = slv.mkInteger(1); Term plus = slv.mkTerm(PLUS, start, start); - Term minus = slv.mkTerm(MINUS, start, start); + Term minus = slv.mkTerm(SUB, start, start); Term ite = slv.mkTerm(ITE, start_bool, start, start); Term And = slv.mkTerm(AND, start_bool, start_bool); diff --git a/examples/api/cpp/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index ce5a1bc8b..b126c9410 100644 --- a/examples/api/cpp/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp @@ -75,7 +75,7 @@ int main() // define the rules Term zero = slv.mkInteger(0); - Term neg_x = slv.mkTerm(UMINUS, x); + Term neg_x = slv.mkTerm(NEG, x); Term plus = slv.mkTerm(PLUS, x, start); // create the grammar object diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 1f8153e44..980ec712f 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -41,7 +41,7 @@ public class LinearArith // Terms Term three_y = slv.mkTerm(Kind.MULT, three, y); - Term diff = slv.mkTerm(Kind.MINUS, y, x); + Term diff = slv.mkTerm(Kind.SUB, y, x); // Formulas Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y); diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java index c815278cc..a573b1966 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -103,7 +103,7 @@ public class QuickStart // It is also possible to get values for compound terms, // even if those did not appear in the original formula. - Term xMinusY = solver.mkTerm(Kind.MINUS, x, y); + Term xMinusY = solver.mkTerm(Kind.SUB, x, y); Term xMinusYVal = solver.getValue(xMinusY); // Further, we can convert the values to java types diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index bc1d7e6b1..05ed4cb91 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -81,7 +81,7 @@ public class SygusFun Term one = slv.mkInteger(1); Term plus = slv.mkTerm(PLUS, start, start); - Term minus = slv.mkTerm(MINUS, start, start); + Term minus = slv.mkTerm(SUB, start, start); Term ite = slv.mkTerm(ITE, start_bool, start, start); Term And = slv.mkTerm(AND, start_bool, start_bool); diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index 230229fdd..d66378627 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -73,7 +73,7 @@ public class SygusGrammar // define the rules Term zero = slv.mkInteger(0); - Term neg_x = slv.mkTerm(UMINUS, x); + Term neg_x = slv.mkTerm(NEG, x); Term plus = slv.mkTerm(PLUS, x, start); // create the grammar object diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py index f3d6249c9..301939719 100644 --- a/examples/api/python/linear_arith.py +++ b/examples/api/python/linear_arith.py @@ -41,7 +41,7 @@ if __name__ == "__main__": # Terms three_y = slv.mkTerm(Kind.Mult, three, y) - diff = slv.mkTerm(Kind.Minus, y, x) + diff = slv.mkTerm(Kind.Sub, y, x) # Formulas x_geq_3y = slv.mkTerm(Kind.Geq, x, three_y) diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index d563bae06..6846eb503 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -95,7 +95,7 @@ if __name__ == "__main__": # It is also possible to get values for compound terms, # even if those did not appear in the original formula. - xMinusY = solver.mkTerm(Kind.Minus, x, y); + xMinusY = solver.mkTerm(Kind.Sub, x, y); xMinusYVal = solver.getValue(xMinusY); # We can now obtain the values as python values diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py index 5532a4cdb..939e1f9ed 100644 --- a/examples/api/python/sygus-fun.py +++ b/examples/api/python/sygus-fun.py @@ -46,7 +46,7 @@ if __name__ == "__main__": one = slv.mkInteger(1) plus = slv.mkTerm(Kind.Plus, start, start) - minus = slv.mkTerm(Kind.Minus, start, start) + minus = slv.mkTerm(Kind.Sub, start, start) ite = slv.mkTerm(Kind.Ite, start_bool, start, start) And = slv.mkTerm(Kind.And, start_bool, start_bool) diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py index 48ddf0b30..d513dc139 100644 --- a/examples/api/python/sygus-grammar.py +++ b/examples/api/python/sygus-grammar.py @@ -42,7 +42,7 @@ if __name__ == "__main__": # define the rules zero = slv.mkInteger(0) - neg_x = slv.mkTerm(Kind.Uminus, x) + neg_x = slv.mkTerm(Kind.Neg, x) plus = slv.mkTerm(Kind.Plus, x, start) # create the grammar object diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 449ec1414..9b17dbc7a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -134,8 +134,8 @@ const static std::unordered_map s_kinds{ {MULT, cvc5::Kind::MULT}, {IAND, cvc5::Kind::IAND}, {POW2, cvc5::Kind::POW2}, - {MINUS, cvc5::Kind::SUB}, - {UMINUS, cvc5::Kind::NEG}, + {SUB, cvc5::Kind::SUB}, + {NEG, cvc5::Kind::NEG}, {DIVISION, cvc5::Kind::DIVISION}, {INTS_DIVISION, cvc5::Kind::INTS_DIVISION}, {INTS_MODULUS, cvc5::Kind::INTS_MODULUS}, @@ -416,8 +416,8 @@ const static std::unordered_map {cvc5::Kind::MULT, MULT}, {cvc5::Kind::IAND, IAND}, {cvc5::Kind::POW2, POW2}, - {cvc5::Kind::SUB, MINUS}, - {cvc5::Kind::NEG, UMINUS}, + {cvc5::Kind::SUB, SUB}, + {cvc5::Kind::NEG, NEG}, {cvc5::Kind::DIVISION, DIVISION}, {cvc5::Kind::DIVISION_TOTAL, INTERNAL_KIND}, {cvc5::Kind::INTS_DIVISION, INTS_DIVISION}, @@ -5185,8 +5185,8 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const Node res; if (echildren.size() > 2) { - if (kind == INTS_DIVISION || kind == XOR || kind == MINUS - || kind == DIVISION || kind == HO_APPLY || kind == REGEXP_DIFF) + if (kind == INTS_DIVISION || kind == XOR || kind == SUB || kind == DIVISION + || kind == HO_APPLY || kind == REGEXP_DIFF) { // left-associative, but cvc5 internally only supports 2 args res = d_nodeMgr->mkLeftAssociative(k, echildren); diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index dba4df07f..7644cff4d 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -419,7 +419,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - MINUS, + SUB, /** * Arithmetic negation. * @@ -429,7 +429,7 @@ enum Kind : int32_t * Create with: * - `Solver::mkTerm(Kind kind, const Term& child) const` */ - UMINUS, + NEG, /** * Real division, division by 0 undefined, left associative. * diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9dd21b148..3618d38cf 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -42,9 +42,9 @@ Smt2::~Smt2() {} void Smt2::addArithmeticOperators() { addOperator(api::PLUS, "+"); - addOperator(api::MINUS, "-"); - // api::MINUS is converted to api::UMINUS if there is only a single operand - Parser::addOperator(api::UMINUS); + addOperator(api::SUB, "-"); + // api::SUB is converted to api::NEG if there is only a single operand + Parser::addOperator(api::NEG); addOperator(api::MULT, "*"); addOperator(api::LT, "<"); addOperator(api::LEQ, "<="); @@ -1090,7 +1090,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) Debug("parser") << "applyParseOp: return unary " << args[0] << std::endl; return args[0]; } - else if (kind == api::MINUS && args.size() == 1) + else if (kind == api::SUB && args.size() == 1) { if (isConstInt(args[0]) && args[0].getRealOrIntegerValueSign() > 0) { @@ -1102,7 +1102,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) << std::endl; return ret; } - api::Term ret = d_solver->mkTerm(api::UMINUS, args[0]); + api::Term ret = d_solver->mkTerm(api::NEG, args[0]); Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fd6ea8df8..cee795648 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -384,8 +384,8 @@ class Smt2 : public Parser * selector expression based on the type of args[0]. * - If the overall kind of the expression is chainable, we may convert it * to a left- or right-associative chain. - * - If the overall kind is MINUS and args has size 1, then we return an - * application of UMINUS. + * - If the overall kind is SUB and args has size 1, then we return an + * application of NEG. * - If the overall expression is a partial application, then we process this * as a chain of HO_APPLY terms. */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 419acafc0..1c9b2092c 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -567,7 +567,7 @@ definedFun[cvc5::ParseOp& p] } : '$uminus' { - p.d_kind = api::UMINUS; + p.d_kind = api::NEG; } | '$sum' { @@ -575,7 +575,7 @@ definedFun[cvc5::ParseOp& p] } | '$difference' { - p.d_kind = api::MINUS; + p.d_kind = api::SUB; } | '$product' { @@ -596,14 +596,14 @@ definedFun[cvc5::ParseOp& p] expr = MK_TERM(api::ITE, MK_TERM(api::GEQ, d, SOLVER->mkReal(0)), MK_TERM(api::TO_INTEGER, expr), - MK_TERM(api::UMINUS, + MK_TERM(api::NEG, MK_TERM(api::TO_INTEGER, - MK_TERM(api::UMINUS, expr)))); + MK_TERM(api::NEG, expr)))); if (remainder) { expr = MK_TERM( api::TO_INTEGER, - MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d))); + MK_TERM(api::SUB, n, MK_TERM(api::MULT, expr, d))); } p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); @@ -619,14 +619,14 @@ definedFun[cvc5::ParseOp& p] expr = MK_TERM(api::ITE, MK_TERM(api::GEQ, expr, SOLVER->mkReal(0)), MK_TERM(api::TO_INTEGER, expr), - MK_TERM(api::UMINUS, + MK_TERM(api::NEG, MK_TERM(api::TO_INTEGER, - MK_TERM(api::UMINUS, expr)))); + MK_TERM(api::NEG, expr)))); if (remainder) { expr = MK_TERM( api::TO_INTEGER, - MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d))); + MK_TERM(api::SUB, n, MK_TERM(api::MULT, expr, d))); } p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); @@ -643,7 +643,7 @@ definedFun[cvc5::ParseOp& p] if (remainder) { expr = MK_TERM(api::TO_INTEGER, - MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d))); + MK_TERM(api::SUB, n, MK_TERM(api::MULT, expr, d))); } p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); @@ -656,8 +656,8 @@ definedFun[cvc5::ParseOp& p] { api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N"); api::Term formals = MK_TERM(api::VARIABLE_LIST, n); - api::Term expr = MK_TERM(api::UMINUS, - MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n))); + api::Term expr = MK_TERM(api::NEG, + MK_TERM(api::TO_INTEGER, MK_TERM(api::NEG, n))); p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); } @@ -669,8 +669,8 @@ definedFun[cvc5::ParseOp& p] MK_TERM(api::ITE, MK_TERM(api::GEQ, n, SOLVER->mkReal(0)), MK_TERM(api::TO_INTEGER, n), - MK_TERM(api::UMINUS, - MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n)))); + MK_TERM(api::NEG, + MK_TERM(api::TO_INTEGER, MK_TERM(api::NEG, n)))); p.d_kind = api::LAMBDA; p.d_expr = MK_TERM(api::LAMBDA, formals, expr); } @@ -678,7 +678,7 @@ definedFun[cvc5::ParseOp& p] { api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N"); api::Term formals = MK_TERM(api::VARIABLE_LIST, n); - api::Term decPart = MK_TERM(api::MINUS, n, MK_TERM(api::TO_INTEGER, n)); + api::Term decPart = MK_TERM(api::SUB, n, MK_TERM(api::TO_INTEGER, n)); api::Term expr = MK_TERM( api::ITE, MK_TERM(api::LT, decPart, SOLVER->mkReal(1, 2)), diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index b8b81df24..b8f25c66e 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -337,9 +337,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector& args) // Unary AND/OR can be replaced with the argument. return args[0]; } - if (kind == api::MINUS && args.size() == 1) + if (kind == api::SUB && args.size() == 1) { - return d_solver->mkTerm(api::UMINUS, args[0]); + return d_solver->mkTerm(api::NEG, args[0]); } if (kind == api::TO_REAL) { diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 0fa3048ae..9f8c6e453 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -790,8 +790,8 @@ TEST_F(TestApiBlackSolver, mkTerm) ASSERT_NO_THROW(d_solver.mkTerm(INTS_DIVISION, {t_int, t_int, t_int})); ASSERT_NO_THROW( d_solver.mkTerm(d_solver.mkOp(INTS_DIVISION), {t_int, t_int, t_int})); - ASSERT_NO_THROW(d_solver.mkTerm(MINUS, {t_int, t_int, t_int})); - ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(MINUS), {t_int, t_int, t_int})); + ASSERT_NO_THROW(d_solver.mkTerm(SUB, {t_int, t_int, t_int})); + ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SUB), {t_int, t_int, t_int})); ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {t_int, t_int, t_int})); ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(EQUAL), {t_int, t_int, t_int})); ASSERT_NO_THROW(d_solver.mkTerm(LT, {t_int, t_int, t_int})); @@ -3000,7 +3000,7 @@ TEST_F(TestApiBlackSolver, proj_issue414) Sort s2 = slv.getRealSort(); Term t1 = slv.mkConst(s2, "_x0"); Term t16 = slv.mkTerm(Kind::PI); - Term t53 = slv.mkTerm(Kind::MINUS, {t1, t16}); + Term t53 = slv.mkTerm(Kind::SUB, {t1, t16}); Term t54 = slv.mkTerm(Kind::SECANT, {t53}); ASSERT_NO_THROW(slv.simplify(t54)); } diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 02b321046..a2abcf847 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -777,8 +777,8 @@ def test_mk_term(solver): solver.mkTerm(solver.mkOp(Kind.Division), [t_int, t_int, t_int]) solver.mkTerm(Kind.IntsDivision, [t_int, t_int, t_int]) solver.mkTerm(solver.mkOp(Kind.IntsDivision), [t_int, t_int, t_int]) - solver.mkTerm(Kind.Minus, [t_int, t_int, t_int]) - solver.mkTerm(solver.mkOp(Kind.Minus), [t_int, t_int, t_int]) + solver.mkTerm(Kind.Sub, [t_int, t_int, t_int]) + solver.mkTerm(solver.mkOp(Kind.Sub), [t_int, t_int, t_int]) solver.mkTerm(Kind.Equal, [t_int, t_int, t_int]) solver.mkTerm(solver.mkOp(Kind.Equal), [t_int, t_int, t_int]) solver.mkTerm(Kind.Lt, [t_int, t_int, t_int]) -- 2.30.2