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

scripts/mk_util.py

@@ -638,7 +638,13 @@ def is_compiler(given, expected):
 def is_CXX_gpp():
     return is_compiler(CXX, 'g++')
 
+def is_clang_in_gpp_form(cc):
+    version_string = subprocess.check_output([cc, '--version'])
+    return version_string.find('clang') != -1
+
 def is_CXX_clangpp():
+    if is_compiler(CXX, 'g++'):
+        return is_clang_in_gpp_form(CXX)
     return is_compiler(CXX, 'clang++')
 
 def get_cpp_files(path):

src/api/api_interp.cpp

@@ -17,6 +17,7 @@ Revision History:
 --*/
 #include<iostream>
 #include<sstream>
+#include<vector>
 #include"z3.h"
 #include"api_log_macros.h"
 #include"api_context.h"

src/ast/ast.cpp

@@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort
 
 void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
     ast_manager& m = const_cast<ast_manager&>(*this);
+
     if (decl->is_associative()) {
         sort * expected = decl->get_domain(0);
         for (unsigned i = 0; i < num_args; i++) {
@@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const {
     if  (n->get_kind() != AST_APP) 
         return; // nothing else to check...
     app const * a = to_app(n);
-    check_sort(a->get_decl(), a->get_num_args(), a->get_args());
+    func_decl* d = a->get_decl();
+    check_sort(d, a->get_num_args(), a->get_args());
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_right_associative()) {
+        check_sorts_core(a->get_arg(1));
+    }
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_left_associative()) {
+        check_sorts_core(a->get_arg(0));
+    }
 }
 
 bool ast_manager::check_sorts(ast const * n) const {

src/ast/float_decl_plugin.cpp

@@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
     if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {
         s = to_sort(parameters[0].get_ast());
     }
+    else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) {
+        s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+    }
     else if (range != 0 && is_float_sort(range)) {
         s = range;
     }
@@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
         sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
         symbol name("asFloat");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
-    }    
+    }
+    else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
+        if (num_parameters != 2)
+            m_manager->raise_exception("invalid number of parameters to to_fp");
+        if (!parameters[0].is_int() || !parameters[1].is_int())
+            m_manager->raise_exception("invalid parameter type to to_fp");
+        int ebits = parameters[0].get_int();
+        int sbits = parameters[1].get_int();
+        
+        sort * fp = mk_float_sort(ebits, sbits);
+        symbol name("asFloat");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
     else {
         // .. Otherwise we only know how to convert rationals/reals. 
         if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) 
@@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter
     return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters));        
 }
 
+func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                          unsigned arity, sort * const * domain, sort * range) {
+    if (!m_bv_plugin)
+        m_manager->raise_exception("fp unsupported; use a logic with BV support");
+    if (arity != 3)
+        m_manager->raise_exception("invalid number of arguments to fp");    
+    if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
+        !is_sort_of(domain[1], m_bv_fid, BV_SORT) ||
+        !is_sort_of(domain[2], m_bv_fid, BV_SORT))
+        m_manager->raise_exception("sort mismtach");
+        
+    sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1);
+    symbol name("fp");
+    return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
+}
+
+func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                                 unsigned arity, sort * const * domain, sort * range) {
+    if (!m_bv_plugin)
+        m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support");
+    if (arity != 2)
+        m_manager->raise_exception("invalid number of arguments to to_fp_unsigned");
+    if (is_rm_sort(domain[0]))
+        m_manager->raise_exception("sort mismtach");
+    if (!is_sort_of(domain[1], m_bv_fid, BV_SORT))
+        m_manager->raise_exception("sort mismtach");
+
+    sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+    symbol name("to_fp_unsigned");
+    return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
+}
+
+func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
+func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
+func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    unsigned arity, sort * const * domain, sort * range) {
+    NOT_IMPLEMENTED_YET();
+}
+
 func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                             unsigned arity, sort * const * domain, sort * range) {
     switch (k) {
@@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
     case OP_TO_IEEE_BV:
         return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_FP:
+        return mk_from3bv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_FP_UNSIGNED:
+        return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_UBV:
+        return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_SBV:
+        return mk_to_sbv(k, num_parameters, parameters, arity, domain, range);
+    case OP_FLOAT_TO_REAL:
+        return mk_to_real(k, num_parameters, parameters, arity, domain, range);
     default:
         m_manager->raise_exception("unsupported floating point operator");
         return 0;
@@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     if (m_bv_plugin)
         op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
 
-    // We also support draft version 3
+    // These are the operators from the final draft of the SMT FloatingPoints standard
-    op_names.push_back(builtin_name("fp", OP_TO_FLOAT));
+    op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
+    op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
 
     op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
     op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
@@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
     op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
     op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
-    op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT));
+    op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));
 
     if (m_bv_plugin) {
-    // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT));
+        op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
-    // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT));
+        op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
-    // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT));
+        op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
-    // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV));
+        op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
-    // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV));
     }
-    
+        
-    op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT));
     // op_names.push_back(builtin_name("fp.toReal", ?));
 }
 
 void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
     sort_names.push_back(builtin_name("FP", FLOAT_SORT));
     sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
+
+    // In the SMT FPA final draft, FP is called FloatingPoint
+    sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
 }
 
 expr * float_decl_plugin::get_some_value(sort * s) {

src/ast/float_decl_plugin.h

@@ -72,6 +72,12 @@ enum float_op_kind {
 
     OP_TO_FLOAT,
     OP_TO_IEEE_BV,
+
+    OP_FLOAT_FP,
+    OP_FLOAT_TO_FP_UNSIGNED,
+    OP_FLOAT_TO_UBV,
+    OP_FLOAT_TO_SBV,
+    OP_FLOAT_TO_REAL,
     
     LAST_FLOAT_OP
 };
@@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin {
                             unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                               unsigned arity, sort * const * domain, sort * range);
-
+    func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                           unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                  unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                             unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                             unsigned arity, sort * const * domain, sort * range);
+    func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                              unsigned arity, sort * const * domain, sort * range);
+    
     virtual void set_manager(ast_manager * m, family_id id);
     unsigned mk_id(mpf const & v);
     void recycled_id(unsigned id);

src/ast/rewriter/float_rewriter.cpp

@@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
     case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
     case OP_TO_IEEE_BV:      SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
+    case OP_FLOAT_FP:        SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break;
+    case OP_FLOAT_TO_UBV:    SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break;
+    case OP_FLOAT_TO_SBV:    SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break;
+    case OP_FLOAT_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
     }
     return st;
 }
@@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
 br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
     return BR_FAILED;
 }
+
+br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+    bv_util bu(m());
+    rational r1, r2, r3;
+    unsigned bvs1, bvs2, bvs3;
+
+    if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) {        
+        SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator()));
+        SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator()));
+        SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator()));
+        scoped_mpf v(m_util.fm());
+        mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator());
+        m_util.fm().set(v, bvs2, bvs3 + 1,
+                        r1.is_one(),
+                        r3.to_mpq().numerator(),
+                        m_util.fm().unbias_exp(bvs2, biased_exp));
+        TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;);
+        result = m_util.mk_value(v);
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) {
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) {
+    return BR_FAILED;
+}

src/ast/rewriter/float_rewriter.h

@@ -73,6 +73,12 @@ public:
     br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
 
     br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
+
+    br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_to_real(expr * arg1, expr_ref & result);
 };
 
 #endif

src/interp/iz3hash.h

@@ -66,7 +66,7 @@ Revision History:
 namespace stl_ext {
   template <>
     class hash<std::string> {
-    stl_ext::hash<char *> H;
+    stl_ext::hash<const char *> H;
   public:
     size_t operator()(const std::string &s) const {
       return H(s.c_str());

src/interp/iz3mgr.cpp

@@ -172,7 +172,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
 
 
   std::vector<symbol> names;
-  std::vector<sort *> types;
+  std::vector<class sort *> types;
   std::vector<expr *>  bound_asts;
   unsigned num_bound = bvs.size();
 
@@ -485,7 +485,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
   get_farkas_coeffs(proof,rats);
   coeffs.resize(rats.size());
   for(unsigned i = 0; i < rats.size(); i++){
-    sort *is = m().mk_sort(m_arith_fid, INT_SORT);
+    class sort *is = m().mk_sort(m_arith_fid, INT_SORT);
     ast coeff = cook(m_arith_util.mk_numeral(rats[i],is));
     coeffs[i] = coeff;
   }

src/interp/iz3mgr.h

@@ -22,6 +22,7 @@ Revision History:
 
 
 #include <assert.h>
+#include <vector>
 #include "iz3hash.h"
 
 #include"well_sorted.h"

src/interp/iz3pp.cpp

@@ -58,20 +58,20 @@ namespace stl_ext {
 class free_func_visitor {
   ast_manager& m;
   func_decl_set m_funcs;
-  obj_hashtable<sort> m_sorts;
+  obj_hashtable<class sort> m_sorts;
 public:        
   free_func_visitor(ast_manager& m): m(m) {}
   void operator()(var * n)        { }
   void operator()(app * n)        { 
     m_funcs.insert(n->get_decl()); 
-    sort* s = m.get_sort(n);
+    class sort* s = m.get_sort(n);
     if (s->get_family_id() == null_family_id) {
       m_sorts.insert(s);
     }
   }
   void operator()(quantifier * n) { }
   func_decl_set& funcs() { return m_funcs; }
-  obj_hashtable<sort>& sorts() { return m_sorts; }
+  obj_hashtable<class sort>& sorts() { return m_sorts; }
 };
 
 class iz3pp_helper : public iz3mgr {
@@ -146,8 +146,8 @@ void iz3pp(ast_manager &m,
   func_decl_set &funcs = visitor.funcs();
   func_decl_set::iterator it  = funcs.begin(), end = funcs.end();
   
-  obj_hashtable<sort>& sorts = visitor.sorts();
+  obj_hashtable<class sort>& sorts = visitor.sorts();
-  obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
+  obj_hashtable<class sort>::iterator sit = sorts.begin(), send = sorts.end();
   
 
   

src/interp/iz3scopes.cpp

@@ -19,6 +19,8 @@ Revision History:
 
 #include <assert.h>
 
+#include <algorithm>
+
 #include "iz3scopes.h"
 
 

src/muz/transforms/dl_mk_rule_inliner.cpp

@@ -527,6 +527,9 @@ namespace datalog {
 
 
     bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) {
+        if (r->has_negation()) {
+            return false;
+        }
 
         SASSERT(rules.is_closed());
         const rule_stratifier& strat = rules.get_stratifier();

src/smt/smt_conflict_resolution.cpp

@@ -759,7 +759,8 @@ namespace smt {
         app * fact     = to_app(m_manager.get_fact(pr));
         app * n1_owner = n1->get_owner();
         app * n2_owner = n2->get_owner();
-        if (fact->get_num_args() != 2 || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) {
+        bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact);
+        if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) {
             CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2),
                    tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n";
                    if (fact->get_num_args() == 2) {

src/smt/theory_arith_aux.h

@@ -476,10 +476,10 @@ namespace smt {
         typename vector<row_entry>::const_iterator it  = r.begin_entries();
         typename vector<row_entry>::const_iterator end = r.end_entries();
         for (; it != end; ++it) {                                                                 
-            if (!it->is_dead() && !it->m_coeff.is_int()) {
+            if (!it->is_dead() && !it->m_coeff.is_int()) 
                 TRACE("gomory_cut", display_row(tout, r, true););
                 return false;
-            }
+            
         }
         return true;
     }

src/tactic/arith/lia2pb_tactic.cpp

@@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic {
             if (m_bm.has_lower(n, l, s) &&
                 m_bm.has_upper(n, u, s) &&  
                 l.is_zero() &&
+                !u.is_neg() && 
                 u.get_num_bits() <= m_max_bits) {
                 
                 return true;

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1836,6 +1836,21 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         // Just keep it here, as there will be something else that uses it.
         mk_triple(args[0], args[1], args[2], result);
     }
+    else if (num == 1 && m_bv_util.is_bv(args[0])) {
+        sort * s = f->get_range();
+        unsigned to_sbits = m_util.get_sbits(s);
+        unsigned to_ebits = m_util.get_ebits(s);
+
+        expr * bv = args[0];
+        int sz = m_bv_util.get_bv_size(bv);
+        SASSERT((unsigned)sz == to_sbits + to_ebits);
+
+        m_bv_util.mk_extract(sz - 1, sz - 1, bv);
+        mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
+                  m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
+                  m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
+                  result);
+    }
     else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {        
         // We also support float to float conversion
         sort * s = f->get_range();
@@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
 }
 
+void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 3);
+    mk_triple(args[0], args[2], args[1], result);
+}
+
+void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
+void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    NOT_IMPLEMENTED_YET();
+}
+
 void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const {
     SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
     SASSERT(to_app(e)->get_num_args() == 3);

src/tactic/fpa/fpa2bv_converter.h

@@ -122,7 +122,13 @@ public:
     void mk_is_subnormal(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);
+
+    void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_to_real(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; }

src/tactic/fpa/fpa2bv_rewriter.h

@@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
             case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
             case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
             default:
                 TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);

src/tactic/fpa/qffpa_tactic.cpp

@@ -36,3 +36,77 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
                     mk_sat_tactic(m, p),
                     mk_fail_if_undecided_tactic());
 }
+
+struct is_non_qffpa_predicate {
+    struct found {};
+    ast_manager & m;
+    float_util    u;
+
+    is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        sort * s = get_sort(n);
+        if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s)))
+            throw found();
+        family_id fid = s->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == u.get_family_id())
+            return;
+
+        throw found();
+    }
+};
+
+struct is_non_qffpabv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       bu;
+    float_util    fu;
+
+    is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        sort * s = get_sort(n);
+        if (!m.is_bool(s) && !(fu.is_float(s) || fu.is_rm(s) || bu.is_bv_sort(s)))
+            throw found();
+        family_id fid = s->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == fu.get_family_id() || fid == bu.get_family_id())
+            return;
+
+        throw found();
+    }
+};
+
+class is_qffpa_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qffpa_predicate>(g);
+    }
+};
+
+class is_qffpabv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qffpabv_predicate>(g);
+    }
+};
+
+probe * mk_is_qffpa_probe() {
+    return alloc(is_qffpa_probe);
+}
+
+probe * mk_is_qffpabv_probe() {
+    return alloc(is_qffpabv_probe);
+}
+    

src/tactic/fpa/qffpa_tactic.h

@@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref());
   ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)")
 */
 
+probe * mk_is_qffpa_probe();
+probe * mk_is_qffpabv_probe();
+/*
+  ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()")
+  ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()")
+*/
+
 #endif

src/tactic/portfolio/default_tactic.cpp

@@ -27,6 +27,7 @@ Notes:
 #include"nra_tactic.h"
 #include"probe_arith.h"
 #include"quant_tactics.h"
+#include"qffpa_tactic.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
@@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                         cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
                                         cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
-                                             mk_smt_tactic())))))))),
+                                        cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p),
+                                             mk_smt_tactic()))))))))),
                                p);
     return st;
 }

src/util/hwf.cpp

@@ -49,8 +49,11 @@ Revision History:
 // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
 // the x87 FPU, even when /arch:SSE2 is on. 
 // Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
+#ifdef __clang__
+#undef USE_INTRINSICS
+#else
 #include <emmintrin.h>
-
+#endif
 
 hwf_manager::hwf_manager() :
     m_mpz_manager(m_mpq_manager)

src/util/mpf.cpp

@@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
     return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
 }
 
+mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
+    return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
+}
+
 void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) {
     o.sbits = sbits;
     o.ebits = ebits;

src/util/mpf.h

@@ -182,6 +182,8 @@ public:
     mpf_exp_t mk_max_exp(unsigned ebits);
     mpf_exp_t mk_min_exp(unsigned ebits);
 
+    mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
+
     /**
        \brief Return the biggest k s.t. 2^k <= a.
        

src/util/rational.h

@@ -104,7 +104,7 @@ public:
     }
 
     bool is_int32() const {
-        if (is_small()) return true; 
+        if (is_small() && is_int()) return true; 
         // we don't assume that if it is small, then it is int32.
         if (!is_int64()) return false;
         int64 v = get_int64();