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

63.55

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

/*
 * ARITHMETIC OPERATIONS INVOLVING RED-BLACK BUFFERS AND TERMS
 */

#include <assert.h>

#include "terms/rba_buffer_terms.h"


/*
 * Add t to buffer b
 * - t must be an arithmetic term
 * - b->ptbl and table->pprods must be equal
 */
void rba_buffer_add_term(rba_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  polynomial_t *p;
  int32_t i;

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

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

  case ARITH_CONSTANT:
  case ARITH_FF_CONSTANT:
    rba_buffer_add_const(b, rational_for_idx(table, i));
    break;

  case ARITH_POLY:
  case ARITH_FF_POLY:
    p = polynomial_for_idx(table, i);
    v = pprods_for_poly(table, p);
    rba_buffer_add_monarray(b, p->mono, v);
    term_table_reset_pbuffer(table);
    break;

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


/*
 * Subtract t from buffer b
 * - t must be an arithmetic term
 * - b->ptbl and table->pprods must be equal
 */
void rba_buffer_sub_term(rba_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  polynomial_t *p;
  int32_t i;

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

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

  case ARITH_CONSTANT:
  case ARITH_FF_CONSTANT:
    rba_buffer_sub_const(b, rational_for_idx(table, i));
    break;

  case ARITH_POLY:
  case ARITH_FF_POLY:
    p = polynomial_for_idx(table, i);
    v = pprods_for_poly(table, p);
    rba_buffer_sub_monarray(b, p->mono, v);
    term_table_reset_pbuffer(table);
    break;

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


/*
 * Multiply b by t
 * - t must be an arithmetic term
 * - b->ptbl and table->pprods must be equal
 */
void rba_buffer_mul_term(rba_buffer_t *b, term_table_t *table, term_t t) {
  pprod_t **v;
  polynomial_t *p;
  int32_t i;

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

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

  case ARITH_CONSTANT:
  case ARITH_FF_CONSTANT:
    rba_buffer_mul_const(b, rational_for_idx(table, i));
    break;

  case ARITH_POLY:
  case ARITH_FF_POLY:
    p = polynomial_for_idx(table, i);
    v = pprods_for_poly(table, p);
    rba_buffer_mul_monarray(b, p->mono, v);
    term_table_reset_pbuffer(table);
    break;

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


/*
 * Add t * a to b
 * - t must be an arithmetic term
 * - b->ptbl and table->pprods must be equal
 */
void rba_buffer_add_const_times_term(rba_buffer_t *b, term_table_t *table, rational_t *a, term_t t) {
  rational_t q;
  pprod_t **v;
  polynomial_t *p;
  int32_t i;

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

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

  case ARITH_CONSTANT:
  case ARITH_FF_CONSTANT:
    q_init(&q);
    q_set(&q, a);
    q_mul(&q, rational_for_idx(table, i));
    rba_buffer_add_const(b, &q);
    q_clear(&q);
    break;

  case ARITH_POLY:
  case ARITH_FF_POLY:
    p = polynomial_for_idx(table, i);
    v = pprods_for_poly(table, p);
    rba_buffer_add_const_times_monarray(b, p->mono, v, a);
    term_table_reset_pbuffer(table);
    break;

  default:
    rba_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 rba_buffer_mul_term_power(rba_buffer_t *b, term_table_t *table, term_t t, uint32_t d) {
  rba_buffer_t aux;
  rational_t q;
  pprod_t **v;
  polynomial_t *p;
  pprod_t *r;
  int32_t i;

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

  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
    rba_buffer_mul_pp(b, r);
    break;

  case ARITH_CONSTANT:
  case ARITH_FF_CONSTANT:
    q_init(&q);
    q_set_one(&q);
    q_mulexp(&q, rational_for_idx(table, i), d); // q = t^d
    rba_buffer_mul_const(b, &q);
    q_clear(&q);
    break;

  case ARITH_POLY:
  case ARITH_FF_POLY:
    p = polynomial_for_idx(table, i);
    v = pprods_for_poly(table, p);
    init_rba_buffer(&aux, b->ptbl);
    rba_buffer_mul_monarray_power(b, p->mono, v, d, &aux);
    delete_rba_buffer(&aux);
    term_table_reset_pbuffer(table);
    break;

  default:
    r = pprod_varexp(b->ptbl, t, d);
    rba_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	* ARITHMETIC OPERATIONS INVOLVING RED-BLACK BUFFERS AND TERMS
21	*/
22
23	#include <assert.h>
24
25	#include "terms/rba_buffer_terms.h"
26
27
28	/*
29	* Add t to buffer b
30	* - t must be an arithmetic term
31	* - b->ptbl and table->pprods must be equal
32	*/
33	void rba_buffer_add_term(rba_buffer_t b, term_table_t table, term_t t) {	92,158✔
34	pprod_t **v;
35	polynomial_t *p;
36	int32_t i;
37
38	assert(b->ptbl == table->pprods);
39	assert(pos_term(t) && good_term(table, t) && (is_arithmetic_term(table, t) \|\| is_finitefield_term(table, t)));
40
41	i = index_of(t);	92,158✔
42	switch (kind_for_idx(table, i)) {	92,158✔
43	case POWER_PRODUCT:	×
44	rba_buffer_add_pp(b, pprod_for_idx(table, i));	×
45	break;	×
46
47	case ARITH_CONSTANT:	8,131✔
48	case ARITH_FF_CONSTANT:
49	rba_buffer_add_const(b, rational_for_idx(table, i));	8,131✔
50	break;	8,131✔
51
52	case ARITH_POLY:	19,137✔
53	case ARITH_FF_POLY:
54	p = polynomial_for_idx(table, i);	19,137✔
55	v = pprods_for_poly(table, p);	19,137✔
56	rba_buffer_add_monarray(b, p->mono, v);	19,137✔
57	term_table_reset_pbuffer(table);	19,137✔
58	break;	19,137✔
59
60	default:	64,890✔
61	rba_buffer_add_var(b, t);	64,890✔
62	break;	64,890✔
63	}
64	}	92,158✔
65
66
67	/*
68	* Subtract t from buffer b
69	* - t must be an arithmetic term
70	* - b->ptbl and table->pprods must be equal
71	*/
72	void rba_buffer_sub_term(rba_buffer_t b, term_table_t table, term_t t) {	67,246✔
73	pprod_t **v;
74	polynomial_t *p;
75	int32_t i;
76
77	assert(b->ptbl == table->pprods);
78	assert(pos_term(t) && good_term(table, t) && (is_arithmetic_term(table, t) \|\| is_finitefield_term(table, t)));
79
80	i = index_of(t);	67,246✔
81	switch (kind_for_idx(table, i)) {	67,246✔
82	case POWER_PRODUCT:	×
83	rba_buffer_sub_pp(b, pprod_for_idx(table, i));	×
84	break;	×
85
86	case ARITH_CONSTANT:	23,724✔
87	case ARITH_FF_CONSTANT:
88	rba_buffer_sub_const(b, rational_for_idx(table, i));	23,724✔
89	break;	23,724✔
90
91	case ARITH_POLY:	7,278✔
92	case ARITH_FF_POLY:
93	p = polynomial_for_idx(table, i);	7,278✔
94	v = pprods_for_poly(table, p);	7,278✔
95	rba_buffer_sub_monarray(b, p->mono, v);	7,278✔
96	term_table_reset_pbuffer(table);	7,278✔
97	break;	7,278✔
98
99	default:	36,244✔
100	rba_buffer_sub_var(b, t);	36,244✔
101	break;	36,244✔
102	}
103	}	67,246✔
104
105
106	/*
107	* Multiply b by t
108	* - t must be an arithmetic term
109	* - b->ptbl and table->pprods must be equal
110	*/
111	void rba_buffer_mul_term(rba_buffer_t b, term_table_t table, term_t t) {	4,515✔
112	pprod_t **v;
113	polynomial_t *p;
114	int32_t i;
115
116	assert(b->ptbl == table->pprods);
117	assert(pos_term(t) && good_term(table, t) && (is_arithmetic_term(table, t) \|\| is_finitefield_term(table, t)));
118
119	i = index_of(t);	4,515✔
120	switch (kind_for_idx(table, i)) {	4,515✔
121	case POWER_PRODUCT:	×
122	rba_buffer_mul_pp(b, pprod_for_idx(table, i));	×
123	break;	×
124
125	case ARITH_CONSTANT:	229✔
126	case ARITH_FF_CONSTANT:
127	rba_buffer_mul_const(b, rational_for_idx(table, i));	229✔
128	break;	229✔
129
130	case ARITH_POLY:	344✔
131	case ARITH_FF_POLY:
132	p = polynomial_for_idx(table, i);	344✔
133	v = pprods_for_poly(table, p);	344✔
134	rba_buffer_mul_monarray(b, p->mono, v);	344✔
135	term_table_reset_pbuffer(table);	344✔
136	break;	344✔
137
138	default:	3,942✔
139	rba_buffer_mul_var(b, t);	3,942✔
140	break;	3,942✔
141	}
142	}	4,515✔
143
144
145	/*
146	* Add t * a to b
147	* - t must be an arithmetic term
148	* - b->ptbl and table->pprods must be equal
149	*/
150	void rba_buffer_add_const_times_term(rba_buffer_t b, term_table_t table, rational_t *a, term_t t) {	1,921✔
151	rational_t q;
152	pprod_t **v;
153	polynomial_t *p;
154	int32_t i;
155
156	assert(b->ptbl == table->pprods);
157	assert(pos_term(t) && good_term(table, t) && (is_arithmetic_term(table, t) \|\| is_finitefield_term(table, t)));
158
159	i = index_of(t);	1,921✔
160	switch (kind_for_idx(table, i)) {	1,921✔
161	case POWER_PRODUCT:	×
162	rba_buffer_add_mono(b, a, pprod_for_idx(table, i));	×
163	break;	×
164
165	case ARITH_CONSTANT:	239✔
166	case ARITH_FF_CONSTANT:
167	q_init(&q);	239✔
168	q_set(&q, a);	239✔
169	q_mul(&q, rational_for_idx(table, i));	239✔
170	rba_buffer_add_const(b, &q);	239✔
171	q_clear(&q);	239✔
172	break;	239✔
173
174	case ARITH_POLY:	13✔
175	case ARITH_FF_POLY:
176	p = polynomial_for_idx(table, i);	13✔
177	v = pprods_for_poly(table, p);	13✔
178	rba_buffer_add_const_times_monarray(b, p->mono, v, a);	13✔
179	term_table_reset_pbuffer(table);	13✔
180	break;	13✔
181
182	default:	1,669✔
183	rba_buffer_add_varmono(b, a, t);	1,669✔
184	break;	1,669✔
185	}
186	}	1,921✔
187
188
189
190	/*
191	* Multiply b by t^d
192	* - t must be an arithmetic term
193	* - p->ptbl and table->pprods must be equal
194	*/
195	void rba_buffer_mul_term_power(rba_buffer_t b, term_table_t table, term_t t, uint32_t d) {	×
196	rba_buffer_t aux;
197	rational_t q;
198	pprod_t **v;
199	polynomial_t *p;
200	pprod_t *r;
201	int32_t i;
202
203	assert(b->ptbl == table->pprods);
204	assert(pos_term(t) && good_term(table, t) && (is_arithmetic_term(table, t) \|\| is_finitefield_term(table, t)));
205
206	i = index_of(t);	×
207	switch (kind_for_idx(table, i)) {	×
208	case POWER_PRODUCT:	×
209	r = pprod_exp(b->ptbl, pprod_for_idx(table, i), d); // r = t^d	×
210	rba_buffer_mul_pp(b, r);	×
211	break;	×
212
213	case ARITH_CONSTANT:	×
214	case ARITH_FF_CONSTANT:
215	q_init(&q);	×
216	q_set_one(&q);	×
217	q_mulexp(&q, rational_for_idx(table, i), d); // q = t^d	×
218	rba_buffer_mul_const(b, &q);	×
219	q_clear(&q);	×
220	break;	×
221
222	case ARITH_POLY:	×
223	case ARITH_FF_POLY:
224	p = polynomial_for_idx(table, i);	×
225	v = pprods_for_poly(table, p);	×
226	init_rba_buffer(&aux, b->ptbl);	×
227	rba_buffer_mul_monarray_power(b, p->mono, v, d, &aux);	×
228	delete_rba_buffer(&aux);	×
229	term_table_reset_pbuffer(table);	×
230	break;	×
231
232	default:	×
233	r = pprod_varexp(b->ptbl, t, d);	×
234	rba_buffer_mul_pp(b, r);	×
235	break;	×
236	}
237	}	×

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