fixes #414

src/context/context.c

@@ -2550,6 +2550,7 @@ static literal_t map_bit_select_to_literal(context_t *ctx, select_term_t *select
 
 static occ_t internalize_to_eterm(context_t *ctx, term_t t) {
   term_table_t *terms;
+  term_t root;
   term_t r;
   uint32_t polarity;
   int32_t code;
@@ -2564,9 +2565,10 @@ static occ_t internalize_to_eterm(context_t *ctx, term_t t) {
     goto abort;
   }
 
-  r = intern_tbl_get_root(&ctx->intern, t);
-  polarity = polarity_of(r);
-  r  = unsigned_term(r);
+  root = intern_tbl_get_root(&ctx->intern, t);
+  polarity = polarity_of(root);
+  root = unsigned_term(root);
+  r = root;
 
   /*
    * r is a positive root in the internalization table
@@ -2589,6 +2591,28 @@ static occ_t internalize_to_eterm(context_t *ctx, term_t t) {
      */
     terms = ctx->terms;
     tau = type_of_root(ctx, r);
+    if (is_unit_type(ctx->types, tau)) {
+      // Canonicalize singleton types to one representative term.
+      r = get_unit_type_rep(terms, tau);
+      r = intern_tbl_get_root(&ctx->intern, r);
+      r = unsigned_term(r);
+      assert(is_pos_term(r) && intern_tbl_is_root(&ctx->intern, r));
+      if (intern_tbl_root_is_mapped(&ctx->intern, r)) {
+        code = intern_tbl_map_of_root(&ctx->intern, r);
+        u = translate_code_to_eterm(ctx, r, code);
+        if (root != r) {
+          if (intern_tbl_root_is_free(&ctx->intern, root)) {
+            intern_tbl_map_root(&ctx->intern, root, occ2code(u));
+          } else {
+            // If root is already mapped, it must map to the same egraph
+            // occurrence we are about to return for the unit-type rep.
+            assert(intern_tbl_map_of_root(&ctx->intern, root) == occ2code(u));  // LCOV_EXCL_LINE - consistency check, unreachable on well-formed inputs
+          }
+        }
+        return u ^ polarity;
+      }
+    }
+
     if (is_boolean_type(tau)) {
       l = internalize_to_literal(ctx, r);
       u = egraph_literal2occ(ctx->egraph, l);
@@ -2765,6 +2789,19 @@ static occ_t internalize_to_eterm(context_t *ctx, term_t t) {
     }
   }
 
+  // If we canonicalized root to a different unit-type representative r,
+  // remember that root internalizes to the same egraph occurrence.
+  if (root != r) {
+    if (intern_tbl_root_is_free(&ctx->intern, root)) {
+      intern_tbl_map_root(&ctx->intern, root, occ2code(u));
+    } else {
+      // If root was mapped during the recursive internalization of r (e.g.,
+      // because root was reached as a sub-term), the mapping must agree
+      // with the occurrence we are about to return.
+      assert(intern_tbl_map_of_root(&ctx->intern, root) == occ2code(u));  // LCOV_EXCL_LINE - consistency check, unreachable on well-formed inputs
+    }
+  }
+
   // fix the polarity
   return u ^ polarity;
 

src/frontend/smt2/smt2_printer.c

@@ -64,33 +64,6 @@ static void smt2_pp_bitvector(smt2_pp_t *printer, value_bv_t *b) {
   }
 }
 
-/*
- * Expand an update and copy its mappings into a private array.
- * The expansion uses table->hset1 as scratch space, which is not reentrant.
- * Copying the map ids avoids corruption if printing recursively expands updates.
- */
-static value_t *copy_update_maps(value_table_t *table, value_t c, value_t *def, type_t *tau, uint32_t *n) {
-  map_hset_t *hset;
-  value_t *maps;
-  uint32_t i;
-
-  vtbl_expand_update(table, c, def, tau);
-  hset = table->hset1;
-  assert(hset != NULL);
-
-  *n = hset->nelems;
-  if (*n == 0) {
-    return NULL;
-  }
-
-  maps = (value_t *) safe_malloc(*n * sizeof(value_t));
-  for (i = 0; i < *n; ++i) {
-    maps[i] = hset->data[i];
-  }
-
-  return maps;
-}
-
 
 /*
  * SMT2 format for integer and rational constants
@@ -305,7 +278,7 @@ void smt2_normalize_and_pp_update(smt2_pp_t *printer, value_table_t *table, valu
   type_t tau;
   uint32_t i, j, n, m;
 
-  maps = copy_update_maps(table, c, &def, &tau, &n);
+  maps = vtbl_copy_update_maps(table, c, &def, &tau, &n);
 
   smt2_pp_function_header(printer, table, c, tau);
 
@@ -447,7 +420,7 @@ static void smt2_pp_array_update(smt2_pp_t *printer, value_table_t *table, value
   type_t tau, range, sigma;
   uint32_t i, j, n, m;
 
-  maps = copy_update_maps(table, c, &def, &tau, &n);
+  maps = vtbl_copy_update_maps(table, c, &def, &tau, &n);
 
   types = table->type_table;
 
@@ -602,7 +575,7 @@ static void smt2_pp_update_definition(smt2_pp_t *printer, value_table_t *table,
   type_t tau, range;
   uint32_t i, n;
 
-  maps = copy_update_maps(table, c, &def, &tau, &n);
+  maps = vtbl_copy_update_maps(table, c, &def, &tau, &n);
 
   range = function_type_range(table->type_table, tau);
 

src/io/concrete_value_printer.c

@@ -30,39 +30,6 @@
 #include "utils/memalloc.h"
 
 
-/*
- * Expand update c and copy the resulting mapping list out of the shared
- * scratch map_hset (table->hset1). Callers must free the returned array
- * with safe_free.
- *
- * vtbl_expand_update uses table->hset1 as scratch, so if the caller later
- * recursively prints another value that expands a different update, hset1
- * would be clobbered. Copying the map ids avoids this reentrancy hazard.
- *
- * Returns NULL when *n == 0.
- */
-static value_t *copy_update_maps(value_table_t *table, value_t c, value_t *def, type_t *tau, uint32_t *n) {
-  map_hset_t *hset;
-  value_t *maps;
-  uint32_t i;
-
-  vtbl_expand_update(table, c, def, tau);
-  hset = table->hset1;
-  assert(hset != NULL);
-
-  *n = hset->nelems;
-  if (*n == 0) {
-    return NULL;
-  }
-
-  maps = (value_t *) safe_malloc(*n * sizeof(value_t));
-  for (i = 0; i < *n; ++i) {
-    maps[i] = hset->data[i];
-  }
-  return maps;
-}
-
-
 /*
  * Printing for each object type
  */
@@ -315,7 +282,7 @@ void vtbl_normalize_and_print_update(FILE *f, value_table_t *table, const char *
   type_t tau;
   uint32_t i, j, n, m;
 
-  maps = copy_update_maps(table, c, &def, &tau, &n);
+  maps = vtbl_copy_update_maps(table, c, &def, &tau, &n);
 
   if (name == NULL) {
     sprintf(fake_name, "fun!%"PRId32, c);
@@ -601,7 +568,7 @@ void vtbl_normalize_and_pp_update(yices_pp_t *printer, value_table_t *table, con
   type_t tau;
   uint32_t i, j, n, m;
 
-  maps = copy_update_maps(table, c, &def, &tau, &n);
+  maps = vtbl_copy_update_maps(table, c, &def, &tau, &n);
 
   if (name == NULL) {
     sprintf(fake_name, "fun!%"PRId32, c);

src/mcsat/preprocessor.c

@@ -170,6 +170,52 @@ composite_term_t* get_composite(term_table_t* terms, term_kind_t kind, term_t t)
   }
 }
 
+static bool type_needs_function_diseq_guard(type_table_t* types, type_t tau) {
+  uint32_t i, n;
+
+  switch (type_kind(types, tau)) {
+  case FUNCTION_TYPE:
+    if (type_has_finite_domain(types, tau) ||
+        is_unit_type(types, function_type_range(types, tau))) {
+      return true;
+    }
+
+    n = function_type_arity(types, tau);
+    for (i = 0; i < n; ++ i) {
+      if (type_needs_function_diseq_guard(types, function_type_domain(types, tau, i))) {
+        return true;
+      }
+    }
+
+    return type_needs_function_diseq_guard(types, function_type_range(types, tau));
+
+  case TUPLE_TYPE:
+    n = tuple_type_arity(types, tau);
+    for (i = 0; i < n; ++ i) {
+      if (type_needs_function_diseq_guard(types, tuple_type_component(types, tau, i))) {
+        return true;
+      }
+    }
+    return false;
+
+  case INSTANCE_TYPE:
+    n = instance_type_arity(types, tau);
+    for (i = 0; i < n; ++ i) {
+      if (type_needs_function_diseq_guard(types, instance_type_param(types, tau, i))) {
+        return true;
+      }
+    }
+    return false;
+
+  default:
+    return false;
+  }
+}
+
+static bool term_needs_function_diseq_guard(term_table_t* terms, term_t t) {
+  return type_needs_function_diseq_guard(terms->types, term_type(terms, t));
+}
+
 static
 term_t mk_composite(preprocessor_t* pre, term_kind_t kind, uint32_t n, term_t* children) {
   term_manager_t* tm = &pre->tm;
@@ -504,13 +550,13 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
 
       n = desc->arity;
 
-      /*
-      // Arrays not supported yet
-      if (current_kind == EQ_TERM && term_type_kind(terms, desc->arg[0]) == FUNCTION_TYPE) {
+      // MCSAT does not yet enforce all extensionality/cardinality constraints
+      // for function-sort disequalities. Reject equality atoms whose type needs
+      // that monitoring; the Boolean abstraction may assert them either way.
+      if (current_kind == EQ_TERM && term_needs_function_diseq_guard(terms, desc->arg[0])) {
         longjmp(*pre->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY);
       }
-      */
-
+
       // Is this a top-level equality assertion
       bool is_equality =
           current_kind == EQ_TERM ||
@@ -1104,6 +1150,14 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
       bool children_done = true;
       n = desc->arity;
 
+      // DISTINCT_TERM is lowered below into pairwise disequalities. Apply the
+      // same function-sort guard before that expansion.
+      for (i = 0; i < n; ++ i) {
+        if (term_needs_function_diseq_guard(terms, desc->arg[i])) {
+          longjmp(*pre->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY);
+        }
+      }
+
       ivector_t children;
       init_ivector(&children, n);