From bd92797663eb29f92163249e92f4f80fe15bc5f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jul 2017 15:25:59 -0700 Subject: [PATCH] fix compiler warnings Signed-off-by: Nikolaj Bjorner --- src/test/bit_vector.cpp | 2 +- src/test/bv_simplifier_plugin.cpp | 58 +++++++++++++++---------------- src/test/check_assumptions.cpp | 2 +- src/test/dl_context.cpp | 54 +++++++++++++++------------- src/test/dl_query.cpp | 2 +- src/test/heap.cpp | 1 + src/test/hwf.cpp | 6 ++-- src/test/list.cpp | 1 + src/test/mpff.cpp | 2 +- src/test/nlsat.cpp | 3 +- src/test/pb2bv.cpp | 8 ++--- src/test/polynorm.cpp | 1 + src/test/proof_checker.cpp | 4 +-- src/test/rational.cpp | 2 +- src/test/sat_user_scope.cpp | 1 + src/test/simple_parser.cpp | 1 + src/test/upolynomial.cpp | 12 +++---- 17 files changed, 83 insertions(+), 77 deletions(-) diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index 7d3f96ae4..6f83bb328 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -48,7 +48,7 @@ static void tst1() { SASSERT(v1.size() == v2.size()); if (v1.size() > 0) { unsigned idx = rand()%v1.size(); - SASSERT(v1.get(idx) == v2[idx]); + VERIFY(v1.get(idx) == v2[idx]); } } else if (op <= 5) { diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index dc930bb82..69b97a9cc 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -133,7 +133,7 @@ public: params[0] = parameter(2); ar = m_manager.mk_app(m_fid, OP_REPEAT, 1, params, 1, es); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | a64) == u64(e.get())); + VERIFY(((a64 << 32) | a64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BREDOR, e1.get()); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); @@ -163,11 +163,11 @@ public: ar = m_manager.mk_app(m_fid, OP_BIT0); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(!bit2bool(e.get())); + VERIFY(!bit2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BIT1); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(bit2bool(e.get())); + VERIFY(bit2bool(e.get())); } @@ -187,113 +187,113 @@ public: ar = m_manager.mk_app(m_fid, OP_BADD, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a + b) == u32(e.get())); + VERIFY((a + b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSUB, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a - b) == u32(e.get())); + VERIFY((a - b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BMUL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a * b) == u32(e.get())); + VERIFY((a * b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a & b) == u32(e.get())); + VERIFY((a & b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a | b) == u32(e.get())); + VERIFY((a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(~(a | b) == u32(e.get())); + VERIFY(~(a | b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a ^ b) == u32(e.get())); + VERIFY((a ^ b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BXNOR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a ^ b)) == u32(e.get())); + VERIFY((~(a ^ b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BNAND, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((~(a & b)) == u32(e.get())); + VERIFY((~(a & b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_ULEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a <= b) == ast2bool(e.get())); + VERIFY((a <= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a >= b) == ast2bool(e.get())); + VERIFY((a >= b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_ULT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a < b) == ast2bool(e.get())); + VERIFY((a < b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_UGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a > b) == ast2bool(e.get())); + VERIFY((a > b) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa <= sb) == ast2bool(e.get())); + VERIFY((sa <= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGEQ, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa >= sb) == ast2bool(e.get())); + VERIFY((sa >= sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SLT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa < sb) == ast2bool(e.get())); + VERIFY((sa < sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_SGT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa > sb) == ast2bool(e.get())); + VERIFY((sa > sb) == ast2bool(e.get())); ar = m_manager.mk_app(m_fid, OP_BSHL, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a << b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a << b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BLSHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((b>=32)?0:(a >> b)) == u32(e.get())); + VERIFY(((b>=32)?0:(a >> b)) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BASHR, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); std::cout << "compare: " << sa << " >> " << b << " = " << (sa >> b) << " with " << i32(e.get()) << "\n"; - SASSERT(b >= 32 || ((sa >> b) == i32(e.get()))); + VERIFY(b >= 32 || ((sa >> b) == i32(e.get()))); if (b != 0) { ar = m_manager.mk_app(m_fid, OP_BSDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((sa / sb) == i32(e.get())); + VERIFY((sa / sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUDIV, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a / b) == u32(e.get())); + VERIFY((a / b) == u32(e.get())); ar = m_manager.mk_app(m_fid, OP_BSREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - //SASSERT((sa % sb) == i32(e.get())); + //VERIFY((sa % sb) == i32(e.get())); ar = m_manager.mk_app(m_fid, OP_BUREM, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a % b) == u32(e.get())); + VERIFY((a % b) == u32(e.get())); // TBD: BSMOD. } ar = m_manager.mk_app(m_fid, OP_CONCAT, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT(((a64 << 32) | b64) == u64(e.get())); + VERIFY(((a64 << 32) | b64) == u64(e.get())); ar = m_manager.mk_app(m_fid, OP_BCOMP, 2, e1e2); m_simp.reduce(ar->get_decl(), ar->get_num_args(), ar->get_args(), e); - SASSERT((a == b) == bit2bool(e.get())); + VERIFY((a == b) == bit2bool(e.get())); } void test() { diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp index fa8327cd4..918513ca0 100644 --- a/src/test/check_assumptions.cpp +++ b/src/test/check_assumptions.cpp @@ -38,7 +38,7 @@ void tst_check_assumptions() expr * npE = np.get(); lbool res1 = ctx.check(1, &npE); - SASSERT(res1==l_true); + VERIFY(res1 == l_true); ctx.assert_expr(npE); diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index ac09722ac..99a0480a6 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -14,6 +14,35 @@ Copyright (c) 2015 Microsoft Corporation using namespace datalog; +void tst_dl_context() { + symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; + + return; + +#if 0 + const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); + const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; + + params_ref params; + for(unsigned rel_index=0; rel_index=0; eager_checking--) { + params.set_bool("eager_emptiness_checking", eager_checking!=0); + + std::cerr << "Testing " << relations[rel_index] << "\n"; + std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; + dl_context_simple_query_test(params); + dl_context_saturate_file(params, test_file); + } + } +#endif + +} + + +#if 0 + + static lbool dl_context_eval_unary_predicate(ast_manager & m, context & ctx, char const* problem_text, const char * pred_name) { parser* p = parser::create(ctx,m); @@ -72,29 +101,4 @@ void dl_context_saturate_file(params_ref & params, const char * f) { ctx.get_rel_context()->saturate(); std::cerr << "Done\n"; } - -void tst_dl_context() { - symbol relations[] = { symbol("tr_skip"), symbol("tr_sparse"), symbol("tr_hashtable"), symbol("smt_relation2") }; - const unsigned rel_cnt = sizeof(relations)/sizeof(symbol); - - return; -#if 0 - const char * test_file = "c:\\tvm\\src\\benchmarks\\datalog\\t0.datalog"; - - params_ref params; - for(unsigned rel_index=0; rel_index=0; eager_checking--) { - params.set_bool("eager_emptiness_checking", eager_checking!=0); - - std::cerr << "Testing " << relations[rel_index] << "\n"; - std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n"; - dl_context_simple_query_test(params); - dl_context_saturate_file(params, test_file); - } - } #endif -} - - - diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index ae7313e41..e69f1fb13 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -40,7 +40,7 @@ void dl_query_ask_for_last_arg(context & ctx, func_decl * pred, relation_fact & lbool is_sat = ctx.query(query); std::cerr << "@@ last arg query should succeed: " << should_be_successful << "\n"; - SASSERT(is_sat != l_undef); + VERIFY(is_sat != l_undef); relation_fact res_fact(m); res_fact.push_back(f.back()); diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 3d5c5308a..17f9cfaa0 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -77,6 +77,7 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) { } static void tst2() { + (void)dump_heap; int_heap2 h(N); for (int i = 0; i < N * 10; i++) { if (i % 1000 == 0) std::cout << "i: " << i << std::endl; diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp index be32b5400..7a030a452 100644 --- a/src/test/hwf.cpp +++ b/src/test/hwf.cpp @@ -44,19 +44,19 @@ static void bug_to_rational() { unsynch_mpq_manager mq; scoped_mpq r(mq); - double ad, rd; + double ad = 0, rd = 0; m.set(a, 0.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.0); m.to_rational(a, r); ad = m.to_double(a); rd = mq.get_double(r); - SASSERT(ad == rd); + VERIFY(ad == rd); m.set(a, 1.5); m.to_rational(a, r); diff --git a/src/test/list.cpp b/src/test/list.cpp index 5672f4246..a7ad76972 100644 --- a/src/test/list.cpp +++ b/src/test/list.cpp @@ -35,6 +35,7 @@ static void tst1() { list * l5 = append(r, l4, l2); TRACE("list", display(tout, l5->begin(), l5->end()); tout << "\n";); list * l6 = append(r, l5, l5); + (void) l6; TRACE("list", display(tout, l6->begin(), l6->end()); tout << "\n";); } diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 44930f2bd..ca2354b8b 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -435,7 +435,7 @@ static void tst_limits(unsigned prec) { bool overflow = false; try { m.inc(a); } catch (mpff_manager::overflow_exception) { overflow = true; } - SASSERT(overflow); + VERIFY(overflow); m.set_max(a); m.dec(a); SASSERT(m.eq(a, b)); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 27a0aa1da..df25db927 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -391,7 +391,6 @@ static void tst7() { params_ref ps; reslimit rlim; nlsat::solver s(rlim, ps); - anum_manager & am = s.am(); nlsat::pmanager & pm = s.pm(); nlsat::var x0, x1, x2, a, b, c, d; a = s.mk_var(false); @@ -423,7 +422,7 @@ static void tst7() { nlsat::literal_vector litsv(lits.size(), lits.c_ptr()); lbool res = s.check(litsv); - SASSERT(res == l_false); + VERIFY(res == l_false); for (unsigned i = 0; i < litsv.size(); ++i) { s.display(std::cout, litsv[i]); std::cout << " "; diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp index c114997c5..fcc309883 100644 --- a/src/test/pb2bv.cpp +++ b/src/test/pb2bv.cpp @@ -83,10 +83,10 @@ static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vectorcheck_sat(0,0); - SASSERT(res == l_true); + VERIFY(res == l_true); slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); res = slv->check_sat(0,0); - SASSERT(res == l_false); + VERIFY(res == l_false); } } diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index a8f4ab861..0bc9dfe3c 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -88,6 +88,7 @@ private: expr_ref_vector& factors = poly.factors(); expr_ref_vector& coefficients = poly.coefficients(); expr_ref& coefficient = poly.coefficient(); + (void) coefficient; m_rw(term); diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 7f9827187..035326b26 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -11,7 +11,6 @@ void tst_checker1() { ast_manager m(PGM_FINE); expr_ref a(m); proof_ref p1(m), p2(m), p3(m), p4(m); - bool result; expr_ref_vector side_conditions(m); a = m.mk_const(symbol("a"), m.mk_bool_sort()); @@ -26,8 +25,7 @@ void tst_checker1() { proof_checker checker(m); p4 = m.mk_lemma(p3.get(), m.mk_or(a.get(), m.mk_not(a.get()))); ast_ll_pp(std::cout, m, p4.get()); - result = checker.check(p4.get(), side_conditions); - SASSERT(result); + VERIFY(checker.check(p4.get(), side_conditions)); } void tst_proof_checker() { diff --git a/src/test/rational.cpp b/src/test/rational.cpp index 834aab92f..ac478af98 100644 --- a/src/test/rational.cpp +++ b/src/test/rational.cpp @@ -196,7 +196,7 @@ static void tst2() { // get_int64, get_uint64 uint64 u1 = uint64_max.get_uint64(); uint64 u2 = UINT64_MAX; - SASSERT(u1 == u2); + VERIFY(u1 == u2); std::cout << "int64_max: " << int64_max << ", INT64_MAX: " << INT64_MAX << ", int64_max.get_int64(): " << int64_max.get_int64() << ", int64_max.get_uint64(): " << int64_max.get_uint64() << "\n"; SASSERT(int64_max.get_int64() == INT64_MAX); SASSERT(int64_min.get_int64() == INT64_MIN); diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index aa717f371..54de5976a 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -35,6 +35,7 @@ static void add_clause(sat::solver& s, random_gen& r, trail_t& t) { } static void display_state(std::ostream& out, sat::solver& s, trail_t& t) { + (void)t; s.display(out); } diff --git a/src/test/simple_parser.cpp b/src/test/simple_parser.cpp index a5d4d8def..934552711 100644 --- a/src/test/simple_parser.cpp +++ b/src/test/simple_parser.cpp @@ -38,6 +38,7 @@ void tst_simple_parser() { TRACE("simple_parser", tout << mk_pp(r, m) << "\n";); p.parse_string("(+ x (* y x) x)", r); float vals[2] = { 2.0f, 3.0f }; + (void)vals; TRACE("simple_parser", tout << mk_pp(r, m) << "\n"; tout << "val: " << eval(r, 2, vals) << "\n";); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index e7dcf2719..3d9815873 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -129,18 +129,18 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana tout << "fourier upper: " << um.sign_variations_at(fseq, uppers[i]) << "\n";); unsigned fsv_lower = um.sign_variations_at(fseq, lowers[i]); unsigned fsv_upper = um.sign_variations_at(fseq, uppers[i]); - SASSERT(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || - um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || + VERIFY(um.eval_sign_at(q.size(), q.c_ptr(), lowers[i]) == 0 || + um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 || // fsv_lower - fsv_upper is an upper bound for the number of roots in the interval // fsv_upper - fsv_upper - num_roots is even // Recall that num_roots == 1 in the interval. - (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); - + (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0)); + // Double checking using Descartes bounds for the interval // Must use square free component. unsigned dab = um.descartes_bound_a_b(q_sqf.size(), q_sqf.c_ptr(), bqm, lowers[i], uppers[i]); TRACE("upolynomial", tout << "Descartes bound: " << dab << "\n";); - SASSERT(dab == 1); + VERIFY(dab == 1); } } std::cout << "\n"; @@ -499,7 +499,7 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a std::cout << "new (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n"; int sign_a = um.eval_sign_at(_p.size(), _p.c_ptr(), a); int sign_b = um.eval_sign_at(_p.size(), _p.c_ptr(), b); - SASSERT(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); + VERIFY(sign_a != 0 && sign_b != 0 && sign_a == -sign_b); } else { std::cout << "new root: " << bqm.to_string(a) << "\n";