mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

various bugfixes and extensions for FPA

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-15 19:25:49 +00:00
parent caafee0033
commit 5344d6f3c0
10 changed files with 396 additions and 341 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/asserted_formulas.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include"arith_simplifier_plugin.h"
#include"array_simplifier_plugin.h"
#include"datatype_simplifier_plugin.h"
#include"fpa_simplifier_plugin.h"
#include"bv_simplifier_plugin.h"
#include"for_each_expr.h"
#include"well_sorted.h"
@ -96,7 +97,8 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie
s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params);
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
}
void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {

412
src/smt/theory_fpa.cpp
View file

@ -54,11 +54,11 @@ namespace smt {
unsigned ebits = m_th.m_fpa_util.get_ebits(s);
unsigned sbits = m_th.m_fpa_util.get_sbits(s);
SASSERT(bv_sz == ebits + sbits);
m_th.m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
result);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
result);
SASSERT(m_th.m_fpa_util.is_float(result));
m_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -97,62 +97,86 @@ namespace smt {
}
theory_fpa::~theory_fpa()
{
{
ast_manager & m = get_manager();
dec_ref_map_values(m, m_conversions);
dec_ref_map_values(m, m_wraps);
dec_ref_map_values(m, m_unwraps);
dec_ref_map_values(m, m_unwraps);
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1);
ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
mpf_manager & mpfm = m_fu.fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits));
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
app * result;
scoped_mpz bias(mpzm);
mpzm.power(mpz(2), m_ebits - 1, bias);
mpzm.dec(bias);
rational all_rat(0);
scoped_mpz all_bits(mpzm);
scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
unsigned bv_sz;
bool r = m_bu.is_numeral(values[0], all_rat, bv_sz);
SASSERT(r);
SASSERT(bv_sz == (m_ebits+m_sbits));
SASSERT(all_rat.is_int());
mpzm.set(all_bits, all_rat.to_mpq().numerator());
scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
mpzm.machine_div2k(all_bits, m_ebits + m_sbits - 1, sgn_z);
mpzm.mod(all_bits, mpfm.m_powers2(m_ebits + m_sbits - 1), all_bits);
if (values.size() == 1) {
SASSERT(m_bu.is_bv(values[0]));
SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits));
mpzm.machine_div2k(all_bits, m_sbits - 1, exp_z);
mpzm.mod(all_bits, mpfm.m_powers2(m_sbits - 1), all_bits);
mpzm.set(sig_z, all_bits);
rational all_r(0);
scoped_mpz all_z(mpzm);
TRACE("t_fpa_detail", tout << "sgn=" << mpzm.to_string(sgn_z) << " ; " <<
"sig=" << mpzm.to_string(sig_z) << " ; " <<
"exp=" << mpzm.to_string(exp_z) << std::endl;);
bool r = m_bu.is_numeral(values[0], all_r, bv_sz);
SASSERT(r);
SASSERT(bv_sz == (m_ebits + m_sbits));
SASSERT(all_r.is_int());
mpzm.set(all_z, all_r.to_mpq().numerator());
mpzm.machine_div2k(all_z, m_ebits + m_sbits - 1, sgn_z);
mpzm.mod(all_z, mpfm.m_powers2(m_ebits + m_sbits - 1), all_z);
mpzm.machine_div2k(all_z, m_sbits - 1, exp_z);
mpzm.mod(all_z, mpfm.m_powers2(m_sbits - 1), all_z);
mpzm.set(sig_z, all_z);
}
else if (values.size() == 3) {
rational sgn_r(0), exp_r(0), sig_r(0);
bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz);
SASSERT(r && bv_sz == 1);
r = m_bu.is_numeral(values[1], exp_r, bv_sz);
SASSERT(r && bv_sz == m_ebits);
r = m_bu.is_numeral(values[2], sig_r, bv_sz);
SASSERT(r && bv_sz == m_sbits - 1);
SASSERT(sgn_r.to_mpq().denominator() == mpz(1));
SASSERT(exp_r.to_mpq().denominator() == mpz(1));
SASSERT(sig_r.to_mpq().denominator() == mpz(1));
mpzm.set(sgn_z, sgn_r.to_mpq().numerator());
mpzm.set(exp_z, exp_r.to_mpq().numerator());
mpzm.set(sig_z, sig_r.to_mpq().numerator());
}
else
UNREACHABLE();
scoped_mpz exp_u = exp_z - bias;
SASSERT(mpzm.is_int64(exp_u));
scoped_mpf f(mpfm);
scoped_mpf f(mpfm);
mpfm.set(f, m_ebits, m_sbits, mpzm.is_one(sgn_z), sig_z, mpzm.get_int64(exp_u));
result = m_fu.mk_value(f);
TRACE("t_fpa", tout << "fpa_value_proc::mk_value [" <<
mk_ismt2_pp(values[0], m) << "] --> " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
mpzm.to_string(sgn_z) << "," <<
mpzm.to_string(exp_z) << "," <<
mpzm.to_string(sig_z) << "] --> " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result;
}
@ -160,8 +184,8 @@ namespace smt {
SASSERT(values.size() == 1);
ast_manager & m = m_th.get_manager();
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: [" <<
mk_ismt2_pp(values[0], m) << "]" << std::endl;);
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
app * result = 0;
sort * s = m.get_sort(values[0]);
@ -199,42 +223,44 @@ namespace smt {
if (!m_wraps.find(e_srt, w)) {
SASSERT(!m_wraps.contains(e_srt));
sort * bv_srt = 0;
sort * bv_srt;
if (m_converter.is_rm(e_srt))
bv_srt = m_bv_util.mk_sort(3);
else {
SASSERT(m_converter.is_float(e_srt));
unsigned ebits = m_fpa_util.get_ebits(e_srt);
unsigned sbits = m_fpa_util.get_sbits(e_srt);
bv_srt = m_bv_util.mk_sort(ebits + sbits);
bv_srt = m_bv_util.mk_sort(ebits + sbits);
}
w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt);
m_wraps.insert(e_srt, w);
m.inc_ref(w);
m.inc_ref(w);
}
return app_ref(m.mk_app(w, e), m);
app_ref res(m);
res = m.mk_app(w, e);
return res;
}
app_ref theory_fpa::unwrap(expr * e, sort * s) {
SASSERT(!m_fpa_util.is_unwrap(e));
ast_manager & m = get_manager();
context & ctx = get_context();
sort * e_srt = m.get_sort(e);
sort * bv_srt = m.get_sort(e);
func_decl *u;
if (!m_unwraps.find(e_srt, u)) {
SASSERT(!m_unwraps.contains(e_srt));
sort * bv_srt = m.get_sort(e);
if (!m_unwraps.find(bv_srt, u)) {
SASSERT(!m_unwraps.contains(bv_srt));
u = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
m_unwraps.insert(s, u);
m_unwraps.insert(bv_srt, u);
m.inc_ref(u);
}
return app_ref(m.mk_app(u, e), m);
app_ref res(m);
res = m.mk_app(u, e);
return res;
}
expr_ref theory_fpa::convert_atom(expr * e) {
@ -244,55 +270,30 @@ namespace smt {
m_rw(e, res);
m_th_rw(res, res);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
SASSERT(m.is_bool(res));
return res;
}
expr_ref theory_fpa::convert_term(expr * e) {
ast_manager & m = get_manager();
TRACE("t_fpa_detail", tout << "converting: " << mk_ismt2_pp(e, m) << " sort is: " << mk_ismt2_pp(m.get_sort(e), m) << std::endl;);
ast_manager & m = get_manager();
context & ctx = get_context();
expr_ref ec(m), res(m);
expr_ref e_conv(m), res(m);
proof_ref pr(m);
m_rw(e, ec);
m_rw(e, e_conv);
SASSERT(is_app(ec));
app_ref eca(to_app(ec), m);
TRACE("t_fpa_detail", tout << "eca = " << mk_ismt2_pp(eca, m) << " sort is: " << mk_ismt2_pp(m.get_sort(eca), m) << std::endl;);
if (m_fpa_util.is_rm(e)) {
expr_ref bv_rm(m);
bv_rm = eca;
TRACE("t_fpa_detail", tout << "bvrm = " << mk_ismt2_pp(bv_rm, m) << " sort is: " << mk_ismt2_pp(m.get_sort(bv_rm), m) << std::endl;);
SASSERT(is_sort_of(m.get_sort(bv_rm), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(bv_rm) == 3);
m_th_rw(bv_rm, res);
if (m_fpa_util.is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(e_conv) == 3);
m_th_rw(e_conv, res);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(eca->get_family_id() == get_family_id());
fpa_op_kind k = (fpa_op_kind)(eca->get_decl_kind());
SASSERT(k == OP_FPA_TO_FP || k == OP_FPA_INTERNAL_BVUNWRAP);
switch (k) {
case OP_FPA_TO_FP: {
SASSERT(eca->get_num_args() == 3);
SASSERT(is_sort_of(m.get_sort(eca->get_arg(0)), m_bv_util.get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(eca->get_arg(1)), m_bv_util.get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(eca->get_arg(2)), m_bv_util.get_family_id(), BV_SORT));
expr *sgn, *sig, *exp;
expr_ref s_sgn(m), s_sig(m), s_exp(m);
m_converter.split_triple(eca, sgn, sig, exp);
m_th_rw(sgn, s_sgn);
m_th_rw(sig, s_sig);
m_th_rw(exp, s_exp);
m_converter.mk_triple(s_sgn, s_sig, s_exp, res);
break;
}
default:
res = eca;
}
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
m_converter.mk_fp(sgn, exp, sig, res);
}
else
UNREACHABLE();
@ -310,7 +311,7 @@ namespace smt {
SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e));
m_rw(e, res);
m_rw(e, res);
m_th_rw(res, res);
return res;
}
@ -327,12 +328,13 @@ namespace smt {
SASSERT(m_fpa_util.is_float(srt));
unsigned ebits = m_fpa_util.get_ebits(srt);
unsigned sbits = m_fpa_util.get_sbits(srt);
expr * bv = to_app(e)->get_arg(0);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
m_converter.mk_triple(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
res);
expr_ref bv(m);
bv = to_app(e)->get_arg(0);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
res);
}
return res;
}
@ -342,7 +344,7 @@ namespace smt {
ast_manager & m = get_manager();
context & ctx = get_context();
expr_ref res(m);
if (m_conversions.contains(e)) {
res = m_conversions.find(e);
TRACE("t_fpa_detail", tout << "cached:" << std::endl;
@ -401,11 +403,12 @@ namespace smt {
void theory_fpa::assert_cnstr(expr * e) {
if (get_manager().is_true(e)) return;
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
context& ctx = get_context();
context & ctx = get_context();
ctx.internalize(e, false);
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
}
void theory_fpa::attach_new_th_var(enode * n) {
@ -433,11 +436,10 @@ namespace smt {
ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m);
bv_atom = convert(atom);
bv_atom = convert_atom(atom);
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
bv_atom = m.mk_and(bv_atom, mk_side_conditions());
expr_ref atom_iff(m);
assert_cnstr(m.mk_iff(atom, bv_atom));
return true;
}
@ -447,7 +449,7 @@ namespace smt {
context & ctx = get_context();
TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
SASSERT(term->get_family_id() == get_family_id());
SASSERT(!ctx.e_internalized(term));
SASSERT(!ctx.e_internalized(term));
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
@ -455,7 +457,7 @@ namespace smt {
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
ctx.mk_enode(term, false, false, true);
if (is_attached_to_var(e))
return false;
@ -476,9 +478,9 @@ namespace smt {
assert_cnstr(mk_side_conditions());
break;
}
default: /* ignore */;
default: /* ignore */;
}
return true;
}
@ -486,33 +488,33 @@ namespace smt {
TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
SASSERT(n->get_owner()->get_family_id() == get_family_id() ||
n->get_owner()->get_family_id() == null_theory_id);
SASSERT(s->get_family_id() == get_family_id());
SASSERT(s->get_family_id() == get_family_id());
if (!is_attached_to_var(n))
if (!is_attached_to_var(n)) {
attach_new_th_var(n);
ast_manager & m = get_manager();
context & ctx = get_context();
ast_manager & m = get_manager();
context & ctx = get_context();
app_ref owner(m);
sort_ref owner_sort(m);
owner = n->get_owner();
owner_sort = m.get_sort(owner);
app_ref owner(m);
sort_ref owner_sort(m);
owner = n->get_owner();
owner_sort = m.get_sort(owner);
if (m_fpa_util.is_rm(owner_sort)) {
// For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range.
if (!m_fpa_util.is_unwrap(owner))
{
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(wrap(owner), limit);
assert_cnstr(valid);
if (m_fpa_util.is_rm(owner_sort)) {
// For every RM term, we need to make sure that it's
// associated bit-vector is within the valid range.
if (!m_fpa_util.is_unwrap(owner)) {
expr_ref valid(m), limit(m);
limit = m_bv_util.mk_numeral(4, 3);
valid = m_bv_util.mk_ule(wrap(owner), limit);
assert_cnstr(valid);
}
}
if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner))
assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner));
}
if (!ctx.relevancy() && !m_fpa_util.is_unwrap(owner))
assert_cnstr(m.mk_eq(unwrap(wrap(owner), owner_sort), owner));
}
void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
@ -527,36 +529,40 @@ namespace smt {
bv_util & bu = m_bv_util;
mpf_manager & mpfm = fu.fm();
app * xe = get_enode(x)->get_owner();
app * ye = get_enode(y)->get_owner();
expr_ref xe(m), ye(m);
xe = get_enode(x)->get_owner();
ye = get_enode(y)->get_owner();
if ((m.is_bool(xe) && m.is_bool(ye)) ||
(m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) {
SASSERT(xe->get_decl()->get_family_id() == get_family_id());
SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id());
return;
}
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
TRACE("t_fpa_detail", tout << "xc=" << mk_ismt2_pp(xc, m) << std::endl;
tout << "yc=" << mk_ismt2_pp(yc, m) << std::endl;);
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
{
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
m_converter.split_fp(xc, x_sgn, x_exp, x_sig);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
m_converter.split_fp(yc, y_sgn, y_exp, y_sig);
c = m.mk_and(m.mk_eq(x_sgn, y_sgn),
m.mk_eq(x_sig, y_sig),
m.mk_eq(x_exp, y_exp));
c = m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig),
m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig));
}
else
c = m.mk_eq(xc, yc);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
assert_cnstr(mk_side_conditions());
return;
@ -572,12 +578,13 @@ namespace smt {
context & ctx = get_context();
mpf_manager & mpfm = m_fpa_util.fm();
app * xe = get_enode(x)->get_owner();
app * ye = get_enode(y)->get_owner();
expr_ref xe(m), ye(m);
xe = get_enode(x)->get_owner();
ye = get_enode(y)->get_owner();
if ((m.is_bool(xe) && m.is_bool(ye)) ||
(m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))) {
SASSERT(xe->get_decl()->get_family_id() == get_family_id());
SASSERT(to_app(xe)->get_decl()->get_family_id() == get_family_id());
return;
}
@ -590,18 +597,18 @@ namespace smt {
if (m_fpa_util.is_float(xe) && m_fpa_util.is_float(ye))
{
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
m_converter.split_fp(xc, x_sgn, x_exp, x_sig);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
c = m.mk_or(m.mk_not(m.mk_eq(x_sgn, y_sgn)),
m.mk_not(m.mk_eq(x_sig, y_sig)),
m.mk_not(m.mk_eq(x_exp, y_exp)));
m_converter.split_fp(yc, y_sgn, y_exp, y_sig);
c = m.mk_not(m.mk_eq(m_bv_util.mk_concat(m_bv_util.mk_concat(x_sgn, x_exp), x_sig),
m_bv_util.mk_concat(m_bv_util.mk_concat(y_sgn, y_exp), y_sig)));
}
else
c = m.mk_not(m.mk_eq(xc, yc));
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
assert_cnstr(mk_side_conditions());
return;
@ -609,7 +616,7 @@ namespace smt {
void theory_fpa::push_scope_eh() {
theory::push_scope_eh();
m_trail_stack.push_scope();
m_trail_stack.push_scope();
}
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
@ -628,8 +635,10 @@ namespace smt {
expr_ref converted(m);
converted = m.mk_and(convert(e), mk_side_conditions());
if (!is_true) converted = m.mk_not(converted);
assert_cnstr(converted);
if (is_true)
assert_cnstr(m.mk_implies(e, converted));
else
assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
}
void theory_fpa::relevant_eh(app * n) {
@ -664,18 +673,17 @@ namespace smt {
assert_cnstr(c);
}
else {
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
assert_cnstr(c);
}
}
}
else if (n->get_family_id() == get_family_id()) {
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
// These are the conversion functions fp.to_* */
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
}
else
UNREACHABLE();
}
void theory_fpa::reset_eh() {
@ -695,6 +703,7 @@ namespace smt {
final_check_status theory_fpa::final_check_eh() {
TRACE("t_fpa", tout << "final_check_eh\n";);
SASSERT(m_converter.m_extra_assertions.empty());
return FC_DONE;
}
@ -705,45 +714,75 @@ namespace smt {
}
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";);
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
ast_manager & m = get_manager();
context & ctx = get_context();
app * owner = n->get_owner();
app_ref owner(m);
owner = n->get_owner();
// If the owner is not internalized, it doesn't have an enode associated.
SASSERT(ctx.e_internalized(owner));
if (m_fpa_util.is_rm_numeral(owner) ||
m_fpa_util.is_numeral(owner))
m_fpa_util.is_numeral(owner)) {
return alloc(expr_wrapper_proc, owner);
}
model_value_proc * res = 0;
app_ref wrapped(m);
wrapped = wrap(owner);
CTRACE("t_fpa", !ctx.e_internalized(wrapped),
tout << "Model dependency not internalized: " <<
mk_ismt2_pp(wrapped, m) <<
" (owner " << (!ctx.e_internalized(owner) ? "not" : "is") <<
" internalized)" << std::endl;);
if (m_fpa_util.is_rm(owner)) {
fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
vp->add_dependency(ctx.get_enode(wrapped));
res = vp;
}
else if (m_fpa_util.is_float(owner)) {
SASSERT(m_bv_util.is_bv(wrapped));
CTRACE("t_fpa_detail", !ctx.e_internalized(wrapped),
tout << "Model dependency not internalized: " <<
mk_ismt2_pp(wrapped, m) <<
" (owner " << (!ctx.e_internalized(owner) ? "not" : "is") <<
" internalized)" << std::endl;);
if (is_app_of(owner, get_family_id(), OP_FPA_FP)) {
SASSERT(to_app(owner)->get_num_args() == 3);
app_ref a0(m), a1(m), a2(m);
a0 = to_app(owner->get_arg(0));
a1 = to_app(owner->get_arg(1));
a2 = to_app(owner->get_arg(2));
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
vp->add_dependency(ctx.get_enode(wrapped));
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
vp->add_dependency(ctx.get_enode(a0));
vp->add_dependency(ctx.get_enode(a1));
vp->add_dependency(ctx.get_enode(a2));
TRACE("t_fpa_detail", tout << "Depends on: " <<
mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl <<
mk_ismt2_pp(a1, m) << " eq. cls. #" << get_enode(a1)->get_root()->get_owner()->get_id() << std::endl <<
mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
res = vp;
}
else
UNREACHABLE();
else if (ctx.e_internalized(wrapped)) {
if (m_fpa_util.is_rm(owner)) {
fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
vp->add_dependency(ctx.get_enode(wrapped));
res = vp;
}
else if (m_fpa_util.is_float(owner)) {
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
enode * en = ctx.get_enode(wrapped);
vp->add_dependency(en);
TRACE("t_fpa_detail", tout << "Depends on: " << mk_ismt2_pp(wrapped, m) << " eq. cls. #" << en->get_root()->get_owner()->get_id() << std::endl;);
res = vp;
}
}
else {
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
return alloc(expr_wrapper_proc, m_fpa_util.mk_pzero(ebits, sbits));
}
SASSERT(res != 0);
return res;
}
@ -754,7 +793,7 @@ namespace smt {
ast_manager & m = get_manager();
context & ctx = get_context();
out << "theory variables:" << std::endl;
out << "fpa theory variables:" << std::endl;
ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
ptr_vector<enode>::const_iterator end = ctx.end_enodes();
for (; it != end; it++) {
@ -762,5 +801,32 @@ namespace smt {
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
out << "bv theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_bv_util.get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
out << "arith theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_arith_util.get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
out << "equivalence classes:\n";
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
expr * r = (*it)->get_root()->get_owner();
out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
}
}
};