improved check for all assigned

src/mcsat/uf/uf_plugin.c

@@ -373,25 +373,7 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
 
   // optimization: skip array checks if some terms, that are present
   // in the eq_graph, don't have an assigned value.
-  variable_db_t* var_db = uf->ctx->var_db;
-  term_t t = NULL_TERM;
-  bool all_assigned = true;
-  int_hmap_pair_t* it;
-  for (it = int_hmap_first_record(&var_db->term_to_variable_map);
-       it != NULL;
-       it = int_hmap_next_record(&var_db->term_to_variable_map, it)) {
-    t = it->key;
-    if (t >= 0 && eq_graph_has_term(&uf->eq_graph, t)) {
-      variable_t t_var = variable_db_get_variable_if_exists(var_db, t);
-      assert(t_var != variable_null);
-      if (!trail_has_value(uf->ctx->trail, t_var)) {
-        all_assigned = false;
-        break;
-      }
-    }
-  }
-
-  if (all_assigned) {
+  if (weq_graph_is_all_assigned(&uf->weq_graph)) {
     assert(uf->conflict.size == 0);
     weq_graph_check_array_conflict(&uf->weq_graph, &uf->conflict);
     if (uf->conflict.size > 0) {

src/mcsat/weq/weak_eq_graph.c

@@ -1373,6 +1373,26 @@ void filter_select_terms(const weq_graph_t* weq,
   delete_int_hset(&array_terms_set);
 }
 
+/* Returns true if all the select terms and arrays terms are fully
+ * assigned, otherwise returns false.
+ */
+bool weq_graph_is_all_assigned(weq_graph_t* weq) {
+  uint32_t i;
+  for (i = 0; i < weq->array_terms.size; ++i) {
+    if (!weq_is_fully_assigned(weq, weq->array_terms.data[i])) {
+      return false;
+    }
+  }
+
+  for (i = 0; i < weq->select_terms.size; ++i) {
+    if (!weq_is_fully_assigned(weq, weq->select_terms.data[i])) {
+      return false;
+    }
+  }
+
+  return true;
+}
+
 /* The main method to check array conflicts. The conflict vector will
  * contain conflicting terms if an array conflict is found. It assumes
  * that all terms (assignable) present in the array_terms and

src/mcsat/weq/weak_eq_graph.h

@@ -111,6 +111,9 @@ void weq_graph_clear(weq_graph_t* weq);
 /** Return array update index lemma term */
 term_t weq_graph_get_array_update_idx_lemma(weq_graph_t* weq, term_t update_term);
 
+/** Check if all select and arrays terms are fully assigned */
+bool weq_graph_is_all_assigned(weq_graph_t* weq);
+
 /** Check for array conflicts */
 void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict);