mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Minor additions and cleanup to the outdated code.

Browse source
This commit is contained in:
Aleksandar Zeljic 2015-06-12 18:35:32 +02:00
parent f45fcbe282
commit 421b3af8bd
2 changed files with 63 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/fpa/fpa2bv_approx_tactic.cpp
View file

@ -30,6 +30,7 @@
#include"fpa2bv_converter_prec.h"
#include"fpa2bv_model_converter.h"
#include"fpa2bv_converter.h"
#include"propagate_values_tactic.h"
#include"fpa2bv_rewriter_prec.h"
#include"fpa2bv_approx_tactic.h"
#include"const_intro_rewriter.h"
@ -402,6 +403,7 @@ class fpa2bv_approx_tactic: public tactic {
mpf_mngr.round_to_integral(rm,est_arg_val[1],est_rhs_value);
break;
}
default:
NOT_IMPLEMENTED_YET();
break;
@ -880,6 +882,8 @@ class fpa2bv_approx_tactic: public tactic {
SASSERT(g->is_well_sorted());
simplify(g);
//fpa2bv
fpa2bv_rewriter_prec fpa2bv_rw(*m_temp_manager, fpa2bv, m_params);
fpa2bv_rw.m_cfg.set_mappings(&const2prec_map);

87
src/tactic/fpa/fpa2bv_rewriter_prec.h
View file

@ -75,9 +75,7 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
return num_steps > m_max_steps;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
@ -93,14 +91,20 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
if (m_conv.is_float(args[0])) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
return BR_FAILED;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
//SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
sort * ds = f->get_domain()[0];
if (m_conv.is_float(ds)) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
else if (m_conv.is_rm(ds)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
@ -125,10 +129,9 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE;
case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE;
case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE;
case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
//AZ: Added precision, if precision is MAX_PRECISION uses the regular implementation of the methods
case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FPA_ADD:
m_conv.mk_add(f,get_precision(f), num, args, result);return BR_DONE;
case OP_FPA_SUB:
@ -141,14 +144,14 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
m_conv.mk_div(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_REM:
m_conv.mk_remainder(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_FMA:
case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_FMA:
m_conv.mk_fusedma(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_SQRT:
m_conv.mk_sqrt(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE;
case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
@ -159,17 +162,45 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg {
case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE;
case OP_FPA_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;);
throw tactic_exception("NYI");
}
}
return BR_FAILED;
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_BVUNWRAP:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
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;);
NOT_IMPLEMENTED_YET();
}
}
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)