mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Refine fpa_decl_plugin::is_unique_value

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2021-09-14 11:45:17 +00:00
parent 12c32663c6
commit e8d6d97ba3
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 14 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ast/fpa_decl_plugin.cpp
View file

@ -929,16 +929,22 @@ bool fpa_decl_plugin::is_unique_value(app* e) const {
case OP_FPA_RM_TOWARD_NEGATIVE: case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_ZERO: case OP_FPA_RM_TOWARD_ZERO:
return true; return true;
case OP_FPA_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */ case OP_FPA_PLUS_INF: /* No; +oo == (fp #b0 #b11 #b00) */
case OP_FPA_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */ case OP_FPA_MINUS_INF: /* No; -oo == (fp #b1 #b11 #b00) */
case OP_FPA_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ case OP_FPA_PLUS_ZERO: /* No; +zero == (fp #b0 #b00 #b000) */
case OP_FPA_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ case OP_FPA_MINUS_ZERO: /* No; -zero == (fp #b1 #b00 #b000) */
case OP_FPA_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ case OP_FPA_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */
case OP_FPA_NUM: /* see NaN */ case OP_FPA_NUM: /* see NaN */
return false; return false;
case OP_FPA_FP: case OP_FPA_FP: {
return false; /*No; generally not because of clashes with +oo, -oo, +zero, -zero, NaN */ if (m_manager->is_value(e->get_arg(0)) &&
// a refinement would require to return true only if there is no clash with these cases. m_manager->is_value(e->get_arg(1)) &&
m_manager->is_value(e->get_arg(2))) {
bv_util bu(*m_manager);
return !bu.is_allone(e->get_arg(1)) && !bu.is_zero(e->get_arg(1));
}
return false;
}
default: default:
return false; return false;
} }