projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 06105f6) | patch
Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)
authorGereon Kremer <gkremer@cs.stanford.edu>
Fri, 29 Apr 2022 20:30:07 +0000 (13:30 -0700)
committerGitHub <noreply@github.com>
Fri, 29 Apr 2022 20:30:07 +0000 (20:30 +0000)
commit7ae818d54bedc96b6fb0000fa17f41ee30f1f8a0
tree71578ea23cc58b7d293089dafc87e7485a310805tree
parent06105f6ccf1cb73fd8e3335c855177c1fcdcd800commit | diff
Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)

This PR removes the usages of CONST_RATIONAL in the nonlinear arithmetic solver.
src/theory/arith/nl/coverings/cdcac.cpp diff | blob | history
src/theory/arith/nl/coverings/proof_generator.cpp diff | blob | history
src/theory/arith/nl/ext/ext_state.cpp diff | blob | history
src/theory/arith/nl/ext/factoring_check.cpp diff | blob | history
src/theory/arith/nl/ext/monomial.cpp diff | blob | history
src/theory/arith/nl/ext/monomial_bounds_check.cpp diff | blob | history
src/theory/arith/nl/ext/proof_checker.cpp diff | blob | history
src/theory/arith/nl/ext/tangent_plane_check.cpp diff | blob | history
src/theory/arith/nl/nl_model.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/poly_conversion.cpp diff | blob | history