From ed02b9d23a148d6d411ed5f1936a4e7704a6bdd7 Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Wed, 17 Apr 2024 19:22:33 -0700
Subject: [PATCH] add method to provide value hint

---
 src/mcsat/nra/nra_plugin.c |  1 +
 src/mcsat/plugin.h         |  3 +++
 src/mcsat/solver.c         | 10 ++++++++++
 3 files changed, 14 insertions(+)

diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c
index 21e2f2e31..978ff374d 100644
--- a/src/mcsat/nra/nra_plugin.c
+++ b/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);
         }
       }
     }
diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h
index 685dbedce..88ceded83 100644
--- a/src/mcsat/plugin.h
+++ b/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 */
diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 51ba2fc98..c8fc0de45 100644
--- a/src/mcsat/solver.c
+++ b/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;
 }