From 4cb07a539ba2c4b2446947ac087b36c339c07a7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Sep 2020 19:06:07 -0700 Subject: [PATCH] more fpa --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- src/ast/fpa/fpa2bv_converter.h | 2 +- src/ast/fpa/fpa2bv_rewriter.cpp | 24 +++++------ src/ast/fpa/fpa2bv_rewriter.h | 2 + src/model/fpa_factory.h | 74 ++++++++++++++++++++++++++++++++ src/smt/theory_fpa.h | 55 +----------------------- 6 files changed, 91 insertions(+), 68 deletions(-) create mode 100644 src/model/fpa_factory.h diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 968f5dd9a..89023c8f5 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -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); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 1c48fa7cb..67e1834a8 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -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(); diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index d53d31ce0..d4d61c5e1 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -273,18 +273,18 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res template class rewriter_tpl; 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); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 2f1db4c37..42467c219 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -79,5 +79,7 @@ struct fpa2bv_rewriter : public rewriter_tpl { 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(); } }; diff --git a/src/model/fpa_factory.h b/src/model/fpa_factory.h new file mode 100644 index 000000000..5930cb575 --- /dev/null +++ b/src/model/fpa_factory.h @@ -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); + } +}; + + diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index f5ce63e70..59ce39e5c 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -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 th_trail_stack;