26675300141

Committed 29 May 2026 08:46PM UTC coverage: 68.798% (+3.4%) from 65.375%

Build # 26675300141

Build Type

push

github

Committed by

ahmed-irfan

Commit Message

Rework clause-deletion heuristic to CaDiCaL-style schedule

Replace the geometric, learned-clause-count-triggered reduce schedule
with a CaDiCaL-style one: trigger on conflict count and rebase the
reduction bound to num_conflicts + r-interval * sqrt(num_conflicts).

- context_solver.c: factor the reduce step into try_reduce_heuristic();
  trigger on num_conflicts instead of num_learned_clauses; widen the
  running reduce_threshold to uint64_t (conflict count is unbounded).
- search_parameters: drop r-threshold/r-fraction/r-factor, add
  r-initial-threshold and r-interval (defaults 300 / 25, matching
  CaDiCaL's reduceinit / reduceint).
- Update doc/YICES-LANGUAGE, doc/sphinx parameters table, and the
  interactive (help ...) entries for the renamed parameters.

Coverage Stats

10 of 10 new or added lines in 1 file covered. (100.0%)

8005 existing lines in 44 files now uncovered.

87475 of 127148 relevant lines covered (68.8%)

1646632.75 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) {	53,042✔
36	s->size = n;	53,042✔
37	s->index = 0;	53,042✔
38	s->data = NULL;	53,042✔
39	if (n > 0) {	53,042✔
40	s->data = (char *) safe_malloc(n);	53,042✔
41	}
42	}	53,042✔
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) {	74,553✔
49	uint32_t p;
50
51	n += s->index;	74,553✔
52	if (n < s->index) {	74,553✔
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;	74,553✔
59	if (p < n) {	74,553✔
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	}	74,553✔
68
69
70	/*
71	* Faster version: make room for one character
72	*/
73	static void string_buffer_extend1(string_buffer_t *s) {	18,495,385✔
74	uint32_t p;
75
76	if (s->index == s->size) {	18,495,385✔
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,495,385✔
87
88
89	/*
90	* Delete: free data array
91	*/
92	void delete_string_buffer(string_buffer_t *s) {	53,042✔
93	safe_free(s->data);	53,042✔
94	s->data = NULL;	53,042✔
95	s->size = 0;	53,042✔
96	s->index = 0;	53,042✔
97	}	53,042✔
98
99
100	/*
101	* Close: append '\0', do not increment the index
102	*/
103	void string_buffer_close(string_buffer_t *s) {	3,183,505✔
104	string_buffer_extend1(s);	3,183,505✔
105	s->data[s->index] = '\0';	3,183,505✔
106	}	3,183,505✔
107
108
109	/*
110	* Append operations
111	*/
112	void string_buffer_append_char(string_buffer_t *s, char c) {	15,311,880✔
113	string_buffer_extend1(s);	15,311,880✔
114	s->data[s->index] = c;	15,311,880✔
115	s->index ++;	15,311,880✔
116	}	15,311,880✔
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) {	10,301✔
120	size_t n;
121
122	n = strlen(s1);	10,301✔
123	if (n > UINT32_MAX) {	10,301✔
124	out_of_memory();	×
125	}
126	string_buffer_extend(s, (uint32_t) n);	10,301✔
127	memcpy(s->data + s->index, s1, n);	10,301✔
128	s->index += n;	10,301✔
129	}	10,301✔
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) {	51,020✔
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);	51,020✔
146	n = sprintf(s->data + s->index, "%"PRId32, x);	51,020✔
147	assert(n <= 12 && n > 0);
148	s->index += n;	51,020✔
149	}	51,020✔
150
151	void string_buffer_append_uint32(string_buffer_t *s, uint32_t x) {	6,795✔
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,795✔
156	n = sprintf(s->data + s->index, "%"PRIu32, x);	6,795✔
157	assert(n <= 12 && n > 0);
158	s->index += n;	6,795✔
159	}	6,795✔
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) {	906✔
192	size_t n1, n;
193	char *s0;
194
195	n1 = mpz_sizeinbase(mpq_numref(q), 10);	906✔
196	n = n1 + mpz_sizeinbase(mpq_denref(q), 10);	906✔
197	if (n > UINT32_MAX - 3 \|\| n < n1) {	906✔
198	// too large or numerical overflow
199	out_of_memory();	×
200	}
201	string_buffer_extend(s, (uint32_t) (n + 3));	906✔
202	s0 = s->data + s->index;	906✔
203	mpq_get_str(s0, 10, q);	906✔
204	s->index += strlen(s0);	906✔
205	}	906✔
206
207	void string_buffer_append_rational(string_buffer_t s, const rational_t r) {	42,668✔
208	if (is_ratgmp(r)) {	42,668✔
209	string_buffer_append_mpq(s, get_gmp(r));	906✔
210	} else {
211	string_buffer_append_int32(s, get_num(r));	41,762✔
212	if (get_den(r) != 1) {	41,762✔
213	string_buffer_append_char(s, '/');	4✔
214	string_buffer_append_uint32(s, get_den(r));	4✔
215	}
216	}
217	}	42,668✔
218
219	void string_buffer_append_bvconst(string_buffer_t s, uint32_t bv, uint32_t n) {	5,527✔
220	char *s0;
221
222	assert(n>0);
223	string_buffer_extend(s, n);	5,527✔
224	s0 = s->data + s->index;	5,527✔
225	s->index += n;	5,527✔
226
227	do {
228	n --;	73,308✔
229	*s0 ++ = bvconst_tst_bit(bv, n) ? '1' : '0';	73,308✔
230	} while (n>0);	73,308✔
231	}	5,527✔
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) {	5✔
250	char *tmp;
251
252	string_buffer_close(s);	5✔
253	tmp = s->data;	5✔
254	*len = s->index;	5✔
255
256	// reset to an empty buffer
257	s->size = 0;	5✔
258	s->index = 0;	5✔
259	s->data = NULL;	5✔
260
261	return tmp;	5✔
262	}
263

SRI-CSL / yices2 / 26675300141

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