mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

FPA: New theory implementation with support for "hidden" variables, relevancy, and eq/diseq.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-28 13:44:29 +00:00
parent 7a15c41c47
commit 23aa614d55
2 changed files with 366 additions and 354 deletions
Download patch file Download diff file Expand all files Collapse all files

638
src/smt/theory_fpa.cpp
View file

@ -22,17 +22,46 @@ Revision History:
#include"theory_bv.h"
#include"smt_model_generator.h"
namespace smt {
namespace smt {
class fpa_factory : public value_factory {
float_util m_util;
virtual app * mk_value_core(mpf const & val, sort * s) {
SASSERT(m_util.get_ebits(s) == val.get_ebits());
SASSERT(m_util.get_sbits(s) == val.get_sbits());
return m_util.mk_value(val);
}
class fpa_atom_trail : public trail<theory_fpa> {
bool_var m_var;
public:
fpa_atom_trail(bool_var v) : m_var(v) {}
virtual ~fpa_atom_trail() {}
fpa_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
m_util(m) {
}
virtual ~fpa_factory() {}
virtual expr * get_some_value(sort * s) { NOT_IMPLEMENTED_YET(); }
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { NOT_IMPLEMENTED_YET(); }
virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); }
virtual void register_value(expr * n) { /* Ignore */ }
app * mk_value(mpf const & x) {
return m_util.mk_value(x);
}
};
class fpa_conv_trail : public trail<theory_fpa> {
ast_manager & m;
obj_map<expr, expr*> & m_conversions;
expr * m_e;
public:
fpa_conv_trail(ast_manager & m, obj_map<expr, expr*> & c, expr * e) : m(m), m_conversions(c), m_e(e) {}
virtual ~fpa_conv_trail() {}
virtual void undo(theory_fpa & th) {
theory_fpa::atom * a = th.get_bv2a(m_var);
a->~atom();
th.erase_bv2a(m_var);
expr * v = m_conversions.find(m_e);
m_conversions.remove(m_e);
m.dec_ref(v);
}
};
@ -43,15 +72,15 @@ namespace smt {
if (m_const2bv.find(f, r)) {
result = r;
}
else {
else {
sort * s = f->get_range();
func_decl *w, *u;
func_decl_ref w(m), u(m);
m_th.get_wrap(s, w, u);
expr_ref bv(m);
bv = m.mk_app(w, m.mk_const(f));
unsigned bv_sz = m_th.m_converter.bu().get_bv_size(bv);
unsigned ebits = m_th.m_converter.fu().get_ebits(f->get_range());
unsigned sbits = m_th.m_converter.fu().get_sbits(f->get_range());
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
unsigned ebits = m_th.m_float_util.get_ebits(f->get_range());
unsigned sbits = m_th.m_float_util.get_sbits(f->get_range());
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),
@ -75,7 +104,7 @@ namespace smt {
SASSERT(is_rm(f->get_range()));
sort * s = f->get_range();
func_decl *w, *u;
func_decl_ref w(m), u(m);
m_th.get_wrap(s, w, u);
result = m.mk_app(w, m.mk_const(f));
@ -87,186 +116,134 @@ namespace smt {
theory_fpa::theory_fpa(ast_manager & m) :
theory(m.mk_family_id("float")),
m_converter(m, this),
m_converter(m, this),
m_rw(m, m_converter, params_ref()),
m_th_rw(m),
m_trail_stack(*this)
m_trail_stack(*this),
m_float_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
m_arith_util(m_converter.au())
{
}
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);
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
TRACE("t_fpa", tout << "fpa_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";);
SASSERT(values.size() == 3);
ast_manager & m = m_th.get_manager();
context & ctx = m_th.get_context();
theory_id bv_id = m.mk_family_id("bv");
theory_bv * th_bv = dynamic_cast<theory_bv *>(ctx.get_theory(bv_id));
SASSERT(th_bv != 0);
float_util & fu = m_th.m_converter.fu();
bv_util & bu = m_th.m_converter.bu();
mpf_manager & mpfm = fu.fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
sort * s = m.get_sort(m_a);
unsigned ebits = fu.get_ebits(s);
unsigned sbits = fu.get_sbits(s);
TRACE("t_fpa", tout << "fpa_value_proc::mk_value for: [" <<
mk_ismt2_pp(values[0], m) << " " <<
mk_ismt2_pp(values[1], m) << " " <<
mk_ismt2_pp(values[2], m) << "]" << std::endl;);
mpf_manager & mpfm = m_fu.fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
unsigned ebits = m_bu.get_bv_size(values[2]);
unsigned sbits = m_bu.get_bv_size(values[1]) + 1;
app * result;
scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
scoped_mpz bias(mpzm);
mpzm.power(mpz(2), ebits - 1, bias);
mpzm.dec(bias);
app * result;
float_op_kind k = (float_op_kind) to_app(m_a)->get_decl_kind();
switch (k)
{
case -1: {
func_decl *w, *u;
m_th.get_wrap(s, w, u);
rational bv_val(0);
scoped_mpz sgn(mpzm), sig(mpzm), exp(bias);
app_ref bv_w(m);
bv_w = m.mk_app(w, m_a);
rational sgn_q(0), sig_q(0), exp_q(bias);
unsigned bv_sz;
if (!th_bv->get_fixed_value(bv_w, bv_val))
result = fu.mk_nan(ebits, sbits);
else {
scoped_mpz all_bits(mpzm);
all_bits = bv_val.to_mpq().numerator();
SASSERT(mpzm.is_one(bv_val.to_mpq().denominator()));
mpzm.machine_div2k(all_bits, ebits + sbits - 1, sgn);
bool r;
r = m_bu.is_numeral(values[0], sgn_q, bv_sz); SASSERT(r); SASSERT(bv_sz == 1);
r = m_bu.is_numeral(values[1], sig_q, bv_sz); SASSERT(r); SASSERT(bv_sz == sbits - 1);
r = m_bu.is_numeral(values[2], exp_q, bv_sz); SASSERT(r); SASSERT(bv_sz == ebits);
scoped_mpz tmp_p(mpzm);
mpzm.power(mpz(2), ebits + sbits - 1, tmp_p);
TRACE("t_fpa", tout << "sgn=" << sgn_q.to_string() << " ; " <<
"sig=" << sig_q.to_string() << " ; " <<
"exp=" << exp_q.to_string() << std::endl;);
if (mpzm.is_one(sgn)) mpzm.sub(all_bits, tmp_p, all_bits);
rational exp_u = exp_q - rational(bias);
SASSERT(exp_u.is_int64());
mpzm.machine_div2k(all_bits, sbits - 1, exp);
scoped_mpz exp_u(mpzm);
mpzm.sub(exp, bias, exp_u);
SASSERT(mpzm.is_int64(exp_u));
mpzm.power(mpz(2), sbits - 1, tmp_p);
mpzm.mod(all_bits, tmp_p, sig);
scoped_mpf f(mpfm);
scoped_mpq sig_mpq(mpqm);
sig_mpq = sig_q.to_mpq();
mpfm.set(f, ebits, sbits, sgn_q.is_one(), sig_mpq.get().numerator(), exp_u.get_int64());
result = m_fu.mk_value(f);
scoped_mpf f(mpfm);
mpfm.set(f, ebits, sbits, mpzm.is_one(sgn), sig, mpzm.get_int64(exp_u));
result = fu.mk_value(f);
}
break;
}
case OP_FLOAT_FP: {
bool is_internalized = ctx.e_internalized(m_a);
if (is_internalized) {
SASSERT(m_a->get_num_args() == 3);
app_ref a_sgn(m), a_sig(m), a_exp(m);
a_sgn = to_app(m_a->get_arg(0));
a_exp = to_app(m_a->get_arg(1));
a_sig = to_app(m_a->get_arg(2));
scoped_mpz bias(mpzm);
mpzm.power(mpz(2), ebits - 1, bias);
mpzm.dec(bias);
rational sgn(0), sig(0), exp(bias);
th_bv->get_fixed_value(a_sgn, sgn);
th_bv->get_fixed_value(a_sig, sig);
th_bv->get_fixed_value(a_exp, exp);
TRACE("t_fpa", tout << "sgn=" << sgn.to_string() << " ; " <<
"sig=" << sig.to_string() << " ; " <<
"exp=" << exp.to_string() << std::endl;);
rational exp_u = exp - rational(bias);
SASSERT(exp_u.is_int64());
scoped_mpf f(mpfm);
scoped_mpq sig_q(mpqm);
sig_q = sig.to_mpq();
mpfm.set(f, ebits, sbits, sgn.is_one(), sig_q.get().numerator(), exp_u.get_int64());
result = fu.mk_value(f);
}
else {
result = fu.mk_nan(ebits, sbits);
}
break;
}
default:
NOT_IMPLEMENTED_YET();
}
TRACE("t_fpa", tout << "fpa_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
TRACE("t_fpa", tout << "fpa_value_proc::mk_value result: " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result;
}
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: " << mk_ismt2_pp(m_a, m_th.get_manager()) << "\n";);
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1);
ast_manager & m = m_th.get_manager();
context & ctx = m_th.get_context();
theory_id bv_id = m.mk_family_id("bv");
theory_bv * th_bv = dynamic_cast<theory_bv *>(ctx.get_theory(bv_id));
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value for: [" <<
mk_ismt2_pp(values[0], m) << "]" << std::endl;);
app * result = 0;
mpf_rounding_mode rm;
if (m_th.m_converter.fu().is_rm_value(m_a, rm)) {
result = m_a.get();
}
else {
sort * s = m.get_sort(m_a);
func_decl *w, *u;
m_th.get_wrap(s, w, u);
sort * s = m.get_sort(values[0]);
unsigned bv_sz;
app_ref bv_w(m);
bv_w = m.mk_app(w, m_a);
rational val(0);
if (ctx.e_internalized(bv_w))
if (!th_bv->get_fixed_value(bv_w, val))
val = rational(0);
rational val(0);
bool r = m_bu.is_numeral(values[0], val, bv_sz);
SASSERT(r);
SASSERT(bv_sz == 3);
switch (val.get_uint64())
{
case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
case BV_RM_TIES_TO_EVEN: result = m_fu.mk_round_nearest_ties_to_even(); break;
case BV_RM_TO_NEGATIVE: result = m_fu.mk_round_toward_negative(); break;
case BV_RM_TO_POSITIVE: result = m_fu.mk_round_toward_positive(); break;
case BV_RM_TO_ZERO:
default: result = m_fu.mk_round_toward_zero();
}
switch (val.get_uint64())
{
case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break;
case BV_RM_TIES_TO_EVEN: result = m_fu.mk_round_nearest_ties_to_even(); break;
case BV_RM_TO_NEGATIVE: result = m_fu.mk_round_toward_negative(); break;
case BV_RM_TO_POSITIVE: result = m_fu.mk_round_toward_positive(); break;
case BV_RM_TO_ZERO:
default: result = m_fu.mk_round_toward_zero();
}
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result;
}
void theory_fpa::get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap)
void theory_fpa::get_wrap(sort * s, func_decl_ref & wrap, func_decl_ref & unwrap)
{
if (!m_wraps.find(s, wrap) || !m_unwraps.find(s, unwrap)) {
func_decl *w, *u;
if (!m_wraps.find(s, w) || !m_unwraps.find(s, u)) {
SASSERT(!m_wraps.contains(s));
SASSERT(!m_unwraps.contains(s));
ast_manager & m = get_manager();
context & ctx = get_context();
sort * bv_srt = 0;
if (m_converter.is_rm(s))
bv_srt = m_converter.bu().mk_sort(3);
bv_srt = m_bv_util.mk_sort(3);
else {
SASSERT(m_converter.is_float(s));
unsigned ebits = m_converter.fu().get_ebits(s);
unsigned sbits = m_converter.fu().get_sbits(s);
bv_srt = m_converter.bu().mk_sort(ebits + sbits);
SASSERT(m_converter.is_float(s));
unsigned ebits = m_float_util.get_ebits(s);
unsigned sbits = m_float_util.get_sbits(s);
bv_srt = m_bv_util.mk_sort(ebits + sbits);
}
wrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &s, bv_srt);
unwrap = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
m_wraps.insert(s, wrap);
m_unwraps.insert(s, unwrap);
get_context().push_trail(insert_obj_map<context, sort, func_decl*>(m_wraps, s));
get_context().push_trail(insert_obj_map<context, sort, func_decl*>(m_unwraps, s));
w = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVWRAP, 0, 0, 1, &s, bv_srt);
u = m.mk_func_decl(get_family_id(), OP_FLOAT_INTERNAL_BVUNWRAP, 0, 0, 1, &bv_srt, s);
m_wraps.insert(s, w);
m_unwraps.insert(s, u);
m.inc_ref(w);
m.inc_ref(u);
}
wrap = w;
unwrap = u;
}
expr_ref theory_fpa::convert_atom(expr * e) {
@ -274,52 +251,91 @@ namespace smt {
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
m_th_rw(res, res);
TRACE("t_fpa", tout << "converted atom:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
TRACE("t_fpa_detail", tout << "converted atom:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
return res;
}
expr_ref theory_fpa::convert_term(expr * e) {
ast_manager & m = get_manager();
context & ctx = get_context();
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
SASSERT(is_app(res));
if (m_converter.fu().is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT));
SASSERT(m_converter.bu().get_bv_size(res) == 3);
if (m_float_util.is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(res), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(res) == 3);
ctx.internalize(res, false);
}
else {
SASSERT(to_app(res)->get_family_id() == get_family_id());
decl_kind k = to_app(res)->get_decl_kind();
if (k == OP_FLOAT_TO_FP) {
SASSERT(to_app(res)->get_num_args() == 3);
SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(0)), m_converter.bu().get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(1)), m_converter.bu().get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(2)), m_converter.bu().get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(0)), m_bv_util.get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(to_app(res)->get_arg(1)), m_bv_util.get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(to_app(res)->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(res, sgn, sig, exp);
m_th_rw(sgn, s_sgn);
m_th_rw(sig, s_sig);
m_th_rw(exp, s_exp);
m_th_rw(exp, s_exp);
m_converter.mk_triple(s_sgn, s_sig, s_exp, res);
}
else {
SASSERT(is_sort_of(m.get_sort(e), get_family_id(), ROUNDING_MODE_SORT));
SASSERT(is_sort_of(m.get_sort(res), m_converter.bu().get_family_id(), BV_SORT));
SASSERT(is_sort_of(m.get_sort(res), m_bv_util.get_family_id(), BV_SORT));
}
}
TRACE("t_fpa", tout << "converted term:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
TRACE("t_fpa_detail", tout << "converted term:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}
expr_ref theory_fpa::convert(expr * e)
{
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;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}
else {
if (m.is_bool(e))
res = convert_atom(e);
else if (m_float_util.is_float(e) || m_float_util.is_rm(e))
res = convert_term(e);
else
UNREACHABLE();
TRACE("t_fpa_detail", tout << "caching:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
m_conversions.insert(e, res);
m.inc_ref(res);
m_trail_stack.push(fpa_conv_trail(m, m_conversions, e));
}
return res;
}
@ -340,14 +356,14 @@ namespace smt {
res = m.mk_and(res, t);
}
m_converter.m_extra_assertions.reset();
TRACE("t_fpa", if (!m.is_true(res)) tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";);
return res;
}
void theory_fpa::assert_cnstr(expr * e) {
void theory_fpa::assert_cnstr(expr * e) {
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
if (get_manager().is_true(e)) return;
TRACE("t_fpa", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
context& ctx = get_context();
ctx.internalize(e, false);
literal lit(ctx.get_literal(e));
@ -359,7 +375,6 @@ namespace smt {
context & ctx = get_context();
theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
m_tvars.push_back(v);
TRACE("t_fpa", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
}
@ -381,7 +396,9 @@ namespace smt {
ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m);
bv_atom = convert_atom(atom);
bv_atom = convert(atom);
TRACE("t_fpa_detail", tout << "converted: " << mk_ismt2_pp(bv_atom, get_manager()) << "\n";);
SASSERT(bv_atom.get()->get_kind() == AST_APP);
bv_atom = m.mk_and(bv_atom, mk_side_conditions());
expr_ref atom_iff(m);
@ -390,13 +407,13 @@ namespace smt {
}
bool theory_fpa::internalize_term(app * term) {
TRACE("t_fpa_detail", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
SASSERT(term->get_family_id() == get_family_id());
SASSERT(!get_context().e_internalized(term));
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("t_fpa_detail", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
SASSERT(term->get_family_id() == get_family_id());
SASSERT(!ctx.e_internalized(term));
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false);
@ -407,8 +424,7 @@ namespace smt {
if (is_attached_to_var(e))
return false;
attach_new_th_var(e);
TRACE("t_fpa", tout << "internalized? " << (ctx.e_internalized(term)?"yes":"no") << std::endl;);
attach_new_th_var(e);
return true;
}
@ -417,22 +433,25 @@ namespace smt {
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());
ast_manager & m = get_manager();
ast_manager & m = get_manager();
if (!is_attached_to_var(n))
attach_new_th_var(n);
app * owner = n->get_owner();
sort * owner_sort = m.get_sort(owner);
if (m_converter.is_rm(owner_sort)) {
bv_util & bu = m_converter.bu();
func_decl *wrap, *unwrap;
app_ref owner(m);
sort_ref owner_sort(m);
owner = n->get_owner();
owner_sort = m.get_sort(owner);
if (m_float_util.is_rm(owner_sort)) {
func_decl_ref wrap(m), unwrap(m);
get_wrap(owner_sort, wrap, unwrap);
if (owner->get_decl() != unwrap)
{
expr_ref converted(m), t(m);
m_rw(owner, converted);
t = bu.mk_ule(converted, bu.mk_numeral(4, 3));
{
expr_ref converted(m), t(m), limit(m);
converted = convert(owner);
limit = m_bv_util.mk_numeral(4, 3);
t = m_bv_util.mk_ule(converted, limit);
assert_cnstr(t);
}
}
@ -446,41 +465,45 @@ namespace smt {
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl; );
context & ctx = get_context();
float_util & fu = m_converter.fu();
bv_util & bu = m_converter.bu();
float_util & fu = m_float_util;
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();
app * ye = get_enode(y)->get_owner();
if (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))
{
SASSERT(xe->get_decl()->get_family_id() == get_family_id());
return;
}
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
{
expr_ref xc(m), yc(m);
xc = convert_term(xe);
yc = convert_term(ye);
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
expr_ref c(m);
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));
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
m.mk_eq(x_exp, y_exp));
}
else if (fu.is_rm(xe) && fu.is_rm(ye)) {
expr_ref xc(m), yc(m);
xc = convert_term(xe);
yc = convert_term(ye);
expr_ref c(m);
else if (fu.is_rm(xe) && fu.is_rm(ye))
c = m.mk_eq(xc, yc);
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
}
else
UNREACHABLE();
// assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
return;
}
@ -492,57 +515,55 @@ namespace smt {
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
context & ctx = get_context();
float_util & fu = m_converter.fu();
bv_util & bu = m_converter.bu();
mpf_manager & mpfm = fu.fm();
mpf_manager & mpfm = m_float_util.fm();
app * xe = get_enode(x)->get_owner();
app * ye = get_enode(y)->get_owner();
if (fu.is_float(xe) && fu.is_float(ye))
if (m_bv_util.is_bv(xe) && m_bv_util.is_bv(ye))
{
expr_ref xc(m), yc(m);
xc = convert_term(xe);
yc = convert_term(ye);
SASSERT(xe->get_decl()->get_family_id() == get_family_id());
return;
}
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
expr_ref c(m);
if (m_float_util.is_float(xe) && m_float_util.is_float(ye))
{
expr *x_sgn, *x_sig, *x_exp;
m_converter.split_triple(xc, x_sgn, x_sig, x_exp);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_triple(yc, y_sgn, y_sig, y_exp);
expr_ref c(m);
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)));
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
}
else if (fu.is_rm(xe) && fu.is_rm(ye)) {
expr_ref xc(m), yc(m);
xc = convert_term(xe);
yc = convert_term(ye);
expr_ref c(m);
else if (m_float_util.is_rm(xe) && m_float_util.is_rm(ye))
c = m.mk_not(m.mk_eq(xc, yc));
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
}
else
UNREACHABLE();
// assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
assert_cnstr(c);
assert_cnstr(mk_side_conditions());
return;
}
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) {
TRACE("t_fpa", tout << num_scopes << "\n";);
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
m_trail_stack.pop_scope(num_scopes);
unsigned num_old_vars = get_old_num_vars(num_scopes);
for (unsigned i = num_old_vars; i < get_num_vars(); i++) {
// m_trans_map.erase(get_enode(m_tvars[i])->get_owner());
}
m_tvars.shrink(num_old_vars);
TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";);
// unsigned num_old_vars = get_old_num_vars(num_scopes);
theory::pop_scope_eh(num_scopes);
}
@ -554,57 +575,68 @@ namespace smt {
TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
expr_ref converted(m);
m_rw(e, converted);
converted = convert(e);
converted = m.mk_and(converted, mk_side_conditions());
if (!is_true) converted = m.mk_not(converted);
assert_cnstr(converted);
}
void theory_fpa::relevant_eh(app * n) {
TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, get_manager()) << "\n";);
NOT_IMPLEMENTED_YET();
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";);
if (m.is_bool(n))
return;
mpf_manager & mpfm = m_float_util.fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
float_util & fu = m_converter.fu();
bv_util & bu = m_converter.bu();
mpf_manager & mpfm = fu.fm();
if (m_float_util.is_float(n) || m_float_util.is_rm(n)) {
sort * s = m.get_sort(n);
func_decl_ref wrap(m), unwrap(m);
get_wrap(s, wrap, unwrap);
if (bu.is_bv(n))
return;
sort * s = m.get_sort(n);
func_decl *wrap, *unwrap;
get_wrap(s, wrap, unwrap);
if (n->get_decl() != unwrap) {
expr * wrapped = m.mk_app(wrap, n);
mpf_rounding_mode rm;
scoped_mpf val(mpfm);
if (fu.is_rm_value(n, rm))
assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rm, 3)));
else if (fu.is_value(n, val)) {
unsigned sz = val.get().get_ebits() + val.get().get_sbits();
scoped_mpq q(fu.fm().mpq_manager());
mpfm.to_rational(val, q);
assert_cnstr(m.mk_eq(wrapped, bu.mk_numeral(rational(q), sz)));
if (n->get_decl() != unwrap) {
expr_ref wrapped(m), c(m);
wrapped = m.mk_app(wrap, n);
mpf_rounding_mode rm;
scoped_mpf val(mpfm);
if (m_float_util.is_rm_value(n, rm)) {
c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
c = m.mk_and(c, mk_side_conditions());
assert_cnstr(c);
}
else if (m_float_util.is_value(n, val)) {
unsigned sz = val.get().get_ebits() + val.get().get_sbits();
expr_ref bv_val_e(m);
bv_val_e = convert(n);
SASSERT(is_app(bv_val_e));
SASSERT(to_app(bv_val_e)->get_num_args() == 3);
app_ref bv_val_a(to_app(bv_val_e.get()), m);
c = m.mk_eq(wrapped, m_bv_util.mk_concat(
m_bv_util.mk_concat(bv_val_a->get_arg(0), bv_val_a->get_arg(1)),
bv_val_a->get_arg(2)));
c = m.mk_and(c, mk_side_conditions());
assert_cnstr(c);
}
else {
c = m.mk_eq(m.mk_app(unwrap, wrapped), n);
c = m.mk_and(c, mk_side_conditions());
assert_cnstr(c);
}
}
else
assert_cnstr(m.mk_eq(m.mk_app(unwrap, wrapped), n));
}
}
void theory_fpa::reset_eh() {
TRACE("t_fpa", tout << "reset_eh for: " << "\n";);
TRACE("t_fpa", tout << "reset_eh\n";);
pop_scope_eh(m_trail_stack.get_num_scopes());
m_converter.reset();
m_rw.reset();
m_bool_var2atom.reset();
m_temporaries.reset();
m_tvars.reset();
m_th_rw.reset();
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
if (m_factory) dealloc(m_factory); m_factory = 0;
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);
theory::reset_eh();
}
@ -615,28 +647,54 @@ namespace smt {
TRACE("t_fpa", display(tout););
}
void theory_fpa::add_value_dep(fpa_value_proc * vp, expr * e) {
SASSERT(m_bv_util.is_bv(e));
ast_manager & m = get_manager();
context & ctx = get_context();
if (ctx.e_internalized(e))
vp->add_dependency(ctx.get_enode(e));
else {
expr_ref n(m);
n = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(e));
if (!ctx.e_internalized(n))
ctx.internalize(n, false);
vp->add_dependency(ctx.get_enode(n));
}
}
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()) << "\n";);
ast_manager & m = get_manager();
float_util & fu = m_converter.fu();
context & ctx = get_context();
app * owner = n->get_owner();
expr * owner = n->get_owner();
sort * o_srt = m.get_sort(owner);
app_ref c_a(m);
c_a = to_app(convert(owner));
SASSERT(ctx.e_internalized(owner));
mpf_rounding_mode rm;
TRACE("t_fpa", tout << "converted = " << mk_ismt2_pp(c_a, get_manager()) << "\n";);
if (fu.is_rm_value(n->get_owner(), rm))
return alloc(expr_wrapper_proc, n->get_owner());
else if (fu.is_value(n->get_owner()))
return alloc(expr_wrapper_proc, n->get_owner());
else if (fu.is_rm(owner))
return alloc(fpa_rm_value_proc, this, app_ref(to_app(owner), m));
else if (fu.is_float(owner))
return alloc(fpa_value_proc, this, app_ref(to_app(owner), m));
UNREACHABLE();
return 0;
model_value_proc * res = 0;
if (m_float_util.is_rm(owner)) {
fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
add_value_dep(vp, c_a);
res = vp;
}
else if (m_float_util.is_float(owner)) {
fpa_value_proc * vp = alloc(fpa_value_proc, this);
expr_ref bv_sgn(m), bv_sig(m), bv_exp(m);
m_converter.split_triple(c_a, bv_sgn, bv_sig, bv_exp);
add_value_dep(vp, bv_sgn);
add_value_dep(vp, bv_sig);
add_value_dep(vp, bv_exp);
res = vp;
}
else
UNREACHABLE();
return res;
}
void theory_fpa::finalize_model(model_generator & mg) {}
@ -649,8 +707,10 @@ namespace smt {
out << "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++)
out << (*it)->get_th_var(get_family_id()) << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
}
}
};

82
src/smt/theory_fpa.h
View file

@ -29,39 +29,10 @@ Revision History:
namespace smt {
class fpa_factory : public value_factory {
float_util m_util;
virtual app * mk_value_core(mpf const & val, sort * s) {
SASSERT(m_util.get_ebits(s) == val.get_ebits());
SASSERT(m_util.get_sbits(s) == val.get_sbits());
return m_util.mk_value(val);
}
public:
fpa_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
m_util(m) {
}
virtual ~fpa_factory() {}
virtual expr * get_some_value(sort * s) { NOT_IMPLEMENTED_YET(); }
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { NOT_IMPLEMENTED_YET(); }
virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); }
virtual void register_value(expr * n) { /* Ignore */ }
app * mk_value(mpf const & x) {
return m_util.mk_value(x);
}
};
class fpa_factory;
class theory_fpa : public theory {
class th_trail_stack : public trail_stack<theory_fpa> {
public:
th_trail_stack(theory_fpa & th) : trail_stack<theory_fpa>(th) {}
virtual ~th_trail_stack() {}
};
typedef trail_stack<theory_fpa> th_trail_stack;
class fpa2bv_converter_wrapped : public fpa2bv_converter {
public:
@ -76,11 +47,13 @@ namespace smt {
class fpa_value_proc : public model_value_proc {
protected:
theory_fpa & m_th;
app_ref m_a;
theory_fpa & m_th;
float_util & m_fu;
bv_util & m_bu;
svector<model_value_dependency> m_dependencies;
public:
fpa_value_proc(theory_fpa * th, app_ref & a) : m_th(*th), m_a(a) {}
fpa_value_proc(theory_fpa * th) :
m_th(*th),m_fu(th->m_float_util),m_bu(th->m_bv_util) {}
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
virtual ~fpa_value_proc() {}
virtual void get_dependencies(buffer<model_value_dependency> & result) {
@ -89,50 +62,27 @@ namespace smt {
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
class fpa_rm_value_proc : public fpa_value_proc {
float_util & m_fu;
bv_util & m_bu;
class fpa_rm_value_proc : public fpa_value_proc {
public:
fpa_rm_value_proc(theory_fpa * th, app_ref & a) :
fpa_value_proc(th, a),
m_fu(th->m_converter.fu()),
m_bu(th->m_converter.bu()) {}
fpa_rm_value_proc(theory_fpa * th) :
fpa_value_proc(th) {}
void add_dependency(enode * n) { fpa_value_proc::add_dependency(n); }
virtual ~fpa_rm_value_proc() {}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
public:
class atom {
public:
virtual ~atom() {}
};
struct pred_atom : public atom {
literal m_var;
literal m_def;
pred_atom(literal v, literal d) : m_var(v), m_def(d) {}
virtual ~pred_atom() {}
};
typedef ptr_vector<pred_atom> bool_var2atom;
void insert_bv2a(bool_var bv, pred_atom * a) { m_bool_var2atom.setx(bv, a, 0); }
void erase_bv2a(bool_var bv) { m_bool_var2atom[bv] = 0; }
pred_atom * get_bv2a(bool_var bv) const { return m_bool_var2atom.get(bv, 0); }
region & get_region() { return m_trail_stack.get_region(); }
protected:
fpa2bv_converter_wrapped m_converter;
fpa2bv_rewriter m_rw;
th_rewriter m_th_rw;
th_trail_stack m_trail_stack;
bool_var2atom m_bool_var2atom;
enode_vector m_temporaries;
vector<theory_var> m_tvars;
fpa_factory * m_factory;
float_util & m_float_util;
bv_util & m_bv_util;
arith_util & m_arith_util;
obj_map<sort, func_decl*> m_wraps;
obj_map<sort, func_decl*> m_unwraps;
float_decl_plugin m_flt_plugin;
obj_map<expr, expr*> m_conversions;
virtual final_check_status final_check_eh() { return FC_DONE; }
virtual bool internalize_atom(app * atom, bool gate_ctx);
@ -161,14 +111,16 @@ namespace smt {
protected:
expr_ref mk_side_conditions();
expr_ref convert(expr * e);
expr_ref convert_atom(expr * e);
expr_ref convert_term(expr * e);
void get_wrap(sort * s, func_decl *& wrap, func_decl *& unwrap);
void get_wrap(sort * s, func_decl_ref & wrap, func_decl_ref & unwrap);
void add_trail(ast * a);
void mk_bv_eq(expr * x, expr * y);
void attach_new_th_var(enode * n);
void assert_cnstr(expr * e);
void add_value_dep(fpa_value_proc * vp, expr * e);
};
};