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

FPA: added support for rewriting quantified floats to quantified bit-vectors.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-05-02 15:24:07 +01:00
parent 7053b7636b
commit 00d5dea9a5
3 changed files with 98 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -150,6 +150,20 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
}
}
void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) {
SASSERT(is_float(srt));
unsigned ebits = m_util.get_ebits(srt);
unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m);
sgn = m.mk_var(base_inx, m_bv_util.mk_sort(1));
s = m.mk_var(base_inx + 1, m_bv_util.mk_sort(sbits-1));
e = m.mk_var(base_inx + 2, m_bv_util.mk_sort(ebits));
mk_triple(sgn, s, e, result);
}
void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
SASSERT(f->get_family_id() == null_family_id);

4
src/tactic/fpa/fpa2bv_converter.h
View file

@ -35,7 +35,7 @@ class fpa2bv_converter {
ast_manager & m;
basic_simplifier_plugin m_simp;
float_util m_util;
mpf_manager & m_mpf_manager;
mpf_manager & m_mpf_manager;
unsynch_mpz_manager & m_mpz_manager;
bv_util m_bv_util;
float_decl_plugin * m_plugin;
@ -48,6 +48,7 @@ public:
~fpa2bv_converter();
float_util & fu() { return m_util; }
bv_util & bu() { return m_bv_util; }
bool is_float(sort * s) { return m_util.is_float(s); }
bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
@ -68,6 +69,7 @@ public:
void mk_value(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_const(func_decl * f, expr_ref & result);
void mk_rm_const(func_decl * f, expr_ref & result);
void mk_var(unsigned base_inx, sort * srt, expr_ref & result);
void mk_plus_inf(func_decl * f, expr_ref & result);
void mk_minus_inf(func_decl * f, expr_ref & result);

84
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -29,6 +29,8 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr_ref_vector m_out;
fpa2bv_converter & m_conv;
sort_ref_vector m_bindings;
expr_ref_vector m_mappings;
unsigned long long m_max_memory;
unsigned m_max_steps;
@ -38,7 +40,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
m_manager(m),
m_out(m),
m_conv(c) {
m_conv(c),
m_bindings(m),
m_mappings(m) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
@ -53,6 +57,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
m_out.finalize();
}
void reset() {
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
@ -140,17 +147,88 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
return BR_FAILED;
}
bool pre_visit(expr * t)
{
if (is_quantifier(t)) {
quantifier * q = to_quantifier(t);
TRACE("fpa2bv", tout << "pre_visit [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
sort_ref_vector new_bindings(m_manager);
for (unsigned i = 0 ; i < q->get_num_decls(); i++)
new_bindings.push_back(q->get_decl_sort(i));
SASSERT(new_bindings.size() == q->get_num_decls());
m_bindings.append(new_bindings);
m_mappings.resize(m_bindings.size(), 0);
}
return true;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
return false;
unsigned curr_sz = m_bindings.size();
SASSERT(old_q->get_num_decls() <= curr_sz);
unsigned num_decls = old_q->get_num_decls();
unsigned old_sz = curr_sz - num_decls;
string_buffer<> name_buffer;
ptr_buffer<sort> new_decl_sorts;
sbuffer<symbol> new_decl_names;
for (unsigned i = 0; i < num_decls; i++) {
symbol const & n = old_q->get_decl_name(i);
sort * s = old_q->get_decl_sort(i);
if (m_conv.is_float(s)) {
unsigned ebits = m_conv.fu().get_ebits(s);
unsigned sbits = m_conv.fu().get_sbits(s);
name_buffer.reset();
name_buffer << n << ".exp";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(ebits));
name_buffer.reset();
name_buffer << n << ".sig";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits-1));
name_buffer.reset();
name_buffer << n << ".sgn";
new_decl_names.push_back(symbol(name_buffer.c_str()));
new_decl_sorts.push_back(m_conv.bu().mk_sort(1));
}
else {
new_decl_sorts.push_back(s);
new_decl_names.push_back(n);
}
}
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
m_bindings.shrink(old_sz);
m_mappings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
" new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
return false;
if (t->get_idx() >= m_bindings.size())
return false;
unsigned inx = m_bindings.size() - t->get_idx() - 1;
if (m_mappings[inx] == 0)
{
unsigned shift = 0;
for (unsigned i = m_bindings.size() - 1; i > inx; i--)
if (m_conv.is_float(m_bindings[i].get())) shift += 2;
expr_ref new_var(m());
m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var);
m_mappings[inx] = new_var;
}
result = m_mappings[inx].get();
result_pr = 0;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}
};