From ea1529e2642188cc88013186e06530357d678ecd Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 13 Jun 2024 00:22:40 -0700 Subject: [PATCH] propagate at base level --- src/mcsat/bv/bv_plugin.c | 50 +++++++++++++++++++++++----------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/src/mcsat/bv/bv_plugin.c b/src/mcsat/bv/bv_plugin.c index 2b234a48d..b98944e50 100644 --- 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); } } }