projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a7c0c7) | patch
Explicitly disallow `mkConst(Rational)` (#7818)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 16 Dec 2021 14:29:10 +0000 (06:29 -0800)
committerGitHub <noreply@github.com>
Thu, 16 Dec 2021 14:29:10 +0000 (14:29 +0000)
commite53d797fa042a7c466ca838ea21abbd3890a39ba
tree3b9b587fb8d500784f635af4f532ec0c747ef098tree
parent4a7c0c73f69aabb20be4c79c47047ce23d3358b0commit | diff
Explicitly disallow `mkConst(Rational)` (#7818)

The Rational payload can be associated with two kinds (CONST_INTEGER
and CONST_RATIONAL), so we should never call
NodeManager::mkConst(Rational), but instead use
NodeManager::mkConstInt() and NodeManager::mkConstReal(). Currently,
calling NodeManager::mkConst(Rational) silently creates an integer
constant, which is dangerous. This commit makes it a compile-time error
instead.
src/expr/CMakeLists.txt diff | blob | history
src/expr/mkmetakind diff | blob | history
src/expr/node_manager.h [deleted file] blob | history
src/expr/node_manager_template.cpp diff | blob | history
src/expr/node_manager_template.h [new file with mode: 0644] blob
src/theory/arith/kinds diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history