25418071995

Committed 06 May 2026 05:24AM UTC coverage: 66.69% (+0.003%) from 66.687%

Build # 25418071995

Build Type

Pull #623

github

Committed by

ahmed-irfan

Commit Message

smt2: address review feedback on algebraic printer (PR #623)

- Assert that libpoly isolating intervals are always strictly open
  (a_open == b_open == 1), matching root-of-with-interval's
  exclusive-bound convention; catches any future libpoly change
- Add comment above smt2_pp_algebraic citing the SMT-COMP 2026
  model-validation format spec
- Cast size_t q->n to unsigned long explicitly before passing to
  mpz_ui_pow_ui to silence truncation warnings on LLP64 targets

Pull Request Pull Request #623: smt2: print algebraic numbers in SMT-COMP 2026 root-of-with-interval …

Coverage Stats

74 of 78 new or added lines in 1 file covered. (94.87%)

27 existing lines in 2 files now uncovered.

83511 of 125222 relevant lines covered (66.69%)

1643495.28 hits per line

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

81.15

/src/utils/string_buffers.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/>.
 */

/*
 * Resizable string buffers
 */

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

#include "utils/memalloc.h"
#include "utils/string_buffers.h"


/*
 * Initialize: n = initial size
 */
void init_string_buffer(string_buffer_t *s, uint32_t n) {
  s->size = n;
  s->index = 0;
  s->data = NULL;
  if (n > 0) {
    s->data = (char *) safe_malloc(n);
  }
}


/*
 * Expand: make room for at least n extra characters after index.
 */
static void string_buffer_extend(string_buffer_t *s, uint32_t n) {
  uint32_t p;

  n += s->index;
  if (n < s->index) {
    // integer overflow: can't make s large enough
    out_of_memory();
  }

  // try 50% larger. If that's still too small, take n as the new size
  p = s->size;
  if (p < n) {
    p ++;
    p += p>>1;
    if (p < n) p = n;

    s->data = (char *) safe_realloc(s->data, p);
    s->size = p;
  }
}


/*
 * Faster version: make room for one character
 */
static void string_buffer_extend1(string_buffer_t *s) {
  uint32_t p;

  if (s->index == s->size) {
    if (s->size == UINT32_MAX) {
      out_of_memory();
    }
    p = s->size + 1;
    p += p>>1;

    s->data = (char *) safe_realloc(s->data, p);
    s->size = p;
  }
}


/*
 * Delete: free data array
 */
void delete_string_buffer(string_buffer_t *s) {
  safe_free(s->data);
  s->data = NULL;
  s->size = 0;
  s->index = 0;
}


/*
 * Close: append '\0', do not increment the index
 */
void string_buffer_close(string_buffer_t *s) {
  string_buffer_extend1(s);
  s->data[s->index] = '\0';
}


/*
 * Append operations
 */
void string_buffer_append_char(string_buffer_t *s, char c) {
  string_buffer_extend1(s);
  s->data[s->index] = c;
  s->index ++;
}

// s1 must be null-terminated, the '\0' is not copied in s
void string_buffer_append_string(string_buffer_t *s, const char *s1) {
  size_t n;

  n = strlen(s1);
  if (n > UINT32_MAX) {
    out_of_memory();
  }
  string_buffer_extend(s, (uint32_t) n);
  memcpy(s->data + s->index, s1, n);
  s->index += n;
}

void string_buffer_append_buffer(string_buffer_t *s, string_buffer_t *s1) {
  uint32_t n;

  n = string_buffer_length(s1);
  string_buffer_extend(s, n);
  memcpy(s->data + s->index, s1->data, n);
  s->index += n;
}


void string_buffer_append_int32(string_buffer_t *s, int32_t x) {
  int32_t n;
  // max space to print a 32bit number in decimal is
  // 12 character (including sign and trailing zero)
  string_buffer_extend(s, 12);
  n = sprintf(s->data + s->index, "%"PRId32, x);
  assert(n <= 12 && n > 0);
  s->index += n;
}

void string_buffer_append_uint32(string_buffer_t *s, uint32_t x) {
  int32_t n;
  // max space to print a 32bit number in decimal is
  // 12 character (including sign and trailing zero)
  string_buffer_extend(s, 12);
  n = sprintf(s->data + s->index, "%"PRIu32, x);
  assert(n <= 12 && n > 0);
  s->index += n;
}

void string_buffer_append_double(string_buffer_t *s, double x) {
  int32_t n, size;

  size = 0;
  do {
    size += 100;
    string_buffer_extend(s, size);
    n = snprintf(s->data + s->index, size, "%f", x);
    assert(n > 0);
  } while (n >= s->size);

  s->index += n;
}

void string_buffer_append_mpz(string_buffer_t *s, mpz_t z) {
  size_t n;
  char *s0;

  // sizeinbase may overestimate the actual length by one
  n = mpz_sizeinbase(z, 10);
  if (n > UINT32_MAX - 2) {
    out_of_memory();
  }
  string_buffer_extend(s, (uint32_t) (n + 2));
  s0 = s->data + s->index;
  mpz_get_str(s0, 10, z);
  // we can't use n here
  s->index += strlen(s0);
}

void string_buffer_append_mpq(string_buffer_t *s, mpq_t q) {
  size_t n1, n;
  char *s0;

  n1 = mpz_sizeinbase(mpq_numref(q), 10);
  n = n1 + mpz_sizeinbase(mpq_denref(q), 10);
  if (n > UINT32_MAX - 3 || n < n1) {
    // too large or numerical overflow
    out_of_memory();
  }
  string_buffer_extend(s, (uint32_t) (n + 3));
  s0 = s->data + s->index;
  mpq_get_str(s0, 10, q);
  s->index += strlen(s0);
}

void string_buffer_append_rational(string_buffer_t *s, const rational_t *r) {
  if (is_ratgmp(r)) {
    string_buffer_append_mpq(s, get_gmp(r));
  } else {
    string_buffer_append_int32(s, get_num(r));
    if (get_den(r) != 1) {
      string_buffer_append_char(s, '/');
      string_buffer_append_uint32(s, get_den(r));
    }
  }
}

void string_buffer_append_bvconst(string_buffer_t *s, uint32_t *bv, uint32_t n) {
  char *s0;

  assert(n>0);
  string_buffer_extend(s, n);
  s0 = s->data + s->index;
  s->index += n;

  do {
    n --;
    *s0 ++ = bvconst_tst_bit(bv, n) ? '1' : '0';
  } while (n>0);
}


/*
 * Print the full buffer
 */
void string_buffer_print(FILE *f, string_buffer_t *s) {
  string_buffer_close(s);
  fputs(s->data, f);
}


/*
 * Export:
 * - close the string (add '\0') then return it
 * - store the string's size in *len
 * - then reset the buffer.
 */
char *string_buffer_export(string_buffer_t *s, uint32_t *len) {
  char *tmp;

  string_buffer_close(s);
  tmp = s->data;
  *len = s->index;

  // reset to an empty buffer
  s->size = 0;
  s->index = 0;
  s->data = NULL;

  return tmp;
}


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	* Resizable string buffers
21	*/
22
23	#include <stdio.h>
24	#include <string.h>
25	#include <inttypes.h>
26	#include <assert.h>
27
28	#include "utils/memalloc.h"
29	#include "utils/string_buffers.h"
30
31
32	/*
33	* Initialize: n = initial size
34	*/
35	void init_string_buffer(string_buffer_t *s, uint32_t n) {	52,992✔
36	s->size = n;	52,992✔
37	s->index = 0;	52,992✔
38	s->data = NULL;	52,992✔
39	if (n > 0) {	52,992✔
40	s->data = (char *) safe_malloc(n);	52,992✔
41	}
42	}	52,992✔
43
44
45	/*
46	* Expand: make room for at least n extra characters after index.
47	*/
48	static void string_buffer_extend(string_buffer_t *s, uint32_t n) {	81,604✔
49	uint32_t p;
50
51	n += s->index;	81,604✔
52	if (n < s->index) {	81,604✔
53	// integer overflow: can't make s large enough
54	out_of_memory();	×
55	}
56
57	// try 50% larger. If that's still too small, take n as the new size
58	p = s->size;	81,604✔
59	if (p < n) {	81,604✔
60	p ++;	5✔
61	p += p>>1;	5✔
62	if (p < n) p = n;	5✔
63
64	s->data = (char *) safe_realloc(s->data, p);	5✔
65	s->size = p;	5✔
66	}
67	}	81,604✔
68
69
70	/*
71	* Faster version: make room for one character
72	*/
73	static void string_buffer_extend1(string_buffer_t *s) {	18,492,524✔
74	uint32_t p;
75
76	if (s->index == s->size) {	18,492,524✔
77	if (s->size == UINT32_MAX) {	1,529✔
78	out_of_memory();	×
79	}
80	p = s->size + 1;	1,529✔
81	p += p>>1;	1,529✔
82
83	s->data = (char *) safe_realloc(s->data, p);	1,529✔
84	s->size = p;	1,529✔
85	}
86	}	18,492,524✔
87
88
89	/*
90	* Delete: free data array
91	*/
92	void delete_string_buffer(string_buffer_t *s) {	52,992✔
93	safe_free(s->data);	52,992✔
94	s->data = NULL;	52,992✔
95	s->size = 0;	52,992✔
96	s->index = 0;	52,992✔
97	}	52,992✔
98
99
100	/*
101	* Close: append '\0', do not increment the index
102	*/
103	void string_buffer_close(string_buffer_t *s) {	3,185,199✔
104	string_buffer_extend1(s);	3,185,199✔
105	s->data[s->index] = '\0';	3,185,199✔
106	}	3,185,199✔
107
108
109	/*
110	* Append operations
111	*/
112	void string_buffer_append_char(string_buffer_t *s, char c) {	15,307,325✔
113	string_buffer_extend1(s);	15,307,325✔
114	s->data[s->index] = c;	15,307,325✔
115	s->index ++;	15,307,325✔
116	}	15,307,325✔
117
118	// s1 must be null-terminated, the '\0' is not copied in s
119	void string_buffer_append_string(string_buffer_t s, const char s1) {	14,490✔
120	size_t n;
121
122	n = strlen(s1);	14,490✔
123	if (n > UINT32_MAX) {	14,490✔
124	out_of_memory();	×
125	}
126	string_buffer_extend(s, (uint32_t) n);	14,490✔
127	memcpy(s->data + s->index, s1, n);	14,490✔
128	s->index += n;	14,490✔
129	}	14,490✔
130
131	void string_buffer_append_buffer(string_buffer_t s, string_buffer_t s1) {	×
132	uint32_t n;
133
134	n = string_buffer_length(s1);	×
135	string_buffer_extend(s, n);	×
136	memcpy(s->data + s->index, s1->data, n);	×
137	s->index += n;	×
138	}	×
139
140
141	void string_buffer_append_int32(string_buffer_t *s, int32_t x) {	54,570✔
142	int32_t n;
143	// max space to print a 32bit number in decimal is
144	// 12 character (including sign and trailing zero)
145	string_buffer_extend(s, 12);	54,570✔
146	n = sprintf(s->data + s->index, "%"PRId32, x);	54,570✔
147	assert(n <= 12 && n > 0);
148	s->index += n;	54,570✔
149	}	54,570✔
150
151	void string_buffer_append_uint32(string_buffer_t *s, uint32_t x) {	6,181✔
152	int32_t n;
153	// max space to print a 32bit number in decimal is
154	// 12 character (including sign and trailing zero)
155	string_buffer_extend(s, 12);	6,181✔
156	n = sprintf(s->data + s->index, "%"PRIu32, x);	6,181✔
157	assert(n <= 12 && n > 0);
158	s->index += n;	6,181✔
159	}	6,181✔
160
UNCOV 161	void string_buffer_append_double(string_buffer_t *s, double x) {	×
162	int32_t n, size;
163
UNCOV 164	size = 0;	×
165	do {
UNCOV 166	size += 100;	×
UNCOV 167	string_buffer_extend(s, size);	×
UNCOV 168	n = snprintf(s->data + s->index, size, "%f", x);	×
169	assert(n > 0);
UNCOV 170	} while (n >= s->size);	×
171
UNCOV 172	s->index += n;	×
UNCOV 173	}	×
174
175	void string_buffer_append_mpz(string_buffer_t *s, mpz_t z) {	4✔
176	size_t n;
177	char *s0;
178
179	// sizeinbase may overestimate the actual length by one
180	n = mpz_sizeinbase(z, 10);	4✔
181	if (n > UINT32_MAX - 2) {	4✔
182	out_of_memory();	×
183	}
184	string_buffer_extend(s, (uint32_t) (n + 2));	4✔
185	s0 = s->data + s->index;	4✔
186	mpz_get_str(s0, 10, z);	4✔
187	// we can't use n here
188	s->index += strlen(s0);	4✔
189	}	4✔
190
191	void string_buffer_append_mpq(string_buffer_t *s, mpq_t q) {	888✔
192	size_t n1, n;
193	char *s0;
194
195	n1 = mpz_sizeinbase(mpq_numref(q), 10);	888✔
196	n = n1 + mpz_sizeinbase(mpq_denref(q), 10);	888✔
197	if (n > UINT32_MAX - 3 \|\| n < n1) {	888✔
198	// too large or numerical overflow
199	out_of_memory();	×
200	}
201	string_buffer_extend(s, (uint32_t) (n + 3));	888✔
202	s0 = s->data + s->index;	888✔
203	mpq_get_str(s0, 10, q);	888✔
204	s->index += strlen(s0);	888✔
205	}	888✔
206
207	void string_buffer_append_rational(string_buffer_t s, const rational_t r) {	41,976✔
208	if (is_ratgmp(r)) {	41,976✔
209	string_buffer_append_mpq(s, get_gmp(r));	888✔
210	} else {
211	string_buffer_append_int32(s, get_num(r));	41,088✔
212	if (get_den(r) != 1) {	41,088✔
213	string_buffer_append_char(s, '/');	4✔
214	string_buffer_append_uint32(s, get_den(r));	4✔
215	}
216	}
217	}	41,976✔
218
219	void string_buffer_append_bvconst(string_buffer_t s, uint32_t bv, uint32_t n) {	5,471✔
220	char *s0;
221
222	assert(n>0);
223	string_buffer_extend(s, n);	5,471✔
224	s0 = s->data + s->index;	5,471✔
225	s->index += n;	5,471✔
226
227	do {
228	n --;	72,210✔
229	*s0 ++ = bvconst_tst_bit(bv, n) ? '1' : '0';	72,210✔
230	} while (n>0);	72,210✔
231	}	5,471✔
232
233
234	/*
235	* Print the full buffer
236	*/
237	void string_buffer_print(FILE f, string_buffer_t s) {	×
238	string_buffer_close(s);	×
239	fputs(s->data, f);	×
240	}	×
241
242
243	/*
244	* Export:
245	* - close the string (add '\0') then return it
246	* - store the string's size in *len
247	* - then reset the buffer.
248	*/
249	char string_buffer_export(string_buffer_t s, uint32_t *len) {	2✔
250	char *tmp;
251
252	string_buffer_close(s);	2✔
253	tmp = s->data;	2✔
254	*len = s->index;	2✔
255
256	// reset to an empty buffer
257	s->size = 0;	2✔
258	s->index = 0;	2✔
259	s->data = NULL;	2✔
260
261	return tmp;	2✔
262	}
263

SRI-CSL / yices2 / 25418071995

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