From 86f39cd4c19f285a82a4857d01eed38c742fa7b3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Nov 2013 19:21:55 +0000 Subject: [PATCH] Changed references to _DEBUG to Z3DEBUG. (gcc does not define _DEBUG for debug builds.) Signed-off-by: Christoph M. Wintersteiger --- src/ast/simplifier/array_simplifier_plugin.cpp | 2 +- src/tactic/fpa/fpa2bv_converter.cpp | 6 +++--- src/tactic/sls/sls_tactic.cpp | 4 ++-- src/util/mpn.cpp | 18 +++++++++--------- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp index bf9ca8ffe..065f8bd96 100644 --- a/src/ast/simplifier/array_simplifier_plugin.cpp +++ b/src/ast/simplifier/array_simplifier_plugin.cpp @@ -68,7 +68,7 @@ bool array_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co set_reduce_invoked(); if (m_presimp) return false; -#if _DEBUG +#if Z3DEBUG for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) { SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i)); } diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index ff24d1ceb..011169496 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -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_exp = m_bv_util.mk_sort(ebits); -#ifdef _DEBUG +#ifdef Z3DEBUG std::string p("fpa2bv"); 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())); result = m.mk_fresh_const( - #ifdef _DEBUG + #ifdef Z3DEBUG "fpa2bv_rm" #else 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) { - #ifdef _DEBUG + #ifdef Z3DEBUG return; // CMW: This works only for quantifier-free formulas. expr_ref new_e(m); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index fff082bd8..ea5d60668 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -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, double & best_score, unsigned & best_const, mpz & best_value) { - #ifdef _DEBUG + #ifdef Z3DEBUG mpz old_value; m_mpz_manager.set(old_value, m_tracker.get_value(fd)); #endif 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) << " --> " << r << std::endl; ); diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 2cc35776f..6a544f583 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -31,7 +31,7 @@ mpn_manager static_mpn_manager; const mpn_digit mpn_manager::zero = 0; mpn_manager::mpn_manager() { -#ifdef _DEBUG +#ifdef Z3DEBUG trace_enabled=true; #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 { int res = 0; - #ifdef _DEBUG + #ifdef Z3DEBUG if (trace_enabled) STRACE("mpn", tout << "[mpn] "; ); #endif @@ -60,7 +60,7 @@ int mpn_manager::compare(mpn_digit const * a, size_t const lnga, res = -1; } - #ifdef _DEBUG + #ifdef Z3DEBUG if (trace_enabled) STRACE("mpn", tout << ((res == 1) ? " > " : (res == -1) ? " < " : " == "); ); #endif @@ -212,7 +212,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum, trace(numer, lnum, denom, lden, "%"); trace_nl(rem, lden); -#ifdef _DEBUG +#ifdef Z3DEBUG mpn_sbuffer temp(lnum+1, 0); mul(quot, lnum-lden+1, denom, lden, temp.c_ptr()); 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 // numer[j+n]...numer[j] - q * (denom[n-1]...denom[0]) mpn_digit q_hat_small = (mpn_digit)q_hat; - #ifdef _DEBUG + #ifdef Z3DEBUG trace_enabled = false; #endif 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++) numer[j+i] = t_ab[i]; } - #ifdef _DEBUG + #ifdef Z3DEBUG trace_enabled = true; #endif 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, mpn_digit const * b, size_t const lngb, const char * op) const { -#ifdef _DEBUG +#ifdef Z3DEBUG if (trace_enabled) STRACE("mpn", tout << "[mpn] " << to_string(a, lnga, 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 { -#ifdef _DEBUG +#ifdef Z3DEBUG if (trace_enabled) STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)); ); #endif } void mpn_manager::trace_nl(mpn_digit const * a, size_t const lnga) const { -#ifdef _DEBUG +#ifdef Z3DEBUG if (trace_enabled) STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)) << std::endl; ); #endif