mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-28 19:40:49 -07:00
parent fa48703445
commit 4958edeb42
3 changed files with 25 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/arith_decl_plugin.h
View file

@ -290,6 +290,9 @@ public:
bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); } 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_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_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); }
bool is_asinh(expr const* n) const { return is_app_of(n, m_afid, OP_ASINH); }
bool is_acosh(expr const* n) const { return is_app_of(n, m_afid, OP_ACOSH); }
bool is_atanh(expr const* n) const { return is_app_of(n, m_afid, OP_ATANH); }
bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); } 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); } bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
@ -311,10 +314,13 @@ public:
MATCH_UNARY(is_sin); MATCH_UNARY(is_sin);
MATCH_UNARY(is_asin); MATCH_UNARY(is_asin);
MATCH_UNARY(is_asinh);
MATCH_UNARY(is_cos); MATCH_UNARY(is_cos);
MATCH_UNARY(is_acos); MATCH_UNARY(is_acos);
MATCH_UNARY(is_acosh);
MATCH_UNARY(is_tan); MATCH_UNARY(is_tan);
MATCH_UNARY(is_atan); MATCH_UNARY(is_atan);
MATCH_UNARY(is_atanh);
}; };

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

@ -946,12 +946,13 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a; numeral a;
expr* x;
if (m_util.is_numeral(arg, a)) { if (m_util.is_numeral(arg, a)) {
result = m_util.mk_numeral(floor(a), true); result = m_util.mk_numeral(floor(a), true);
return BR_DONE; return BR_DONE;
} }
else if (m_util.is_to_real(arg)) { else if (m_util.is_to_real(arg, x)) {
result = to_app(arg)->get_arg(0); result = x;
return BR_DONE; return BR_DONE;
} }
else { else {
@ -982,8 +983,8 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
new_args.push_back(m_util.mk_numeral(a, true)); new_args.push_back(m_util.mk_numeral(a, true));
} }
else { else {
SASSERT(m_util.is_to_real(c)); VERIFY (m_util.is_to_real(c, x));
new_args.push_back(to_app(c)->get_arg(0)); new_args.push_back(x);
} }
} }
SASSERT(num_args == new_args.size()); SASSERT(num_args == new_args.size());
@ -1315,9 +1316,10 @@ br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
} }
br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ATAN)) { expr* x;
if (m_util.is_atan(arg, x)) {
// tan(atan(x)) == x // tan(atan(x)) == x
result = to_app(arg)->get_arg(0); result = x;
return BR_DONE; return BR_DONE;
} }
@ -1497,9 +1499,10 @@ br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) {
} }
br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ASINH)) { expr* x;
if (m_util.is_asinh(arg, x)) {
// sinh(asinh(x)) == x // sinh(asinh(x)) == x
result = to_app(arg)->get_arg(0); result = x;
return BR_DONE; return BR_DONE;
} }
expr * t; expr * t;
@ -1512,12 +1515,12 @@ br_status arith_rewriter::mk_sinh_core(expr * arg, expr_ref & result) {
} }
br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ACOSH)) { expr* t;
// cosh(acosh(x)) == x if (m_util.is_acosh(arg, t)) {
result = to_app(arg)->get_arg(0); // cosh(acosh(t)) == t
result = t;
return BR_DONE; return BR_DONE;
} }
expr * t;
if (m_util.is_times_minus_one(arg, t)) { if (m_util.is_times_minus_one(arg, t)) {
// cosh(-t) == cosh // cosh(-t) == cosh
result = m_util.mk_cosh(t); result = m_util.mk_cosh(t);
@ -1527,12 +1530,12 @@ br_status arith_rewriter::mk_cosh_core(expr * arg, expr_ref & result) {
} }
br_status arith_rewriter::mk_tanh_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_tanh_core(expr * arg, expr_ref & result) {
if (is_app_of(arg, get_fid(), OP_ATANH)) { expr * t;
// tanh(atanh(x)) == x if (m_util.is_atanh(arg, t)) {
result = to_app(arg)->get_arg(0); // tanh(atanh(t)) == t
result = t;
return BR_DONE; return BR_DONE;
} }
expr * t;
if (m_util.is_times_minus_one(arg, t)) { if (m_util.is_times_minus_one(arg, t)) {
// tanh(-t) == -tanh(t) // tanh(-t) == -tanh(t)
result = m_util.mk_uminus(m_util.mk_tanh(t)); result = m_util.mk_uminus(m_util.mk_tanh(t));

1
src/smt/smt_consequences.cpp
View file

@ -125,7 +125,6 @@ namespace smt {
unsigned num_units = assigned_literals().size(); unsigned num_units = assigned_literals().size();
app_ref eq(m_manager); app_ref eq(m_manager);
TRACE("context", TRACE("context",
tout << "pop: " << num_levels << "\n";
tout << "vars: " << vars.size() << "\n"; tout << "vars: " << vars.size() << "\n";
tout << "lits: " << num_units << "\n";); tout << "lits: " << num_units << "\n";);
m_case_split_queue->init_search_eh(); m_case_split_queue->init_search_eh();