mcsat arrays finite (#442)

* mcsat arrays finite extra read term is only added if the index is finite * add new test; disabled old test
SRI-CSL · Apr 29, 2023 · 5c440f4 · 5c440f4
1 parent 6e5b85a
commit 5c440f4
Show file tree

Hide file tree

Showing 4 changed files with 4,203 additions and 4 deletions.
diff --git a/src/mcsat/uf/uf_plugin.c b/src/mcsat/uf/uf_plugin.c
@@ -233,10 +233,12 @@ void uf_plugin_add_to_eq_graph(uf_plugin_t* uf, term_t t, bool record) {
     term_t r1 = app_term(terms, t, t_desc->arity - 2, t_desc->arg + 1);
     variable_db_get_variable(uf->ctx->var_db, r1);
     weq_graph_add_select_term(&uf->weq_graph, r1);
-    // TODO: can we check if the domain is finite? if so, we can guard this extra select term
-    term_t r2 = app_term(terms, t_desc->arg[0], t_desc->arity - 2, t_desc->arg + 1);
-    variable_db_get_variable(uf->ctx->var_db, r2);
-    weq_graph_add_select_term(&uf->weq_graph, r2);
+    // if the domain is finite then we add this extra read term
+    if (is_finite_type(terms->types, term_type(terms, t_desc->arg[1]))) {
+      term_t r2 = app_term(terms, t_desc->arg[0], t_desc->arity - 2, t_desc->arg + 1);
+      variable_db_get_variable(uf->ctx->var_db, r2);
+      weq_graph_add_select_term(&uf->weq_graph, r2);
+    }
     break;
   case ARITH_RDIV:
     t_desc = arith_rdiv_term_desc(terms, t);