add method to provide value hint

src/mcsat/nra/nra_plugin.c

@@ -2186,6 +2186,7 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
             ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var);
           }
           nra->ctx->hint_next_decision(nra->ctx, constraint_var);
+          nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value);
         }
       }
     }

src/mcsat/plugin.h

@@ -116,6 +116,9 @@ struct plugin_context_s {
   /** Request a variable to be a next decision variable */
   void (*hint_next_decision) (plugin_context_t* self, variable_t x);
 
+  /** Add model value hint in the value cache */
+  void (*hint_value) (plugin_context_t* self, variable_t x, const mcsat_value_t* val);
+
 };
 
 /** Token to add entries to the trail */

src/mcsat/solver.c

@@ -707,6 +707,15 @@ void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t
   mcsat_add_decision_hint(mctx->mcsat, x);
 }
 
+static
+void mcsat_plugin_context_hint_value(plugin_context_t* self, variable_t x, const mcsat_value_t* val) {
+  mcsat_plugin_context_t* mctx;
+  mctx = (mcsat_plugin_context_t*) self;
+  if (!trail_has_value(mctx->mcsat->trail, x)) {
+    mcsat_model_set_value(&mctx->mcsat->trail->model, x, val);
+  }
+}
+
 static
 void mcsat_plugin_context_decision_calls(plugin_context_t* self, type_kind_t type) {
   mcsat_plugin_context_t* mctx;
@@ -738,6 +747,7 @@ void mcsat_plugin_context_construct(mcsat_plugin_context_t* ctx, mcsat_solver_t*
   ctx->ctx.cmp_variables = mcsat_plugin_context_cmp_variables;
   ctx->ctx.request_top_decision = mcsat_plugin_context_request_top_decision;
   ctx->ctx.hint_next_decision = mcsat_plugin_context_hint_next_decision;
+  ctx->ctx.hint_value = mcsat_plugin_context_hint_value;
   ctx->mcsat = mcsat;
   ctx->plugin_name = plugin_name;
 }