projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c274b57) | patch
Rename TO_FP operator kinds. (#8285)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 15 Mar 2022 00:18:52 +0000 (17:18 -0700)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 00:18:52 +0000 (00:18 +0000)
commitd2f0f6d468473cffee92d9835d9b4d0c88550253
treecc810ffb5af3b6fe2c7b21a4e09a0ac65a4de120tree
parentc274b572b3f634e4f098dff564942d6dc452a22fcommit | diff
Rename TO_FP operator kinds. (#8285)

FLOATINGPOINT_TO_FP_FP -> FLOATINGPOINT_TO_FP_FROM_FP
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_IEEE_BV
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_SBV
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_UBV
FLOATINGPOINT_TO_FP_REAL -> FLOATINGPOINT_TO_FP_FROM_REAL
15 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/api/java/io/github/cvc5/api/Solver.java diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/theory/fp/fp_word_blaster.cpp diff | blob | history
src/theory/fp/kinds diff | blob | history
src/theory/fp/theory_fp.cpp diff | blob | history
src/theory/fp/theory_fp_rewriter.cpp diff | blob | history
src/theory/fp/theory_fp_type_rules.cpp diff | blob | history
test/unit/api/cpp/op_black.cpp diff | blob | history
test/unit/api/java/OpTest.java diff | blob | history
test/unit/api/python/test_op.py diff | blob | history