From a94aff23e60fe985fc099d388918ad6f5fba25ff Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 Jun 2016 13:23:12 +0100 Subject: [PATCH 1/4] Added clearer FP conversion functions to the Python API. Implements #476 --- src/api/python/z3.py | 86 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 942201b0e..c9aa9beb5 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8994,6 +8994,92 @@ def fpToFP(a1, a2=None, a3=None, ctx=None): else: raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.") +def fpBVToFP(v, sort, ctx=None): + """Create a Z3 floating-point conversion expression that represents the + conversion from a bit-vector term to a floating-point term. + + >>> x_bv = BitVecVal(0x3F800000, 32) + >>> x_fp = fpBVToFP(x_bv, Float32()) + >>> x_fp + fpToFP(1065353216) + >>> simplify(x_fp) + 1 + """ + _z3_assert(is_bv(v), "First argument must be a Z3 floating-point rounding mode expression.") + _z3_assert(is_fp_sort(sort), "Second argument must be a Z3 floating-point sort.") + ctx = _get_ctx(ctx) + return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx) + +def fpFPToFP(rm, v, sort, ctx=None): + """Create a Z3 floating-point conversion expression that represents the + conversion from a floating-point term to a floating-point term of different precision. + + >>> x_sgl = FPVal(1.0, Float32()) + >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) + >>> x_dbl + fpToFP(RNE(), 1) + >>> simplify(x_dbl) + 1 + >>> x_dbl.sort() + FPSort(11, 53) + """ + _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") + _z3_assert(is_fp(v), "Second argument must be a Z3 floating-point expression.") + _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") + ctx = _get_ctx(ctx) + return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) + +def fpRealToFP(rm, v, sort, ctx=None): + """Create a Z3 floating-point conversion expression that represents the + conversion from a real term to a floating-point term. + + >>> x_r = RealVal(1.5) + >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) + >>> x_fp + fpToFP(RNE(), 3/2) + >>> simplify(x_fp) + 1.5 + """ + _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") + _z3_assert(is_real(v), "Second argument must be a Z3 expression or real sort.") + _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") + ctx = _get_ctx(ctx) + return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) + +def fpSignedToFP(rm, v, sort, ctx=None): + """Create a Z3 floating-point conversion expression that represents the + conversion from a signed bit-vector term (encoding an integer) to a floating-point term. + + >>> x_signed = BitVecVal(-5, BitVecSort(32)) + >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) + >>> x_fp + fpToFP(RNE(), 4294967291) + >>> simplify(x_fp) + -1.25*(2**2) + """ + _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") + _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") + _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") + ctx = _get_ctx(ctx) + return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) + +def fpUnsignedToFP(rm, v, sort, ctx=None): + """Create a Z3 floating-point conversion expression that represents the + conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. + + >>> x_signed = BitVecVal(-5, BitVecSort(32)) + >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) + >>> x_fp + fpToFPUnsigned(RNE(), 4294967291) + >>> simplify(x_fp) + 1*(2**32) + """ + _z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression.") + _z3_assert(is_bv(v), "Second argument must be a Z3 expression or real sort.") + _z3_assert(is_fp_sort(sort), "Third argument must be a Z3 floating-point sort.") + ctx = _get_ctx(ctx) + return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx) + def fpToFPUnsigned(rm, x, s, ctx=None): """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.""" if __debug__: From b54ef3623b796586af7f2915077946409d1734e3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 Jun 2016 20:26:05 +0100 Subject: [PATCH 2/4] added collect-statistics tactic --- src/tactic/core/collect_statistics_tactic.cpp | 173 ++++++++++++++++++ src/tactic/core/collect_statistics_tactic.h | 33 ++++ 2 files changed, 206 insertions(+) create mode 100644 src/tactic/core/collect_statistics_tactic.cpp create mode 100644 src/tactic/core/collect_statistics_tactic.h diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp new file mode 100644 index 000000000..f50195673 --- /dev/null +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -0,0 +1,173 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + collect_statistics_tactic.cpp + +Abstract: + + A tactic for collection of various statistics. + +Author: + + Mikolas Janota (mikjan) 2016-06-03 + Christoph (cwinter) 2016-06-03 + +Notes: + +--*/ +#include +#include + +#include"ast.h" +#include"params.h" +#include"arith_decl_plugin.h" +#include"array_decl_plugin.h" +#include"bv_decl_plugin.h" +#include"datatype_decl_plugin.h" +#include"fpa_decl_plugin.h" +#include"tactical.h" +#include"stats.h" + +#include"collect_statistics_tactic.h" + +class collect_statistics_tactic : public tactic { + ast_manager & m; + params_ref m_params; + basic_decl_plugin m_basic_pi; + arith_decl_plugin m_arith_pi; + array_decl_plugin m_array_pi; + bv_decl_plugin m_bv_pi; + datatype_decl_plugin m_datatype_pi; + fpa_decl_plugin m_fpa_pi; + + typedef std::unordered_map stats_type; + stats_type m_stats; + +public: + collect_statistics_tactic(ast_manager & m, params_ref const & p) : + m(m), + m_params(p) { + } + + virtual ~collect_statistics_tactic() {} + + virtual tactic * translate(ast_manager & m_) { + return alloc(collect_statistics_tactic, m_, m_params); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + } + + virtual void collect_param_descrs(param_descrs & r) {} + + virtual void operator()(goal_ref const & g, goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, + expr_dependency_ref & core) { + mc = 0; + tactic_report report("collect-statistics", *g); + + collect_proc cp(m, m_stats); + expr_mark visited; + const unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) + for_each_expr(cp, visited, g->form(i)); + + std::cout << "(" << std::endl; + stats_type::iterator it = m_stats.begin(); + stats_type::iterator end = m_stats.end(); + for (; it != end; it++) + std::cout << " :" << it->first << " " << it->second << std::endl; + std::cout << ")" << std::endl; + + g->inc_depth(); + result.push_back(g.get()); + } + + virtual void cleanup() {} + + virtual void collect_statistics(statistics & st) const { + } + + virtual void reset_statistics() { reset(); } + virtual void reset() { cleanup(); } + +protected: + class collect_proc { + public: + ast_manager & m; + stats_type & m_stats; + obj_hashtable m_seen_sorts; + obj_hashtable m_seen_func_decls; + + collect_proc(ast_manager & m, stats_type & s) : m(m), m_stats(s) {} + + void operator()(var * v) { + m_stats["bound-variables"]++; + this->operator()(v->get_sort()); + } + + void operator()(quantifier * q) { + m_stats["quantifiers"]++; + SASSERT(is_app(q->get_expr())); + app * body = to_app(q->get_expr()); + this->operator()(body); + } + + void operator()(app * n) { + m_stats["function-applications"]++; + this->operator()(n->get_decl()); + } + + void operator()(sort * s) { + if (m.is_uninterp(s)) { + if (!m_seen_sorts.contains(s)) { + m_stats["uninterpreted-sorts"]++; + m_seen_sorts.insert(s); + } + m_stats["uninterpreted-sort-occurrences"]++; + } + else { + params_ref prms; + prms.set_bool("pp.single_line", true); + std::stringstream ss; + ss << mk_ismt2_pp(s, m, prms); + m_stats[ss.str().c_str()]++; + } + } + + void operator()(func_decl * f) { + for (unsigned i = 0; i < f->get_arity(); i++) + this->operator()(f->get_domain()[i]); + this->operator()(f->get_range()); + + if (f->get_family_id() == null_family_id) { + if (!m_seen_func_decls.contains(f)) { + if (f->get_arity() == 0) + m_stats["uninterpreted-constants"]++; + else + m_stats["uninterpreted-functions"]++; + m_seen_func_decls.insert(f); + } + + if (f->get_arity() > 0) + m_stats["uninterpreted-function-occurrences"]++; + } + else { + params_ref prms; + prms.set_bool("pp.single_line", true); + std::stringstream ss; + ss << mk_ismt2_pp(f, m, prms); + m_stats[ss.str().c_str()]++; + } + m_stats["function-applications"]++; + } + }; +}; + + +tactic * mk_collect_statistics_tactic(ast_manager & m, params_ref const & p) { + return clean(alloc(collect_statistics_tactic, m, p)); +} diff --git a/src/tactic/core/collect_statistics_tactic.h b/src/tactic/core/collect_statistics_tactic.h new file mode 100644 index 000000000..5734af3c7 --- /dev/null +++ b/src/tactic/core/collect_statistics_tactic.h @@ -0,0 +1,33 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + collect_statistics_tactic.h + +Abstract: + + A tactic for collection of various statistics. + +Author: + + Mikolas Janota (mikjan) 2016-06-03 + Christoph (cwinter) 2016-06-03 + +Notes: + +--*/ +#ifndef COLLECT_STATISTICS_H_ +#define COLLECT_STATISTICS_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_collect_statistics_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("collect-statistics", "Collects various statistics.", "mk_collect_statistics_tactic(m, p)") +*/ + + +#endif From 626b9160bfb1e7032202b489ff9bb86a64b087e5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 3 Jun 2016 20:45:42 +0100 Subject: [PATCH 3/4] collect-statistics additions --- src/tactic/core/collect_statistics_tactic.cpp | 20 ++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index f50195673..99af8f773 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -133,8 +133,14 @@ protected: params_ref prms; prms.set_bool("pp.single_line", true); std::stringstream ss; - ss << mk_ismt2_pp(s, m, prms); - m_stats[ss.str().c_str()]++; + ss << "(declare-sort " << mk_ismt2_pp(s, m, prms) << ")"; + m_stats[ss.str()]++; + + if (s->get_info()->get_num_parameters() > 0) { + std::stringstream ssname; + ssname << "(declare-sort (_ " << s->get_name() << " *))"; + m_stats[ssname.str()]++; + } } } @@ -160,8 +166,16 @@ protected: prms.set_bool("pp.single_line", true); std::stringstream ss; ss << mk_ismt2_pp(f, m, prms); - m_stats[ss.str().c_str()]++; + m_stats[ss.str()]++; + + std::stringstream ssfname; + if (f->get_num_parameters() > 0) + ssfname << "(declare-fun (_ " << f->get_name() << " *) *)"; + else + ssfname << "(declare-fun " << f->get_name() << " *)"; + m_stats[ssfname.str()]++; } + m_stats["function-applications"]++; } }; From f2a869fb5807f01e007c8ac55a7076b72e6628db Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 4 Jun 2016 11:01:46 +0100 Subject: [PATCH 4/4] std::unordered_map -> std::map --- src/tactic/core/collect_statistics_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 99af8f773..8e8879fef 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -18,7 +18,7 @@ Notes: --*/ #include -#include +#include #include"ast.h" #include"params.h" @@ -42,7 +42,7 @@ class collect_statistics_tactic : public tactic { datatype_decl_plugin m_datatype_pi; fpa_decl_plugin m_fpa_pi; - typedef std::unordered_map stats_type; + typedef std::map stats_type; stats_type m_stats; public: