Decision hint queue

src/exists_forall/ef_values.c

@@ -557,7 +557,7 @@ void postprocess_ef_table(ef_table_t *vtable, bool check) {
       }
     }
   }
-  m = queue.size;
+  m = queue.capacity;
   j = 0;
   while(!int_queue_is_empty(&queue)) {
     tvalue = int_queue_pop(&queue);

src/mcsat/nra/nra_plugin.c

@@ -860,18 +860,24 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop,
         }
         lp_value_destruct(&v);
       }
-      // If the value is implied at zero level, propagate it
-      if (!nra->ctx->options->model_interpolation && !x_in_conflict && !trail_has_value(nra->ctx->trail, x) && trail_is_at_base_level(nra->ctx->trail)) {
-        const lp_feasibility_set_t* feasible = feasible_set_db_get(nra->feasible_set_db, x);
-        if (lp_feasibility_set_is_point(feasible)) {
+      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)) {
           lp_value_t x_value;
           lp_value_construct_none(&x_value);
-          lp_feasibility_set_pick_value(feasible, &x_value);
+          lp_feasibility_set_pick_value(feasible_set, &x_value);
           if (lp_value_is_rational(&x_value)) {
-            mcsat_value_t value;
-            mcsat_value_construct_lp_value(&value, &x_value);
-            prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base);
-            mcsat_value_destruct(&value);
+            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);
+              prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base);
+              mcsat_value_destruct(&value);
+            } else {
+              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);
         }
@@ -1069,7 +1075,7 @@ void nra_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
   }
 
   // Propagate
-  while(trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) {
+  while (trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) {
     // Current trail element
     var = trail_at(trail, nra->trail_i);
     nra->trail_i ++;

src/mcsat/plugin.h

@@ -113,6 +113,9 @@ struct plugin_context_s {
   /** Request a variable to be a top decision variable */
   void (*request_top_decision) (plugin_context_t* self, variable_t x);
 
+  /** Request a variable to be a next decision variable */
+  void (*hint_next_decision) (plugin_context_t* self, variable_t x);
+
 };
 
 /** Token to add entries to the trail */
@@ -334,10 +337,9 @@ void plugin_construct(plugin_t* plugin) {
   plugin->pop                       = NULL;
   plugin->build_model               = NULL;
   plugin->gc_mark                   = NULL;
-  plugin->gc_mark_and_clear          = NULL;
+  plugin->gc_mark_and_clear         = NULL;
   plugin->gc_sweep                  = NULL;
   plugin->set_exception_handler     = NULL;
 }
 
-
 #endif /* PLUGIN_H_ */