mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

more fpa

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-30 19:06:07 -07:00
parent 6708a764f5
commit 4cb07a539b
6 changed files with 91 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -4297,7 +4297,7 @@ app_ref fpa2bv_converter_wrapped::wrap(expr* e) {
if (is_rm(es))
bv_srt = m_bv_util.mk_sort(3);
else {
SASSERT(m_converter.is_float(es));
SASSERT(is_float(es));
unsigned ebits = m_util.get_ebits(es);
unsigned sbits = m_util.get_sbits(es);
bv_srt = m_bv_util.mk_sort(ebits + sbits);

2
src/ast/fpa/fpa2bv_converter.h
View file

@ -44,6 +44,7 @@ protected:
arith_util m_arith_util;
datatype_util m_dt_util;
seq_util m_seq_util;
fpa_util m_util;
mpf_manager & m_mpf_manager;
unsynch_mpz_manager & m_mpz_manager;
fpa_decl_plugin * m_plugin;
@ -58,7 +59,6 @@ protected:
friend class bv2fpa_converter;
public:
fpa_util m_util;
fpa2bv_converter(ast_manager & m);
~fpa2bv_converter();

24
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -273,18 +273,18 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
template class rewriter_tpl<fpa2bv_rewriter_cfg>;
expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) {
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m) << std::endl;);
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, m_cfg.m()) << std::endl;);
expr_ref res(m_cfg.m());
proof_ref pr(m_cfg.m());
(*this)(e, res);
rw(res, res);
SASSERT(is_app(res));
SASSERT(m.is_bool(res));
SASSERT(m_cfg.m().is_bool(res));
return res;
}
expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
SASSERT(m_fpa_util.is_rm(e) || m_fpa_util.is_float(e));
SASSERT(fu().is_rm(e) || fu().is_float(e));
ast_manager& m = m_cfg.m();
expr_ref e_conv(m), res(m);
@ -295,20 +295,20 @@ expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;);
if (m_cfg.m_conv.m_util.is_rm(e)) {
SASSERT(m_cfg.m_conv.m_util.is_bv2rm(e_conv));
if (fu().is_rm(e)) {
SASSERT(fu().is_bv2rm(e_conv));
expr_ref bv_rm(m);
rw(to_app(e_conv)->get_arg(0), bv_rm);
res = m_cfg.m_conv.m_util.mk_bv2rm(bv_rm);
res = fu().mk_bv2rm(bv_rm);
}
else if (m_cfg.m_conv.m_util.is_float(e)) {
SASSERT(m_cfg.m_conv.m_util.is_fp(e_conv));
else if (fu().is_float(e)) {
SASSERT(fu().is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_cfg.m_conv.split_fp(e_conv, sgn, exp, sig);
rw(sgn);
rw(exp);
rw(sig);
res = m_cfg.m_conv.m_util.mk_fp(sgn, exp, sig);
res = fu().mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
@ -317,7 +317,7 @@ expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) {
}
expr_ref fpa2bv_rewriter::convert_conversion_term(th_rewriter& rw, expr * e) {
SASSERT(to_app(e)->get_family_id() == m_cfg.m_conv.m_util.get_family_id());
SASSERT(to_app(e)->get_family_id() == fu().get_family_id());
/* This is for the conversion functions fp.to_* */
expr_ref res(m_cfg.m());
(*this)(e, res);
@ -330,11 +330,11 @@ expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) {
expr_ref res(m);
TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;);
if (m_cfg.m_conv.m_util.is_fp(e))
if (fu().is_fp(e))
res = e;
else if (m.is_bool(e))
res = convert_atom(rw, e);
else if (m_cfg.m_conv.m_util.is_float(e) || m_cfg.m_conv.m_util.is_rm(e))
else if (fu().is_float(e) || fu().is_rm(e))
res = convert_term(rw, e);
else
res = convert_conversion_term(rw, e);

2
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -79,5 +79,7 @@ struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
expr_ref convert_term(th_rewriter& rw, expr * e);
expr_ref convert_conversion_term(th_rewriter& rw, expr * e);
expr_ref convert(th_rewriter& rw, expr * e);
fpa_util& fu() { return m_cfg.m_conv.fu(); }
};

74
src/model/fpa_factory.h Normal file
View file

@ -0,0 +1,74 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
fpa_factory.h
Abstract:
Floating-Point Theory Plugin
Author:
Christoph (cwinter) 2014-04-23
--*/
#pragma once
#include "ast/seq_decl_plugin.h"
#include "model/model_core.h"
#include "model/value_factory.h"
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) {}
~fpa_value_factory() override {}
expr * get_some_value(sort * s) override {
mpf_manager & mpfm = m_util.fm();
if (m_util.is_rm(s))
return m_util.mk_round_toward_zero();
else {
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
return m_util.mk_value(q);
}
}
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
mpf_manager & mpfm = m_util.fm();
if (m_util.is_rm(s))
v1 = v2 = m_util.mk_round_toward_zero();
else {
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;
}
expr * get_fresh_value(sort * s) override { return get_some_value(s); }
void register_value(expr * n) override { /* Ignore */ }
app * mk_value(mpf const & x) {
return m_util.mk_value(x);
}
};

55
src/smt/theory_fpa.h
View file

@ -23,64 +23,11 @@ Revision History:
#include "ast/fpa/fpa2bv_converter.h"
#include "ast/fpa/fpa2bv_rewriter.h"
#include "ast/rewriter/th_rewriter.h"
#include "model/value_factory.h"
#include "model/fpa_factory.h"
#include "smt/smt_model_generator.h"
namespace smt {
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) {}
~fpa_value_factory() override {}
expr * get_some_value(sort * s) override {
mpf_manager & mpfm = m_util.fm();
if (m_util.is_rm(s))
return m_util.mk_round_toward_zero();
else
{
scoped_mpf q(mpfm);
mpfm.set(q, m_util.get_ebits(s), m_util.get_sbits(s), 0);
return m_util.mk_value(q);
}
}
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
mpf_manager & mpfm = m_util.fm();
if (m_util.is_rm(s))
v1 = v2 = m_util.mk_round_toward_zero();
else
{
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;
}
expr * get_fresh_value(sort * s) override { return get_some_value(s); }
void register_value(expr * n) override { /* 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;