From 1db7e0a149fee3313c70fd0ac38027021f67a0c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Apr 2014 15:54:28 +0200 Subject: [PATCH] fix compiler warnings reported by Robert White Signed-off-by: Nikolaj Bjorner --- src/api/api_interp.cpp | 2 +- src/api/api_opt.cpp | 34 +++++++++++++++++----------------- src/ast/scoped_proof.h | 2 +- src/interp/iz3hash.h | 2 +- src/smt/theory_arith_eq.h | 2 +- src/tactic/sls/sls_tracker.h | 3 ++- src/util/sorting_network.h | 4 ++-- 7 files changed, 25 insertions(+), 24 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 2c88a1978..48e13d571 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -317,7 +317,7 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < tok.size()){ + if(eqpos < tok.size()){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index b1e4b9203..e40d690fc 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -36,7 +36,7 @@ extern "C" { }; inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast(o); } inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast(o); } - inline opt::context& to_optimize_ref(Z3_optimize o) { return *to_optimize(o)->m_opt; } + inline opt::context* to_optimize_ref(Z3_optimize o) { return to_optimize(o)->m_opt; } Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) { Z3_TRY; @@ -70,7 +70,7 @@ extern "C" { LOG_Z3_optimize_assert(c, o, a); RESET_ERROR_CODE(); CHECK_FORMULA(a,); - to_optimize_ref(o).add_hard_constraint(to_expr(a)); + to_optimize_ref(o)->add_hard_constraint(to_expr(a)); Z3_CATCH; } @@ -80,7 +80,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_FORMULA(a,0); rational w(weight); - return to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id)); + return to_optimize_ref(o)->add_soft_constraint(to_expr(a), w, to_symbol(id)); Z3_CATCH_RETURN(0); } @@ -89,7 +89,7 @@ extern "C" { LOG_Z3_optimize_maximize(c, o, t); RESET_ERROR_CODE(); CHECK_VALID_AST(t,0); - return to_optimize_ref(o).add_objective(to_app(t), true); + return to_optimize_ref(o)->add_objective(to_app(t), true); Z3_CATCH_RETURN(0); } @@ -98,7 +98,7 @@ extern "C" { LOG_Z3_optimize_minimize(c, o, t); RESET_ERROR_CODE(); CHECK_VALID_AST(t,0); - return to_optimize_ref(o).add_objective(to_app(t), false); + return to_optimize_ref(o)->add_objective(to_app(t), false); Z3_CATCH_RETURN(0); } @@ -107,19 +107,19 @@ extern "C" { LOG_Z3_optimize_check(c, o); RESET_ERROR_CODE(); lbool r = l_undef; - cancel_eh eh(to_optimize_ref(o)); + cancel_eh eh(*to_optimize_ref(o)); unsigned timeout = 0; // to_optimize(o)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); try { - r = to_optimize_ref(o).optimize(); + r = to_optimize_ref(o)->optimize(); } catch (z3_exception& ex) { mk_c(c)->handle_exception(ex); r = l_undef; } - // to_optimize_ref(d).cleanup(); + // to_optimize_ref(d)->cleanup(); } return of_lbool(r); Z3_CATCH_RETURN(Z3_L_UNDEF); @@ -130,7 +130,7 @@ extern "C" { LOG_Z3_optimize_get_model(c, o); RESET_ERROR_CODE(); model_ref _m; - to_optimize_ref(o).get_model(_m); + to_optimize_ref(o)->get_model(_m); Z3_model_ref * m_ref = alloc(Z3_model_ref); if (_m) { m_ref->m_model = _m; @@ -148,10 +148,10 @@ extern "C" { LOG_Z3_optimize_set_params(c, o, p); RESET_ERROR_CODE(); param_descrs descrs; - to_optimize_ref(o).collect_param_descrs(descrs); + to_optimize_ref(o)->collect_param_descrs(descrs); to_params(p)->m_params.validate(descrs); params_ref pr = to_param_ref(p); - to_optimize_ref(o).updt_params(pr); + to_optimize_ref(o)->updt_params(pr); Z3_CATCH; } @@ -161,7 +161,7 @@ extern "C" { RESET_ERROR_CODE(); Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref); mk_c(c)->save_object(d); - to_optimize_ref(o).collect_param_descrs(d->m_descrs); + to_optimize_ref(o)->collect_param_descrs(d->m_descrs); Z3_param_descrs r = of_param_descrs(d); RETURN_Z3(r); Z3_CATCH_RETURN(0); @@ -172,7 +172,7 @@ extern "C" { Z3_TRY; LOG_Z3_optimize_get_lower(c, o, idx); RESET_ERROR_CODE(); - expr_ref e = to_optimize_ref(o).get_lower(idx); + expr_ref e = to_optimize_ref(o)->get_lower(idx); mk_c(c)->save_ast_trail(e); RETURN_Z3(of_expr(e)); Z3_CATCH_RETURN(0); @@ -183,7 +183,7 @@ extern "C" { Z3_TRY; LOG_Z3_optimize_get_upper(c, o, idx); RESET_ERROR_CODE(); - expr_ref e = to_optimize_ref(o).get_upper(idx); + expr_ref e = to_optimize_ref(o)->get_upper(idx); mk_c(c)->save_ast_trail(e); RETURN_Z3(of_expr(e)); Z3_CATCH_RETURN(0); @@ -193,7 +193,7 @@ extern "C" { Z3_TRY; LOG_Z3_optimize_to_string(c, o); RESET_ERROR_CODE(); - return mk_c(c)->mk_external_string(to_optimize_ref(o).to_string()); + return mk_c(c)->mk_external_string(to_optimize_ref(o)->to_string()); Z3_CATCH_RETURN(""); } @@ -203,7 +203,7 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; param_descrs descrs; - to_optimize_ref(d).collect_param_descrs(descrs); + to_optimize_ref(d)->collect_param_descrs(descrs); descrs.display(buffer); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); @@ -214,7 +214,7 @@ extern "C" { LOG_Z3_optimize_get_statistics(c, d); RESET_ERROR_CODE(); Z3_stats_ref * st = alloc(Z3_stats_ref); - to_optimize_ref(d).collect_statistics(st->m_stats); + to_optimize_ref(d)->collect_statistics(st->m_stats); mk_c(c)->save_object(st); Z3_stats r = of_stats(st); RETURN_Z3(r); diff --git a/src/ast/scoped_proof.h b/src/ast/scoped_proof.h index e37290c03..68c186e85 100644 --- a/src/ast/scoped_proof.h +++ b/src/ast/scoped_proof.h @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#ifndef _SCOPED_PROOF__H_ +#ifndef _SCOPED_PROOF_H_ #define _SCOPED_PROOF_H_ #include "ast.h" diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 2b364bc1b..d1bfd9f7b 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -464,7 +464,7 @@ namespace hash_space { Value &operator[](const Key& key) { std::pair kvp(key,Value()); - return lookup(kvp,true)->val.second; + return this->lookup(kvp,true)->val.second; } }; diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 04e16e778..368ccb87d 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -193,7 +193,7 @@ namespace smt { return true; } - if (!r.get_base_var() == x && x > y) { + if (r.get_base_var() != x && x > y) { std::swap(x, y); k.neg(); } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 188df66b1..a074af2f8 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -20,6 +20,7 @@ Notes: #ifndef _SLS_TRACKER_H_ #define _SLS_TRACKER_H_ +#include #include"for_each_expr.h" #include"ast_smt2_pp.h" #include"bv_decl_plugin.h" @@ -1482,4 +1483,4 @@ public: } }; -#endif \ No newline at end of file +#endif diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index a1f58a3a7..b9cf86433 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -380,7 +380,7 @@ Notes: literal y2 = min(as[0], bs[0]); out.push_back(y1); out.push_back(y2); - cmp(as[0], bs[0], y1, y2); + psort_nw::cmp(as[0], bs[0], y1, y2); } else if (a == 0) { out.append(b, bs); @@ -455,7 +455,7 @@ Notes: for (unsigned i = 0; i < sz; ++i) { literal y1 = max(as[i+1],bs[i]); literal y2 = min(as[i+1],bs[i]); - cmp(as[i+1], bs[i], y1, y2); + psort_nw::cmp(as[i+1], bs[i], y1, y2); out.push_back(y1); out.push_back(y2); }