diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index 7cf8f32bd..dbe7d5232 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/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) {
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index 416275306..c4503349b 100644
--- a/src/ast/float_decl_plugin.h
+++ b/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
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index ad0709423..9678af216 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/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;
+}
\ No newline at end of file
diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h
index e4258895d..7c86a5bc3 100644
--- a/src/ast/rewriter/float_rewriter.h
+++ b/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
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index afcac48ac..9ec11d085 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/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) {
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index 77ff50e9b..21d5a2d23 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/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());
+ }
}
diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h
index 291120e92..1ee374941 100644
--- a/src/tactic/fpa/fpa2bv_converter.h
+++ b/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();
diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h
index 62c6f1a2d..91682c6e1 100644
--- a/src/tactic/fpa/fpa2bv_rewriter.h
+++ b/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;);
diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h
index 660565463..8ca2183c1 100644
--- a/src/tactic/fpa/qffpa_tactic.h
+++ b/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
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 4cf530b1e..7a274a830 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/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));
}