projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 676b43d) | patch
api: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8034)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 3 Feb 2022 02:18:51 +0000 (18:18 -0800)
committerGitHub <noreply@github.com>
Thu, 3 Feb 2022 02:18:51 +0000 (02:18 +0000)
commit3cc0fe4d64cea1bfc155005e7fd7d8bc8f0c6ec3
treec0b46df83fe1a1d983427fdfcfbacb69a0d18565tree
parent676b43d08a40b7e83002461e8a76421280f8ce4fcommit | diff
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).
20 files changed:
examples/api/cpp/linear_arith.cpp diff | blob | history
examples/api/cpp/quickstart.cpp diff | blob | history
examples/api/cpp/sygus-fun.cpp diff | blob | history
examples/api/cpp/sygus-grammar.cpp diff | blob | history
examples/api/java/LinearArith.java diff | blob | history
examples/api/java/QuickStart.java diff | blob | history
examples/api/java/SygusFun.java diff | blob | history
examples/api/java/SygusGrammar.java diff | blob | history
examples/api/python/linear_arith.py diff | blob | history
examples/api/python/quickstart.py diff | blob | history
examples/api/python/sygus-fun.py diff | blob | history
examples/api/python/sygus-grammar.py diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/parser/tptp/Tptp.g diff | blob | history
src/parser/tptp/tptp.cpp diff | blob | history
test/unit/api/cpp/solver_black.cpp diff | blob | history
test/unit/api/python/test_solver.py diff | blob | history