30150074613

Committed 25 Jul 2026 07:51AM UTC coverage: 71.208% (+0.001%) from 71.207%

Build # 30150074613

Build Type

push

github

Committed by

web-flow

Commit Message

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

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.

Coverage Stats

29 of 46 new or added lines in 3 files covered. (63.04%)

1 existing line in 1 file now uncovered.

95573 of 134216 relevant lines covered (71.21%)

1669601.34 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

93.6

/src/solvers/quant/quant_pattern.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * QUANTIFIER PATTERNS
 */

#if defined(CYGWIN) || defined(MINGW)
#define EXPORTED __declspec(dllexport)
#define __YICES_DLLSPEC__ EXPORTED
#else
#define EXPORTED __attribute__((visibility("default")))
#endif

#include "solvers/quant/quant_pattern.h"
#include "utils/index_vectors.h"
#include "terms/term_explorer.h"
#include "yices.h"

#define TRACE 0

#if TRACE

#include <stdio.h>

#include "solvers/cdcl/smt_core_printer.h"
#include "solvers/egraph/egraph_printer.h"

#endif



/*******************
 *  PATTERN TABLE  *
 ******************/

/*
 * Make the table 50% larger
 */
static void extend_pattern_table(pattern_table_t *table) {
  uint32_t n;

  n = table->size + 1;
  n += n>>1;
  if (n >= MAX_PATTERN_TABLE_SIZE) {
    out_of_memory();
  }
  table->data = (pattern_t *) safe_realloc(table->data, n * sizeof(pattern_t));
  table->size = n;
}


/*
 * Remove all patterns of index >= n
 */
static void shrink_pattern_table(pattern_table_t *table, uint32_t n) {
  uint32_t i;
  pattern_t *pat;

  assert(n <= table->npatterns);

  for(i=n; i<table->npatterns; i++) {
    pat = table->data + i;
    delete_index_vector(pat->pvars);
    delete_index_vector(pat->fun);
    delete_index_vector(pat->fapps);
    delete_index_vector(pat->consts);

    delete_ivector(&pat->matches);
  }

  table->npatterns = n;
}


/*
 * Initialize: default size
 */
void init_pattern_table(pattern_table_t *table) {
  assert(DEF_PATTERN_TABLE_SIZE < MAX_PATTERN_TABLE_SIZE);

  table->size = DEF_PATTERN_TABLE_SIZE;
  table->npatterns = 0;
  table->data = (pattern_t *) safe_malloc(DEF_PATTERN_TABLE_SIZE * sizeof(pattern_t));
}


/*
 * Empty the table: delete all pattern objects
 */
void reset_pattern_table(pattern_table_t *table) {
  shrink_pattern_table(table, 0);
}


/*
 * Delete the table
 */
void delete_pattern_table(pattern_table_t *table) {
  shrink_pattern_table(table, 0);

  safe_free(table->data);
  table->data = NULL;
}


/*
 * Allocate a new pattern index i
 * - data[i] is not initialized
 */
int32_t pattern_table_alloc(pattern_table_t *table) {
  uint32_t i;

  i = table->npatterns;
  if (i == table->size) {
    extend_pattern_table(table);
  }
  assert(i < table->size);
  table->npatterns = i+1;

  return i;
}


/*
 * Create a new pattern
 */
int32_t pattern_table_add_pattern(pattern_table_t *ptbl, term_t p, term_t *pv, uint32_t npv,
    term_t *f, uint32_t nf, term_t *fa, uint32_t nfa, term_t *c, uint32_t nc) {
  pattern_t *pat;
  int32_t i;

  i = pattern_table_alloc(ptbl);
  pat = ptbl->data + i;

  pat->p = p;
  pat->pvars = make_index_vector(pv, npv);
  pat->fun = make_index_vector(f, nf);
  pat->fapps = make_index_vector(fa, nfa);
  pat->consts = make_index_vector(c, nc);
  pat->code = -1;
  init_ivector(&pat->matches, 4);

  return i;
}


/*
 * Recursively push all variables, functions, function applications and constants that occur in term t
 */
void quant_process_pattern_term(term_table_t *terms, term_t t, ivector_t *pv, ivector_t *f,
    ivector_t *fa, ivector_t *c) {
  term_t x, u;
  term_kind_t kind;
  uint32_t i, n;

  x = unsigned_term(t);
  kind = term_kind(terms, x);

  // process all children (if any)
  n = term_num_children(terms, x);
  for(i=0; i<n; 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);
  }

  switch (kind) {
  case CONSTANT_TERM:
  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
    // nothing to do
    break;

  case UNINTERPRETED_TERM:
    // add to vector c
    if (is_function_term(terms, x)) {
      ivector_push(f, x);
#if 0
      printf("    adding function: ");
      yices_pp_term(stdout, x, 120, 1, 0);
#endif
    } else {
      ivector_push(c, x);
#if 0
      printf("    adding constant: ");
      yices_pp_term(stdout, x, 120, 1, 0);
#endif
    }
    break;

  case VARIABLE:
    // add to vector pv
    ivector_push(pv, x);
#if 0
    printf("    adding var: ");
    yices_pp_term(stdout, x, 120, 1, 0);
#endif
    break;

  case APP_TERM:
    // add to vector fa
    ivector_push(fa, x);
#if 0
    printf("    adding fapp: ");
    yices_pp_term(stdout, x, 120, 1, 0);
#endif
    break;

  case ARITH_EQ_ATOM:
  case EQ_TERM:            // equality
  case ARITH_BINEQ_ATOM:
  case BV_EQ_ATOM:
  case ITE_TERM:
  case ITE_SPECIAL:
  case DISTINCT_TERM:
  case OR_TERM:            // n-ary OR
  case XOR_TERM:           // n-ary XOR
  case TUPLE_TERM:
    // nothing to do
    break;

  default:
    // arithmetic/bitvector operators and atoms and other interpreted terms:
    // nothing to collect here; their leaves are gathered via the recursion above
    break;
  }
}


/*
 * Recursively check if an fapp contains all uvars, and if yes, push in out vector
 */
static bool quant_infer_single_fapps(term_table_t *terms, term_t t, int_hmap_t *uvarMap, uint32_t nuvars, ivector_t *out) {
  term_t x, u;
  term_kind_t kind;
  uint32_t i, n;
  int_hmap_pair_t *p, *p2;
  int_hmap_t tmpMap;
  int_hmap_t *childMap;
  bool skip;

  skip = false;
  childMap = &tmpMap;
  x = unsigned_term(t);
  kind = term_kind(terms, x);

//#if TRACE
//  printf("    processing term ");
//  yices_pp_term(stdout, t, 1200, 1, 0);
//#endif

  // process all children (if any)
  n = term_num_children(terms, x);
  if (n != 0) {
    init_int_hmap(childMap, 0);
    for(i=0; i<n; 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);

      // add child map to parent based on the kind of child
      switch (term_kind(terms, u)) {
      case CONSTANT_TERM:
      case ARITH_CONSTANT:
      case BV64_CONSTANT:
      case BV_CONSTANT:
      case UNINTERPRETED_TERM:
      case VARIABLE:
      case APP_TERM:
        for (p2 = int_hmap_first_record(childMap);
             p2 != NULL;
             p2 = int_hmap_next_record(childMap, p2)) {
          p = int_hmap_get(uvarMap, p2->key);
          p->val = p2->val;
        }
        break;

      case ARITH_EQ_ATOM:
      case EQ_TERM:            // equality
      case ARITH_BINEQ_ATOM:
      case BV_EQ_ATOM:
      case ITE_TERM:
      case ITE_SPECIAL:
      case DISTINCT_TERM:
      case OR_TERM:            // n-ary OR
      case XOR_TERM:           // n-ary XOR
        // reset the map
        break;

      default:
        // interpreted operator/atom: do not propagate its variables upward
        break;
      }

    }
    delete_int_hmap(childMap);
  }

  // find fapps
  switch (kind) {
  case CONSTANT_TERM:
  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
  case UNINTERPRETED_TERM:
    // nothing to do
    break;

  case VARIABLE:
    p = int_hmap_get(uvarMap, x);
    p->val = 1;
#if TRACE
    printf("    found var: ");
    yices_pp_term(stdout, x, 120, 1, 0);
#endif
    break;

  case APP_TERM:
    if (!skip && uvarMap->nelems == nuvars) {
      ivector_push(out, x);
#if TRACE
      printf("    found fapp: ");
      yices_pp_term(stdout, x, 120, 1, 0);
#endif
    }
    break;

  case ARITH_EQ_ATOM:
  case EQ_TERM:            // equality
  case ARITH_BINEQ_ATOM:
  case BV_EQ_ATOM:
  case ITE_TERM:
  case ITE_SPECIAL:
  case DISTINCT_TERM:
  case OR_TERM:            // n-ary OR
  case XOR_TERM:           // n-ary XOR
    // reset the map
    skip = true;
    break;

  default:
    // interpreted operator/atom: cannot serve as a single-fapp pattern
    skip = true;
    break;
  }

#if TRACE
  printf("    term (%d): ", skip);
  yices_pp_term(stdout, t, 1200, 1, 0);
  printf("    table: ");
  for (p = int_hmap_first_record(uvarMap);
       p != NULL;
       p = int_hmap_next_record(uvarMap, p)) {
//    yices_pp_term_array(stdout, 1, &p->key, 120, 0, 0, 1);
    printf("%s -> %d, ", yices_term_to_string(p->key, 120, 1, 0), p->val);
  }
  printf("\n");
#endif

  return skip;
}

/*
 * Infer single patterns for term t, by recursively finding fapps which contain all uvars
 */
void quant_infer_single_pattern(term_table_t *terms, term_t t, ivector_t *uvars, ivector_t *out) {
  int_hmap_t uvarMap;

  init_int_hmap(&uvarMap, 0);
  quant_infer_single_fapps(terms, t, &uvarMap, uvars->size, out);
  delete_int_hmap(&uvarMap);
}


/*
 * Recursively fill uvars to fapps, and fapps to uvars tables
 */
static bool quant_infer_multi_fapps(term_table_t *terms, term_t t, ptr_hmap_t *uv2fapp, ptr_hmap_t *fapp2uv) {
  term_t x, u;
  term_kind_t kind;
  uint32_t i, n;
  bool skip;
  ptr_hmap_pair_t *u2f, *f2u;

  skip = false;
  x = unsigned_term(t);
  kind = term_kind(terms, x);

#if TRACE
  printf("    processing term ");
  yices_pp_term(stdout, t, 1200, 1, 0);
#endif

  // process all children (if any)
  n = term_num_children(terms, x);
  if (n != 0) {
    for(i=0; i<n; 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);
    }
  }

  // find fapps
  switch (kind) {
  case CONSTANT_TERM:
  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
  case UNINTERPRETED_TERM:
  case VARIABLE:
    // nothing to do
    break;

  case APP_TERM:
    if (!skip) {
#if TRACE
      printf("    fapp: ");
      yices_pp_term(stdout, x, 120, 1, 0);
#endif
      n = term_num_children(terms, x);
      if (n != 0) {
        for(i=0; i<n; i++) {
          u = term_child(terms, x, i);
          if (term_kind(terms, u) == VARIABLE) {
            if (is_neg_term(u)) {
              u = opposite_term(u);
            }
#if TRACE
            printf("      var: ");
            yices_pp_term(stdout, u, 120, 1, 0);
#endif
            assert(is_pos_term(u));
            u2f = ptr_hmap_get(uv2fapp, u);
            if (u2f->val == NULL) {
              u2f->val = safe_malloc(sizeof(ivector_t));
              init_ivector(u2f->val, 0);
            }
            ivector_push(u2f->val, x);

            f2u = ptr_hmap_get(fapp2uv, x);
            if (f2u->val == NULL) {
              f2u->val = safe_malloc(sizeof(ivector_t));
              init_ivector(f2u->val, 0);
            }
            ivector_push(f2u->val, u);
          } else if (term_kind(terms, u) == APP_TERM) {
            f2u = ptr_hmap_find(fapp2uv, u);
            if (f2u != NULL) {
              uint32_t j, m;
              ivector_t *uvars;
              uvars = f2u->val;
              m = uvars->size;
              for(j=0; j<m; j++) {
                u = uvars->data[j];
                assert (term_kind(terms, u) == VARIABLE);
#if TRACE
                  printf("      var: ");
                  yices_pp_term(stdout, u, 120, 1, 0);
#endif
                assert(is_pos_term(u));
                u2f = ptr_hmap_get(uv2fapp, u);
                assert(u2f->val != NULL);
                ivector_push(u2f->val, x);

                f2u = ptr_hmap_get(fapp2uv, x);
                if (f2u->val == NULL) {
                  f2u->val = safe_malloc(sizeof(ivector_t));
                  init_ivector(f2u->val, 0);
                }
                ivector_push(f2u->val, u);
              }
            }
          }
        }
      }
    }
    break;

  case ARITH_EQ_ATOM:
  case EQ_TERM:            // equality
  case ARITH_BINEQ_ATOM:
  case BV_EQ_ATOM:
  case ITE_TERM:
  case ITE_SPECIAL:
  case DISTINCT_TERM:
  case OR_TERM:            // n-ary OR
  case XOR_TERM:           // n-ary XOR
    // reset the map
    skip = true;
    break;

  default:
    // interpreted operator/atom: cannot host multi-fapp mappings
    skip = true;
    break;
  }

  return skip;
}

/*
 * Infer multi patterns for term t, by recursively finding fapps which contain all uvars
 */
void quant_infer_multi_pattern(term_table_t *terms, term_t t, ivector_t *uvars, ivector_t *out) {
  ptr_hmap_t uv2fapp, fapp2uv;
  ptr_hmap_pair_t *p;
  ptr_hmap_t *map;
  ivector_t* v;
  uint32_t i, n;

  init_ptr_hmap(&uv2fapp, 0);
  init_ptr_hmap(&fapp2uv, 0);

  quant_infer_multi_fapps(terms, t, &uv2fapp, &fapp2uv);

  map = &uv2fapp;
#if TRACE
  printf("\n  uv2fapps (%d):\n", map->nelems);
#endif
  for (p = ptr_hmap_first_record(map);
       p != NULL;
       p = ptr_hmap_next_record(map, p)) {
    v = p->val;
    ivector_remove_duplicates(v);
#if TRACE
    printf("    %s -> ", yices_term_to_string(p->key, 100, 1, 0));
    yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
#endif
  }

  map = &fapp2uv;
#if TRACE
  printf("\n  fapp2uv (%d):\n", map->nelems);
#endif
  for (p = ptr_hmap_first_record(map);
       p != NULL;
       p = ptr_hmap_next_record(map, p)) {
    v = p->val;
    ivector_remove_duplicates(v);
#if TRACE
    printf("    %s -> ", yices_term_to_string(p->key, 100, 1, 0));
    yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
#endif
  }
#if TRACE
  printf("\n");
#endif

  int_hmap_t uvMap;
  int_hmap_pair_t *ip;
  ivector_t multiPat;
  term_t u, f, pat;

  init_int_hmap(&uvMap, 0);
  init_ivector(&multiPat, 2);

  n = uvars->size;
  for(i=0; i<n; i++) {
    ip = int_hmap_get(&uvMap, uvars->data[i]);
    assert(ip->val < 0);
    ip->val = 1;
  }

  while(true) {
    u = NULL_TERM;
    for (ip = int_hmap_first_record(&uvMap);
         ip != NULL;
         ip = int_hmap_next_record(&uvMap, ip)) {
      if (ip->val == 1) {
        ip->val = 2;
        u = ip->key;
        break;
      }
    }
    if (u == NULL_TERM) {
      break;
    }

#if TRACE
    printf("    choosing uvar: ");
    yices_pp_term(stdout, u, 120, 1, 0);
#endif

    p = ptr_hmap_find(&uv2fapp, u);
    if (p == NULL) {
      ivector_reset(&multiPat);
      break;
    }
    v = p->val;
    n = v->size;
    assert(n != 0);
    f = v->data[n-1];
    ivector_push(&multiPat, f);
#if TRACE
    printf("    choosing fapp: ");
    yices_pp_term(stdout, f, 120, 1, 0);
#endif

    p = ptr_hmap_find(&fapp2uv, f);
    assert(p != NULL);
    v = p->val;
    n = v->size;
#if TRACE
    printf("    uvars: ");
    yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
#endif

    for(i=0; i<n; i++) {
      ip = int_hmap_find(&uvMap, v->data[i]);
      assert(ip != NULL);
      ip->val = 2;
    }
  }

  if (multiPat.size != 0) {
    if (multiPat.size == 1) {
      pat = multiPat.data[0];
    } else {
      pat = yices_tuple(multiPat.size, multiPat.data);
    }
    if (pat == NULL_TERM) {
//      yices_print_error(stdout);
      assert(0);
    }
    ivector_push(out, pat);

#if TRACE
    printf("  Multi pattern: ");
    yices_pp_term(stdout, pat, 120, 1, 0);
#endif
  }

  delete_int_hmap(&uvMap);
  delete_ivector(&multiPat);

  map = &uv2fapp;
  for (p = ptr_hmap_first_record(map);
       p != NULL;
       p = ptr_hmap_next_record(map, p)) {
    v = p->val;
    if (v != NULL) {
      delete_ivector(v);
      safe_free(v);
    }
  }
  delete_ptr_hmap(map);

  map = &fapp2uv;
  for (p = ptr_hmap_first_record(map);
       p != NULL;
       p = ptr_hmap_next_record(map, p)) {
    v = p->val;
    if (v != NULL) {
      delete_ivector(v);
      safe_free(v);
    }
  }
  delete_ptr_hmap(map);
}





1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* QUANTIFIER PATTERNS
21	*/
22
23	#if defined(CYGWIN) \|\| defined(MINGW)
24	#define EXPORTED __declspec(dllexport)
25	#define __YICES_DLLSPEC__ EXPORTED
26	#else
27	#define EXPORTED __attribute__((visibility("default")))
28	#endif
29
30	#include "solvers/quant/quant_pattern.h"
31	#include "utils/index_vectors.h"
32	#include "terms/term_explorer.h"
33	#include "yices.h"
34
35	#define TRACE 0
36
37	#if TRACE
38
39	#include <stdio.h>
40
41	#include "solvers/cdcl/smt_core_printer.h"
42	#include "solvers/egraph/egraph_printer.h"
43
44	#endif
45
46
47
48	/*******************
49	* PATTERN TABLE *
50	******************/
51
52	/*
53	* Make the table 50% larger
54	*/
55	static void extend_pattern_table(pattern_table_t *table) {	×
56	uint32_t n;
57
58	n = table->size + 1;	×
59	n += n>>1;	×
60	if (n >= MAX_PATTERN_TABLE_SIZE) {	×
61	out_of_memory();	×
62	}
63	table->data = (pattern_t ) safe_realloc(table->data, n sizeof(pattern_t));	×
64	table->size = n;	×
65	}	×
66
67
68	/*
69	* Remove all patterns of index >= n
70	*/
71	static void shrink_pattern_table(pattern_table_t *table, uint32_t n) {	55✔
72	uint32_t i;
73	pattern_t *pat;
74
75	assert(n <= table->npatterns);
76
77	for(i=n; i<table->npatterns; i++) {	338✔
78	pat = table->data + i;	283✔
79	delete_index_vector(pat->pvars);	283✔
80	delete_index_vector(pat->fun);	283✔
81	delete_index_vector(pat->fapps);	283✔
82	delete_index_vector(pat->consts);	283✔
83
84	delete_ivector(&pat->matches);	283✔
85	}
86
87	table->npatterns = n;	55✔
88	}	55✔
89
90
91	/*
92	* Initialize: default size
93	*/
94	void init_pattern_table(pattern_table_t *table) {	55✔
95	assert(DEF_PATTERN_TABLE_SIZE < MAX_PATTERN_TABLE_SIZE);
96
97	table->size = DEF_PATTERN_TABLE_SIZE;	55✔
98	table->npatterns = 0;	55✔
99	table->data = (pattern_t ) safe_malloc(DEF_PATTERN_TABLE_SIZE sizeof(pattern_t));	55✔
100	}	55✔
101
102
103	/*
104	* Empty the table: delete all pattern objects
105	*/
106	void reset_pattern_table(pattern_table_t *table) {	×
107	shrink_pattern_table(table, 0);	×
108	}	×
109
110
111	/*
112	* Delete the table
113	*/
114	void delete_pattern_table(pattern_table_t *table) {	55✔
115	shrink_pattern_table(table, 0);	55✔
116
117	safe_free(table->data);	55✔
118	table->data = NULL;	55✔
119	}	55✔
120
121
122	/*
123	* Allocate a new pattern index i
124	* - data[i] is not initialized
125	*/
126	int32_t pattern_table_alloc(pattern_table_t *table) {	283✔
127	uint32_t i;
128
129	i = table->npatterns;	283✔
130	if (i == table->size) {	283✔
131	extend_pattern_table(table);	×
132	}
133	assert(i < table->size);
134	table->npatterns = i+1;	283✔
135
136	return i;	283✔
137	}
138
139
140	/*
141	* Create a new pattern
142	*/
143	int32_t pattern_table_add_pattern(pattern_table_t ptbl, term_t p, term_t pv, uint32_t npv,	283✔
144	term_t f, uint32_t nf, term_t fa, uint32_t nfa, term_t *c, uint32_t nc) {
145	pattern_t *pat;
146	int32_t i;
147
148	i = pattern_table_alloc(ptbl);	283✔
149	pat = ptbl->data + i;	283✔
150
151	pat->p = p;	283✔
152	pat->pvars = make_index_vector(pv, npv);	283✔
153	pat->fun = make_index_vector(f, nf);	283✔
154	pat->fapps = make_index_vector(fa, nfa);	283✔
155	pat->consts = make_index_vector(c, nc);	283✔
156	pat->code = -1;	283✔
157	init_ivector(&pat->matches, 4);	283✔
158
159	return i;	283✔
160	}
161
162
163	/*
164	* Recursively push all variables, functions, function applications and constants that occur in term t
165	*/
166	void quant_process_pattern_term(term_table_t terms, term_t t, ivector_t pv, ivector_t *f,	4,445✔
167	ivector_t fa, ivector_t c) {
168	term_t x, u;
169	term_kind_t kind;
170	uint32_t i, n;
171
172	x = unsigned_term(t);	4,445✔
173	kind = term_kind(terms, x);	4,445✔
174
175	// process all children (if any)
176	n = term_num_children(terms, x);	4,445✔
177	for(i=0; i<n; i++) {	8,436✔
178	u = term_ith_subterm(terms, x, i);	3,991✔
179	if (u == NULL_TERM) continue; // constant monomial of a sum: nothing to recurse into	3,991✔
180	quant_process_pattern_term(terms, u, pv, f, fa, c);	3,989✔
181	}
182
183	switch (kind) {	4,445✔
184	case CONSTANT_TERM:	32✔
185	case ARITH_CONSTANT:
186	case BV64_CONSTANT:
187	case BV_CONSTANT:
188	// nothing to do
189	break;	32✔
190
191	case UNINTERPRETED_TERM:	1,159✔
192	// add to vector c
193	if (is_function_term(terms, x)) {	1,159✔
194	ivector_push(f, x);	1,020✔
195	#if 0
196	printf(" adding function: ");
197	yices_pp_term(stdout, x, 120, 1, 0);
198	#endif
199	} else {
200	ivector_push(c, x);	139✔
201	#if 0
202	printf(" adding constant: ");
203	yices_pp_term(stdout, x, 120, 1, 0);
204	#endif
205	}
206	break;	1,159✔
207
208	case VARIABLE:	1,747✔
209	// add to vector pv
210	ivector_push(pv, x);	1,747✔
211	#if 0
212	printf(" adding var: ");
213	yices_pp_term(stdout, x, 120, 1, 0);
214	#endif
215	break;	1,747✔
216
217	case APP_TERM:	1,020✔
218	// add to vector fa
219	ivector_push(fa, x);	1,020✔
220	#if 0
221	printf(" adding fapp: ");
222	yices_pp_term(stdout, x, 120, 1, 0);
223	#endif
224	break;	1,020✔
225
226	case ARITH_EQ_ATOM:	483✔
227	case EQ_TERM: // equality
228	case ARITH_BINEQ_ATOM:
229	case BV_EQ_ATOM:
230	case ITE_TERM:
231	case ITE_SPECIAL:
232	case DISTINCT_TERM:
233	case OR_TERM: // n-ary OR
234	case XOR_TERM: // n-ary XOR
235	case TUPLE_TERM:
236	// nothing to do
237	break;	483✔
238
239	default:	4✔
240	// arithmetic/bitvector operators and atoms and other interpreted terms:
241	// nothing to collect here; their leaves are gathered via the recursion above
242	break;	4✔
243	}
244	}	4,445✔
245
246
247	/*
248	* Recursively check if an fapp contains all uvars, and if yes, push in out vector
249	*/
250	static bool quant_infer_single_fapps(term_table_t terms, term_t t, int_hmap_t uvarMap, uint32_t nuvars, ivector_t *out) {	2,630✔
251	term_t x, u;
252	term_kind_t kind;
253	uint32_t i, n;
254	int_hmap_pair_t p, p2;
255	int_hmap_t tmpMap;
256	int_hmap_t *childMap;
257	bool skip;
258
259	skip = false;	2,630✔
260	childMap = &tmpMap;	2,630✔
261	x = unsigned_term(t);	2,630✔
262	kind = term_kind(terms, x);	2,630✔
263
264	//#if TRACE
265	// printf(" processing term ");
266	// yices_pp_term(stdout, t, 1200, 1, 0);
267	//#endif
268
269	// process all children (if any)
270	n = term_num_children(terms, x);	2,630✔
271	if (n != 0) {	2,630✔
272	init_int_hmap(childMap, 0);	978✔
273	for(i=0; i<n; i++) {	3,449✔
274	u = term_ith_subterm(terms, x, i);	2,471✔
275	if (u == NULL_TERM) continue; // constant monomial of a sum	2,471✔
276	int_hmap_reset(childMap);	2,469✔
277	skip \|= quant_infer_single_fapps(terms, u, childMap, nuvars, out);	2,469✔
278
279	// add child map to parent based on the kind of child
280	switch (term_kind(terms, u)) {	2,469✔
281	case CONSTANT_TERM:	2,182✔
282	case ARITH_CONSTANT:
283	case BV64_CONSTANT:
284	case BV_CONSTANT:
285	case UNINTERPRETED_TERM:
286	case VARIABLE:
287	case APP_TERM:
288	for (p2 = int_hmap_first_record(childMap);	2,182✔
289	p2 != NULL;	4,167✔
290	p2 = int_hmap_next_record(childMap, p2)) {	1,985✔
291	p = int_hmap_get(uvarMap, p2->key);	1,985✔
292	p->val = p2->val;	1,985✔
293	}
294	break;	2,182✔
295
296	case ARITH_EQ_ATOM:	283✔
297	case EQ_TERM: // equality
298	case ARITH_BINEQ_ATOM:
299	case BV_EQ_ATOM:
300	case ITE_TERM:
301	case ITE_SPECIAL:
302	case DISTINCT_TERM:
303	case OR_TERM: // n-ary OR
304	case XOR_TERM: // n-ary XOR
305	// reset the map
306	break;	283✔
307
308	default:	4✔
309	// interpreted operator/atom: do not propagate its variables upward
310	break;	4✔
311	}
312
313	}
314	delete_int_hmap(childMap);	978✔
315	}
316
317	// find fapps
318	switch (kind) {	2,630✔
319	case CONSTANT_TERM:	693✔
320	case ARITH_CONSTANT:
321	case BV64_CONSTANT:
322	case BV_CONSTANT:
323	case UNINTERPRETED_TERM:
324	// nothing to do
325	break;	693✔
326
327	case VARIABLE:	959✔
328	p = int_hmap_get(uvarMap, x);	959✔
329	p->val = 1;	959✔
330	#if TRACE
331	printf(" found var: ");
332	yices_pp_term(stdout, x, 120, 1, 0);
333	#endif
334	break;	959✔
335
336	case APP_TERM:	541✔
337	if (!skip && uvarMap->nelems == nuvars) {	541✔
338	ivector_push(out, x);	310✔
339	#if TRACE
340	printf(" found fapp: ");
341	yices_pp_term(stdout, x, 120, 1, 0);
342	#endif
343	}
344	break;	541✔
345
346	case ARITH_EQ_ATOM:	433✔
347	case EQ_TERM: // equality
348	case ARITH_BINEQ_ATOM:
349	case BV_EQ_ATOM:
350	case ITE_TERM:
351	case ITE_SPECIAL:
352	case DISTINCT_TERM:
353	case OR_TERM: // n-ary OR
354	case XOR_TERM: // n-ary XOR
355	// reset the map
356	skip = true;	433✔
357	break;	433✔
358
359	default:	4✔
360	// interpreted operator/atom: cannot serve as a single-fapp pattern
361	skip = true;	4✔
362	break;	4✔
363	}
364
365	#if TRACE
366	printf(" term (%d): ", skip);
367	yices_pp_term(stdout, t, 1200, 1, 0);
368	printf(" table: ");
369	for (p = int_hmap_first_record(uvarMap);
370	p != NULL;
371	p = int_hmap_next_record(uvarMap, p)) {
372	// yices_pp_term_array(stdout, 1, &p->key, 120, 0, 0, 1);
373	printf("%s -> %d, ", yices_term_to_string(p->key, 120, 1, 0), p->val);
374	}
375	printf("\n");
376	#endif
377
378	return skip;	2,630✔
379	}
380
381	/*
382	* Infer single patterns for term t, by recursively finding fapps which contain all uvars
383	*/
384	void quant_infer_single_pattern(term_table_t terms, term_t t, ivector_t uvars, ivector_t *out) {	161✔
385	int_hmap_t uvarMap;
386
387	init_int_hmap(&uvarMap, 0);	161✔
388	quant_infer_single_fapps(terms, t, &uvarMap, uvars->size, out);	161✔
389	delete_int_hmap(&uvarMap);	161✔
390	}	161✔
391
392
393	/*
394	* Recursively fill uvars to fapps, and fapps to uvars tables
395	*/
396	static bool quant_infer_multi_fapps(term_table_t terms, term_t t, ptr_hmap_t uv2fapp, ptr_hmap_t *fapp2uv) {	681✔
397	term_t x, u;
398	term_kind_t kind;
399	uint32_t i, n;
400	bool skip;
401	ptr_hmap_pair_t u2f, f2u;
402
403	skip = false;	681✔
404	x = unsigned_term(t);	681✔
405	kind = term_kind(terms, x);	681✔
406
407	#if TRACE
408	printf(" processing term ");
409	yices_pp_term(stdout, t, 1200, 1, 0);
410	#endif
411
412	// process all children (if any)
413	n = term_num_children(terms, x);	681✔
414	if (n != 0) {	681✔
415	for(i=0; i<n; i++) {	911✔
416	u = term_ith_subterm(terms, x, i);	649✔
417	if (u == NULL_TERM) continue; // constant monomial of a sum	649✔
418	skip \|= quant_infer_multi_fapps(terms, u, uv2fapp, fapp2uv);	649✔
419	}
420	}
421
422	// find fapps
423	switch (kind) {	681✔
424	case CONSTANT_TERM:	419✔
425	case ARITH_CONSTANT:
426	case BV64_CONSTANT:
427	case BV_CONSTANT:
428	case UNINTERPRETED_TERM:
429	case VARIABLE:
430	// nothing to do
431	break;	419✔
432
433	case APP_TERM:	111✔
434	if (!skip) {	111✔
435	#if TRACE
436	printf(" fapp: ");
437	yices_pp_term(stdout, x, 120, 1, 0);
438	#endif
439	n = term_num_children(terms, x);	111✔
440	if (n != 0) {	111✔
441	for(i=0; i<n; i++) {	452✔
442	u = term_child(terms, x, i);	341✔
443	if (term_kind(terms, u) == VARIABLE) {	341✔
444	if (is_neg_term(u)) {	183✔
445	u = opposite_term(u);	5✔
446	}
447	#if TRACE
448	printf(" var: ");
449	yices_pp_term(stdout, u, 120, 1, 0);
450	#endif
451	assert(is_pos_term(u));
452	u2f = ptr_hmap_get(uv2fapp, u);	183✔
453	if (u2f->val == NULL) {	183✔
454	u2f->val = safe_malloc(sizeof(ivector_t));	78✔
455	init_ivector(u2f->val, 0);	78✔
456	}
457	ivector_push(u2f->val, x);	183✔
458
459	f2u = ptr_hmap_get(fapp2uv, x);	183✔
460	if (f2u->val == NULL) {	183✔
461	f2u->val = safe_malloc(sizeof(ivector_t));	87✔
462	init_ivector(f2u->val, 0);	87✔
463	}
464	ivector_push(f2u->val, u);	183✔
465	} else if (term_kind(terms, u) == APP_TERM) {	158✔
466	f2u = ptr_hmap_find(fapp2uv, u);	12✔
467	if (f2u != NULL) {	12✔
468	uint32_t j, m;
469	ivector_t *uvars;
470	uvars = f2u->val;	11✔
471	m = uvars->size;	11✔
472	for(j=0; j<m; j++) {	52✔
473	u = uvars->data[j];	41✔
474	assert (term_kind(terms, u) == VARIABLE);
475	#if TRACE
476	printf(" var: ");
477	yices_pp_term(stdout, u, 120, 1, 0);
478	#endif
479	assert(is_pos_term(u));
480	u2f = ptr_hmap_get(uv2fapp, u);	41✔
481	assert(u2f->val != NULL);
482	ivector_push(u2f->val, x);	41✔
483
484	f2u = ptr_hmap_get(fapp2uv, x);	41✔
485	if (f2u->val == NULL) {	41✔
486	f2u->val = safe_malloc(sizeof(ivector_t));	3✔
487	init_ivector(f2u->val, 0);	3✔
488	}
489	ivector_push(f2u->val, u);	41✔
490	}
491	}
492	}
493	}
494	}
495	}
496	break;	111✔
497
498	case ARITH_EQ_ATOM:	151✔
499	case EQ_TERM: // equality
500	case ARITH_BINEQ_ATOM:
501	case BV_EQ_ATOM:
502	case ITE_TERM:
503	case ITE_SPECIAL:
504	case DISTINCT_TERM:
505	case OR_TERM: // n-ary OR
506	case XOR_TERM: // n-ary XOR
507	// reset the map
508	skip = true;	151✔
509	break;	151✔
510
UNCOV 511	default:	×
512	// interpreted operator/atom: cannot host multi-fapp mappings
NEW 513	skip = true;	×
NEW 514	break;	×
515	}
516
517	return skip;	681✔
518	}
519
520	/*
521	* Infer multi patterns for term t, by recursively finding fapps which contain all uvars
522	*/
523	void quant_infer_multi_pattern(term_table_t terms, term_t t, ivector_t uvars, ivector_t *out) {	32✔
524	ptr_hmap_t uv2fapp, fapp2uv;
525	ptr_hmap_pair_t *p;
526	ptr_hmap_t *map;
527	ivector_t* v;
528	uint32_t i, n;
529
530	init_ptr_hmap(&uv2fapp, 0);	32✔
531	init_ptr_hmap(&fapp2uv, 0);	32✔
532
533	quant_infer_multi_fapps(terms, t, &uv2fapp, &fapp2uv);	32✔
534
535	map = &uv2fapp;	32✔
536	#if TRACE
537	printf("\n uv2fapps (%d):\n", map->nelems);
538	#endif
539	for (p = ptr_hmap_first_record(map);	32✔
540	p != NULL;	110✔
541	p = ptr_hmap_next_record(map, p)) {	78✔
542	v = p->val;	78✔
543	ivector_remove_duplicates(v);	78✔
544	#if TRACE
545	printf(" %s -> ", yices_term_to_string(p->key, 100, 1, 0));
546	yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
547	#endif
548	}
549
550	map = &fapp2uv;	32✔
551	#if TRACE
552	printf("\n fapp2uv (%d):\n", map->nelems);
553	#endif
554	for (p = ptr_hmap_first_record(map);	32✔
555	p != NULL;	122✔
556	p = ptr_hmap_next_record(map, p)) {	90✔
557	v = p->val;	90✔
558	ivector_remove_duplicates(v);	90✔
559	#if TRACE
560	printf(" %s -> ", yices_term_to_string(p->key, 100, 1, 0));
561	yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
562	#endif
563	}
564	#if TRACE
565	printf("\n");
566	#endif
567
568	int_hmap_t uvMap;
569	int_hmap_pair_t *ip;
570	ivector_t multiPat;
571	term_t u, f, pat;
572
573	init_int_hmap(&uvMap, 0);	32✔
574	init_ivector(&multiPat, 2);	32✔
575
576	n = uvars->size;	32✔
577	for(i=0; i<n; i++) {	124✔
578	ip = int_hmap_get(&uvMap, uvars->data[i]);	92✔
579	assert(ip->val < 0);
580	ip->val = 1;	92✔
581	}
582
583	while(true) {
584	u = NULL_TERM;	81✔
585	for (ip = int_hmap_first_record(&uvMap);	81✔
586	ip != NULL;	226✔
587	ip = int_hmap_next_record(&uvMap, ip)) {	145✔
588	if (ip->val == 1) {	205✔
589	ip->val = 2;	60✔
590	u = ip->key;	60✔
591	break;	60✔
592	}
593	}
594	if (u == NULL_TERM) {	81✔
595	break;	21✔
596	}
597
598	#if TRACE
599	printf(" choosing uvar: ");
600	yices_pp_term(stdout, u, 120, 1, 0);
601	#endif
602
603	p = ptr_hmap_find(&uv2fapp, u);	60✔
604	if (p == NULL) {	60✔
605	ivector_reset(&multiPat);	11✔
606	break;	11✔
607	}
608	v = p->val;	49✔
609	n = v->size;	49✔
610	assert(n != 0);
611	f = v->data[n-1];	49✔
612	ivector_push(&multiPat, f);	49✔
613	#if TRACE
614	printf(" choosing fapp: ");
615	yices_pp_term(stdout, f, 120, 1, 0);
616	#endif
617
618	p = ptr_hmap_find(&fapp2uv, f);	49✔
619	assert(p != NULL);
620	v = p->val;	49✔
621	n = v->size;	49✔
622	#if TRACE
623	printf(" uvars: ");
624	yices_pp_term_array(stdout, v->size, v->data, 120, UINT32_MAX, 0, 1);
625	#endif
626
627	for(i=0; i<n; i++) {	148✔
628	ip = int_hmap_find(&uvMap, v->data[i]);	99✔
629	assert(ip != NULL);
630	ip->val = 2;	99✔
631	}
632	}
633
634	if (multiPat.size != 0) {	32✔
635	if (multiPat.size == 1) {	21✔
636	pat = multiPat.data[0];	×
637	} else {
638	pat = yices_tuple(multiPat.size, multiPat.data);	21✔
639	}
640	if (pat == NULL_TERM) {
641	// yices_print_error(stdout);
642	assert(0);
643	}
644	ivector_push(out, pat);	21✔
645
646	#if TRACE
647	printf(" Multi pattern: ");
648	yices_pp_term(stdout, pat, 120, 1, 0);
649	#endif
650	}
651
652	delete_int_hmap(&uvMap);	32✔
653	delete_ivector(&multiPat);	32✔
654
655	map = &uv2fapp;	32✔
656	for (p = ptr_hmap_first_record(map);	32✔
657	p != NULL;	110✔
658	p = ptr_hmap_next_record(map, p)) {	78✔
659	v = p->val;	78✔
660	if (v != NULL) {	78✔
661	delete_ivector(v);	78✔
662	safe_free(v);	78✔
663	}
664	}
665	delete_ptr_hmap(map);	32✔
666
667	map = &fapp2uv;	32✔
668	for (p = ptr_hmap_first_record(map);	32✔
669	p != NULL;	122✔
670	p = ptr_hmap_next_record(map, p)) {	90✔
671	v = p->val;	90✔
672	if (v != NULL) {	90✔
673	delete_ivector(v);	90✔
674	safe_free(v);	90✔
675	}
676	}
677	delete_ptr_hmap(map);	32✔
678	}	32✔
679
680
681
682

SRI-CSL / yices2 / 30150074613

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous