Added QF_FPABV logic, default tactic, and the asIEEEBV conversion function.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/ast/float_decl_plugin.cpp

@@ -348,13 +348,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
         // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float!        
         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));    
+        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())) 
             m_manager->raise_exception("expecting two integer parameters to asFloat");        
-		if (arity != 2 && arity != 3)
+        if (arity != 2 && arity != 3)
 			m_manager->raise_exception("invalid number of arguments to asFloat operator");
 		if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort)
             m_manager->raise_exception("sort mismatch");
@@ -373,6 +373,23 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
     }
 }
 
+func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                             unsigned arity, sort * const * domain, sort * range) {
+    if (!m_bv_plugin)
+        m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support");
+    if (arity != 1)
+        m_manager->raise_exception("invalid number of arguments to asIEEEBV");
+    if (!is_float_sort(domain[0]))
+        m_manager->raise_exception("sort mismatch");
+
+    // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector.
+    unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
+    parameter ps[] = { parameter(float_sz) };
+    sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
+    symbol name("asIEEEBV");
+    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_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                             unsigned arity, sort * const * domain, sort * range) {
     switch (k) {
@@ -420,6 +437,8 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_FUSED_MA:
         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);
     default:
         m_manager->raise_exception("unsupported floating point operator");
         return 0;
@@ -462,7 +481,10 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
     op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
 
-    op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));    
+    op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
+
+    if (m_bv_plugin)
+        op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
 }
 
 void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/float_decl_plugin.h

@@ -67,6 +67,7 @@ enum float_op_kind {
     OP_FLOAT_IS_SIGN_MINUS,
 
     OP_TO_FLOAT,
+    OP_TO_IEEE_BV,
     
     LAST_FLOAT_OP
 };
@@ -118,6 +119,8 @@ class float_decl_plugin : public decl_plugin {
                             unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters,
                             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);
 
     virtual void set_manager(ast_manager * m, family_id id);
     unsigned mk_id(mpf const & v);
@@ -159,7 +162,7 @@ class float_util {
     ast_manager &       m_manager;
     float_decl_plugin * m_plugin;
     family_id           m_fid;
-    arith_util          m_a_util;
+    arith_util          m_a_util;    
 public:
     float_util(ast_manager & m);
     ~float_util();
@@ -209,7 +212,7 @@ public:
 
     bool is_to_float(expr * n) { return is_app_of(n, m_fid, OP_TO_FLOAT); }
 
-    app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); }
+    app * mk_to_float(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_TO_FLOAT, arg1, arg2); }    
     app * mk_add(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_ADD, arg1, arg2, arg3); }
     app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
     app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
@@ -238,6 +241,8 @@ public:
     app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }
 
     bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); }
+    
+    app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); }
 };
 
 #endif

src/ast/rewriter/float_rewriter.cpp

@@ -59,6 +59,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_FLOAT_IS_NZERO:  SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
     case OP_FLOAT_IS_PZERO:  SASSERT(num_args == 1); st = mk_is_pzero(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;
     }
     return st;
 }
@@ -439,3 +440,7 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
 
     return BR_FAILED;
 }
+
+br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) {
+    return BR_FAILED;
+}

src/ast/rewriter/float_rewriter.h

@@ -67,6 +67,8 @@ public:
     br_status mk_is_nzero(expr * arg1, expr_ref & result);
     br_status mk_is_pzero(expr * arg1, expr_ref & result);
     br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
+
+    br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
 };
 
 #endif

src/cmd_context/cmd_context.cpp

@@ -460,6 +460,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "LIA" ||        
         s == "LRA" || 
         s == "QF_FPA" ||
+        s == "QF_FPABV" ||
         s == "HORN";
 }
 
@@ -478,6 +479,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
         s == "QF_ABV" ||
         s == "QF_AUFBV" ||
         s == "QF_BVRE" ||
+        s == "QF_FPABV" ||
         s == "HORN";
 }
 
@@ -502,7 +504,7 @@ bool cmd_context::logic_has_seq() const {
 }
 
 bool cmd_context::logic_has_floats() const {
-    return !has_logic() || m_logic == "QF_FPA";
+    return !has_logic() || m_logic == "QF_FPA" || m_logic == "QF_FPABV";
 }
 
 bool cmd_context::logic_has_array_core(symbol const & s) const {
@@ -599,7 +601,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
         logic_has_arith_core(s) || logic_has_bv_core(s) || 
         logic_has_array_core(s) || logic_has_seq_core(s) ||
         logic_has_horn(s) ||
-        s == "QF_FPA";
+        s == "QF_FPA" || s == "QF_FPABV";
 }
 
 void cmd_context::set_logic(symbol const & s) {

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1399,6 +1399,13 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
     }
 }
 
+void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    expr * sgn, * s, * e;
+    split(args[0], sgn, s, e);    
+    result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, s), e);
+}
+
 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);
@@ -2035,7 +2042,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
             tout << bv_mdl->get_constant(i)->get_name() << " --> " << 
                 mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
         );
-
+    
+    obj_hashtable<func_decl> seen;
 
     for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
          it != m_const2bv.end();
@@ -2053,6 +2061,10 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         expr * sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
         expr * exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
 
+        seen.insert(to_app(a->get_arg(0))->get_decl());
+        seen.insert(to_app(a->get_arg(1))->get_decl());
+        seen.insert(to_app(a->get_arg(2))->get_decl());
+
         if (!sgn && !sig && !exp)
             continue;
         
@@ -2080,7 +2092,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
 
         float_mdl->register_decl(var, fu.mk_value(fp_val));
-
+        
         mpzm.del(sig_z);
     }
 
@@ -2104,9 +2116,36 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 			case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
 			case BV_RM_TO_ZERO: 
 			default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
-			}				
+			}
+            seen.insert(var);
 		}		
 	}
 
     fu.fm().del(fp_val);
+
+    // Keep all the non-float constants.
+    unsigned sz = bv_mdl->get_num_constants();
+    for (unsigned i = 0; i < sz; i++)
+    {
+        func_decl * c = bv_mdl->get_constant(i);
+        if (seen.contains(c))
+            continue;
+        float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
+    }
+
+    // And keep everything else
+    sz = bv_mdl->get_num_functions();
+    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));
+    }
+
+    sz = bv_mdl->get_num_uninterpreted_sorts();
+    for (unsigned i = 0; i < sz; i++)
+    {
+        sort * s = bv_mdl->get_uninterpreted_sort(i);
+        ptr_vector<expr> u = bv_mdl->get_universe(s);
+        float_mdl->register_usort(s, u.size(), u.c_ptr());
+    }
 }

src/tactic/fpa/fpa2bv_converter.h

@@ -100,6 +100,7 @@ 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);
 
     fpa2bv_model_converter * mk_model_converter();
 

src/tactic/fpa/fpa2bv_rewriter.h

@@ -129,6 +129,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
             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;
             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.h

@@ -27,6 +27,7 @@ class tactic;
 tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref());
 /*
   ADD_TACTIC("qffpa", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffpa_tactic(m, p)")
+  ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)")
 */
 
 #endif

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -79,6 +79,7 @@ static void init(strategic_solver * s) {
     s->set_tactic_for(symbol("UFBV"),      alloc(ufbv_fct));
     s->set_tactic_for(symbol("BV"),        alloc(ufbv_fct));        
     s->set_tactic_for(symbol("QF_FPA"),    alloc(qffpa_fct));
+    s->set_tactic_for(symbol("QF_FPABV"),    alloc(qffpa_fct));
     s->set_tactic_for(symbol("HORN"),      alloc(horn_fct));
 }