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

Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
This commit is contained in:
Christoph M. Wintersteiger 2015-01-21 14:25:31 +00:00
commit d56d63e3e8
110 changed files with 11348 additions and 4084 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) {

16
src/smt/smt_setup.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include"theory_dummy.h"
#include"theory_dl.h"
#include"theory_seq_empty.h"
#include"theory_fpa.h"
namespace smt {
@ -679,6 +680,15 @@ namespace smt {
setup_mi_arith();
}
void setup::setup_QF_FP() {
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
}
void setup::setup_QF_FPBV() {
setup_QF_BV();
m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
}
bool is_arith(static_features const & st) {
return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0;
}
@ -780,6 +790,10 @@ namespace smt {
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
}
void setup::setup_fpa() {
m_context.register_plugin(alloc(theory_fpa, m_manager));
}
void setup::setup_unknown() {
setup_arith();
setup_arrays();
@ -787,6 +801,7 @@ namespace smt {
setup_datatypes();
setup_dl();
setup_seq();
setup_fpa();
}
void setup::setup_unknown(static_features & st) {
@ -798,6 +813,7 @@ namespace smt {
setup_AUFLIA(false);
setup_datatypes();
setup_bv();
setup_fpa();
return;
}

6
src/smt/smt_setup.h
View file

@ -75,6 +75,8 @@ namespace smt {
void setup_QF_AX(static_features const & st);
void setup_QF_AUFLIA();
void setup_QF_AUFLIA(static_features const & st);
void setup_QF_FP();
void setup_QF_FPBV();
void setup_LRA();
void setup_AUFLIA(bool simple_array = true);
void setup_AUFLIA(static_features const & st);
@ -91,10 +93,12 @@ namespace smt {
void setup_bv();
void setup_arith();
void setup_dl();
void setup_seq();
void setup_seq();
void setup_instgen();
void setup_i_arith();
void setup_mi_arith();
void setup_fpa();
public:
setup(context & c, smt_params & params);
void mark_already_configured() { m_already_configured = true; }

804
src/smt/theory_fpa.cpp
View file

@ -17,30 +17,816 @@ Revision History:
--*/
#include"ast_smt2_pp.h"
#include"smt_context.h"
#include"theory_fpa.h"
#include"theory_bv.h"
#include"smt_model_generator.h"
namespace smt {
class fpa2bv_conversion_trail_elem : public trail<theory_fpa> {
ast_manager & m;
obj_map<expr, expr*> & m_conversions;
expr * m_e;
public:
fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
m(m), m_conversions(c), m_e(e) {}
virtual ~fpa2bv_conversion_trail_elem() {}
virtual void undo(theory_fpa & th) {
expr * v = m_conversions.find(m_e);
m_conversions.remove(m_e);
m.dec_ref(v);
}
};
void theory_fpa::fpa2bv_converter_wrapped::mk_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_const2bv.find(f, r)) {
result = r;
}
else {
sort * s = f->get_range();
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
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_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);
}
}
void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);
SASSERT(f->get_arity() == 0);
expr * r;
if (m_rm_const2bv.find(f, r)) {
result = r;
}
else {
SASSERT(is_rm(f->get_range()));
result = m_th.wrap(m.mk_const(f));
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
}
}
theory_fpa::theory_fpa(ast_manager & m) :
theory(m.mk_family_id("fpa")),
m_converter(m, this),
m_rw(m, m_converter, params_ref()),
m_th_rw(m),
m_trail_stack(*this),
m_fpa_util(m_converter.fu()),
m_bv_util(m_converter.bu()),
m_arith_util(m_converter.au())
{
params_ref p;
p.set_bool("arith_lhs", true);
m_th_rw.updt_params(p);
}
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) {
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();
app * result;
scoped_mpz bias(mpzm);
mpzm.power(mpz(2), m_ebits - 1, bias);
mpzm.dec(bias);
scoped_mpz sgn_z(mpzm), sig_z(mpzm), exp_z(mpzm);
unsigned bv_sz;
if (values.size() == 1) {
SASSERT(m_bu.is_bv(values[0]));
SASSERT(m_bu.get_bv_size(values[0]) == (m_ebits + m_sbits));
rational all_r(0);
scoped_mpz all_z(mpzm);
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);
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 [" <<
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;
}
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();
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]);
unsigned bv_sz;
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();
}
TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " <<
mk_ismt2_pp(result, m_th.get_manager()) << "\n";);
return result;
}
app_ref theory_fpa::wrap(expr * e) {
SASSERT(!m_fpa_util.is_wrap(e));
ast_manager & m = get_manager();
context & ctx = get_context();
sort * e_srt = m.get_sort(e);
func_decl *w;
if (!m_wraps.find(e_srt, w)) {
SASSERT(!m_wraps.contains(e_srt));
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);
}
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);
}
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 * bv_srt = m.get_sort(e);
func_decl *u;
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(bv_srt, u);
m.inc_ref(u);
}
app_ref res(m);
res = m.mk_app(u, e);
return res;
}
expr_ref theory_fpa::convert_atom(expr * e) {
ast_manager & m = get_manager();
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
m_th_rw(res, res);
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 e_conv(m), res(m);
proof_ref pr(m);
m_rw(e, e_conv);
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)) {
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();
SASSERT(res.get() != 0);
return res;
}
expr_ref theory_fpa::convert_conversion_term(expr * e) {
/* This is for the conversion functions fp.to_* */
ast_manager & m = get_manager();
context & ctx = get_context();
expr_ref res(m);
proof_ref pr(m);
SASSERT(m_arith_util.is_real(e) || m_bv_util.is_bv(e));
m_rw(e, res);
m_th_rw(res, res);
return res;
}
expr_ref theory_fpa::convert_unwrap(expr * e) {
SASSERT(m_fpa_util.is_unwrap(e));
ast_manager & m = get_manager();
sort * srt = m.get_sort(e);
expr_ref res(m);
if (m_fpa_util.is_rm(srt)) {
res = to_app(e)->get_arg(0);
}
else {
SASSERT(m_fpa_util.is_float(srt));
unsigned ebits = m_fpa_util.get_ebits(srt);
unsigned sbits = m_fpa_util.get_sbits(srt);
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;
}
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_fpa_util.is_unwrap(e))
res = convert_unwrap(e);
else if (m.is_bool(e))
res = convert_atom(e);
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e);
else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
res = convert_conversion_term(e);
else
UNREACHABLE();
TRACE("t_fpa_detail", tout << "converted; 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(fpa2bv_conversion_trail_elem(m, m_conversions, e));
}
return res;
}
expr_ref theory_fpa::mk_side_conditions()
{
ast_manager & m = get_manager();
context & ctx = get_context();
simplifier & simp = ctx.get_simplifier();
expr_ref res(m), t(m);
proof_ref t_pr(m);
res = m.mk_true();
expr_ref_vector::iterator it = m_converter.m_extra_assertions.begin();
expr_ref_vector::iterator end = m_converter.m_extra_assertions.end();
for (; it != end; it++) {
simp(*it, t, t_pr);
res = m.mk_and(res, t);
}
m_converter.m_extra_assertions.reset();
m_th_rw(res);
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) {
if (get_manager().is_true(e)) return;
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
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);
TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
}
void theory_fpa::attach_new_th_var(enode * n) {
context & ctx = get_context();
theory_var v = mk_var(n);
ctx.attach_th_var(n, this, v);
TRACE("t_fpa_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
}
bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
TRACE("t_fpa", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
SASSERT(atom->get_family_id() == get_family_id());
NOT_IMPLEMENTED_YET();
ast_manager & m = get_manager();
context & ctx = get_context();
if (ctx.b_internalized(atom))
return true;
unsigned num_args = atom->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(atom->get_arg(i), false);
literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m);
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());
assert_cnstr(m.mk_iff(atom, bv_atom));
return true;
}
void theory_fpa::new_eq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
bool theory_fpa::internalize_term(app * term) {
ast_manager & m = get_manager();
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));
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false);
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;
attach_new_th_var(e);
// The conversion operators fp.to_* appear in non-FP constraints.
// The corresponding constraints will not be translated and added
// via convert(...) and assert_cnstr(...) in initialize_atom(...).
// Therefore, we translate and assert them here.
fpa_op_kind k = (fpa_op_kind)term->get_decl_kind();
switch (k) {
case OP_FPA_TO_UBV:
case OP_FPA_TO_SBV:
case OP_FPA_TO_REAL: {
expr_ref conv(m);
conv = convert(term);
assert_cnstr(m.mk_eq(term, conv));
assert_cnstr(mk_side_conditions());
break;
}
default: /* ignore */;
}
return true;
}
void theory_fpa::apply_sort_cnstr(enode * n, sort * s) {
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());
if (!is_attached_to_var(n)) {
attach_new_th_var(n);
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);
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));
}
}
void theory_fpa::new_diseq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
void theory_fpa::new_eq_eh(theory_var x, theory_var y) {
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " = " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
context & ctx = get_context();
fpa_util & fu = m_fpa_util;
bv_util & bu = m_bv_util;
mpf_manager & mpfm = fu.fm();
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(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_fp(xc, x_sgn, x_exp, x_sig);
expr *y_sgn, *y_sig, *y_exp;
m_converter.split_fp(yc, y_sgn, y_exp, y_sig);
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);
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
assert_cnstr(mk_side_conditions());
return;
}
void theory_fpa::new_diseq_eh(theory_var x, theory_var y) {
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
context & ctx = get_context();
mpf_manager & mpfm = m_fpa_util.fm();
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(to_app(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_fpa_util.is_float(xe) && m_fpa_util.is_float(ye))
{
expr *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_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));
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));
assert_cnstr(mk_side_conditions());
return;
}
void theory_fpa::push_scope_eh() {
NOT_IMPLEMENTED_YET();
theory::push_scope_eh();
m_trail_stack.push_scope();
}
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
NOT_IMPLEMENTED_YET();
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
m_trail_stack.pop_scope(num_scopes);
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);
}
void theory_fpa::assign_eh(bool_var v, bool is_true) {
ast_manager & m = get_manager();
context & ctx = get_context();
expr * e = ctx.bool_var2expr(v);
TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";);
expr_ref converted(m);
converted = m.mk_and(convert(e), mk_side_conditions());
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) {
ast_manager & m = get_manager();
TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";);
mpf_manager & mpfm = m_fpa_util.fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
sort * s = m.get_sort(n);
if (!m_fpa_util.is_unwrap(n)) {
expr_ref wrapped(m), c(m);
wrapped = wrap(n);
mpf_rounding_mode rm;
scoped_mpf val(mpfm);
if (m_fpa_util.is_rm_numeral(n, rm)) {
c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3));
assert_cnstr(c);
}
else if (m_fpa_util.is_numeral(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);
expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
c = m.mk_eq(wrapped, m_bv_util.mk_concat(3, args));
c = m.mk_and(c, mk_side_conditions());
assert_cnstr(c);
}
else {
c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n);
assert_cnstr(c);
}
}
}
else if (n->get_family_id() == get_family_id()) {
// 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() {
TRACE("t_fpa", tout << "reset_eh\n";);
pop_scope_eh(m_trail_stack.get_num_scopes());
m_converter.reset();
m_rw.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();
}
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;
}
void theory_fpa::init_model(model_generator & mg) {
TRACE("t_fpa", tout << "initializing model" << std::endl; display(tout););
m_factory = alloc(fpa_value_factory, get_manager(), get_family_id());
mg.register_factory(m_factory);
}
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()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
ast_manager & m = get_manager();
context & ctx = get_context();
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)) {
return alloc(expr_wrapper_proc, owner);
}
model_value_proc * res = 0;
app_ref wrapped(m);
wrapped = wrap(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(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 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;
}
void theory_fpa::finalize_model(model_generator & mg) {}
void theory_fpa::display(std::ostream & out) const
{
ast_manager & m = get_manager();
context & ctx = get_context();
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++) {
theory_var v = (*it)->get_th_var(get_family_id());
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;
}
}
};

163
src/smt/theory_fpa.h
View file

@ -20,26 +20,173 @@ Revision History:
#define _THEORY_FPA_H_
#include"smt_theory.h"
#include"trail.h"
#include"fpa2bv_converter.h"
#include"fpa2bv_rewriter.h"
#include"th_rewriter.h"
#include"value_factory.h"
#include"smt_model_generator.h"
namespace smt {
class theory_fpa : public theory {
fpa2bv_converter m_converter;
virtual final_check_status final_check_eh() { return FC_DONE; }
virtual bool internalize_atom(app*, bool);
virtual bool internalize_term(app*) { return internalize_atom(0, false); }
class fpa_value_factory : public value_factory {
fpa_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_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
m_util(m) {}
virtual ~fpa_value_factory() {}
virtual expr * get_some_value(sort * s) {
mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
return m_util.mk_value(q);
}
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
mpf_manager & mpfm = m_util.fm();
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
v1 = m_util.mk_value(q);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 1);
v2 = m_util.mk_value(q);
return true;
}
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 theory_fpa : public theory {
protected:
typedef trail_stack<theory_fpa> th_trail_stack;
class fpa2bv_converter_wrapped : public fpa2bv_converter {
public:
theory_fpa & m_th;
fpa2bv_converter_wrapped(ast_manager & m, theory_fpa * th) :
fpa2bv_converter(m),
m_th(*th) {}
virtual ~fpa2bv_converter_wrapped() {}
virtual void mk_const(func_decl * f, expr_ref & result);
virtual void mk_rm_const(func_decl * f, expr_ref & result);
};
class fpa_value_proc : public model_value_proc {
protected:
theory_fpa & m_th;
ast_manager & m;
fpa_util & m_fu;
bv_util & m_bu;
buffer<model_value_dependency> m_deps;
unsigned m_ebits;
unsigned m_sbits;
public:
fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()),
m_ebits(ebits), m_sbits(sbits) {}
virtual ~fpa_value_proc() {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_deps);
}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
class fpa_rm_value_proc : public model_value_proc {
theory_fpa & m_th;
ast_manager & m;
fpa_util & m_fu;
bv_util & m_bu;
buffer<model_value_dependency> m_deps;
public:
fpa_rm_value_proc(theory_fpa * th) :
m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()) {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_deps);
}
virtual ~fpa_rm_value_proc() {}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values);
};
protected:
fpa2bv_converter_wrapped m_converter;
fpa2bv_rewriter m_rw;
th_rewriter m_th_rw;
th_trail_stack m_trail_stack;
fpa_value_factory * m_factory;
fpa_util & m_fpa_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;
obj_map<expr, expr*> m_conversions;
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void apply_sort_cnstr(enode * n, sort * s);
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void reset_eh();
virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
virtual char const * get_name() const { return "fpa"; }
virtual char const * get_name() const { return "fpa"; }
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
void assign_eh(bool_var v, bool is_true);
virtual void relevant_eh(app * n);
virtual void init_model(model_generator & m);
virtual void finalize_model(model_generator & mg);
public:
theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {}
theory_fpa(ast_manager& m);
virtual ~theory_fpa();
virtual void display(std::ostream & out) const;
protected:
expr_ref mk_side_conditions();
expr_ref convert(expr * e);
expr_ref convert_atom(expr * e);
expr_ref convert_term(expr * e);
expr_ref convert_conversion_term(expr * e);
expr_ref convert_unwrap(expr * e);
void add_trail(ast * a);
void attach_new_th_var(enode * n);
void assert_cnstr(expr * e);
app_ref wrap(expr * e);
app_ref unwrap(expr * e, sort * s);
};
};
#endif /* _THEORY_FPA_H_ */