From db6d95f9a9e6e6266f96e67d313174bdc208b222 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 1 Nov 2023 12:01:54 -0700 Subject: [PATCH 1/3] fix warnings --- src/mcsat/bool/clause_db.c | 3 --- src/mcsat/bv/bv_explainer.c | 2 -- src/mcsat/solver.c | 2 -- src/solvers/bv/bv64_intervals.c | 8 ++++---- src/solvers/bv/bv_intervals.c | 8 ++++---- src/solvers/cdcl/new_sat_solver.c | 2 +- src/solvers/simplex/simplex.c | 2 +- src/terms/power_products.c | 4 ++-- 8 files changed, 12 insertions(+), 19 deletions(-) diff --git a/src/mcsat/bool/clause_db.c b/src/mcsat/bool/clause_db.c index 8b144ea94..16fc84578 100644 --- a/src/mcsat/bool/clause_db.c +++ b/src/mcsat/bool/clause_db.c @@ -146,7 +146,6 @@ clause_ref_t clause_get_ref(const clause_db_t* db, const mcsat_tagged_clause_t* static bool clause_check(const mcsat_tagged_clause_t* clause, const variable_db_t* var_db, bool assert) { const mcsat_literal_t* lit; - uint32_t i; if (clause->tag.type == CLAUSE_DEFINITION) { if (!variable_db_is_variable(var_db, clause->tag.var, assert)) { @@ -155,14 +154,12 @@ bool clause_check(const mcsat_tagged_clause_t* clause, const variable_db_t* var_ } } - i = 0; lit = clause->clause.literals; while (*lit != mcsat_literal_null) { if (!variable_db_is_variable(var_db, literal_get_variable(*lit), assert)) { assert(!assert); return false; } - i ++; lit ++; } diff --git a/src/mcsat/bv/bv_explainer.c b/src/mcsat/bv/bv_explainer.c index 9521bb600..8e61fef97 100644 --- a/src/mcsat/bv/bv_explainer.c +++ b/src/mcsat/bv/bv_explainer.c @@ -227,8 +227,6 @@ void bv_explainer_get_conflict(bv_explainer_t* exp, const ivector_t* conflict_in } if (ctx_trace_enabled(exp->ctx, "mcsat::bv::conflict::check")) { - static int conflict_count = 0; - conflict_count ++; bv_explainer_check_conflict(exp, conflict_out); } diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 085cdeed7..3660f5ab1 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2035,8 +2035,6 @@ void mcsat_analyze_conflicts(mcsat_solver_t* mcsat, uint32_t* restart_resource) if (trace_enabled(trace, "mcsat::conflict::check")) { // Don't check bool conflicts: they are implied by the formula (clauses) if (plugin_i != mcsat->bool_plugin_id) { - static int conflict_count = 0; - conflict_count ++; conflict_check(&conflict); } } diff --git a/src/solvers/bv/bv64_intervals.c b/src/solvers/bv/bv64_intervals.c index 46eaa8ab4..af19fac16 100644 --- a/src/solvers/bv/bv64_intervals.c +++ b/src/solvers/bv/bv64_intervals.c @@ -36,12 +36,12 @@ */ static inline bool add_underflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) { assert(a == ((b + c) & mask64(n))); - return is_neg64(b, n) & is_neg64(c, n) & is_pos64(a, n); + return is_neg64(b, n) && is_neg64(c, n) && is_pos64(a, n); } static inline bool add_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) { assert(a == ((b + c) & mask64(n))); - return is_pos64(b, n) & is_pos64(c, n) & is_neg64(a, n); + return is_pos64(b, n) && is_pos64(c, n) && is_neg64(a, n); } @@ -52,12 +52,12 @@ static inline bool add_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n */ static inline bool sub_underflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) { assert(a == ((b - c) & mask64(n))); - return is_neg64(b, n) & is_pos64(c, n) & is_pos64(a, n); + return is_neg64(b, n) && is_pos64(c, n) && is_pos64(a, n); } static inline bool sub_overflow64(uint64_t a, uint64_t b, uint64_t c, uint32_t n) { assert(a == ((b - c) & mask64(n))); - return is_pos64(b, n) & is_neg64(c, n) & is_neg64(a, n); + return is_pos64(b, n) && is_neg64(c, n) && is_neg64(a, n); } diff --git a/src/solvers/bv/bv_intervals.c b/src/solvers/bv/bv_intervals.c index ae92a88e9..abc84d003 100644 --- a/src/solvers/bv/bv_intervals.c +++ b/src/solvers/bv/bv_intervals.c @@ -390,12 +390,12 @@ static void bv_interval_add_u_core(bv_interval_t *a, uint32_t *l, uint32_t *u, u */ static inline bool add_overflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) { // sign bit of a0 = 0, sign bit of b = 0, sign bit of a = 1 - return !sa & !bvconst_tst_bit(b, n-1) & bvconst_tst_bit(a, n-1); + return !sa && !bvconst_tst_bit(b, n-1) && bvconst_tst_bit(a, n-1); } static inline bool add_underflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) { // sign bit of a0 = 1, sign bit of b = 1, sign bit of a = 0 - return sa & bvconst_tst_bit(b, n-1) & !bvconst_tst_bit(a, n-1); + return sa && bvconst_tst_bit(b, n-1) && !bvconst_tst_bit(a, n-1); } @@ -482,12 +482,12 @@ static void bv_interval_sub_u_core(bv_interval_t *a, uint32_t *l, uint32_t *u, u */ static inline bool sub_overflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) { // sign bit of a0 = 0, sign bit of b = 1, sign bit of a = 1 - return !sa & bvconst_tst_bit(b, n-1) & bvconst_tst_bit(a, n-1); + return !sa && bvconst_tst_bit(b, n-1) && bvconst_tst_bit(a, n-1); } static inline bool sub_underflow(uint32_t *a, uint32_t *b, bool sa, uint32_t n) { // sign bit of a0 = 1, sign bit of b = 0, sign bit of a = 0 - return sa & !bvconst_tst_bit(b, n-1) & !bvconst_tst_bit(a, n-1); + return sa && !bvconst_tst_bit(b, n-1) && !bvconst_tst_bit(a, n-1); } diff --git a/src/solvers/cdcl/new_sat_solver.c b/src/solvers/cdcl/new_sat_solver.c index bca8cb1e4..60e0db3f5 100644 --- a/src/solvers/cdcl/new_sat_solver.c +++ b/src/solvers/cdcl/new_sat_solver.c @@ -3827,7 +3827,7 @@ static inline bool var_is_eliminated(const sat_solver_t *solver, bvar_t x) { * Check whether variable x is active (i.e., not assigned at level 0) and not eliminated */ static bool var_is_active(const sat_solver_t *solver, bvar_t x) { - return var_is_unassigned(solver, x) & ! var_is_eliminated(solver, x); + return var_is_unassigned(solver, x) && ! var_is_eliminated(solver, x); } /* diff --git a/src/solvers/simplex/simplex.c b/src/solvers/simplex/simplex.c index 32a17a522..91ff5dce2 100644 --- a/src/solvers/simplex/simplex.c +++ b/src/solvers/simplex/simplex.c @@ -7172,7 +7172,7 @@ static void create_branch_atom(simplex_solver_t *solver, thvar_t x) { int32_t new_idx, lb, ub; literal_t l; - assert(arith_var_is_int(&solver->vtbl, x) & ! arith_var_value_is_int(&solver->vtbl, x)); + assert(arith_var_is_int(&solver->vtbl, x) && ! arith_var_value_is_int(&solver->vtbl, x)); bound = &solver->bound; lb = arith_var_lower_index(&solver->vtbl, x); diff --git a/src/terms/power_products.c b/src/terms/power_products.c index ea6592bae..e71d181a1 100644 --- a/src/terms/power_products.c +++ b/src/terms/power_products.c @@ -865,13 +865,13 @@ bool pprod_equal(pprod_t *p1, pprod_t *p2) { if (p1 == p2) return true; - if (pp_is_var(p1) | pp_is_var(p2)) { + if (pp_is_var(p1) || pp_is_var(p2)) { // p1 and p2 are distinct variables // or only one of them is a variable return false; } - if (pp_is_empty(p1) | pp_is_empty(p2)) { + if (pp_is_empty(p1) || pp_is_empty(p2)) { // one empty and the other is not return false; } From 21159a590646973cc655522af128b1fc169dca9a Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 1 Nov 2023 12:08:56 -0700 Subject: [PATCH 2/3] enable Werror in CI --- .github/actions/build/action.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/actions/build/action.yml b/.github/actions/build/action.yml index 7fefd31a1..f2b6023e5 100644 --- a/.github/actions/build/action.yml +++ b/.github/actions/build/action.yml @@ -42,8 +42,7 @@ runs: shell: bash run: | autoconf - #CFLAGS='-Werror' ${{ inputs.env }} ./configure ${{ inputs.config-opt }} - ${{ inputs.env }} ./configure ${{ inputs.config-opt }} + CFLAGS='-Werror' ${{ inputs.env }} ./configure ${{ inputs.config-opt }} # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default? export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH} make MODE=${{ inputs.mode }} From f627fceeb955382b51c04877b945785327f04948 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Sat, 18 Nov 2023 12:19:15 -0800 Subject: [PATCH 3/3] one more warning fix --- src/mcsat/weq/weak_eq_graph.c | 1 - 1 file changed, 1 deletion(-) diff --git a/src/mcsat/weq/weak_eq_graph.c b/src/mcsat/weq/weak_eq_graph.c index 4232a1618..bc271182e 100644 --- a/src/mcsat/weq/weak_eq_graph.c +++ b/src/mcsat/weq/weak_eq_graph.c @@ -1456,7 +1456,6 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) { bool updates_present = false; uint32_t i; term_table_t* terms = weq->ctx->terms; - composite_term_t* t_desc = NULL; for (i = 0; ok && i < array_terms.size; ++i) { if (!eq_graph_term_has_value(weq->eq_graph, array_terms.data[i])) { ok = false;