Merge branch 'master' into fix-some-printing

.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 }}

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 ++;
   }
 

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

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);
     }
   }
@@ -2553,6 +2551,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
     assert(x_value >= 0);
     trail_add_propagation(mcsat->trail, x_var, &value, plugin_i, mcsat->trail->decision_level);
     mcsat_value_destruct(&value);
+    mcsat_process_registeration_queue(mcsat);
   }
 
   mcsat_pop(mcsat);

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;

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

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

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);
 }
 
 /*

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);

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;
   }

tests/api/test_model_hint.c

@@ -32,6 +32,23 @@ static context_t *make_mcsat_context(void) {
   return NULL;
 }
 
+static term_t make_simple_eq_constraint(term_t var[2]) {
+  type_t integer;
+  term_t x, y, p;
+
+  integer = yices_int_type();
+  x = yices_new_uninterpreted_term(integer);
+  yices_set_term_name(x, "x");
+  y = yices_new_uninterpreted_term(integer);
+  yices_set_term_name(y, "y");
+
+  var[0] = x;
+  var[1] = y;
+
+  p = yices_arith_eq_atom(x, y); // p is x = y
+  return p;
+}
+
 /*
  * Create assertion x^2 + y^2 < 1
  * - return terms x and y in var:
@@ -208,11 +225,36 @@ static void check_unsat_with_model(bool use_hint) {
   yices_free_context(ctx);
 }
 
+void check_simple() {
+  context_t *ctx;
+  model_t *model;
+  term_t vars[2];
+  term_t assertion;
+  int32_t code;
+
+  ctx = make_mcsat_context();
+  assertion = make_simple_eq_constraint(vars);
+
+  model = yices_new_model();
+  code = yices_model_set_int32(model, vars[1], 4);
+  if (code < 0) {
+    yices_print_error(stderr);
+    exit(1);
+  }
+
+  smt_status_t status;
+  status = check_with_model_and_hint(ctx, model, assertion, 1, vars, 0);
+  assert(status == STATUS_SAT);
+
+  yices_free_model(model);
+  yices_free_context(ctx);
+}
 
 int main(void) {  
   yices_init();
   if (yices_has_mcsat()) {
     printf("MCSAT supported\n");
+    check_simple();
     check_with_sat_model(false);
     check_with_sat_model(true);
     check_with_unsat_model(false);