16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Run Details

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

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

59.41

/src/terms/bvarith_buffer_terms.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/>.
 */

/*
 * BIT-VECTOR OPERATION INVOLVING BUFFERS AND TERMS
 */

#include <assert.h>

#include "terms/bvarith_buffer_terms.h"
#include "terms/term_utils.h"


/*
 * Initialize an auxiliary buffer aux, using the same store and prod table as b
 */
static void init_aux_buffer(bvarith_buffer_t *aux, bvarith_buffer_t *b) {
  init_bvarith_buffer(aux, b->ptbl, b->store);
  bvarith_buffer_prepare(aux, b->bitsize);
}


/*
 * Try to convert t to an arithmetic expression
 * - t must be a bv-array term
 * - return true if that succeeds, and store the result in buffer b
 * - otherwise return false and leave b unchanged.
 *
 * We currently just check for the case t = (bvnot x) or t = x.
 * If t is (bvnot x), we store -1 - x in b.
 */
static bool convert_bvarray_to_bvarith(term_table_t *table, term_t t, bvarith_buffer_t *b) {
  term_t t0;
  bool negated;

  if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
    if (negated) {
      // t is (bvnot t0) == (-t0) - 1
      bvarith_buffer_sub_one(b);
      bvarith_buffer_sub_term(b, table, t0);
    } else {
      bvarith_buffer_add_term(b, table, t0);
    }
    bvarith_buffer_normalize(b);
    return true;
  }

  return false;
}


/*
 * Copy t's value into buffer b
 * - t must be defined in table and be a bitvector term
 * - b->ptbl must be the same as table->pprods
 */
void bvarith_buffer_set_term(bvarith_buffer_t *b, term_table_t *table, term_t t) {
  uint32_t n;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t));

  n = term_bitsize(table, t);
  bvarith_buffer_prepare(b, n); // reset b
  bvarith_buffer_add_term(b, table, t);
}



/*
 * Add t to buffer b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith_buffer_add_term(bvarith_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  bvpoly_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith_buffer_add_pp(b, pprod_for_idx(table, i));
    break;

  case BV_CONSTANT:
    bvarith_buffer_add_const(b, bvconst_for_idx(table, i)->data);
    break;

  case BV_POLY:
    p = bvpoly_for_idx(table, i);
    v = pprods_for_bvpoly(table, p);
    bvarith_buffer_add_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith_buffer_sub_one(b);
        bvarith_buffer_sub_term(b, table, t0);
      } else {
        bvarith_buffer_add_term(b, table, t0);
      }
    } else {
      bvarith_buffer_add_var(b, t);
    }
    break;

  default:
    bvarith_buffer_add_var(b, t);
    break;
  }
}


/*
 * Subtract t from buffer b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith_buffer_sub_term(bvarith_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  bvpoly_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith_buffer_sub_pp(b, pprod_for_idx(table, i));
    break;

  case BV_CONSTANT:
    bvarith_buffer_sub_const(b, bvconst_for_idx(table, i)->data);
    break;

  case BV_POLY:
    p = bvpoly_for_idx(table, i);
    v = pprods_for_bvpoly(table, p);
    bvarith_buffer_sub_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith_buffer_add_one(b);
        bvarith_buffer_add_term(b, table, t0);
      } else {
        bvarith_buffer_sub_term(b, table, t0);
      }
    } else {
      bvarith_buffer_sub_var(b, t);
    }
    break;

  default:
    bvarith_buffer_sub_var(b, t);
    break;
  }
}



/*
 * Multiply b by t
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - b->ptbl must be the same as table->pprods
 */
void bvarith_buffer_mul_term(bvarith_buffer_t *b, term_table_t *table, term_t t) {
  bvarith_buffer_t aux;
  pprod_t **v;
  bvpoly_t *p;
  int32_t i;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith_buffer_mul_pp(b, pprod_for_idx(table, i));
    break;

  case BV_CONSTANT:
    bvarith_buffer_mul_const(b, bvconst_for_idx(table, i)->data);
    break;

  case BV_POLY:
    p = bvpoly_for_idx(table, i);
    v = pprods_for_bvpoly(table, p);
    bvarith_buffer_mul_bvpoly(b, p, v);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    init_aux_buffer(&aux, b);
    if (convert_bvarray_to_bvarith(table, t, &aux)) {
      bvarith_buffer_mul_buffer(b, &aux);
    } else {
      bvarith_buffer_mul_var(b, t);
    }
    delete_bvarith_buffer(&aux);
    break;

  default:
    bvarith_buffer_mul_var(b, t);
    break;
  }
}


/*
 * Add a * t to b
 * - t must be defined in table and be a bitvector term of same bitsize as b
 * - a must be have the same bitsize as b (as many words a b->width)
 * - b->ptbl must be the same as table->pprods
 */
void bvarith_buffer_add_const_times_term(bvarith_buffer_t *b, term_table_t *table, uint32_t *a, term_t t) {
  bvconstant_t c;
  pprod_t **v;
  bvpoly_t *p;
  int32_t i;
  term_t t0;
  bool negated;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    bvarith_buffer_add_mono(b, a, pprod_for_idx(table, i));
    break;

  case BV_CONSTANT:
    init_bvconstant(&c);
    bvconstant_copy(&c, b->bitsize, bvconst_for_idx(table, i)->data);
    bvconst_mul(c.data, b->width, a);
    bvarith_buffer_add_const(b, c.data);
    delete_bvconstant(&c);
    break;

  case BV_POLY:
    p = bvpoly_for_idx(table, i);
    v = pprods_for_bvpoly(table, p);
    bvarith_buffer_add_const_times_bvpoly(b, p, v, a);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    if (bvarray_convertible_to_term(table, t, &t0, &negated)) {
      if (negated) {
        // t is (bvnot t0) == (-t0) - 1
        bvarith_buffer_sub_const(b, a);
        init_bvconstant(&c);
        bvconstant_copy(&c, b->bitsize, a);
        bvconstant_negate(&c);  // c is -a
        bvarith_buffer_add_const_times_term(b, table, c.data, t0);
        delete_bvconstant(&c);
      } else {
        bvarith_buffer_add_const_times_term(b, table, a, t0);
      }
    } else {
      bvarith_buffer_add_varmono(b, a, t);
    }
    break;

  default:
    bvarith_buffer_add_varmono(b, a, t);
    break;
  }
}


/*
 * Multiply b by t^d
 * - t must be an arithmetic term
 * - p->ptbl and table->pprods must be equal
 */
void bvarith_buffer_mul_term_power(bvarith_buffer_t *b, term_table_t *table, term_t t, uint32_t d) {
  bvarith_buffer_t aux, aux2;
  bvconstant_t c;
  bvpoly_t *p;
  pprod_t **v;
  pprod_t *r;
  int32_t i;

  assert(b->ptbl == table->pprods);
  assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
         term_bitsize(table, t) == b->bitsize);

  i = index_of(t);
  switch (kind_for_idx(table, i)) {
  case POWER_PRODUCT:
    r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d
    bvarith_buffer_mul_pp(b, r);
    break;

  case BV_CONSTANT:
    init_bvconstant(&c);
    bvconstant_copy64(&c, b->bitsize, 1); // c := 1
    bvconst_mulpower(c.data, b->width, bvconst_for_idx(table, i)->data, d); // c := t^d
    bvarith_buffer_mul_const(b, c.data);
    delete_bvconstant(&c);
    break;

  case BV_POLY:
    p = bvpoly_for_idx(table, i);
    v = pprods_for_bvpoly(table, p);
    init_aux_buffer(&aux, b);
    bvarith_buffer_mul_bvpoly_power(b, p, v, d, &aux);
    delete_bvarith_buffer(&aux);
    term_table_reset_pbuffer(table);
    break;

  case BV_ARRAY:
    init_aux_buffer(&aux, b);
    if (convert_bvarray_to_bvarith(table, t, &aux)) {
      init_aux_buffer(&aux2, b);
      bvarith_buffer_mul_buffer_power(b, &aux, d, &aux2);
      delete_bvarith_buffer(&aux2);
    } else {
      r = pprod_varexp(b->ptbl, t, d);
      bvarith_buffer_mul_pp(b, r);
    }
    delete_bvarith_buffer(&aux);
    break;

  default:
    r = pprod_varexp(b->ptbl, t, d);
    bvarith_buffer_mul_pp(b, r);
    break;
  }
}

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	* BIT-VECTOR OPERATION INVOLVING BUFFERS AND TERMS
21	*/
22
23	#include <assert.h>
24
25	#include "terms/bvarith_buffer_terms.h"
26	#include "terms/term_utils.h"
27
28
29	/*
30	* Initialize an auxiliary buffer aux, using the same store and prod table as b
31	*/
32	static void init_aux_buffer(bvarith_buffer_t aux, bvarith_buffer_t b) {	34✔
33	init_bvarith_buffer(aux, b->ptbl, b->store);	34✔
34	bvarith_buffer_prepare(aux, b->bitsize);	34✔
35	}	34✔
36
37
38	/*
39	* Try to convert t to an arithmetic expression
40	* - t must be a bv-array term
41	* - return true if that succeeds, and store the result in buffer b
42	* - otherwise return false and leave b unchanged.
43	*
44	* We currently just check for the case t = (bvnot x) or t = x.
45	* If t is (bvnot x), we store -1 - x in b.
46	*/
47	static bool convert_bvarray_to_bvarith(term_table_t table, term_t t, bvarith_buffer_t b) {	34✔
48	term_t t0;
49	bool negated;
50
51	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	34✔
52	if (negated) {	1✔
53	// t is (bvnot t0) == (-t0) - 1
54	bvarith_buffer_sub_one(b);	1✔
55	bvarith_buffer_sub_term(b, table, t0);	1✔
56	} else {
57	bvarith_buffer_add_term(b, table, t0);	×
58	}
59	bvarith_buffer_normalize(b);	1✔
60	return true;	1✔
61	}
62
63	return false;	33✔
64	}
65
66
67	/*
68	* Copy t's value into buffer b
69	* - t must be defined in table and be a bitvector term
70	* - b->ptbl must be the same as table->pprods
71	*/
72	void bvarith_buffer_set_term(bvarith_buffer_t b, term_table_t table, term_t t) {	×
73	uint32_t n;
74
75	assert(b->ptbl == table->pprods);
76	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t));
77
78	n = term_bitsize(table, t);	×
79	bvarith_buffer_prepare(b, n); // reset b	×
80	bvarith_buffer_add_term(b, table, t);	×
81	}	×
82
83
84
85	/*
86	* Add t to buffer b
87	* - t must be defined in table and be a bitvector term of same bitsize as b
88	* - b->ptbl must be the same as table->pprods
89	*/
90	void bvarith_buffer_add_term(bvarith_buffer_t b, term_table_t table, term_t t) {	802✔
91	pprod_t **v;
92	bvpoly_t *p;
93	int32_t i;
94	term_t t0;
95	bool negated;
96
97	assert(b->ptbl == table->pprods);
98	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
99	term_bitsize(table, t) == b->bitsize);
100
101	i = index_of(t);	802✔
102	switch (kind_for_idx(table, i)) {	802✔
103	case POWER_PRODUCT:	2✔
104	bvarith_buffer_add_pp(b, pprod_for_idx(table, i));	2✔
105	break;	2✔
106
107	case BV_CONSTANT:	107✔
108	bvarith_buffer_add_const(b, bvconst_for_idx(table, i)->data);	107✔
109	break;	107✔
110
111	case BV_POLY:	7✔
112	p = bvpoly_for_idx(table, i);	7✔
113	v = pprods_for_bvpoly(table, p);	7✔
114	bvarith_buffer_add_bvpoly(b, p, v);	7✔
115	term_table_reset_pbuffer(table);	7✔
116	break;	7✔
117
118	case BV_ARRAY:	97✔
119	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	97✔
120	if (negated) {	8✔
121	// t is (bvnot t0) == (-t0) - 1
122	bvarith_buffer_sub_one(b);	8✔
123	bvarith_buffer_sub_term(b, table, t0);	8✔
124	} else {
125	bvarith_buffer_add_term(b, table, t0);	×
126	}
127	} else {
128	bvarith_buffer_add_var(b, t);	89✔
129	}
130	break;	97✔
131
132	default:	589✔
133	bvarith_buffer_add_var(b, t);	589✔
134	break;	589✔
135	}
136	}	802✔
137
138
139	/*
140	* Subtract t from buffer b
141	* - t must be defined in table and be a bitvector term of same bitsize as b
142	* - b->ptbl must be the same as table->pprods
143	*/
144	void bvarith_buffer_sub_term(bvarith_buffer_t b, term_table_t table, term_t t) {	168✔
145	pprod_t **v;
146	bvpoly_t *p;
147	int32_t i;
148	term_t t0;
149	bool negated;
150
151	assert(b->ptbl == table->pprods);
152	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
153	term_bitsize(table, t) == b->bitsize);
154
155	i = index_of(t);	168✔
156	switch (kind_for_idx(table, i)) {	168✔
157	case POWER_PRODUCT:	1✔
158	bvarith_buffer_sub_pp(b, pprod_for_idx(table, i));	1✔
159	break;	1✔
160
161	case BV_CONSTANT:	67✔
162	bvarith_buffer_sub_const(b, bvconst_for_idx(table, i)->data);	67✔
163	break;	67✔
164
165	case BV_POLY:	5✔
166	p = bvpoly_for_idx(table, i);	5✔
167	v = pprods_for_bvpoly(table, p);	5✔
168	bvarith_buffer_sub_bvpoly(b, p, v);	5✔
169	term_table_reset_pbuffer(table);	5✔
170	break;	5✔
171
172	case BV_ARRAY:	38✔
173	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	38✔
174	if (negated) {	2✔
175	// t is (bvnot t0) == (-t0) - 1
176	bvarith_buffer_add_one(b);	2✔
177	bvarith_buffer_add_term(b, table, t0);	2✔
178	} else {
179	bvarith_buffer_sub_term(b, table, t0);	×
180	}
181	} else {
182	bvarith_buffer_sub_var(b, t);	36✔
183	}
184	break;	38✔
185
186	default:	57✔
187	bvarith_buffer_sub_var(b, t);	57✔
188	break;	57✔
189	}
190	}	168✔
191
192
193
194	/*
195	* Multiply b by t
196	* - t must be defined in table and be a bitvector term of same bitsize as b
197	* - b->ptbl must be the same as table->pprods
198	*/
199	void bvarith_buffer_mul_term(bvarith_buffer_t b, term_table_t table, term_t t) {	49✔
200	bvarith_buffer_t aux;
201	pprod_t **v;
202	bvpoly_t *p;
203	int32_t i;
204
205	assert(b->ptbl == table->pprods);
206	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
207	term_bitsize(table, t) == b->bitsize);
208
209	i = index_of(t);	49✔
210	switch (kind_for_idx(table, i)) {	49✔
211	case POWER_PRODUCT:	1✔
212	bvarith_buffer_mul_pp(b, pprod_for_idx(table, i));	1✔
213	break;	1✔
214
215	case BV_CONSTANT:	3✔
216	bvarith_buffer_mul_const(b, bvconst_for_idx(table, i)->data);	3✔
217	break;	3✔
218
219	case BV_POLY:	4✔
220	p = bvpoly_for_idx(table, i);	4✔
221	v = pprods_for_bvpoly(table, p);	4✔
222	bvarith_buffer_mul_bvpoly(b, p, v);	4✔
223	term_table_reset_pbuffer(table);	4✔
224	break;	4✔
225
226	case BV_ARRAY:	22✔
227	init_aux_buffer(&aux, b);	22✔
228	if (convert_bvarray_to_bvarith(table, t, &aux)) {	22✔
229	bvarith_buffer_mul_buffer(b, &aux);	1✔
230	} else {
231	bvarith_buffer_mul_var(b, t);	21✔
232	}
233	delete_bvarith_buffer(&aux);	22✔
234	break;	22✔
235
236	default:	19✔
237	bvarith_buffer_mul_var(b, t);	19✔
238	break;	19✔
239	}
240	}	49✔
241
242
243	/*
244	* Add a * t to b
245	* - t must be defined in table and be a bitvector term of same bitsize as b
246	* - a must be have the same bitsize as b (as many words a b->width)
247	* - b->ptbl must be the same as table->pprods
248	*/
249	void bvarith_buffer_add_const_times_term(bvarith_buffer_t b, term_table_t table, uint32_t *a, term_t t) {	×
250	bvconstant_t c;
251	pprod_t **v;
252	bvpoly_t *p;
253	int32_t i;
254	term_t t0;
255	bool negated;
256
257	assert(b->ptbl == table->pprods);
258	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
259	term_bitsize(table, t) == b->bitsize);
260
261	i = index_of(t);	×
262	switch (kind_for_idx(table, i)) {	×
263	case POWER_PRODUCT:	×
264	bvarith_buffer_add_mono(b, a, pprod_for_idx(table, i));	×
265	break;	×
266
267	case BV_CONSTANT:	×
268	init_bvconstant(&c);	×
269	bvconstant_copy(&c, b->bitsize, bvconst_for_idx(table, i)->data);	×
270	bvconst_mul(c.data, b->width, a);	×
271	bvarith_buffer_add_const(b, c.data);	×
272	delete_bvconstant(&c);	×
273	break;	×
274
275	case BV_POLY:	×
276	p = bvpoly_for_idx(table, i);	×
277	v = pprods_for_bvpoly(table, p);	×
278	bvarith_buffer_add_const_times_bvpoly(b, p, v, a);	×
279	term_table_reset_pbuffer(table);	×
280	break;	×
281
282	case BV_ARRAY:	×
283	if (bvarray_convertible_to_term(table, t, &t0, &negated)) {	×
284	if (negated) {	×
285	// t is (bvnot t0) == (-t0) - 1
286	bvarith_buffer_sub_const(b, a);	×
287	init_bvconstant(&c);	×
288	bvconstant_copy(&c, b->bitsize, a);	×
289	bvconstant_negate(&c); // c is -a	×
290	bvarith_buffer_add_const_times_term(b, table, c.data, t0);	×
291	delete_bvconstant(&c);	×
292	} else {
293	bvarith_buffer_add_const_times_term(b, table, a, t0);	×
294	}
295	} else {
296	bvarith_buffer_add_varmono(b, a, t);	×
297	}
298	break;	×
299
300	default:	×
301	bvarith_buffer_add_varmono(b, a, t);	×
302	break;	×
303	}
304	}	×
305
306
307	/*
308	* Multiply b by t^d
309	* - t must be an arithmetic term
310	* - p->ptbl and table->pprods must be equal
311	*/
312	void bvarith_buffer_mul_term_power(bvarith_buffer_t b, term_table_t table, term_t t, uint32_t d) {	12✔
313	bvarith_buffer_t aux, aux2;
314	bvconstant_t c;
315	bvpoly_t *p;
316	pprod_t **v;
317	pprod_t *r;
318	int32_t i;
319
320	assert(b->ptbl == table->pprods);
321	assert(pos_term(t) && good_term(table, t) && is_bitvector_term(table, t) &&
322	term_bitsize(table, t) == b->bitsize);
323
324	i = index_of(t);	12✔
325	switch (kind_for_idx(table, i)) {	12✔
326	case POWER_PRODUCT:	×
327	r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d	×
328	bvarith_buffer_mul_pp(b, r);	×
329	break;	×
330
331	case BV_CONSTANT:	×
332	init_bvconstant(&c);	×
333	bvconstant_copy64(&c, b->bitsize, 1); // c := 1	×
334	bvconst_mulpower(c.data, b->width, bvconst_for_idx(table, i)->data, d); // c := t^d	×
335	bvarith_buffer_mul_const(b, c.data);	×
336	delete_bvconstant(&c);	×
337	break;	×
338
339	case BV_POLY:	×
340	p = bvpoly_for_idx(table, i);	×
341	v = pprods_for_bvpoly(table, p);	×
342	init_aux_buffer(&aux, b);	×
343	bvarith_buffer_mul_bvpoly_power(b, p, v, d, &aux);	×
344	delete_bvarith_buffer(&aux);	×
345	term_table_reset_pbuffer(table);	×
346	break;	×
347
348	case BV_ARRAY:	12✔
349	init_aux_buffer(&aux, b);	12✔
350	if (convert_bvarray_to_bvarith(table, t, &aux)) {	12✔
351	init_aux_buffer(&aux2, b);	×
352	bvarith_buffer_mul_buffer_power(b, &aux, d, &aux2);	×
353	delete_bvarith_buffer(&aux2);	×
354	} else {
355	r = pprod_varexp(b->ptbl, t, d);	12✔
356	bvarith_buffer_mul_pp(b, r);	12✔
357	}
358	delete_bvarith_buffer(&aux);	12✔
359	break;	12✔
360
361	default:	×
362	r = pprod_varexp(b->ptbl, t, d);	×
363	bvarith_buffer_mul_pp(b, r);	×
364	break;	×
365	}
366	}	12✔

SRI-CSL / yices2 / 16032530443

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