propagate at base level

SRI-CSL · Jun 13, 2024 · ea1529e · ea1529e
1 parent f067614
commit ea1529e
Showing 1 changed file with 29 additions and 21 deletions.
diff --git a/src/mcsat/bv/bv_plugin.c b/src/mcsat/bv/bv_plugin.c
@@ -709,30 +709,38 @@ void bv_plugin_process_unit_constraint(bv_plugin_t* bv, trail_token_t* prop, var
       uint32_t x_bitsize = bv_term_bitsize(ctx->terms, x_term);
       bool is_fixed = bv_bdd_manager_bdd_is_point(bddm, feasible, x_bitsize);
       if (is_fixed) {
-        bool is_boolean = variable_db_get_type_kind(var_db, x) == BOOL_TYPE;
-        bvconstant_t x_bv_value;
-        init_bvconstant(&x_bv_value);
-        bvconstant_set_bitsize(&x_bv_value, x_bitsize);
-        bv_bdd_manager_pick_value(bddm, x_term, feasible, &x_bv_value);
-        if (ctx_trace_enabled(ctx, "mcsat::bv::propagate")) {
-          ctx_trace_printf(ctx, "propagating value for :\n");
-          ctx_trace_term(ctx, x_term);
-        }
-
-        int_hmap_pair_t* find = int_hmap_get(&bv->variable_propagation_type, x);
-        find->val = BV_PROP_SINGLETON;
-        (*bv->stats.propagations) ++;
+        if (trail_is_at_base_level(bv->ctx->trail)) {
+          bool is_boolean = variable_db_get_type_kind(var_db, x) == BOOL_TYPE;
+          bvconstant_t x_bv_value;
+          init_bvconstant(&x_bv_value);
+          bvconstant_set_bitsize(&x_bv_value, x_bitsize);
+          bv_bdd_manager_pick_value(bddm, x_term, feasible, &x_bv_value);
+          if (ctx_trace_enabled(ctx, "mcsat::bv::propagate")) {
+            ctx_trace_printf(ctx, "propagating value for :\n");
+            ctx_trace_term(ctx, x_term);
+          }
 
-        if (is_boolean) {
-          bool x_value = bvconst_tst_bit(x_bv_value.data, 0);
-          prop->add(prop, x, x_value ? &mcsat_value_true : &mcsat_value_false);
+          int_hmap_pair_t* find = int_hmap_get(&bv->variable_propagation_type, x);
+          find->val = BV_PROP_SINGLETON;
+          (*bv->stats.propagations) ++;
+
+          if (is_boolean) {
+            bool x_value = bvconst_tst_bit(x_bv_value.data, 0);
+            prop->add(prop, x, x_value ? &mcsat_value_true : &mcsat_value_false);
+          } else {
+            mcsat_value_t x_value;
+            mcsat_value_construct_bv_value(&x_value, &x_bv_value);
+            prop->add(prop, x, &x_value);
+            mcsat_value_destruct(&x_value);
+          }
+          delete_bvconstant(&x_bv_value);
         } else {
-          mcsat_value_t x_value;
-          mcsat_value_construct_bv_value(&x_value, &x_bv_value);
-          prop->add(prop, x, &x_value);
-          mcsat_value_destruct(&x_value);
+          if (ctx_trace_enabled(ctx, "mcsat::bv::propagate")) {
+            ctx_trace_printf(ctx, "hinting variable :\n");
+            ctx_trace_term(ctx, x_term);
+          }
+	  bv->ctx->hint_next_decision(bv->ctx, x);
         }
-        delete_bvconstant(&x_bv_value);
       }
     }
   }