projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b9485d) | patch
Make rewriter more robust against RAN becoming rational (#8564)
authorGereon Kremer <gkremer@cs.stanford.edu>
Tue, 5 Apr 2022 04:32:43 +0000 (21:32 -0700)
committerGitHub <noreply@github.com>
Tue, 5 Apr 2022 04:32:43 +0000 (04:32 +0000)
commit5495cc021e6e7a52c6e94d8be6a471168a91c691
tree2e8bfcf2d20c7bad5beed7f051467789489a6b6btree
parent5b9485d6f2da4834c329793b28e4a63ed4c39829commit | diff
Make rewriter more robust against RAN becoming rational (#8564)

We use real algebraic number to represent multiplicities of sum terms within the arithmetic rewriter. Unfortunately, such real algebraic numbers can realize that they are in fact rational at awkward times. This makes isRational() unsuitable for checking this, instead we should construct the node and check afterwards.
src/theory/arith/rewriter/node_utils.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/arith/arith-rewrite-with-ran.smt2 [new file with mode: 0644] blob