more decision hints

src/mcsat/nra/nra_plugin.c

@@ -860,6 +860,7 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
         }
         lp_value_destruct(&v);
       }
+
       if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x)) {
         const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x);
         if (lp_feasibility_set_is_point(feasible_set)) {
@@ -880,6 +881,25 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
             }
           }
           lp_value_destruct(&x_value);
+
+        } else if (variable_db_is_int(nra->ctx->var_db, x) &&
+                   !lp_feasibility_set_is_full(feasible_set)) {
+          lp_interval_t x_interval;
+          lp_interval_construct_full(&x_interval);
+          feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval);
+          int interval_dist = lp_interval_size_approx(&x_interval);
+          if (0 < interval_dist && interval_dist <= 1) {
+            // interval distance 1 means that the absolute distance
+            // between the upper and lower bound is 1.
+            // interval distance 0 means that the interval is a point.
+            // So, we are hinting to the main mcsat solver to decide on this variable
+            // as the possible integer values for the variable is highly likely one.
+            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);
+          }
+          lp_interval_destruct(&x_interval);
         }
       }
     }