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).

diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp
index 979959d210e5c8ae6451d2c461a1f3c331a08990..9b027844ade6bf2a8586d25c9f919e490ba89ac6 100644 (file)
--- 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 7758c5f79c19c1eee70467d3ca4d33e01c249e85..5bcb6bc66553e50f2fe75416b5fbd49770bdf9c2 100644 (file)
--- 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 0f96e72a7d6f38c6747da42ce3dcea9e7638ba1c..e7a554177042e094d151fb6833e4d80dea839f22 100644 (file)
--- 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 ce5a1bc8b715ce6a50223dd2e6041d16dde615a2..b126c941004382d42ca46257d67f27dcfd75dbd1 100644 (file)
--- 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 1f8153e44b06a3994f68bbb9eabad882b97d02e8..980ec712fed8ca7858d1f6ffef492ce475603fbd 100644 (file)
--- 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 c815278cc471b6bf09435b569153d1f0f4dd125f..a573b1966bad2e47b21c7c703c88463c55a0d16d 100644 (file)
--- 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 bc1d7e6b1490098bfed316f1a8cd82f81f5fc835..05ed4cb9168b281d5f935f3ba5f3e177ee9fa5d2 100644 (file)
--- 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 230229fdd37922bb458367753c4f2d7cb9e828ab..d6637862788a6e578ed860500f6eeaa5628617a8 100644 (file)
--- 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 f3d6249c963b32882efb3c776e4971cfba2bd3d8..301939719f6829805915f98c0a772e8779b01382 100644 (file)
--- 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 d563bae0638abace046cd1ea8686939f63994d30..6846eb503d69e9c1d2c2617e78ff5dc8a026ffea 100644 (file)
--- 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 5532a4cdbc89ed299c3772f861c3b9023d74280a..939e1f9ed43d98b374b801b3b10f616d6e9fdb4e 100644 (file)
--- 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 48ddf0b30c9d59f72017a490915a695678010f18..d513dc139836dac90fd8c62c22caeb06c6a88044 100644 (file)
--- 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 449ec1414e18ed514efce1d04966839a89ecfdbc..9b17dbc7aff3a400ae9319e498e5fe206186df36 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -134,8 +134,8 @@ const static std::unordered_map<Kind, cvc5::Kind> 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, Kind, cvc5::kind::KindHashFunction>
         {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<Term>& 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 dba4df07fa96c0d015fe6667479caab5ef90373b..7644cff4da1d87c7259b8db37dcd95f9808e6a75 100644 (file)
--- 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<Term>& 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 9dd21b148300a6154f44510867c45091507f1cf6..3618d38cff5159acbac128208438f0e4157dd747 100644 (file)
--- 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<api::Term>& 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<api::Term>& 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 fd6ea8df84ebd1c33b526ee3a119eeaf61bc22cc..cee79564863bdfe9af098adfad7fbf8d2c73043d 100644 (file)
--- 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 419acafc014c7f8a71e1cf34eca0e60619aeb279..1c9b2092cde48531e76eafdd49dbfd68ee5fce65 100644 (file)
--- 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 b8b81df249a30519bf05247a529d51d8b95fcda2..b8f25c66e61e8866a17c65a29b1e2f0d50b81e93 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -337,9 +337,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& 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 0fa3048aeec3090e0cbfcda7cfce314a469f83f9..9f8c6e453a432cec955c7a234e0658c35452435f 100644 (file)
--- 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 02b321046cdff2311b99c636aa681df97745160e..a2abcf847bc7a246e98fef00d51df7e922a16853 100644 (file)
--- 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])