From 9d6a5320bec8e7d09ae73ea05b3c2cbd29267488 Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <ahmed.irfan@sri.com>
Date: Fri, 15 Nov 2024 12:07:48 -0800
Subject: [PATCH] clear all caches before setting hints

---
 src/mcsat/solver.c |  2 +-
 src/mcsat/trail.c  | 14 ++++++++++++++
 src/mcsat/trail.h  |  3 +++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c
index 9c2e4d2f3..e028ade67 100644
--- a/src/mcsat/solver.c
+++ b/src/mcsat/solver.c
@@ -2654,7 +2654,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
 
   value_table_t* vtbl = model_get_vtbl(mdl);
 
-  trail_clear_extra_cache(mcsat->trail);
+  trail_clear_cache(mcsat->trail);
   trail_update_extra_cache(mcsat->trail);
 
   for (uint32_t i = 0; i < n_mdl_filter; ++i) {
diff --git a/src/mcsat/trail.c b/src/mcsat/trail.c
index 025ec0c28..4660a0422 100644
--- a/src/mcsat/trail.c
+++ b/src/mcsat/trail.c
@@ -381,6 +381,15 @@ void trail_copy_unassigned_cache(mcsat_trail_t* trail, mcsat_model_t* to_cache,
   }
 }
 
+inline static
+void trail_clear_unassigned_cache(mcsat_trail_t* trail, mcsat_model_t* cache) {
+  for (variable_t var = 0; var < cache->size; ++var) {
+    if (!trail_has_value(trail, var) && mcsat_model_get_value(cache, var)->type != VALUE_NONE) {
+      mcsat_model_unset_value(cache, var);
+    }
+  }
+}
+
 inline static
 void trail_clear_unassigned_bool_cache(mcsat_trail_t* trail, mcsat_model_t* cache) {
   for (variable_t var = 0; var < cache->size; ++var) {
@@ -449,3 +458,8 @@ void trail_clear_extra_cache(mcsat_trail_t* trail) {
   trail->target_depth = 0;
   trail->best_depth = 0;
 }
+
+void trail_clear_cache(mcsat_trail_t* trail) {
+  trail_clear_unassigned_cache(trail, &trail->model);
+  trail_clear_extra_cache(trail);
+}
diff --git a/src/mcsat/trail.h b/src/mcsat/trail.h
index 24a6d216a..ad10b2431 100644
--- a/src/mcsat/trail.h
+++ b/src/mcsat/trail.h
@@ -301,4 +301,7 @@ void trail_update_extra_cache(mcsat_trail_t* trail);
 /** clear target/best cache */
 void trail_clear_extra_cache(mcsat_trail_t* trail);
 
+/** clear all caches */
+void trail_clear_cache(mcsat_trail_t* trail);
+
 #endif /* MCSAT_TRAIL_H_ */