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

fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-13 11:12:27 -07:00
parent 247e94a7c0
commit 3a70b6aab4
3 changed files with 28 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/ast/arith_decl_plugin.h
View file

@ -290,6 +290,8 @@ public:
bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); }
bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); }
bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); }
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
MATCH_UNARY(is_uminus);
MATCH_UNARY(is_to_real);
@ -307,8 +309,13 @@ public:
MATCH_BINARY(is_idiv);
MATCH_BINARY(is_power);
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
MATCH_UNARY(is_sin);
MATCH_UNARY(is_asin);
MATCH_UNARY(is_cos);
MATCH_UNARY(is_acos);
MATCH_UNARY(is_tan);
MATCH_UNARY(is_atan);
};
class arith_util : public arith_recognizers {
@ -355,6 +362,9 @@ public:
app * mk_int(int i) {
return mk_numeral(rational(i), true);
}
app * mk_real(int i) {
return mk_numeral(rational(i), false);
}
app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); }
app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); }
app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }

19
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1196,11 +1196,17 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
}
br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ASIN)) {
expr * m, *x;
if (m_util.is_asin(arg, x)) {
// sin(asin(x)) == x
result = to_app(arg)->get_arg(0);
result = x;
return BR_DONE;
}
if (m_util.is_acos(arg, x)) {
// sin(acos(x)) == sqrt(1 - x^2)
result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false));
return BR_REWRITE_FULL;
}
rational k;
if (is_numeral(arg, k) && k.is_zero()) {
// sin(0) == 0
@ -1214,7 +1220,6 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
return BR_REWRITE_FULL;
}
expr * m;
if (is_pi_offset(arg, k, m)) {
rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
SASSERT(k_prime >= rational(0) && k_prime < rational(2));
@ -1250,11 +1255,15 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
}
br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ACOS)) {
expr* x;
if (m_util.is_acos(arg, x)) {
// cos(acos(x)) == x
result = to_app(arg)->get_arg(0);
result = x;
return BR_DONE;
}
if (m_util.is_asin(arg, x)) {
// cos(asin(x)) == ...
}
rational k;
if (is_numeral(arg, k) && k.is_zero()) {

4
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -782,8 +782,8 @@ struct purify_arith_proc {
obj_map<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end();
for (; it != end; ++it) {
emc->insert(it->m_key->get_decl(),
u().mk_add(u().mk_acos(it->m_value.second),
m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), mk_real_zero(), u().mk_pi())));
m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), u().mk_acos(it->m_value.second),
u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi())));
}
}