From ffcb9741dcdb6fc70af64d27843789fee9402209 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Oct 2012 00:05:38 -0700 Subject: [PATCH] Fixed warnings reported by gcc 4.7.1 Signed-off-by: Leonardo de Moura --- src/muz_qe/dl_context.cpp | 3 +++ src/shell/main.cpp | 2 ++ src/test/interval.cpp | 6 ++++++ src/test/mpff.cpp | 2 ++ src/test/mpq.cpp | 2 ++ src/test/mpz.cpp | 2 ++ src/test/polynomial.cpp | 6 ++++++ src/test/polynomial_factorization.cpp | 2 ++ src/test/quant_solve.cpp | 3 ++- src/test/trigo.cpp | 2 ++ src/test/upolynomial.cpp | 2 ++ src/util/mpz.cpp | 12 ------------ 12 files changed, 31 insertions(+), 13 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 4cb4b1145..ae7bc360d 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1551,6 +1551,8 @@ namespace datalog { } } +#if 0 + // [Leo] dead code? static func_decl* get_head_relation(ast_manager& m, expr* fml) { while (is_quantifier(fml)) { fml = to_quantifier(fml)->get_expr(); @@ -1564,6 +1566,7 @@ namespace datalog { return 0; } } +#endif void context::display_smt2( unsigned num_queries, diff --git a/src/shell/main.cpp b/src/shell/main.cpp index a19474ceb..822590867 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -107,6 +107,8 @@ public: m_statistics(g_display_statistics) { } + virtual ~extra_params() {} + virtual void register_params(ini_params & p) { datalog_params::register_params(p); p.register_bool_param("STATISTICS", m_statistics, "display statistics"); diff --git a/src/test/interval.cpp b/src/test/interval.cpp index 4621c0416..ef733394b 100644 --- a/src/test/interval.cpp +++ b/src/test/interval.cpp @@ -91,6 +91,7 @@ static void assert_conj(std::ostream & out, unsynch_mpq_manager & m, char const out << "))\n"; } +#if 0 static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool l_open, int l_val, bool u_inf, bool u_open, int u_val) { if (!l_inf && !u_inf) { if (l_val > u_val) @@ -121,6 +122,7 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool return true; } +#endif static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) { switch (rand()%3) { @@ -381,6 +383,7 @@ static void tst_div(unsigned N, unsigned magnitude) { #include"im_float_config.h" +#if 0 static void tst_float() { unsynch_mpq_manager qm; mpf_manager fm; @@ -414,6 +417,7 @@ static void tst_float() { del_f_interval(ifc, a); del_f_interval(ifc, b); del_f_interval(ifc, c); } +#endif void tst_pi() { unsynch_mpq_manager nm; @@ -429,6 +433,7 @@ void tst_pi() { del_interval(imc, r); } +#if 0 static void tst_pi_float() { std::cout << "pi float...\n"; unsynch_mpq_manager qm; @@ -446,6 +451,7 @@ static void tst_pi_float() { } del_f_interval(ifc, r); } +#endif #define NUM_TESTS 1000 #define SMALL_MAG 3 diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index d58a4517e..35afcccf3 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -533,10 +533,12 @@ static void tst_limits(unsigned prec) { SASSERT(!m.is_minus_epsilon(a)); } +#if 0 static void tst_add_corner(unsigned prec) { mpff_manager m(prec); scoped_mpff a(m), b(m); } +#endif static void tst_decimal(int64 n, uint64 d, bool to_plus_inf, unsigned prec, char const * expected, unsigned decimal_places = UINT_MAX) { mpff_manager m(prec); diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp index 5c221d617..68c7d8bb3 100644 --- a/src/test/mpq.cpp +++ b/src/test/mpq.cpp @@ -55,6 +55,7 @@ static void tst1() { m.del(v3); } +#if 0 static void mk_random_num_str(unsigned buffer_sz, char * buffer) { unsigned div_pos; unsigned sz = (rand() % (buffer_sz-2)) + 1; @@ -80,6 +81,7 @@ static void mk_random_num_str(unsigned buffer_sz, char * buffer) { } buffer[sz-1] = 0; } +#endif static void bug1() { synch_mpq_manager m; diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp index 70b49f5a7..d7944ae95 100644 --- a/src/test/mpz.cpp +++ b/src/test/mpz.cpp @@ -77,6 +77,7 @@ static void tst2b() { m.del(v3); } +#if 0 static void mk_random_num_str(unsigned buffer_sz, char * buffer) { unsigned sz = (rand() % (buffer_sz-2)) + 1; SASSERT(sz < buffer_sz); @@ -87,6 +88,7 @@ static void mk_random_num_str(unsigned buffer_sz, char * buffer) { buffer[0] = '-'; buffer[sz-1] = 0; } +#endif static void bug1() { synch_mpz_manager m; diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp index 0a5b4a87b..beb53c0fc 100644 --- a/src/test/polynomial.cpp +++ b/src/test/polynomial.cpp @@ -704,6 +704,7 @@ static void tst_psc(polynomial_ref const & p, polynomial_ref const & q, polynomi } } +#if 0 static void tst_psc_perf(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x) { polynomial::manager & m = p.m(); polynomial_ref_vector S(m); @@ -716,6 +717,7 @@ static void tst_psc_perf(polynomial_ref const & p, polynomial_ref const & q, pol std::cout << "S_" << i << ": " << m.size(S.get(i)) << std::endl; // polynomial_ref(S.get(i), m) << std::endl; } } +#endif static void tst_psc() { polynomial::numeral_manager nm; @@ -1258,6 +1260,7 @@ static void tst_translate() { ); } +#if 0 static void tst_p25() { unsynch_mpq_manager qm; polynomial::manager m(qm); @@ -1279,6 +1282,7 @@ static void tst_p25() { p = (x0 + x1 + x2 + x3 + x4 + x5 + x6)^25; std::cout << "size(p): " << size(p) << "\n"; } +#endif static void tst_mm() { unsynch_mpq_manager qm; @@ -1571,6 +1575,7 @@ static void tst_gcd2() { tst_gcd(p, p_prime, x1^4); } +#if 0 static void tst_gcd3() { enable_trace("polynomial_gcd"); enable_trace("polynomial_gcd_detail"); @@ -1620,6 +1625,7 @@ static void tst_gcd4() { (1000000*x + 1)*(333333333*x + 1)*(77777777*x + 1)*(11111111*x + 1)*(x + 128384747)*(x + 82837437)*(x + 22848481); tst_gcd(p, derivative(p, 0), (x + 3)^9); } +#endif static void tst_newton_interpolation() { // enable_trace("newton"); diff --git a/src/test/polynomial_factorization.cpp b/src/test/polynomial_factorization.cpp index 3b33f2d38..06c67b9c2 100644 --- a/src/test/polynomial_factorization.cpp +++ b/src/test/polynomial_factorization.cpp @@ -172,6 +172,7 @@ int random_polynomial[20][2][11] = { } }; +#if 0 static void tst_square_free_finite_1() { polynomial::numeral_manager nm; polynomial::manager pm(nm); @@ -616,6 +617,7 @@ static void tst_factor_square_free_univariate_3() { upm.reset(deg70_u); } +#endif void tst_factor_swinnerton_dyer_big(unsigned max) { polynomial::numeral_manager nm; diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index 16fc3bcfd..2899522b3 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -44,6 +44,7 @@ static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe:: } +#if 0 static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) { return; // quant_elim option got removed... @@ -73,7 +74,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) fatal_error(0); } } - +#endif static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) { diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp index 66805ed45..da26d0f39 100644 --- a/src/test/trigo.cpp +++ b/src/test/trigo.cpp @@ -116,6 +116,7 @@ static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) { } } +#if 0 static void tst_mpf_bug() { mpf_manager fm; scoped_mpf a(fm), b(fm), c(fm); @@ -126,6 +127,7 @@ static void tst_mpf_bug() { fm.mul(MPF_ROUND_TOWARD_NEGATIVE, a, b, c); std::cout << "c: " << fm.to_double(c) << "\n"; } +#endif static void tst_e(std::ostream & out) { unsynch_mpq_manager nm; diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index 80bc8f278..b38c3af34 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -726,6 +726,7 @@ static void tst_sturm2() { um.display(std::cout, seq2); } +#if 0 static void tst_isolate_roots2() { polynomial::numeral_manager nm; polynomial::manager m(nm); @@ -793,6 +794,7 @@ static void tst_gcd2() { } um.display(std::cout, _p_sqf.size(), _p_sqf.c_ptr()); std::cout << "\n"; } +#endif static void tst_isolate_roots5() { polynomial::numeral_manager nm; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 16a3f1a9e..c77978647 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1713,18 +1713,6 @@ void mpz_manager::machine_div2k(mpz & a, unsigned k) { #endif } -#ifndef _MP_GMP -static void display_bits(std::ostream & out, digit_t a) { - for (unsigned i = 0; i < sizeof(digit_t) * 8; i++) { - if (a % 2 == 0) - out << "0"; - else - out << "1"; - a /= 2; - } -} -#endif - template void mpz_manager::mul2k(mpz & a, unsigned k) { if (k == 0 || is_zero(a))