Merge branch 'master' of https://github.com/Z3Prover/z3

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__:

src/tactic/core/collect_statistics_tactic.cpp

@@ -0,0 +1,187 @@
+/*++
+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<string>
+#include<map>
+
+#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::map<std::string, unsigned long> 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<sort>      m_seen_sorts;
+        obj_hashtable<func_decl> 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 << "(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()]++;
+                }
+            }
+        }
+
+        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()]++;
+
+                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"]++;
+        }
+    };
+};
+
+
+tactic * mk_collect_statistics_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(collect_statistics_tactic, m, p));
+}

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