mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
Fixed warnings reported by gcc 4.7.1
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
0f3cba350e
commit
ffcb9741dc
12 changed files with 31 additions and 13 deletions
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -1713,18 +1713,6 @@ void mpz_manager<SYNCH>::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<bool SYNCH>
|
||||
void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
|
||||
if (k == 0 || is_zero(a))
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue