projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e55e6b3) | patch
Add mkRealAlgebraicNumber (#7923)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 12 Jan 2022 18:18:19 +0000 (10:18 -0800)
committerGitHub <noreply@github.com>
Wed, 12 Jan 2022 18:18:19 +0000 (18:18 +0000)
commita9990d56eb3bc6f27e5bc5557db0247e4dc6a070
treec58dd57c0f32f694a0cc5ddbe4c39345e71f71e5tree
parente55e6b3bd4384f0b80e04d7acc6b6d613a244dd4commit | diff
Add mkRealAlgebraicNumber (#7923)

This PR adds the convenience function NodeManager::mkRealAlgebraicNumber().
src/expr/node_manager_template.cpp diff | blob | history
src/expr/node_manager_template.h diff | blob | history
src/theory/arith/kinds diff | blob | history
src/util/real_algebraic_number_poly_imp.cpp diff | blob | history
src/util/real_algebraic_number_poly_imp.h diff | blob | history