mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Fix translation of FPA numerals in ast_smt_pp. Fixes #2145.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2019-02-22 12:55:01 +00:00
parent bceff4b3fa
commit 699834261e
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 14 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/ast/ast_smt_pp.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "util/vector.h"
#include "util/smt2_util.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "ast/array_decl_plugin.h"
@ -223,7 +224,7 @@ class smt_printer {
}
}
else if (m_manager.is_ite(d)) {
m_out << "ite";
m_out << "ite";
}
else if (m_manager.is_implies(d)) {
m_out << "=>";
@ -266,7 +267,7 @@ class smt_printer {
else {
m_out << "(_ " << sym << " ";
}
for (unsigned i = 0; i < num_params; ++i) {
parameter const& p = params[i];
if (p.is_ast()) {
@ -320,7 +321,7 @@ class smt_printer {
if (num_sorts > 0) {
m_out << "(";
}
m_out << m_renaming.get_symbol(s->get_name(), false);
m_out << m_renaming.get_symbol(s->get_name(), false);
if (num_sorts > 0) {
for (unsigned i = 0; i < num_sorts; ++i) {
m_out << " ";
@ -388,10 +389,7 @@ class smt_printer {
m_out << "(_ bv" << val << " " << bv_size << ")";
}
else if (m_futil.is_numeral(n, float_val)) {
m_out << "((_ to_fp " <<
float_val.get().get_ebits() << " " <<
float_val.get().get_sbits() << ") RTZ " <<
m_futil.fm().to_string(float_val).c_str() << ")";
m_out << mk_ismt2_pp(n, m_manager);
}
else if (m_bvutil.is_bit2bool(n)) {
unsigned bit = n->get_decl()->get_parameter(0).get_int();
@ -402,7 +400,7 @@ class smt_printer {
else if (m_manager.is_label(n, pos, names) && !names.empty()) {
m_out << "(! ";
pp_marked_expr(n->get_arg(0));
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")";
}
else if (m_manager.is_label_lit(n, names) && !names.empty()) {
m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")";
@ -435,7 +433,7 @@ class smt_printer {
pp_arg(curr, n);
m_out << ")";
}
}
else if (m_manager.is_distinct(decl)) {
ptr_vector<expr> args(num_args, n->get_args());
unsigned idx = 0;
@ -613,7 +611,7 @@ class smt_printer {
pp_id(n);
m_out << " ";
pp_expr(n);
m_out << ")";
m_out << ")";
m_out << ")";
newline();
}
@ -781,7 +779,7 @@ public:
datatype_util util(m_manager);
SASSERT(util.is_datatype(s));
sort_ref_vector ps(m_manager);
sort_ref_vector ps(m_manager);
ptr_vector<datatype::def> defs;
util.get_defs(s, defs);
@ -790,7 +788,7 @@ public:
if (mark.is_marked(sr)) return; // already processed
mark.mark(sr, true);
}
m_out << "(declare-datatypes (";
bool first_def = true;
for (datatype::def* d : defs) {
@ -800,7 +798,7 @@ public:
m_out << ") (";
bool first_sort = true;
for (datatype::def* d : defs) {
if (!first_sort) m_out << "\n "; else first_sort = false;
if (!first_sort) m_out << "\n "; else first_sort = false;
if (!d->params().empty()) {
m_out << "(par (";
bool first_param = true;
@ -814,7 +812,7 @@ public:
bool first_constr = true;
for (datatype::constructor* f : *d) {
if (!first_constr) m_out << " "; else first_constr = false;
m_out << "(";
m_out << "(";
m_out << m_renaming.get_symbol(f->name(), false);
for (datatype::accessor* a : *f) {
m_out << " (" << m_renaming.get_symbol(a->name(), false) << " ";
@ -828,7 +826,7 @@ public:
}
m_out << ")";
}
m_out << "))";
m_out << "))";
newline();
}
@ -864,7 +862,7 @@ public:
}
m_out << ") ";
visit_sort(d->get_range());
m_out << ")";
m_out << ")";
}
void visit_pred(func_decl* d) {