mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

Exposed internal FPA func_decl kinds. Added missing FPA simplifications. Fixes #1242.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-11 14:36:58 +01:00
parent d131aba8a9
commit e88487021a
5 changed files with 97 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_ast.cpp
View file

@ -1206,14 +1206,14 @@ extern "C" {
case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
case OP_FPA_INTERNAL_MIN_I: return Z3_OP_FPA_MIN_I;
case OP_FPA_INTERNAL_MAX_I: return Z3_OP_FPA_MAX_I;
case OP_FPA_INTERNAL_BV2RM:
case OP_FPA_INTERNAL_BVWRAP:
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED:
case OP_FPA_INTERNAL_BVWRAP: return Z3_OP_FPA_BVWRAP;
case OP_FPA_INTERNAL_BV2RM: return Z3_OP_FPA_BV2RM;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED;
case OP_FPA_INTERNAL_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED;
return Z3_OP_UNINTERPRETED;
default:
return Z3_OP_INTERNAL;

73
src/api/z3_api.h
View file

@ -397,23 +397,23 @@ typedef enum
(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
- Z3_OP_BSMUL_NO_OVFL: a predicate to check that bit-wise signed multiplication does not overflow.
Signed multiplication overflows if the operands have the same sign and the result of multiplication
Signed multiplication overflows if the operands have the same sign and the result of multiplication
does not fit within the available bits. \sa Z3_mk_bvmul_no_overflow.
- Z3_OP_BUMUL_NO_OVFL: check that bit-wise unsigned multiplication does not overflow.
Unsigned multiplication overflows if the result does not fit within the available bits.
\sa Z3_mk_bvmul_no_overflow.
- Z3_OP_BSMUL_NO_UDFL: check that bit-wise signed multiplication does not underflow.
Signed multiplication underflows if the operands have opposite signs and the result of multiplication
does not fit within the avaialble bits. Z3_mk_bvmul_no_underflow.
- Z3_OP_BSDIV_I: Binary signed division.
- Z3_OP_BSDIV_I: Binary signed division.
It has the same semantics as Z3_OP_BSDIV, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BUDIV_I: Binary unsigned division.
It has the same semantics as Z3_OP_BUDIV, but created in a context where the second operand can be assumed to be non-zero.
- Z3_OP_BSREM_I: Binary signed remainder.
It has the same semantics as Z3_OP_BSREM, but created in a context where the second operand can be assumed to be non-zero.
@ -979,7 +979,47 @@ typedef enum
- Z3_OP_FPA_TO_IEEE_BV: Floating-point conversion to IEEE-754 bit-vector
- Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information.
- Z3_OP_FPA_BVWRAP: (Implicitly) represents the internal bitvector-
representation of a floating-point term (used for the lazy encoding
of non-relevant terms in theory_fpa)
- Z3_OP_FPA_BV2RM: Conversion of a 3-bit bit-vector term to a
floating-point rouding-mode term
The conversion uses the following values:
0 = 000 = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
1 = 001 = Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
2 = 010 = Z3_OP_FPA_RM_TOWARD_POSITIVE,
3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO.
- Z3_OP_FPA_MIN_I: The same as Z3_OP_FPA_MIN, but the arguments are
expected not to be zeroes with different signs.
- Z3_OP_FPA_MAX_I: The same as Z3_OP_FPA_MAX, but the arguments are
expected not to be zeroes with different signs.
- Z3_OP_FPA_MIN_UNSPECIFIED: The same as Z3_OP_FPA_MIN, but the
arguments are expected to be zeroes with different signs.
- Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the
arguments are expected to be zeroes with different signs.
- Z3_OP_FPA_TO_UBV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_UBV.
- Z3_OP_FPA_TO_SBV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_SBV.
- Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_IEEE_BV.
- Z3_OP_FPA_TO_REAL_UNSPECIFIED: A term representing the unspecified
results of Z3_OP_FPA_TO_IEEE_BV.
- Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
information is exposed. Tools may use the string representation of the
function declaration to obtain more information.
- Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
*/
@ -1266,6 +1306,15 @@ typedef enum {
Z3_OP_FPA_MIN_I,
Z3_OP_FPA_MAX_I,
Z3_OP_FPA_BVWRAP,
Z3_OP_FPA_BV2RM,
Z3_OP_FPA_MIN_UNSPECIFIED,
Z3_OP_FPA_MAX_UNSPECIFIED,
Z3_OP_FPA_TO_UBV_UNSPECIFIED,
Z3_OP_FPA_TO_SBV_UNSPECIFIED,
Z3_OP_FPA_TO_REAL_UNSPECIFIED,
Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED,
Z3_OP_INTERNAL,
Z3_OP_UNINTERPRETED
@ -3361,7 +3410,7 @@ extern "C" {
\brief Convert string to integer.
def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
@ -3369,7 +3418,7 @@ extern "C" {
\brief Integer to string conversion.
def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
*/
*/
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
/**
@ -4859,12 +4908,12 @@ extern "C" {
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
/**
\brief Create a fresh func_interp object, add it to a model for a specified function.
It has reference count 0.
\brief Create a fresh func_interp object, add it to a model for a specified function.
It has reference count 0.
\param c context
\param m model
\param f function declaration
\param f function declaration
\param default_value default value for function interpretation
def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
@ -4950,7 +4999,7 @@ extern "C" {
\param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function.
\param value value of the function when the parameters match args.
It is assumed that entries added to a function cover disjoint arguments.
It is assumed that entries added to a function cover disjoint arguments.
If an two entries are added with the same arguments, only the second insertion survives and the
first inserted entry is removed.

2
src/ast/fpa_decl_plugin.h
View file

@ -168,8 +168,6 @@ class fpa_decl_plugin : public decl_plugin {
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters,

28
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -94,8 +94,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break;
case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
case OP_FPA_INTERNAL_MIN_I:
case OP_FPA_INTERNAL_MAX_I:
case OP_FPA_INTERNAL_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break;
case OP_FPA_INTERNAL_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break;
case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
SASSERT(num_args == 2); st = BR_FAILED; break;
@ -454,6 +454,18 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
}
}
br_status fpa_rewriter::mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
else
result = m_util.mk_min(arg1, arg2);
return BR_DONE;
}
return BR_FAILED;
}
br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_nan(arg1)) {
result = arg2;
@ -489,6 +501,18 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
}
}
br_status fpa_rewriter::mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_fm), v2(m_fm);
if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) {
if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))
result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2);
else
result = m_util.mk_max(arg1, arg2);
return BR_DONE;
}
return BR_FAILED;
}
br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
mpf_rounding_mode rm;
if (m_util.is_rm_numeral(arg1, rm)) {

2
src/ast/rewriter/fpa_rewriter.h
View file

@ -85,6 +85,8 @@ public:
br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result);
br_status mk_to_real(expr * arg, expr_ref & result);
br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);
br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result);