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

Changed references to _DEBUG to Z3DEBUG.

Browse source 
(gcc does not define _DEBUG for debug builds.)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-11-08 19:21:55 +00:00
parent 412f912c46
commit 86f39cd4c1
4 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -68,7 +68,7 @@ bool array_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
set_reduce_invoked(); set_reduce_invoked();
if (m_presimp) if (m_presimp)
return false; return false;
#if _DEBUG #if Z3DEBUG
for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) { for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) {
SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i)); SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i));
} }

6
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -140,7 +140,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
s_sig = m_bv_util.mk_sort(sbits-1); s_sig = m_bv_util.mk_sort(sbits-1);
s_exp = m_bv_util.mk_sort(ebits); s_exp = m_bv_util.mk_sort(ebits);
#ifdef _DEBUG #ifdef Z3DEBUG
std::string p("fpa2bv"); std::string p("fpa2bv");
std::string name = f->get_name().str(); std::string name = f->get_name().str();
@ -271,7 +271,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
SASSERT(is_rm_sort(f->get_range())); SASSERT(is_rm_sort(f->get_range()));
result = m.mk_fresh_const( result = m.mk_fresh_const(
#ifdef _DEBUG #ifdef Z3DEBUG
"fpa2bv_rm" "fpa2bv_rm"
#else #else
0 0
@ -2345,7 +2345,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
} }
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef _DEBUG #ifdef Z3DEBUG
return; return;
// CMW: This works only for quantifier-free formulas. // CMW: This works only for quantifier-free formulas.
expr_ref new_e(m); expr_ref new_e(m);

4
src/tactic/sls/sls_tactic.cpp
View file

@ -189,14 +189,14 @@ class sls_tactic : public tactic {
bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp, bool what_if(goal_ref const & g, func_decl * fd, const unsigned & fd_inx, const mpz & temp,
double & best_score, unsigned & best_const, mpz & best_value) { double & best_score, unsigned & best_const, mpz & best_value) {
#ifdef _DEBUG #ifdef Z3DEBUG
mpz old_value; mpz old_value;
m_mpz_manager.set(old_value, m_tracker.get_value(fd)); m_mpz_manager.set(old_value, m_tracker.get_value(fd));
#endif #endif
double r = incremental_score(g, fd, temp); double r = incremental_score(g, fd, temp);
#ifdef _DEBUG #ifdef Z3DEBUG
TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
" --> " << r << std::endl; ); " --> " << r << std::endl; );

18
src/util/mpn.cpp
View file

@ -31,7 +31,7 @@ mpn_manager static_mpn_manager;
const mpn_digit mpn_manager::zero = 0; const mpn_digit mpn_manager::zero = 0;
mpn_manager::mpn_manager() { mpn_manager::mpn_manager() {
#ifdef _DEBUG #ifdef Z3DEBUG
trace_enabled=true; trace_enabled=true;
#endif #endif
} }
@ -43,7 +43,7 @@ int mpn_manager::compare(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb) const { mpn_digit const * b, size_t const lngb) const {
int res = 0; int res = 0;
#ifdef _DEBUG #ifdef Z3DEBUG
if (trace_enabled) if (trace_enabled)
STRACE("mpn", tout << "[mpn] "; ); STRACE("mpn", tout << "[mpn] "; );
#endif #endif
@ -60,7 +60,7 @@ int mpn_manager::compare(mpn_digit const * a, size_t const lnga,
res = -1; res = -1;
} }
#ifdef _DEBUG #ifdef Z3DEBUG
if (trace_enabled) if (trace_enabled)
STRACE("mpn", tout << ((res == 1) ? " > " : (res == -1) ? " < " : " == "); ); STRACE("mpn", tout << ((res == 1) ? " > " : (res == -1) ? " < " : " == "); );
#endif #endif
@ -212,7 +212,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
trace(numer, lnum, denom, lden, "%"); trace(numer, lnum, denom, lden, "%");
trace_nl(rem, lden); trace_nl(rem, lden);
#ifdef _DEBUG #ifdef Z3DEBUG
mpn_sbuffer temp(lnum+1, 0); mpn_sbuffer temp(lnum+1, 0);
mul(quot, lnum-lden+1, denom, lden, temp.c_ptr()); mul(quot, lnum-lden+1, denom, lden, temp.c_ptr());
size_t real_size; size_t real_size;
@ -340,7 +340,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
// Replace numer[j+n]...numer[j] with // Replace numer[j+n]...numer[j] with
// numer[j+n]...numer[j] - q * (denom[n-1]...denom[0]) // numer[j+n]...numer[j] - q * (denom[n-1]...denom[0])
mpn_digit q_hat_small = (mpn_digit)q_hat; mpn_digit q_hat_small = (mpn_digit)q_hat;
#ifdef _DEBUG #ifdef Z3DEBUG
trace_enabled = false; trace_enabled = false;
#endif #endif
mul(&q_hat_small, 1, denom.c_ptr(), n, t_ms.c_ptr()); mul(&q_hat_small, 1, denom.c_ptr(), n, t_ms.c_ptr());
@ -354,7 +354,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
for (size_t i = 0; i < n+1; i++) for (size_t i = 0; i < n+1; i++)
numer[j+i] = t_ab[i]; numer[j+i] = t_ab[i];
} }
#ifdef _DEBUG #ifdef Z3DEBUG
trace_enabled = true; trace_enabled = true;
#endif #endif
STRACE("mpn_div", tout << "q_hat=" << q_hat << " r_hat=" << r_hat; STRACE("mpn_div", tout << "q_hat=" << q_hat << " r_hat=" << r_hat;
@ -416,7 +416,7 @@ void mpn_manager::display_raw(std::ostream & out, mpn_digit const * a, size_t co
void mpn_manager::trace(mpn_digit const * a, size_t const lnga, void mpn_manager::trace(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb, mpn_digit const * b, size_t const lngb,
const char * op) const { const char * op) const {
#ifdef _DEBUG #ifdef Z3DEBUG
if (trace_enabled) if (trace_enabled)
STRACE("mpn", tout << "[mpn] " << to_string(a, lnga, char_buf, sizeof(char_buf)); STRACE("mpn", tout << "[mpn] " << to_string(a, lnga, char_buf, sizeof(char_buf));
tout << " " << op << " " << to_string(b, lngb, char_buf, sizeof(char_buf)); tout << " " << op << " " << to_string(b, lngb, char_buf, sizeof(char_buf));
@ -425,14 +425,14 @@ void mpn_manager::trace(mpn_digit const * a, size_t const lnga,
} }
void mpn_manager::trace(mpn_digit const * a, size_t const lnga) const { void mpn_manager::trace(mpn_digit const * a, size_t const lnga) const {
#ifdef _DEBUG #ifdef Z3DEBUG
if (trace_enabled) if (trace_enabled)
STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)); ); STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)); );
#endif #endif
} }
void mpn_manager::trace_nl(mpn_digit const * a, size_t const lnga) const { void mpn_manager::trace_nl(mpn_digit const * a, size_t const lnga) const {
#ifdef _DEBUG #ifdef Z3DEBUG
if (trace_enabled) if (trace_enabled)
STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)) << std::endl; ); STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)) << std::endl; );
#endif #endif