projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6d3ef3f) | patch
Have RAN fall back to RANs (#7976)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 24 Jan 2022 17:49:02 +0000 (09:49 -0800)
committerGitHub <noreply@github.com>
Mon, 24 Jan 2022 17:49:02 +0000 (17:49 +0000)
commitf0014b7ed0f810cba313aafde9236571625d2927
treec95b30298f09cce083af22e1bfe63ffdf60e7d31tree
parent6d3ef3f8b8256f5e17f5a045e42b5dc1effb281fcommit | diff
Have RAN fall back to RANs (#7976)

Right now, the RealAlgebraicNumber can not be used if libpoly is not available. This makes using it in the arithmetic rewriter incredibly awkward. This PR makes it fall back to a wrapper around Rational if libpoly is disabled, making its usage way easier.
src/util/real_algebraic_number_poly_imp.cpp diff | blob | history
src/util/real_algebraic_number_poly_imp.h diff | blob | history