[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 22 Mar 2022 08:36:54 +0000 (01:36 -0700)
committerGitHub <noreply@github.com>
Tue, 22 Mar 2022 08:36:54 +0000 (08:36 +0000)
commit3a97480ffab492f8272ad9c7c192d04b43eeea60
treee13ee458f669cd46ec8c0cb6b6d91829f00b0bb0
parent23c0a0b79688cf86f16029aa0ef19864c63d7c85
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind  (#8334)

This commit removes the `FLOATINGPOINT_TO_FP_GENERIC` kind, which was
only used in the parser and immediately rewritten by the floating-point
arithmetic solver. It extends the `ParseOp` class to handle indexed
operators of which we do not know the kind (`to_fp` in this case) by
storing the name and the indices. The name is then resolved later when
we have parsed the arguments.
20 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/api/cpp/cvc5_kind.h
src/api/java/io/github/cvc5/api/Solver.java
src/parser/parse_op.cpp
src/parser/parse_op.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/printer/smt2/smt2_printer.cpp
src/proof/lfsc/lfsc_node_converter.cpp
src/theory/fp/kinds
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp_rewriter.cpp
src/theory/fp/theory_fp_type_rules.cpp
src/theory/fp/theory_fp_type_rules.h
src/util/floatingpoint.h
test/unit/api/cpp/op_black.cpp
test/unit/api/java/OpTest.java
test/unit/api/python/test_op.py