From 1ae6ec66f582e1a1673f012db378608aa54b9bd9 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 11 Dec 2024 11:53:55 -0800 Subject: [PATCH] Update nra_plugin.c (#543) --- src/mcsat/nra/nra_plugin.c | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 7bdbb6a97..64758c87a 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -802,7 +802,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, // We don't do any hinting for complicated algebraic values if (lp_value_is_rational(&x_value)) { - if (lp_feasibility_set_is_point(feasible_set)) { + if (lp_feasibility_set_is_point(feasible_set) || (x_is_int_var && lp_feasibility_set_is_point_int(feasible_set))) { if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) { mcsat_value_t value; mcsat_value_construct_lp_value(&value, &x_value); @@ -814,13 +814,6 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } nra->ctx->hint_next_decision(nra->ctx, x); } - } else if (x_is_int_var && lp_feasibility_set_is_point_int(feasible_set)) { - // hint integer variable; - // a good candidate for next decision as the feasibility set contains a single integer solution - if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { - ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x); - } - nra->ctx->hint_next_decision(nra->ctx, x); } else if (!lp_feasibility_set_is_full(feasible_set)) { lp_interval_t x_interval; lp_interval_construct_full(&x_interval); // [-inf, +inf]