Fix ef-solve crash and spurious "model error" on UF-in-arithmetic quantifiers (#657)

ef-solve on a forall body with an uninterpreted-function application inside
arithmetic (e.g. (f x) in (< x C)) crashed, and on release builds aborted with
a bogus "FATAL ERROR: ... model error" bug report. Two independent causes:

- quant_pattern.c walked terms with term_child, which only supports composite
  terms. Arithmetic/bitvector polynomials, products, and projections (which
  term_num_children still counts) hit term_child's composite path and read a
  wrong descriptor -> ASan/debug crash, release UB. Add a shared
  term_ith_subterm() in term_explorer.c that reads those components off the
  descriptor, and use it in the three quant pattern walkers.

- ef_generalize3 built a full model via yices_model_from_map, which rejects
  function-typed existentials. For a problem with an uninterpreted-function
  existential and arithmetic universals (unsupported by projection-based
  generalization) this is now reported as 'unknown' instead of a fatal bug.

Adds regression test tests/regress/efsmt/ef-tests/iss657.ys.

Author: ahmed-irfan

src/exists_forall/efsolver.c

@@ -985,6 +985,28 @@ static term_t ef_generalize2(ef_prob_t *prob, term_t cex_cnstr, uint32_t i, term
 }
 
 
+/*
+ * Check whether constraint i has an existential variable of function type.
+ * Projection-based generalization can't build a concrete model that assigns
+ * such a variable a value, so it can't handle these problems.
+ */
+static bool ef_cnstr_has_function_evar(ef_solver_t *solver, uint32_t i) {
+  ef_cnstr_t *cnstr;
+  term_table_t *terms;
+  uint32_t j, n;
+
+  terms = solver->prob->terms;
+  cnstr = solver->prob->cnstr + i;
+  n = ef_constraint_num_evars(cnstr);
+  for (j=0; j<n; j++) {
+    if (is_function_term(terms, cnstr->evars[j])) {
+      return true;
+    }
+  }
+  return false;
+}
+
+
 /*
  * Option 3: generalize by computing an implicant then
  * applying projection.
@@ -1013,6 +1035,15 @@ static term_t ef_generalize3(ef_solver_t *solver, term_t cex_cnstr, uint32_t i)
   assert(n == solver->all_values.size);
   mdl = yices_model_from_map(n, solver->all_vars.data, solver->all_values.data);
   if (mdl == NULL) {
+    if (ef_cnstr_has_function_evar(solver, i)) {
+      // An existential variable is an uninterpreted function; its value can't be
+      // represented in the concrete map needed for projection, so we can't
+      // refine the exists context and make progress. Report 'unknown' rather
+      // than a spurious bug: this combination of an uninterpreted-function
+      // existential with arithmetic universals is not supported by the ef-solver.
+      solver->status = EF_STATUS_UNKNOWN;
+      return NULL_TERM;
+    }
     // error in the model construction
     solver->status = EF_STATUS_MDL_ERROR;
     solver->error_code = yices_error_code();

src/solvers/quant/quant_pattern.c

@@ -175,7 +175,8 @@ void quant_process_pattern_term(term_table_t *terms, term_t t, ivector_t *pv, iv
   // process all children (if any)
   n = term_num_children(terms, x);
   for(i=0; i<n; i++) {
-    u = term_child(terms, x, i);
+    u = term_ith_subterm(terms, x, i);
+    if (u == NULL_TERM) continue;  // constant monomial of a sum: nothing to recurse into
     quant_process_pattern_term(terms, u, pv, f, fa, c);
   }
 
@@ -236,9 +237,9 @@ void quant_process_pattern_term(term_table_t *terms, term_t t, ivector_t *pv, iv
     break;
 
   default:
-//    printf("Unsupported term (kind %d): ", kind);
-//    yices_pp_term(stdout, x, 120, 1, 0);
-    assert(false);
+    // arithmetic/bitvector operators and atoms and other interpreted terms:
+    // nothing to collect here; their leaves are gathered via the recursion above
+    break;
   }
 }
 
@@ -270,7 +271,8 @@ static bool quant_infer_single_fapps(term_table_t *terms, term_t t, int_hmap_t *
   if (n != 0) {
     init_int_hmap(childMap, 0);
     for(i=0; i<n; i++) {
-      u = term_child(terms, x, i);
+      u = term_ith_subterm(terms, x, i);
+      if (u == NULL_TERM) continue;  // constant monomial of a sum
       int_hmap_reset(childMap);
       skip |= quant_infer_single_fapps(terms, u, childMap, nuvars, out);
 
@@ -304,9 +306,8 @@ static bool quant_infer_single_fapps(term_table_t *terms, term_t t, int_hmap_t *
         break;
 
       default:
-//        printf("Unsupported term (kind %d): ", kind);
-//        yices_pp_term(stdout, x, 120, 1, 0);
-        assert(false);
+        // interpreted operator/atom: do not propagate its variables upward
+        break;
       }
 
     }
@@ -356,9 +357,9 @@ static bool quant_infer_single_fapps(term_table_t *terms, term_t t, int_hmap_t *
     break;
 
   default:
-//    printf("Unsupported term (kind %d): ", kind);
-//    yices_pp_term(stdout, x, 120, 1, 0);
-    assert(false);
+    // interpreted operator/atom: cannot serve as a single-fapp pattern
+    skip = true;
+    break;
   }
 
 #if TRACE
@@ -412,7 +413,8 @@ static bool quant_infer_multi_fapps(term_table_t *terms, term_t t, ptr_hmap_t *u
   n = term_num_children(terms, x);
   if (n != 0) {
     for(i=0; i<n; i++) {
-      u = term_child(terms, x, i);
+      u = term_ith_subterm(terms, x, i);
+      if (u == NULL_TERM) continue;  // constant monomial of a sum
       skip |= quant_infer_multi_fapps(terms, u, uv2fapp, fapp2uv);
     }
   }
@@ -507,9 +509,9 @@ static bool quant_infer_multi_fapps(term_table_t *terms, term_t t, ptr_hmap_t *u
     break;
 
   default:
-//    printf("Unsupported term (kind %d): ", kind);
-//    yices_pp_term(stdout, x, 120, 1, 0);
-    assert(false);
+    // interpreted operator/atom: cannot host multi-fapp mappings
+    skip = true;
+    break;
   }
 
   return skip;

src/terms/term_explorer.c

@@ -484,6 +484,48 @@ term_t term_child(term_table_t *table, term_t t, uint32_t i) {
 }
 
 
+/*
+ * i-th subterm of t (see header): like term_child, but also supports the
+ * arithmetic/bitvector sums, products, and projections that term_num_children
+ * counts. Reads their components straight from the descriptor (no coefficient
+ * is materialized). Returns NULL_TERM for a sum's constant monomial.
+ */
+term_t term_ith_subterm(term_table_t *table, term_t t, uint32_t i) {
+  term_t v;
+
+  assert(good_term(table, t) && i < term_num_children(table, t));
+
+  if (is_neg_term(t)) {
+    return term_child(table, t, i); // (not u): a single child u
+  }
+
+  switch (term_kind(table, t)) {
+  case ARITH_POLY:
+    v = poly_term_desc(table, t)->mono[i].var;
+    break;
+  case ARITH_FF_POLY:
+    v = finitefield_poly_term_desc(table, t)->mono[i].var;
+    break;
+  case BV64_POLY:
+    v = bvpoly64_term_desc(table, t)->mono[i].var;
+    break;
+  case BV_POLY:
+    v = bvpoly_term_desc(table, t)->mono[i].var;
+    break;
+  case POWER_PRODUCT:
+    return pprod_term_desc(table, t)->prod[i].var;
+  case SELECT_TERM:
+  case BIT_TERM:
+    return proj_term_arg(table, t);
+  default:
+    return term_child(table, t, i);
+  }
+
+  // sums store their constant with variable const_idx: no subterm to recurse into
+  return (v == const_idx) ? NULL_TERM : v;
+}
+
+
 /*
  * All children of t:
  * - t must be a valid term in table

src/terms/term_explorer.h

@@ -82,6 +82,18 @@ extern uint32_t term_num_children(term_table_t *table, term_t t);
 extern term_t term_child(term_table_t *table, term_t t, uint32_t i);
 
 
+/*
+ * i-th subterm of t, for a generic recursive term traversal.
+ * - t must be a valid term in table; i must be in [0 ... n-1] where
+ *   n = term_num_children(table, t)
+ * Unlike term_child, this also handles the kinds that term_num_children counts
+ * but term_child does not: arithmetic/bitvector sums, products, and projections
+ * (select/bit). For every other kind it behaves exactly like term_child.
+ * - returns NULL_TERM for the constant monomial of a sum (no subterm there)
+ */
+extern term_t term_ith_subterm(term_table_t *table, term_t t, uint32_t i);
+
+
 /*
  * All children of t:
  * - t must be a valid term in table

tests/regress/efsmt/ef-tests/iss657.ys

@@ -0,0 +1,8 @@
+;; Issue #657: ef-solve on a problem with an uninterpreted-function
+;; existential (cryWidthUnknown) and an arithmetic universal (x).
+;; This combination is not supported by the projection-based ef-solver, so
+;; the expected answer is 'unknown'. It used to crash / report a spurious bug.
+(define cryWidthUnknown::(-> int int))
+(define k_2_to_64::int 18446744073709551616)
+(assert (forall (x::int) (or (> (cryWidthUnknown x) 64) (< x k_2_to_64))))
+(ef-solve)

tests/regress/efsmt/ef-tests/iss657.ys.gold

@@ -0,0 +1 @@
+unknown

tests/regress/efsmt/ef-tests/iss657.ys.options

@@ -0,0 +1 @@
+--mode=ef