projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1483676) | patch
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 27 May 2021 19:08:24 +0000 (12:08 -0700)
committerGitHub <noreply@github.com>
Thu, 27 May 2021 19:08:24 +0000 (19:08 +0000)
commitc95d4c5473e8c26832fef89a9a42275517a42613
tree36f42cad17c22b39c232c97b111df1e1e9a382f2tree
parent1483676841847216a7cfe15e5d201a924739d014commit | diff
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)

This is to make it consistent with the name of the SMT-LIB operator
(fp.add).
13 files changed:
examples/api/java/FloatingPointArith.java diff | blob | history
examples/api/python/floating_point.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/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/fp/fp_converter.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/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/util/floatingpoint.cpp diff | blob | history
src/util/floatingpoint.h diff | blob | history