From 0b893afee4934428def0955f22a8e56e57e27c29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Nov 2019 17:13:15 -0800 Subject: [PATCH] pretty print algebraic numbers from fast pretty printer Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt_pp.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index c0c62c379..4524b7f15 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -33,6 +33,8 @@ Revision History: #include "ast/fpa_decl_plugin.h" #include "ast/for_each_ast.h" #include "ast/decl_collector.h" +#include "math/polynomial/algebraic_numbers.h" + // --------------------------------------- // smt_renaming @@ -372,6 +374,12 @@ class smt_printer { display_rational(val, is_int); } } + else if (m_autil.is_irrational_algebraic_numeral(n)) { + anum const & aval = m_autil.to_irrational_algebraic_numeral(n); + std::ostringstream buffer; + m_autil.am().display_root_smt2(buffer, aval); + m_out << buffer.str(); + } else if (m_sutil.str.is_string(n, s)) { std::string encs = s.encode(); m_out << "\"";