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

Bugfix for FPA in solver.to_smt2

Browse source 
Fixes #541
This commit is contained in:
Christoph M. Wintersteiger 2016-03-29 16:37:09 +01:00
parent 19e73fb2ad
commit 6be24b3201
1 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/ast_smt_pp.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include"bv_decl_plugin.h" #include"bv_decl_plugin.h"
#include"array_decl_plugin.h" #include"array_decl_plugin.h"
#include"datatype_decl_plugin.h" #include"datatype_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"vector.h" #include"vector.h"
#include"for_each_ast.h" #include"for_each_ast.h"
#include"decl_collector.h" #include"decl_collector.h"
@ -162,11 +163,13 @@ class smt_printer {
arith_util m_autil; arith_util m_autil;
bv_util m_bvutil; bv_util m_bvutil;
seq_util m_sutil; seq_util m_sutil;
fpa_util m_futil;
family_id m_basic_fid; family_id m_basic_fid;
family_id m_bv_fid; family_id m_bv_fid;
family_id m_arith_fid; family_id m_arith_fid;
family_id m_array_fid; family_id m_array_fid;
family_id m_dt_fid; family_id m_dt_fid;
family_id m_fpa_fid;
family_id m_label_fid; family_id m_label_fid;
symbol m_logic; symbol m_logic;
symbol m_AUFLIRA; symbol m_AUFLIRA;
@ -253,7 +256,10 @@ class smt_printer {
m_out << "String"; m_out << "String";
return; return;
} }
if (is_sort_symbol && sym != symbol("BitVec")) { if (is_sort_symbol &&
sym != symbol("BitVec") &&
sym != symbol("FloatingPoint") &&
sym != symbol("RoundingMode")) {
m_out << "(" << sym << " "; m_out << "(" << sym << " ";
} }
else if (!is_sort_symbol && is_sort_param(num_params, params)) { else if (!is_sort_symbol && is_sort_param(num_params, params)) {
@ -406,6 +412,7 @@ class smt_printer {
zstring s; zstring s;
unsigned num_args = n->get_num_args(); unsigned num_args = n->get_num_args();
func_decl* decl = n->get_decl(); func_decl* decl = n->get_decl();
scoped_mpf float_val(m_futil.fm());
if (m_autil.is_numeral(n, val, is_int)) { if (m_autil.is_numeral(n, val, is_int)) {
if (val.is_neg()) { if (val.is_neg()) {
val.neg(); val.neg();
@ -443,6 +450,12 @@ class smt_printer {
m_out << "bv" << val << "[" << bv_size << "]"; 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() << ")";
}
else if (m_bvutil.is_bit2bool(n)) { else if (m_bvutil.is_bit2bool(n)) {
unsigned bit = n->get_decl()->get_parameter(0).get_int(); unsigned bit = n->get_decl()->get_parameter(0).get_int();
if (m_is_smt2) { if (m_is_smt2) {
@ -818,6 +831,7 @@ public:
m_autil(m), m_autil(m),
m_bvutil(m), m_bvutil(m),
m_sutil(m), m_sutil(m),
m_futil(m),
m_logic(logic), m_logic(logic),
m_AUFLIRA("AUFLIRA"), m_AUFLIRA("AUFLIRA"),
// It's much easier to read those testcases with that. // It's much easier to read those testcases with that.
@ -831,6 +845,7 @@ public:
m_arith_fid = m.mk_family_id("arith"); m_arith_fid = m.mk_family_id("arith");
m_array_fid = m.mk_family_id("array"); m_array_fid = m.mk_family_id("array");
m_dt_fid = m.mk_family_id("datatype"); m_dt_fid = m.mk_family_id("datatype");
m_fpa_fid = m.mk_family_id("fpa");
} }
void operator()(expr* n) { void operator()(expr* n) {