Try harder to show that a RAN is rational (#8230)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 7 Mar 2022 15:31:07 +0000 (16:31 +0100)
committerGitHub <noreply@github.com>
Mon, 7 Mar 2022 15:31:07 +0000 (15:31 +0000)
commit879f73516b9c0e0fe820adcdc3460cbb9c772062
tree0f80975ddd752d76935f5737ffba54796a0485aa
parent3809343bf829523e425225cbf641a4fc62c713f7
Try harder to show that a RAN is rational (#8230)

We try to rewrite real algebraic numbers to rationals. This is important to, e.g., allow the linear solver to see rational constants at all. Refining real algebraic numbers is done lazily, and (almost) any operation may trigger a refinement that makes libpoly realize it actually is rational. Thus, even the mere act of creating a node out of a real algebraic number may do this (it hashes it).
This PR thus introduces a fixed-point loop into the RAN node constructor that defends against this case.
Fixes #8226.
src/expr/node_manager_template.cpp
test/regress/CMakeLists.txt
test/regress/regress0/nl/issue8226-ran-refinement.smt2 [new file with mode: 0644]