mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
FPA: Elminated nzero/pzero AST kinds
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
0cedd32ea2
commit
c0a027fc80
|
@ -1155,8 +1155,6 @@ extern "C" {
|
|||
case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO;
|
||||
case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL;
|
||||
case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL;
|
||||
case OP_FPA_IS_PZERO: return Z3_OP_FPA_IS_PZERO;
|
||||
case OP_FPA_IS_NZERO: return Z3_OP_FPA_IS_NZERO;
|
||||
case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE;
|
||||
case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE;
|
||||
case OP_FPA_FP: return Z3_OP_FPA_FP;
|
||||
|
|
|
@ -143,9 +143,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
|
||||
case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
|
||||
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;
|
||||
|
|
|
@ -294,8 +294,6 @@ func_decl * fpa_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_paramet
|
|||
symbol name;
|
||||
switch (k) {
|
||||
case OP_FPA_IS_ZERO: name = "fp.isZero"; break;
|
||||
case OP_FPA_IS_NZERO: name = "fp.isNZero"; break;
|
||||
case OP_FPA_IS_PZERO: name = "fp.isPZero"; break;
|
||||
case OP_FPA_IS_NEGATIVE: name = "fp.isNegative"; break;
|
||||
case OP_FPA_IS_POSITIVE: name = "fp.isPositive"; break;
|
||||
case OP_FPA_IS_NAN: name = "fp.isNaN"; break;
|
||||
|
@ -717,8 +715,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
|||
case OP_FPA_GE:
|
||||
return mk_bin_rel_decl(k, num_parameters, parameters, arity, domain, range);
|
||||
case OP_FPA_IS_ZERO:
|
||||
case OP_FPA_IS_NZERO:
|
||||
case OP_FPA_IS_PZERO:
|
||||
case OP_FPA_IS_NEGATIVE:
|
||||
case OP_FPA_IS_POSITIVE:
|
||||
case OP_FPA_IS_NAN:
|
||||
|
|
|
@ -71,8 +71,6 @@ enum fpa_op_kind {
|
|||
OP_FPA_IS_ZERO,
|
||||
OP_FPA_IS_NORMAL,
|
||||
OP_FPA_IS_SUBNORMAL,
|
||||
OP_FPA_IS_PZERO,
|
||||
OP_FPA_IS_NZERO,
|
||||
OP_FPA_IS_NEGATIVE,
|
||||
OP_FPA_IS_POSITIVE,
|
||||
|
||||
|
@ -325,8 +323,6 @@ public:
|
|||
app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_ZERO, arg1); }
|
||||
app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NORMAL, arg1); }
|
||||
app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_SUBNORMAL, arg1); }
|
||||
app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NZERO, arg1); }
|
||||
app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_PZERO, arg1); }
|
||||
app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); }
|
||||
app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_POSITIVE, arg1); }
|
||||
app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FPA_IS_NEGATIVE, arg1); }
|
||||
|
|
|
@ -57,8 +57,6 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
|
||||
case OP_FPA_GE: SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break;
|
||||
case OP_FPA_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
|
||||
case OP_FPA_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
|
||||
case OP_FPA_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
|
||||
case OP_FPA_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break;
|
||||
case OP_FPA_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
|
||||
case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
|
||||
|
|
Loading…
Reference in a new issue