projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e3bec47) | patch
Eliminate the use of CAST_TO_REAL (#8759)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 15 May 2022 17:11:42 +0000 (12:11 -0500)
committerGitHub <noreply@github.com>
Sun, 15 May 2022 17:11:42 +0000 (17:11 +0000)
commita3745c4b50c41e5a1ebd632c3a9e768c9bf8d67f
tree4fc3c7810719f475af068df0bd946060406725c0tree
parente3bec47e98e76ad6e4a11259af096abb20f7de57commit | diff
Eliminate the use of CAST_TO_REAL (#8759)

This simplifies the implementation of the API by not relying on CAST_TO_REAL. This was used as a way of manually marking integral reals as having real type.
12 files changed:
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/expr/subtype_elim_node_converter.cpp diff | blob | history
src/expr/subtype_elim_node_converter.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/proof/alethe/alethe_nosubtype_node_converter.cpp diff | blob | history
src/proof/lfsc/lfsc_node_converter.cpp diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/theory_arith_type_rules.cpp diff | blob | history
src/theory/evaluator.cpp diff | blob | history