mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix compiler warnings reported by Robert White

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-04-02 15:54:28 +02:00
parent 7fd6549a40
commit 1db7e0a149
7 changed files with 25 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_interp.cpp
View file

@ -317,7 +317,7 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
for(unsigned i = 0; i < tokens.size(); i++){
std::string &tok = tokens[i];
size_t eqpos = tok.find('=');
if(eqpos >= 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;

34
src/api/api_opt.cpp
View file

@ -36,7 +36,7 @@ extern "C" {
};
inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); }
inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast<Z3_optimize>(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<opt::context> eh(to_optimize_ref(o));
cancel_eh<opt::context> 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);

2
src/ast/scoped_proof.h
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#ifndef _SCOPED_PROOF__H_
#ifndef _SCOPED_PROOF_H_
#define _SCOPED_PROOF_H_
#include "ast.h"

2
src/interp/iz3hash.h
View file

@ -464,7 +464,7 @@ namespace hash_space {
Value &operator[](const Key& key) {
std::pair<Key,Value> kvp(key,Value());
return lookup(kvp,true)->val.second;
return this->lookup(kvp,true)->val.second;
}
};

2
src/smt/theory_arith_eq.h
View file

@ -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();
}

3
src/tactic/sls/sls_tracker.h
View file

@ -20,6 +20,7 @@ Notes:
#ifndef _SLS_TRACKER_H_
#define _SLS_TRACKER_H_
#include<math.h>
#include"for_each_expr.h"
#include"ast_smt2_pp.h"
#include"bv_decl_plugin.h"
@ -1482,4 +1483,4 @@ public:
}
};
#endif
#endif

4
src/util/sorting_network.h
View file

@ -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<psort_expr>::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<psort_expr>::cmp(as[i+1], bs[i], y1, y2);
out.push_back(y1);
out.push_back(y2);
}