9226448713

Committed 24 May 2024 03:34PM UTC coverage: 65.988% (+0.3%) from 65.728%

Build # 9226448713

Build Type

Pull #513

github

Committed by

web-flow

Commit Message

Merge da66d3d5d into f06761440

Pull Request Pull Request #513: Finite Field support

Run Details

2396 of 3347 new or added lines in 66 files covered. (71.59%)

18 existing lines in 12 files now uncovered.

81769 of 123915 relevant lines covered (65.99%)

1493770.28 hits per line

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

0.0

/src/io/type_printer.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/>.
 */

/*
 * Print functions for types
 */

#include <assert.h>
#include <stdint.h>
#include <string.h>
#include <inttypes.h>

#include "io/type_printer.h"


/*
 * Ids for bool, int, and real types
 * (bool = 0, int = 1, real = 2).
 */
static const char * const type2string[] = {
  "bool", "int", "real"
};

/*
 * Type id: either bool, int, real or a default id
 */
void print_type_id(FILE *f, type_t tau) {
  assert(0 <= tau);

  if (tau <= real_id) {
    fputs(type2string[tau], f);
  } else {
    fprintf(f, "tau!%"PRId32, tau);
  }
}


/*
 * Name of macro id
 */
void print_macro_name(FILE *f, type_table_t *tbl, int32_t id) {
  type_mtbl_t *mtbl;

  mtbl = tbl->macro_tbl;
  assert(mtbl != NULL);
  fputs(type_macro_name(mtbl, id), f);
}


/*
 * Print name of type tau
 */
void print_type_name(FILE *f, type_table_t *tbl, type_t tau) {
  char *name;

  assert(good_type(tbl, tau));

  if (tau <= real_id) {
    fputs(type2string[tau], f);
  } else {
    name = type_name(tbl, tau);
    if (name != NULL) {
      fputs(name, f);
    } else {
      fprintf(f, "tau!%"PRId32, tau);
    }
  }
}


/*
 * Print type tau
 */
static void print_type_recur(FILE *f, type_table_t *tbl, type_t tau, int32_t level) {
  char *name;
  uint32_t i, n;

  assert(good_type(tbl, tau));

  if (tau <= real_id) {
    fputs(type2string[tau], f);
  } else {
    name = type_name(tbl, tau);
    if (name != NULL && level <= 0) {
      fputs(name, f);
    } else {
      switch (type_kind(tbl, tau)) {
      case BITVECTOR_TYPE:
        fprintf(f, "(bitvector %"PRIu32")", bv_type_size(tbl, tau));
        break;
      case FF_TYPE:
        fprintf(f, "(finitefield ");
        q_print(f, ff_type_size(tbl, tau));
        fprintf(f, ")");
        break;
      case SCALAR_TYPE:
        fprintf(f, "(enum!%"PRId32" %"PRIu32")", tau, scalar_type_cardinal(tbl, tau));
        break;
      case UNINTERPRETED_TYPE:
        fprintf(f, "unint!%"PRId32, tau);
        break;
      case VARIABLE_TYPE:
        fprintf(f, "var!%"PRIu32, type_variable_id(tbl, tau));
        break;
      case TUPLE_TYPE:
        fputs("(tuple", f);
        n = tuple_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          fputc(' ', f);
          print_type_recur(f, tbl, tuple_type_component(tbl, tau, i), level - 1);
        }
        fputc(')', f);
        break;
      case FUNCTION_TYPE:
        fputs("(-> ", f);
        n = function_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          print_type_recur(f, tbl, function_type_domain(tbl, tau, i), level - 1);
          fputc(' ', f);
        }
        print_type_recur(f, tbl, function_type_range(tbl, tau), level - 1);
        fputc(')', f);
        break;
      case INSTANCE_TYPE:
        fputc('(', f);
        print_macro_name(f, tbl, instance_type_cid(tbl, tau));
        n = instance_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          fputc(' ', f);
          print_type_recur(f, tbl, instance_type_param(tbl, tau, i), level - 1);
        }
        fputc(')', f);
        break;
      default:
        assert(false);
        break;
      }
    }
  }
}


/*
 * Expand names only at the outer level
 */
void print_type_exp(FILE *f, type_table_t *tbl, type_t tau) {
  print_type_recur(f, tbl, tau, 1);
}


/*
 * Don't expand names
 */
void print_type(FILE *f, type_table_t *tbl, type_t tau) {
  print_type_recur(f, tbl, tau, 0);
}

/*
 * Definition: name := type
 */
void print_type_def(FILE *f, type_table_t *tbl, type_t tau) {
  print_type_name(f, tbl, tau);
  fputs(" := ", f);
  print_type_recur(f, tbl, tau, 1);
}


/*
 * Macro definition
 */
void print_macro_def(FILE *f, type_table_t *tbl, int32_t id) {
  type_macro_t *d;
  uint32_t i, n;

  d = type_macro(tbl, id);
  if (d->body == NULL_TYPE) {
    fprintf(f, "(declare-sort %s %"PRIu32")\n", d->name, d->arity);
  } else {
    fprintf(f, "(define-sort %s (", d->name);
    n = d->arity;
    assert(n >= 1);
    print_type_name(f, tbl, d->vars[0]);
    for (i=1; i<n; i++) {
      fputc(' ', f);
      print_type_name(f, tbl, d->vars[i]);
    }
    fputs(") ", f);
    print_type(f, tbl, d->body);
    fputs(")\n", f);
  }
}



/*
 * Print type flags as a combination of 34letters
 */
static void print_type_flags(FILE *f, uint8_t flags) {
  char c[5];

  c[0] = '-';
  c[1] = '-';
  c[2] = '-';
  c[3] = '-';
  c[4] = '\0';

  if (flags & TYPE_IS_MAXIMAL_MASK) {
    c[0] = 'M';
  }
  if (flags & TYPE_IS_MINIMAL_MASK) {
    c[1] = 'm';
  }
  if (flags & TYPE_IS_UNIT_MASK) {
    c[2] = 'U'; // unit type
  } else if (flags & TYPE_IS_FINITE_MASK) {
    if (flags & CARD_IS_EXACT_MASK) {
      c[2] = 'S'; // small finite type
    } else {
      c[2] = 'L'; // large finite type
    }
  } else {
    c[2] = 'I'; // infinite type
  }

  if (flags & TYPE_IS_GROUND_MASK) {
    c[3] = 'G';  // ground type
  }

  fputs(c, f);
}



/*
 * Maximal length of all names in tbl
 * - return 0 if no type has a name
 */
static uint32_t max_name_length(type_table_t *tbl) {
  char *name;
  uint32_t max, l, n, i;

  max = 0;
  n = ntypes(tbl);
  for (i=0; i<n; i++) {
    if (type_kind(tbl, i) != UNUSED_TYPE) {
      name = type_name(tbl, i);
      if (name != NULL) {
        l = strlen(name);
        if (l > max) {
          max = l;
        }
      }
    }
  }

  return max;
}

/*
 * Print n blanks
 */
static void print_spaces(FILE *f, uint32_t n) {
  while (n > 0) {
    fputc(' ', f);
    n --;
  }
}


/*
 * Print string s, and add enough spaces to get to length l.
 * - if s is too long, print s and add one space
 */
static void print_padded_string(FILE *f, char *s, uint32_t l) {
  if (s == NULL) {
    print_spaces(f, l);
  } else if (l >= strlen(s)) {
    while (*s != '\0') {
      fputc(*s, f);
      s ++;
      l --;
    }
    print_spaces(f, l);
  } else {
    fprintf(f, "%s ", s);
  }
}


/*
 * Print the full type table
 */
void print_type_table(FILE *f, type_table_t *tbl) {
  uint32_t i, n, j, m;
  uint32_t name_size;

  name_size = max_name_length(tbl) + 2;
  if (name_size < 4) {
    name_size = 4;
  } else if (name_size > 20) {
    name_size = 20;
  }

  n = ntypes(tbl);
  for (i=0; i<n; i++) {
    if (type_kind(tbl, i) != UNUSED_TYPE) {
      // id, flags, card
      fprintf(f, "%4"PRIu32" ", i);
      print_type_flags(f, type_flags(tbl, i));
      fprintf(f, " %10"PRIu32"   ", type_card(tbl, i));

      // name + one space
      print_padded_string(f, type_name(tbl, i), name_size);

      // definition
      switch (type_kind(tbl, i)) {
      case BOOL_TYPE:
      case INT_TYPE:
      case REAL_TYPE:
        fputs(type2string[i], f);
        fputc('\n', f);
        break;
      case BITVECTOR_TYPE:
        fprintf(f, "(bitvector %"PRIu32")\n", bv_type_size(tbl, i));
        break;
      case FF_TYPE:
        fprintf(f, "(finitefield");
        q_print(f, ff_type_size(tbl, i));
        fprintf(f, ")\n");
        break;
      case SCALAR_TYPE:
        fprintf(f, "(enum, card = %"PRIu32")\n", scalar_type_cardinal(tbl, i));
        break;
      case UNINTERPRETED_TYPE:
        fputs("(uninterpreted)\n", f);
        break;
      case VARIABLE_TYPE:
        fprintf(f, "(variable, id = %"PRIu32")\n", type_variable_id(tbl, i));
        break;
      case TUPLE_TYPE:
        fputs("(tuple", f);
        m = tuple_type_arity(tbl, i);
        for (j=0; j<m; j++) {
          fputc(' ', f);
          print_type_name(f, tbl, tuple_type_component(tbl, i, j));
        }
        fputs(")\n", f);
        break;
      case FUNCTION_TYPE:
        fputs("(-> ", f);
        m = function_type_arity(tbl, i);
        for (j=0; j<m; j++) {
          print_type_name(f, tbl, function_type_domain(tbl, i, j));
          fputc(' ', f);
        }
        print_type_name(f, tbl, function_type_range(tbl, i));
        fputs(")\n", f);
        break;
      case INSTANCE_TYPE:
        fputc('(', f);
        print_macro_name(f, tbl, instance_type_cid(tbl, i));
        m = instance_type_arity(tbl, i);
        for (j=0; j<m; j++) {
          fputc(' ', f);
          print_type_name(f, tbl, instance_type_param(tbl, i, j));
        }
        fputs(")\n", f);
        break;
      default:
        fputs("invalid type code\n", f);
        break;
      }
    }
  }
}


/*
 * All macros
 */
void print_type_macros(FILE *f, type_table_t *tbl) {
  type_mtbl_t *mtbl;
  uint32_t i, n;

  mtbl = tbl->macro_tbl;
  if (mtbl != NULL) {
    n = type_macro_nelems(mtbl);
    for (i=0; i<n; i++) {
      if (good_type_macro(mtbl, i)) {
        print_macro_def(f, tbl, i);
      }
    }
  }
}


/*
 * PRETTY PRINTING
 */

/*
 * Print type name
 */
void pp_type_name(yices_pp_t *printer, type_table_t *tbl, type_t tau) {
  char *name;

  assert(good_type(tbl, tau));

  if (tau <= real_id) {
    name = (char*) type2string[tau];
  } else {
    name = type_name(tbl, tau);
  }
  if (name != NULL) {
    pp_string(printer, name);
  } else {
    pp_id(printer, "tau!", tau);
  }
}


/*
 * Print type expression for tau: expand the type names if level > 0
 */
static void pp_type_recur(yices_pp_t *printer, type_table_t *tbl, type_t tau, int32_t level) {
  char *name;
  uint32_t i, n;

  assert(good_type(tbl, tau));

  if (tau <= real_id) {
    pp_string(printer, (char *) type2string[tau]);
  } else {
    name = type_name(tbl, tau);
    if (name != NULL && level <= 0) {
      pp_string(printer, name);
    } else {
      switch (type_kind(tbl, tau)) {
      case BITVECTOR_TYPE:
        pp_open_block(printer, PP_OPEN_BV_TYPE);
        pp_uint32(printer, bv_type_size(tbl, tau));
        pp_close_block(printer, true);
        break;

      case FF_TYPE:
        pp_open_block(printer, PP_OPEN_FF_TYPE);
        pp_rational(printer, ff_type_size(tbl, tau));
        pp_close_block(printer, true);
        break;

      case SCALAR_TYPE:
      case UNINTERPRETED_TYPE:
        if (name != NULL) {
          pp_string(printer, name);
        } else {
          pp_id(printer, "tau!", tau);
        }
        break;

      case VARIABLE_TYPE:
        if (name != NULL) {
          pp_string(printer, name);
        } else {
          pp_id(printer, "var!", type_variable_id(tbl, tau));
        }
        break;

      case TUPLE_TYPE:
        pp_open_block(printer, PP_OPEN_TUPLE_TYPE);
        n = tuple_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          pp_type_recur(printer, tbl, tuple_type_component(tbl, tau, i), level - 1);
        }
        pp_close_block(printer, true);
        break;

      case FUNCTION_TYPE:
        pp_open_block(printer, PP_OPEN_FUN_TYPE);
        n = function_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          pp_type_recur(printer, tbl, function_type_domain(tbl, tau, i), level - 1);
        }
        pp_type_recur(printer, tbl, function_type_range(tbl, tau), level - 1);
        pp_close_block(printer, true);
        break;

      case INSTANCE_TYPE:
        pp_open_block(printer, PP_OPEN_PAR);
        assert(tbl->macro_tbl != NULL);
        pp_string(printer, type_macro_name(tbl->macro_tbl, instance_type_cid(tbl, tau)));
        n = instance_type_arity(tbl, tau);
        for (i=0; i<n; i++) {
          pp_type_recur(printer, tbl, instance_type_param(tbl, tau, i), level - 1);
        }
        pp_close_block(printer, true);
        break;

      default:
        assert(false);
        break;
      }
    }
  }
}


/*
 * Expand top-level names
 */
void pp_type_exp(yices_pp_t *printer, type_table_t *tbl, type_t tau) {
  pp_type_recur(printer, tbl, tau, 1);
}


/*
 * Don't expand top-level names
 */
void pp_type(yices_pp_t *printer, type_table_t *tbl, type_t tau) {
  pp_type_recur(printer, tbl, tau, 0);
}


/*
 * Pretty printing of the full table
 */
void pp_type_table(FILE *f, type_table_t *tbl) {
  yices_pp_t printer;
  pp_area_t area;
  uint32_t i, n;

  area.width = 60;
  area.height = 2;
  area.offset = 11;
  area.truncate = true;
  area.stretch = false;

  init_yices_pp(&printer, f, &area, PP_VMODE, 0);

  n = ntypes(tbl);
  for (i=0; i<n; i++) {
    if (type_kind(tbl, i) != UNUSED_TYPE) {
      fprintf(f, "type[%"PRIu32"]: ", i);
      if (i < 10) fputc(' ', f);
      if (i < 100) fputc(' ', f);
      pp_type(&printer, tbl, i);
      flush_yices_pp(&printer);
    }
  }

  delete_yices_pp(&printer, false);
}



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	* Print functions for types
21	*/
22
23	#include <assert.h>
24	#include <stdint.h>
25	#include <string.h>
26	#include <inttypes.h>
27
28	#include "io/type_printer.h"
29
30
31	/*
32	* Ids for bool, int, and real types
33	* (bool = 0, int = 1, real = 2).
34	*/
35	static const char * const type2string[] = {
36	"bool", "int", "real"
37	};
38
39	/*
40	* Type id: either bool, int, real or a default id
41	*/
42	void print_type_id(FILE *f, type_t tau) {	×
43	assert(0 <= tau);
44
45	if (tau <= real_id) {	×
46	fputs(type2string[tau], f);	×
47	} else {
48	fprintf(f, "tau!%"PRId32, tau);	×
49	}
50	}	×
51
52
53	/*
54	* Name of macro id
55	*/
56	void print_macro_name(FILE f, type_table_t tbl, int32_t id) {	×
57	type_mtbl_t *mtbl;
58
59	mtbl = tbl->macro_tbl;	×
60	assert(mtbl != NULL);
61	fputs(type_macro_name(mtbl, id), f);	×
62	}	×
63
64
65	/*
66	* Print name of type tau
67	*/
68	void print_type_name(FILE f, type_table_t tbl, type_t tau) {	×
69	char *name;
70
71	assert(good_type(tbl, tau));
72
73	if (tau <= real_id) {	×
74	fputs(type2string[tau], f);	×
75	} else {
76	name = type_name(tbl, tau);	×
77	if (name != NULL) {	×
78	fputs(name, f);	×
79	} else {
80	fprintf(f, "tau!%"PRId32, tau);	×
81	}
82	}
83	}	×
84
85
86	/*
87	* Print type tau
88	*/
89	static void print_type_recur(FILE f, type_table_t tbl, type_t tau, int32_t level) {	×
90	char *name;
91	uint32_t i, n;
92
93	assert(good_type(tbl, tau));
94
95	if (tau <= real_id) {	×
96	fputs(type2string[tau], f);	×
97	} else {
98	name = type_name(tbl, tau);	×
99	if (name != NULL && level <= 0) {	×
100	fputs(name, f);	×
101	} else {
102	switch (type_kind(tbl, tau)) {	×
103	case BITVECTOR_TYPE:	×
104	fprintf(f, "(bitvector %"PRIu32")", bv_type_size(tbl, tau));	×
105	break;	×
NEW 106	case FF_TYPE:	×
NEW 107	fprintf(f, "(finitefield ");	×
NEW 108	q_print(f, ff_type_size(tbl, tau));	×
NEW 109	fprintf(f, ")");	×
NEW 110	break;	×
111	case SCALAR_TYPE:	×
112	fprintf(f, "(enum!%"PRId32" %"PRIu32")", tau, scalar_type_cardinal(tbl, tau));	×
113	break;	×
114	case UNINTERPRETED_TYPE:	×
115	fprintf(f, "unint!%"PRId32, tau);	×
116	break;	×
117	case VARIABLE_TYPE:	×
118	fprintf(f, "var!%"PRIu32, type_variable_id(tbl, tau));	×
119	break;	×
120	case TUPLE_TYPE:	×
121	fputs("(tuple", f);	×
122	n = tuple_type_arity(tbl, tau);	×
123	for (i=0; i<n; i++) {	×
124	fputc(' ', f);	×
125	print_type_recur(f, tbl, tuple_type_component(tbl, tau, i), level - 1);	×
126	}
127	fputc(')', f);	×
128	break;	×
129	case FUNCTION_TYPE:	×
130	fputs("(-> ", f);	×
131	n = function_type_arity(tbl, tau);	×
132	for (i=0; i<n; i++) {	×
133	print_type_recur(f, tbl, function_type_domain(tbl, tau, i), level - 1);	×
134	fputc(' ', f);	×
135	}
136	print_type_recur(f, tbl, function_type_range(tbl, tau), level - 1);	×
137	fputc(')', f);	×
138	break;	×
139	case INSTANCE_TYPE:	×
140	fputc('(', f);	×
141	print_macro_name(f, tbl, instance_type_cid(tbl, tau));	×
142	n = instance_type_arity(tbl, tau);	×
143	for (i=0; i<n; i++) {	×
144	fputc(' ', f);	×
145	print_type_recur(f, tbl, instance_type_param(tbl, tau, i), level - 1);	×
146	}
147	fputc(')', f);	×
148	break;	×
149	default:	×
150	assert(false);
151	break;	×
152	}
153	}
154	}
155	}	×
156
157
158	/*
159	* Expand names only at the outer level
160	*/
161	void print_type_exp(FILE f, type_table_t tbl, type_t tau) {	×
162	print_type_recur(f, tbl, tau, 1);	×
163	}	×
164
165
166	/*
167	* Don't expand names
168	*/
169	void print_type(FILE f, type_table_t tbl, type_t tau) {	×
170	print_type_recur(f, tbl, tau, 0);	×
171	}	×
172
173	/*
174	* Definition: name := type
175	*/
176	void print_type_def(FILE f, type_table_t tbl, type_t tau) {	×
177	print_type_name(f, tbl, tau);	×
178	fputs(" := ", f);	×
179	print_type_recur(f, tbl, tau, 1);	×
180	}	×
181
182
183	/*
184	* Macro definition
185	*/
186	void print_macro_def(FILE f, type_table_t tbl, int32_t id) {	×
187	type_macro_t *d;
188	uint32_t i, n;
189
190	d = type_macro(tbl, id);	×
191	if (d->body == NULL_TYPE) {	×
192	fprintf(f, "(declare-sort %s %"PRIu32")\n", d->name, d->arity);	×
193	} else {
194	fprintf(f, "(define-sort %s (", d->name);	×
195	n = d->arity;	×
196	assert(n >= 1);
197	print_type_name(f, tbl, d->vars[0]);	×
198	for (i=1; i<n; i++) {	×
199	fputc(' ', f);	×
200	print_type_name(f, tbl, d->vars[i]);	×
201	}
202	fputs(") ", f);	×
203	print_type(f, tbl, d->body);	×
204	fputs(")\n", f);	×
205	}
206	}	×
207
208
209
210	/*
211	* Print type flags as a combination of 34letters
212	*/
213	static void print_type_flags(FILE *f, uint8_t flags) {	×
214	char c[5];
215
216	c[0] = '-';	×
217	c[1] = '-';	×
218	c[2] = '-';	×
219	c[3] = '-';	×
220	c[4] = '\0';	×
221
222	if (flags & TYPE_IS_MAXIMAL_MASK) {	×
223	c[0] = 'M';	×
224	}
225	if (flags & TYPE_IS_MINIMAL_MASK) {	×
226	c[1] = 'm';	×
227	}
228	if (flags & TYPE_IS_UNIT_MASK) {	×
229	c[2] = 'U'; // unit type	×
230	} else if (flags & TYPE_IS_FINITE_MASK) {	×
231	if (flags & CARD_IS_EXACT_MASK) {	×
232	c[2] = 'S'; // small finite type	×
233	} else {
234	c[2] = 'L'; // large finite type	×
235	}
236	} else {
237	c[2] = 'I'; // infinite type	×
238	}
239
240	if (flags & TYPE_IS_GROUND_MASK) {	×
241	c[3] = 'G'; // ground type	×
242	}
243
244	fputs(c, f);	×
245	}	×
246
247
248
249	/*
250	* Maximal length of all names in tbl
251	* - return 0 if no type has a name
252	*/
253	static uint32_t max_name_length(type_table_t *tbl) {	×
254	char *name;
255	uint32_t max, l, n, i;
256
257	max = 0;	×
258	n = ntypes(tbl);	×
259	for (i=0; i<n; i++) {	×
260	if (type_kind(tbl, i) != UNUSED_TYPE) {	×
261	name = type_name(tbl, i);	×
262	if (name != NULL) {	×
263	l = strlen(name);	×
264	if (l > max) {	×
265	max = l;	×
266	}
267	}
268	}
269	}
270
271	return max;	×
272	}
273
274	/*
275	* Print n blanks
276	*/
277	static void print_spaces(FILE *f, uint32_t n) {	×
278	while (n > 0) {	×
279	fputc(' ', f);	×
280	n --;	×
281	}
282	}	×
283
284
285	/*
286	* Print string s, and add enough spaces to get to length l.
287	* - if s is too long, print s and add one space
288	*/
289	static void print_padded_string(FILE f, char s, uint32_t l) {	×
290	if (s == NULL) {	×
291	print_spaces(f, l);	×
292	} else if (l >= strlen(s)) {	×
293	while (*s != '\0') {	×
294	fputc(*s, f);	×
295	s ++;	×
296	l --;	×
297	}
298	print_spaces(f, l);	×
299	} else {
300	fprintf(f, "%s ", s);	×
301	}
302	}	×
303
304
305	/*
306	* Print the full type table
307	*/
308	void print_type_table(FILE f, type_table_t tbl) {	×
309	uint32_t i, n, j, m;
310	uint32_t name_size;
311
312	name_size = max_name_length(tbl) + 2;	×
313	if (name_size < 4) {	×
314	name_size = 4;	×
315	} else if (name_size > 20) {	×
316	name_size = 20;	×
317	}
318
319	n = ntypes(tbl);	×
320	for (i=0; i<n; i++) {	×
321	if (type_kind(tbl, i) != UNUSED_TYPE) {	×
322	// id, flags, card
323	fprintf(f, "%4"PRIu32" ", i);	×
324	print_type_flags(f, type_flags(tbl, i));	×
325	fprintf(f, " %10"PRIu32" ", type_card(tbl, i));	×
326
327	// name + one space
328	print_padded_string(f, type_name(tbl, i), name_size);	×
329
330	// definition
331	switch (type_kind(tbl, i)) {	×
332	case BOOL_TYPE:	×
333	case INT_TYPE:
334	case REAL_TYPE:
335	fputs(type2string[i], f);	×
336	fputc('\n', f);	×
337	break;	×
338	case BITVECTOR_TYPE:	×
339	fprintf(f, "(bitvector %"PRIu32")\n", bv_type_size(tbl, i));	×
340	break;	×
NEW 341	case FF_TYPE:	×
NEW 342	fprintf(f, "(finitefield");	×
NEW 343	q_print(f, ff_type_size(tbl, i));	×
NEW 344	fprintf(f, ")\n");	×
NEW 345	break;	×
346	case SCALAR_TYPE:	×
347	fprintf(f, "(enum, card = %"PRIu32")\n", scalar_type_cardinal(tbl, i));	×
348	break;	×
349	case UNINTERPRETED_TYPE:	×
350	fputs("(uninterpreted)\n", f);	×
351	break;	×
352	case VARIABLE_TYPE:	×
353	fprintf(f, "(variable, id = %"PRIu32")\n", type_variable_id(tbl, i));	×
354	break;	×
355	case TUPLE_TYPE:	×
356	fputs("(tuple", f);	×
357	m = tuple_type_arity(tbl, i);	×
358	for (j=0; j<m; j++) {	×
359	fputc(' ', f);	×
360	print_type_name(f, tbl, tuple_type_component(tbl, i, j));	×
361	}
362	fputs(")\n", f);	×
363	break;	×
364	case FUNCTION_TYPE:	×
365	fputs("(-> ", f);	×
366	m = function_type_arity(tbl, i);	×
367	for (j=0; j<m; j++) {	×
368	print_type_name(f, tbl, function_type_domain(tbl, i, j));	×
369	fputc(' ', f);	×
370	}
371	print_type_name(f, tbl, function_type_range(tbl, i));	×
372	fputs(")\n", f);	×
373	break;	×
374	case INSTANCE_TYPE:	×
375	fputc('(', f);	×
376	print_macro_name(f, tbl, instance_type_cid(tbl, i));	×
377	m = instance_type_arity(tbl, i);	×
378	for (j=0; j<m; j++) {	×
379	fputc(' ', f);	×
380	print_type_name(f, tbl, instance_type_param(tbl, i, j));	×
381	}
382	fputs(")\n", f);	×
383	break;	×
384	default:	×
385	fputs("invalid type code\n", f);	×
386	break;	×
387	}
388	}
389	}
390	}	×
391
392
393	/*
394	* All macros
395	*/
396	void print_type_macros(FILE f, type_table_t tbl) {	×
397	type_mtbl_t *mtbl;
398	uint32_t i, n;
399
400	mtbl = tbl->macro_tbl;	×
401	if (mtbl != NULL) {	×
402	n = type_macro_nelems(mtbl);	×
403	for (i=0; i<n; i++) {	×
404	if (good_type_macro(mtbl, i)) {	×
405	print_macro_def(f, tbl, i);	×
406	}
407	}
408	}
409	}	×
410
411
412	/*
413	* PRETTY PRINTING
414	*/
415
416	/*
417	* Print type name
418	*/
419	void pp_type_name(yices_pp_t printer, type_table_t tbl, type_t tau) {	×
420	char *name;
421
422	assert(good_type(tbl, tau));
423
424	if (tau <= real_id) {	×
425	name = (char*) type2string[tau];	×
426	} else {
427	name = type_name(tbl, tau);	×
428	}
429	if (name != NULL) {	×
430	pp_string(printer, name);	×
431	} else {
432	pp_id(printer, "tau!", tau);	×
433	}
434	}	×
435
436
437	/*
438	* Print type expression for tau: expand the type names if level > 0
439	*/
440	static void pp_type_recur(yices_pp_t printer, type_table_t tbl, type_t tau, int32_t level) {	×
441	char *name;
442	uint32_t i, n;
443
444	assert(good_type(tbl, tau));
445
446	if (tau <= real_id) {	×
447	pp_string(printer, (char *) type2string[tau]);	×
448	} else {
449	name = type_name(tbl, tau);	×
450	if (name != NULL && level <= 0) {	×
451	pp_string(printer, name);	×
452	} else {
453	switch (type_kind(tbl, tau)) {	×
454	case BITVECTOR_TYPE:	×
455	pp_open_block(printer, PP_OPEN_BV_TYPE);	×
456	pp_uint32(printer, bv_type_size(tbl, tau));	×
457	pp_close_block(printer, true);	×
458	break;	×
459
NEW 460	case FF_TYPE:	×
NEW 461	pp_open_block(printer, PP_OPEN_FF_TYPE);	×
NEW 462	pp_rational(printer, ff_type_size(tbl, tau));	×
NEW 463	pp_close_block(printer, true);	×
NEW 464	break;	×
465
UNCOV 466	case SCALAR_TYPE:	×
467	case UNINTERPRETED_TYPE:
468	if (name != NULL) {	×
469	pp_string(printer, name);	×
470	} else {
471	pp_id(printer, "tau!", tau);	×
472	}
473	break;	×
474
475	case VARIABLE_TYPE:	×
476	if (name != NULL) {	×
477	pp_string(printer, name);	×
478	} else {
479	pp_id(printer, "var!", type_variable_id(tbl, tau));	×
480	}
481	break;	×
482
483	case TUPLE_TYPE:	×
484	pp_open_block(printer, PP_OPEN_TUPLE_TYPE);	×
485	n = tuple_type_arity(tbl, tau);	×
486	for (i=0; i<n; i++) {	×
487	pp_type_recur(printer, tbl, tuple_type_component(tbl, tau, i), level - 1);	×
488	}
489	pp_close_block(printer, true);	×
490	break;	×
491
492	case FUNCTION_TYPE:	×
493	pp_open_block(printer, PP_OPEN_FUN_TYPE);	×
494	n = function_type_arity(tbl, tau);	×
495	for (i=0; i<n; i++) {	×
496	pp_type_recur(printer, tbl, function_type_domain(tbl, tau, i), level - 1);	×
497	}
498	pp_type_recur(printer, tbl, function_type_range(tbl, tau), level - 1);	×
499	pp_close_block(printer, true);	×
500	break;	×
501
502	case INSTANCE_TYPE:	×
503	pp_open_block(printer, PP_OPEN_PAR);	×
504	assert(tbl->macro_tbl != NULL);
505	pp_string(printer, type_macro_name(tbl->macro_tbl, instance_type_cid(tbl, tau)));	×
506	n = instance_type_arity(tbl, tau);	×
507	for (i=0; i<n; i++) {	×
508	pp_type_recur(printer, tbl, instance_type_param(tbl, tau, i), level - 1);	×
509	}
510	pp_close_block(printer, true);	×
511	break;	×
512
513	default:	×
514	assert(false);
515	break;	×
516	}
517	}
518	}
519	}	×
520
521
522	/*
523	* Expand top-level names
524	*/
525	void pp_type_exp(yices_pp_t printer, type_table_t tbl, type_t tau) {	×
526	pp_type_recur(printer, tbl, tau, 1);	×
527	}	×
528
529
530	/*
531	* Don't expand top-level names
532	*/
533	void pp_type(yices_pp_t printer, type_table_t tbl, type_t tau) {	×
534	pp_type_recur(printer, tbl, tau, 0);	×
535	}	×
536
537
538	/*
539	* Pretty printing of the full table
540	*/
541	void pp_type_table(FILE f, type_table_t tbl) {	×
542	yices_pp_t printer;
543	pp_area_t area;
544	uint32_t i, n;
545
546	area.width = 60;	×
547	area.height = 2;	×
548	area.offset = 11;	×
549	area.truncate = true;	×
550	area.stretch = false;	×
551
552	init_yices_pp(&printer, f, &area, PP_VMODE, 0);	×
553
554	n = ntypes(tbl);	×
555	for (i=0; i<n; i++) {	×
556	if (type_kind(tbl, i) != UNUSED_TYPE) {	×
557	fprintf(f, "type[%"PRIu32"]: ", i);	×
558	if (i < 10) fputc(' ', f);	×
559	if (i < 100) fputc(' ', f);	×
560	pp_type(&printer, tbl, i);	×
561	flush_yices_pp(&printer);	×
562	}
563	}
564
565	delete_yices_pp(&printer, false);	×
566	}	×
567
568

SRI-CSL / yices2 / 9226448713

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