Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/smt/diff_logic.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include"vector.h"
 #include"heap.h"
+#include"statistics.h"
 #include"trace.h"
 #include"warning.h"
 

src/tactic/fpa/fpa2bv_converter.cpp

@@ -38,6 +38,17 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
 fpa2bv_converter::~fpa2bv_converter() {
     dec_ref_map_key_values(m, m_const2bv);
     dec_ref_map_key_values(m, m_rm_const2bv);
+    dec_ref_map_key_values(m, m_uf2bvuf);
+    
+    obj_map<func_decl, func_decl_triple>::iterator it  = m_uf23bvuf.begin();
+    obj_map<func_decl, func_decl_triple>::iterator end = m_uf23bvuf.end();
+    for (; it != end; ++it) {
+        m.dec_ref(it->m_key);
+        m.dec_ref(it->m_value.f_sgn);
+        m.dec_ref(it->m_value.f_sig);
+        m.dec_ref(it->m_value.f_exp);
+    }
+    m_uf23bvuf.reset();
 }
 
 void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
@@ -150,6 +161,104 @@ 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_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result)
+{
+    TRACE("fpa2bv_dbg", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; );
+    SASSERT(f->get_arity() == num);
+
+    expr_ref_buffer new_args(m);
+
+    for (unsigned i = 0; i < num ; i ++)
+    if (is_float(args[i]))
+    {
+        expr * sgn, * sig, * exp;
+        split(args[i], sgn, sig, exp);
+        new_args.push_back(sgn);
+        new_args.push_back(sig);
+        new_args.push_back(exp);
+    }
+    else
+        new_args.push_back(args[i]);
+
+    func_decl * fd;    
+    func_decl_triple fd3;
+    if (m_uf2bvuf.find(f, fd)) {
+        result = m.mk_app(fd, new_args.size(), new_args.c_ptr());
+    }
+    else if (m_uf23bvuf.find(f, fd3))
+    {
+        expr_ref a_sgn(m), a_sig(m), a_exp(m);
+        a_sgn = m.mk_app(fd3.f_sgn, new_args.size(), new_args.c_ptr());
+        a_sig = m.mk_app(fd3.f_sig, new_args.size(), new_args.c_ptr());
+        a_exp = m.mk_app(fd3.f_exp, new_args.size(), new_args.c_ptr());            
+        mk_triple(a_sgn, a_sig, a_exp, result);
+    }
+    else {
+        sort_ref_buffer new_domain(m);
+    
+        for (unsigned i = 0; i < f->get_arity() ; i ++)
+            if (is_float(f->get_domain()[i]))
+            {
+                new_domain.push_back(m_bv_util.mk_sort(1));            
+                new_domain.push_back(m_bv_util.mk_sort(m_util.get_sbits(f->get_domain()[i])-1));
+                new_domain.push_back(m_bv_util.mk_sort(m_util.get_ebits(f->get_domain()[i])));                                
+            }
+            else
+                new_domain.push_back(f->get_domain()[i]);
+
+        if (!is_float(f->get_range()))
+        {
+            func_decl * fbv = m.mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), f->get_range(), *f->get_info());
+            TRACE("fpa2bv_dbg", tout << "New UF func_decl : " << mk_ismt2_pp(fbv, m) << std::endl; );
+            m_uf2bvuf.insert(f, fbv);
+            m.inc_ref(f);
+            m.inc_ref(fbv);
+            result = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
+        }
+        else
+        {
+            string_buffer<> name_buffer;
+            name_buffer.reset(); name_buffer << f->get_name() << ".sgn";        
+            func_decl * f_sgn = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(1));
+            name_buffer.reset(); name_buffer << f->get_name() << ".sig";
+            func_decl * f_sig = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_sbits(f->get_range())-1));
+            name_buffer.reset(); name_buffer << f->get_name() << ".exp";
+            func_decl * f_exp = m.mk_func_decl(symbol(name_buffer.c_str()), new_domain.size(), new_domain.c_ptr(), m_bv_util.mk_sort(m_util.get_ebits(f->get_range())));
+            expr_ref a_sgn(m), a_sig(m), a_exp(m);
+            a_sgn = m.mk_app(f_sgn, new_args.size(), new_args.c_ptr());
+            a_sig = m.mk_app(f_sig, new_args.size(), new_args.c_ptr());
+            a_exp = m.mk_app(f_exp, new_args.size(), new_args.c_ptr());            
+            TRACE("fpa2bv_dbg", tout << "New UF func_decls : " << std::endl;
+                                tout << mk_ismt2_pp(f_sgn, m) << std::endl;
+                                tout << mk_ismt2_pp(f_sig, m) << std::endl;
+                                tout << mk_ismt2_pp(f_exp, m) << std::endl; );
+            m_uf23bvuf.insert(f, func_decl_triple(f_sgn, f_sig, f_exp));
+            m.inc_ref(f);
+            m.inc_ref(f_sgn);
+            m.inc_ref(f_sig);
+            m.inc_ref(f_exp);
+            mk_triple(a_sgn, a_sig, a_exp, result);
+        }               
+    }    
+
+    TRACE("fpa2bv_dbg", tout << "UF result: " << mk_ismt2_pp(result, m) << std::endl; );
+
+    SASSERT(is_well_sorted(m, result));
+}
 
 void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
     SASSERT(f->get_family_id() == null_family_id);
@@ -1939,7 +2048,8 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {    
     #ifdef _DEBUG
-    // return;
+    return;
+    // CMW: This works only for quantifier-free formulas.
     expr_ref new_e(m);
     new_e = m.mk_fresh_const(prefix, m.get_sort(e));
     extra_assertions.push_back(m.mk_eq(new_e, e));    
@@ -2293,6 +2403,25 @@ void fpa2bv_model_converter::display(std::ostream & out) {
              unsigned indent = n.size() + 4;
              out << mk_ismt2_pp(it->m_value, m, indent) << ")";
     }
+    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
+         it != m_uf2bvuf.end();
+         it++) {
+             const symbol & n = it->m_key->get_name();
+             out << "\n  (" << n << " ";
+             unsigned indent = n.size() + 4;
+             out << mk_ismt2_pp(it->m_value, m, indent) << ")";
+    }
+    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
+         it != m_uf23bvuf.end();
+         it++) {
+             const symbol & n = it->m_key->get_name();
+             out << "\n  (" << n << " ";
+             unsigned indent = n.size() + 4;
+             out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " << 
+             mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " << 
+             mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
+             ")";
+    }
     out << ")" << std::endl;
 }
 
@@ -2413,6 +2542,20 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         }        
     }
 
+    for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
+         it != m_uf2bvuf.end();
+         it++) 
+        seen.insert(it->m_value);
+
+    for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
+         it != m_uf23bvuf.end();
+         it++) 
+    {
+        seen.insert(it->m_value.f_sgn);
+        seen.insert(it->m_value.f_sig);
+        seen.insert(it->m_value.f_exp);
+    }
+
     fu.fm().del(fp_val);
 
     // Keep all the non-float constants.
@@ -2420,7 +2563,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     for (unsigned i = 0; i < sz; i++)
     {
         func_decl * c = bv_mdl->get_constant(i);
-        if (!seen.contains(c))            
+        if (!seen.contains(c))
             float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
     }
 
@@ -2429,7 +2572,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     for (unsigned i = 0; i < sz; i++)
     {
         func_decl * c = bv_mdl->get_function(i);
-        float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
+        if (!seen.contains(c))
+            float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
     }
 
     sz = bv_mdl->get_num_uninterpreted_sorts();
@@ -2443,6 +2587,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 
 model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
                                             obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv) {
-    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv);
+                                            obj_map<func_decl, expr*> const & rm_const2bv,
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
+                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
+    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
 }

src/tactic/fpa/fpa2bv_converter.h

@@ -31,23 +31,39 @@ typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2,
 
 class fpa2bv_model_converter;
 
+struct func_decl_triple {
+        func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
+        func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
+        {
+            f_sgn = sgn;
+            f_sig = sig;
+            f_exp = exp;
+        }
+        func_decl * f_sgn;
+        func_decl * f_sig;        
+        func_decl * f_exp;        
+    };
+
 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;
 
     obj_map<func_decl, expr*>  m_const2bv;
     obj_map<func_decl, expr*>  m_rm_const2bv;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;        
+    obj_map<func_decl, func_decl_triple>  m_uf23bvuf;
     
 public:
     fpa2bv_converter(ast_manager & m);    
     ~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()); }
@@ -66,8 +82,10 @@ public:
 
     void mk_rounding_mode(func_decl * f, expr_ref & result);
     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_const(func_decl * f, expr_ref & result);    
     void mk_rm_const(func_decl * f, expr_ref & result);
+    void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, 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);
@@ -100,10 +118,12 @@ public:
     void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
     void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);    
 
     obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
     obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
+    obj_map<func_decl, func_decl*> const & uf2bvuf() const { return m_uf2bvuf; }
+    obj_map<func_decl, func_decl_triple> const & uf23bvuf() const { return m_uf23bvuf; }
 
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector extra_assertions;
@@ -148,10 +168,14 @@ class fpa2bv_model_converter : public model_converter {
     ast_manager               & m;
     obj_map<func_decl, expr*>   m_const2bv;
     obj_map<func_decl, expr*>   m_rm_const2bv;
+    obj_map<func_decl, func_decl*>  m_uf2bvuf;        
+    obj_map<func_decl, func_decl_triple>  m_uf23bvuf;
 
 public:
     fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv) : 
+                                            obj_map<func_decl, expr*> const & rm_const2bv,
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
+                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf) : 
       m(m) {
           // Just create a copy?
           for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
@@ -170,6 +194,21 @@ public:
                m.inc_ref(it->m_key);
                m.inc_ref(it->m_value);
           }
+          for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
+               it != uf2bvuf.end();
+               it++) 
+          {
+               m_uf2bvuf.insert(it->m_key, it->m_value);
+               m.inc_ref(it->m_key);
+               m.inc_ref(it->m_value);
+          }
+          for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
+               it != uf23bvuf.end();
+               it++) 
+          {
+               m_uf23bvuf.insert(it->m_key, it->m_value);
+               m.inc_ref(it->m_key);               
+          }
       }
 
     virtual ~fpa2bv_model_converter() {
@@ -202,6 +241,8 @@ protected:
 
 model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
                                             obj_map<func_decl, expr*> const & const2bv,
-                                            obj_map<func_decl, expr*> const & rm_const2bv);
+                                            obj_map<func_decl, expr*> const & rm_const2bv,
+                                            obj_map<func_decl, func_decl*> const & uf2bvuf,      
+                                            obj_map<func_decl, func_decl_triple> const & uf23bvuf);
 
 #endif

src/tactic/fpa/fpa2bv_rewriter.h

@@ -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);        
@@ -136,21 +143,112 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
                 throw tactic_exception("NYI");
             }
         }
+
+        if (f->get_family_id() == null_family_id)
+        {
+            bool is_float_uf = m_conv.is_float(f->get_range());
+            unsigned i = 0;
+            while (!is_float_uf && i < num)
+            {
+                is_float_uf = m_conv.is_float(f->get_domain()[i]);
+                i++;
+            }
+
+            if (is_float_uf)
+            {
+                m_conv.mk_uninterpreted_function(f, num, args, result);
+                return BR_DONE;
+            }
+        }
         
         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());
+            if (m_conv.is_float(t->get_sort()))
+                m_conv.mk_var(t->get_idx() + shift, t->get_sort(), new_var);
+            else
+                new_var = m().mk_var(t->get_idx() + shift, t->get_sort());
+            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;
     }
 };
 

src/tactic/fpa/fpa2bv_tactic.cpp

@@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic {
             }
 
             if (g->models_enabled())  
-                mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv());
+                mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.uf23bvuf());
 
             g->inc_depth();
             result.push_back(g.get());