From f4f5978d415c22e19caf5eb795c87201b0c3038b Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Tue, 12 Nov 2024 18:35:50 -0800
Subject: [PATCH] reintroduce interval approx hints (#537)

---
 src/mcsat/nra/nra_plugin.c | 30 ++++++++++++++++++++++++++++--
 1 file changed, 28 insertions(+), 2 deletions(-)

diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
index 6acdc476e..7bdbb6a97 100644
--- a/src/mcsat/nra/nra_plugin.c
+++ b/src/mcsat/nra/nra_plugin.c
@@ -814,13 +814,39 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
           }
           nra->ctx->hint_next_decision(nra->ctx, x);
         }
-      } else if (lp_feasibility_set_is_point_int(feasible_set)) {
-        // hint integer (also real) variable; 
+      } 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]
+        // now we over-approx the feasible set using an interval and
+        // the result is stored in x_interval, e.g., [1.6, 2.5]
+        // union [4.2, 4.6] is approximated by [1.6, 4.6].
+        feasible_set_db_approximate_value(nra->feasible_set_db, x, &x_interval);
+        int interval_dist = lp_interval_size_approx(&x_interval);
+        if (interval_dist <= 1) {
+          // interval distance of an interval [a, b] is defined as log2(|b - a|) + 1.
+          // interval distance 1 means that the absolute log2 distance
+          // between the upper and lower bound is 1.
+          // Consider the the interval [3,4], the interval distance is 1, and has
+          // two integer value: 3 and 4.
+          // Now consider the interval [5.5, 6.1], the interval distance is 0 and
+          // has one integer value: 6. log2(.6) = log2(6) - log2(10).
+          // Here, 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 (lp_value_is_integer(&x_value)) {
+            // it is good idea to decide on this variable (integers or reals)
+            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_value_destruct(&x_value);