From 203c5015c8522656ebaa3a0db02333a653f5949d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 May 2015 15:17:21 -0700 Subject: [PATCH] fix debian amd64 warnings Signed-off-by: Nikolaj Bjorner --- src/math/simplex/sparse_matrix.h | 2 +- src/muz/rel/udoc_relation.cpp | 1 - src/opt/mus.cpp | 3 ++- src/sat/sat_sls.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 2 +- src/shell/opt_frontend.cpp | 6 +++--- src/smt/theory_arith_core.h | 2 +- src/smt/theory_wmaxsat.cpp | 5 +++-- src/tactic/sls/bvsls_opt_engine.cpp | 5 +++-- 9 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index ee28e1475..c02375e7e 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -48,7 +48,7 @@ namespace simplex { } }; - static const int dead_id = -1; + static const unsigned dead_id = UINT_MAX; /** \brief A row_entry is: m_var*m_coeff diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index b6fa339ff..6d69550ef 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -559,7 +559,6 @@ namespace datalog { filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols) : m_cols(col_cnt), m_equalities(union_ctx) { udoc_relation const& r = get(_r); - doc_manager& dm = r.get_dm(); m_size = r.column_num_bits(identical_cols[0]); m_empty_bv.resize(r.get_num_bits(), false); for (unsigned i = 0; i < col_cnt; ++i) { diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 7f265ab0f..566f4ec0b 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -54,7 +54,8 @@ struct mus::imp { unsigned add_soft(expr* cls) { - SASSERT(is_uninterp_const(cls) || m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0))); + SASSERT(is_uninterp_const(cls) || + (m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0)))); unsigned idx = m_cls2expr.size(); m_expr2cls.insert(cls, idx); m_cls2expr.push_back(cls); diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index 0744ef37a..ad26554af 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -273,7 +273,7 @@ namespace sat { clause const& c = *m_clauses[i]; bool is_sat = c.satisfied_by(m_model); SASSERT(is_sat != m_false.contains(i)); - SASSERT(is_sat == m_num_true[i] > 0); + SASSERT(is_sat == (m_num_true[i] > 0)); } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7224de971..ff201042b 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -36,7 +36,7 @@ Notes: #include"model_v2_pp.h" #include"tactic.h" #include"ast_pp.h" -#include +#include struct goal2sat::imp { struct frame { diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index a7b4f807e..6e39313fd 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -89,11 +89,11 @@ class wcnf { ast_manager& m; stream_buffer& in; - app_ref read_clause(unsigned& weight) { + app_ref read_clause(int& weight) { int parsed_lit; int var; parsed_lit = in.parse_int(); - weight = static_cast(parsed_lit); + weight = parsed_lit; app_ref result(m), p(m); expr_ref_vector ors(m); while (true) { @@ -137,7 +137,7 @@ public: parse_spec(num_vars, num_clauses, max_weight); } else { - unsigned weight = 0; + int weight = 0; app_ref cls = read_clause(weight); if (weight == max_weight) { opt.add_hard_constraint(cls); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 34657de63..f481e35d0 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -72,7 +72,7 @@ namespace smt { m_value .push_back(inf_numeral()); } m_old_value .push_back(inf_numeral()); - SASSERT(m_var_occs.size() == r); + SASSERT(m_var_occs.size() == static_cast(r)); m_var_occs .push_back(atoms()); SASSERT(m_var_occs.back().empty()); m_unassigned_atoms .push_back(0); diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 539a3e909..0c9e64e93 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -55,7 +55,8 @@ void theory_wmaxsat::get_assignment(svector& result) { } else { std::sort(m_cost_save.begin(), m_cost_save.end()); - for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { + unsigned j = 0; + for (theory_var i = 0; i < m_vars.size(); ++i) { if (j < m_cost_save.size() && m_cost_save[j] == i) { result.push_back(false); ++j; @@ -120,7 +121,7 @@ bool_var theory_wmaxsat::register_var(app* var, bool attach) { theory_var v = mk_var(x); ctx.attach_th_var(x, this, v); m_bool2var.insert(bv, v); - SASSERT(v == m_var2bool.size()); + SASSERT(v == static_cast(m_var2bool.size())); m_var2bool.push_back(bv); SASSERT(ctx.bool_var2enode(bv)); } diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index a674e8a25..96fad9a5a 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -318,7 +318,8 @@ mpz bvsls_opt_engine::find_best_move( } // reset to what it was before - double check = incremental_score(fd, old_value); + //double check = + incremental_score(fd, old_value); m_obj_evaluator.update(fd, old_value); } @@ -363,4 +364,4 @@ bool bvsls_opt_engine::randomize_wrt_hard() { } return false; -} \ No newline at end of file +}