12367760548

Committed 17 Dec 2024 06:41AM UTC coverage: 65.285% (-0.6%) from 65.92%

Build # 12367760548

Build Type

push

github

Committed by

web-flow

Commit Message

Fixes GitHub coverage issue (#544)

* Update action.yml

* Update action.yml

Run Details

81020 of 124102 relevant lines covered (65.29%)

1509382.01 hits per line

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

95.0

/src/terms/extended_rationals.h

/*
 * 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/>.
 */

/*
 * Extended numbers = pairs of rationals (c, d)
 * representing a number of the form c + d.delta
 * where delta is infinitesimal.
 */

#ifndef __EXTENDED_RATIONALS_H
#define __EXTENDED_RATIONALS_H

#include <stdio.h>
#include <stdint.h>
#include <stdbool.h>

#include "terms/rationals.h"


/*
 * extended rational: pairs of rationals (c, d)
 */
typedef struct {
  rational_t main;   // stores c
  rational_t delta;  // stores d
} xrational_t;






/*********************************************
 *  COMPARISONS/TESTS ON EXTENDED RATIONALS  *
 ********************************************/

/*
 * Comparison: returns a negative number if r1 < r2
 *             returns 0 if r1 = r2
 *             returns a positive number if r1 > r2
 */
extern int xq_cmp(xrational_t *r1, xrational_t *r2);



/*
 * Variants of xq_cmp:
 * - xq_le(r1, r2) is nonzero iff r1 <= r2
 * - xq_lt(r1, r2) is nonzero iff r1 < r2
 * - xq_gt(r1, r2) is nonzero iff r1 > r2
 * - xq_ge(r1, r2) is nonzero iff r1 >= r2
 * - xq_eq(r1, r2) is nonzero iff r1 = r2
 * - xq_neq(r1, r2) is nonzero iff r1 != r2
 */
static inline bool xq_le(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) <= 0;
}

static inline bool xq_lt(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) < 0;
}

static inline bool xq_ge(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) >= 0;
}

static inline bool xq_gt(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) > 0;
}

static inline bool xq_eq(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) == 0;
}

static inline bool xq_neq(xrational_t *r1, xrational_t *r2) {
  return xq_cmp(r1, r2) != 0;
}


/*
 * Compare r with a rational q (i.e., with q + 0.delta)
 * returns a negative number if r < q
 * returns 0 if r = q
 * returns a positive number if r > q
 */
extern int xq_cmp_q(xrational_t *r, rational_t *q);


/*
 * Variants of xq_cmp_q:
 *  xq_le_q(r, q) tests whether r <= q
 *  xq_lt_q(r, q) tests whether r < q
 *  xq_gt_q(r, q) tests whether r > q
 *  xq_ge_q(r, q) tests whether r >= q
 *  xq_eq_q(r, q) tests whether r == q
 *  xq_neg_q(r, q) tests whether r != q
 */
static inline bool xq_le_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) <= 0;
}

static inline bool xq_lt_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) < 0;
}

static inline bool xq_ge_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) >= 0;
}

static inline bool xq_gt_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) > 0;
}

static inline bool xq_eq_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) == 0;
}

static inline bool xq_neq_q(xrational_t *r, rational_t *q) {
  return xq_cmp_q(r, q) != 0;
}

/*
 * Check whether r is 0, +1, or -1
 */
static inline bool xq_is_zero(xrational_t *r) {
  return q_is_zero(&r->main) && q_is_zero(&r->delta);
}

static inline bool xq_is_one(xrational_t *r) {
  return q_is_one(&r->main) && q_is_zero(&r->delta);
}

static inline bool xq_is_minus_one(xrational_t *r) {
  return q_is_minus_one(&r->main) && q_is_zero(&r->delta);
}


/*
 * Check whether r is a rational or an integer
 */
static inline bool xq_is_rational(xrational_t *r) {
  return q_is_zero(&r->delta);
}

static inline bool xq_is_integer(xrational_t *r) {
  return q_is_zero(&r->delta) && q_is_integer(&r->main);
}



/*
 * Get the sign of r
 * - xq_sgn(r) = 0 if r = 0
 * - xq_sgn(r) = -1 if r < 0
 * - xq_sgn(r) = +1 if r > 0
 */
static inline int xq_sgn(xrational_t *r) {
  if (q_is_zero(&r->main)) {
    return q_sgn(&r->delta);
  } else {
    return q_sgn(&r->main);
  }
}




/******************************************
 *  ASSIGNMENT AND ARITHMETIC OPERATIONS  *
 *****************************************/

/*
 * Set r to 0 + 0.delta
 */
static inline void xq_init(xrational_t *r) {
  q_init(&r->main);
  q_init(&r->delta);
}


/*
 * Clear r: free the gmp numbers attached to rx if any
 * then set r to 0 + 0.delta
 */
static inline void xq_clear(xrational_t *r) {
  q_clear(&r->main);
  q_clear(&r->delta);
}




/*
 * Assignment operations:
 * - r must be initialized first to avoid memory leaks
 */

/*
 * Assign r1 to r
 */
static inline void xq_set(xrational_t *r, xrational_t *r1) {
  q_set(&r->main, &r1->main);
  q_set(&r->delta, &r1->delta);
}

/*
 * Assign -r1 to r
 */
static inline void xq_set_neg(xrational_t *r, xrational_t *r1) {
  q_set_neg(&r->main, &r1->main);
  q_set_neg(&r->delta, &r1->delta);
}

/*
 * Assign a + 0.delta to r
 */
static inline void xq_set_q(xrational_t *r, rational_t *a) {
  q_set(&r->main, a);
  q_clear(&r->delta);
}

/*
 * Assign a + delta to r
 */
static inline void xq_set_q_plus_delta(xrational_t *r, rational_t *a) {
  q_set(&r->main, a);
  q_set_one(&r->delta);
}

/*
 * Assign a - delta to r
 */
static inline void xq_set_q_minus_delta(xrational_t *r, rational_t *a) {
  q_set(&r->main, a);
  q_set_minus_one(&r->delta);
}


/*
 * Assign +/-1 + 0.delta to r
 */
static inline void xq_set_one(xrational_t *r) {
  q_set_one(&r->main);
  q_clear(&r->delta);
}

static inline void xq_set_minus_one(xrational_t *r) {
  q_set_minus_one(&r->main);
  q_clear(&r->delta);
}




/*
 * OPERATIONS
 */

/*
 * Add r2 to r1
 */
static inline void xq_add(xrational_t *r1, xrational_t *r2) {
  q_add(&r1->main, &r2->main);
  q_add(&r1->delta, &r2->delta);
}

/*
 * Add a rational q2 to r1
 */
static inline void xq_add_q(xrational_t *r1, rational_t *q2) {
  q_add(&r1->main, q2);
}

/*
 * Subtract r2 from r1
 */
static inline void xq_sub(xrational_t *r1, xrational_t *r2) {
  q_sub(&r1->main, &r2->main);
  q_sub(&r1->delta, &r2->delta);
}

/*
 * Subtract a rational q2 from r1
 */
static inline void xq_sub_q(xrational_t *r1, rational_t *q2) {
  q_sub(&r1->main, q2);
}


/*
 * Negate r
 */
static inline void xq_neg(xrational_t *r) {
  q_neg(&r->main);
  q_neg(&r->delta);
}

/*
 * Multiply r by q
 */
static inline void xq_mul(xrational_t *r, rational_t *q) {
  q_mul(&r->main, q);
  q_mul(&r->delta, q);
}


/*
 * Divide r by q
 */
static inline void xq_div(xrational_t *r, rational_t *q) {
  q_div(&r->main, q);
  q_div(&r->delta, q);
}



/*
 * Add q * r2 to r1
 */
static inline void xq_addmul(xrational_t *r1, xrational_t *r2, rational_t *q) {
  q_addmul(&r1->main, &r2->main, q);
  q_addmul(&r1->delta, &r2->delta, q);
}

/*
 * Subtract q * r2 from r1
 */
static inline void xq_submul(xrational_t *r1, xrational_t *r2, rational_t *q) {
  q_submul(&r1->main, &r2->main, q);
  q_submul(&r1->delta, &r2->delta, q);
}


/*
 * Add q1 * q2 to r
 */
static inline void xq_addmul_q(xrational_t *r, rational_t *q1, rational_t *q2) {
  q_addmul(&r->main, q1, q2);
}


/*
 * Subtract q1 * q2 from r
 */
static inline void xq_submul_q(xrational_t *r, rational_t *q1, rational_t *q2) {
  q_submul(&r->main, q1, q2);
}


/*
 * Add +/-1 or +/-delta to r
 */
static inline void xq_add_one(xrational_t *r) {
  q_add_one(&r->main);
}

static inline void xq_sub_one(xrational_t *r) {
  q_sub_one(&r->main);
}

static inline void xq_add_delta(xrational_t *r) {
  q_add_one(&r->delta);
}

static inline void xq_sub_delta(xrational_t *r) {
  q_sub_one(&r->delta);
}




/*
 * Round r to floor or ceiling
 */
extern void xq_ceil(xrational_t *r);
extern void xq_floor(xrational_t *r);



/*
 * Print r on stream f
 */
extern void xq_print(FILE *f, xrational_t *r);


#endif /* __EXTENDED_RATIONALS_H */

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	* Extended numbers = pairs of rationals (c, d)
21	* representing a number of the form c + d.delta
22	* where delta is infinitesimal.
23	*/
24
25	#ifndef __EXTENDED_RATIONALS_H
26	#define __EXTENDED_RATIONALS_H
27
28	#include <stdio.h>
29	#include <stdint.h>
30	#include <stdbool.h>
31
32	#include "terms/rationals.h"
33
34
35	/*
36	* extended rational: pairs of rationals (c, d)
37	*/
38	typedef struct {
39	rational_t main; // stores c
40	rational_t delta; // stores d
41	} xrational_t;
42
43
44
45
46
47
48	/*********************************************
49	* COMPARISONS/TESTS ON EXTENDED RATIONALS *
50	********************************************/
51
52	/*
53	* Comparison: returns a negative number if r1 < r2
54	* returns 0 if r1 = r2
55	* returns a positive number if r1 > r2
56	*/
57	extern int xq_cmp(xrational_t r1, xrational_t r2);
58
59
60
61	/*
62	* Variants of xq_cmp:
63	* - xq_le(r1, r2) is nonzero iff r1 <= r2
64	* - xq_lt(r1, r2) is nonzero iff r1 < r2
65	* - xq_gt(r1, r2) is nonzero iff r1 > r2
66	* - xq_ge(r1, r2) is nonzero iff r1 >= r2
67	* - xq_eq(r1, r2) is nonzero iff r1 = r2
68	* - xq_neq(r1, r2) is nonzero iff r1 != r2
69	*/
70	static inline bool xq_le(xrational_t r1, xrational_t r2) {	1,115,096✔
71	return xq_cmp(r1, r2) <= 0;	1,115,096✔
72	}
73
74	static inline bool xq_lt(xrational_t r1, xrational_t r2) {	1,364,230✔
75	return xq_cmp(r1, r2) < 0;	1,364,230✔
76	}
77
78	static inline bool xq_ge(xrational_t r1, xrational_t r2) {	2,277,796✔
79	return xq_cmp(r1, r2) >= 0;	2,277,796✔
80	}
81
82	static inline bool xq_gt(xrational_t r1, xrational_t r2) {	1,585,848✔
83	return xq_cmp(r1, r2) > 0;	1,585,848✔
84	}
85
86	static inline bool xq_eq(xrational_t r1, xrational_t r2) {	1,279,509✔
87	return xq_cmp(r1, r2) == 0;	1,279,509✔
88	}
89
90	static inline bool xq_neq(xrational_t r1, xrational_t r2) {	×
91	return xq_cmp(r1, r2) != 0;	×
92	}
93
94
95	/*
96	* Compare r with a rational q (i.e., with q + 0.delta)
97	* returns a negative number if r < q
98	* returns 0 if r = q
99	* returns a positive number if r > q
100	*/
101	extern int xq_cmp_q(xrational_t r, rational_t q);
102
103
104	/*
105	* Variants of xq_cmp_q:
106	* xq_le_q(r, q) tests whether r <= q
107	* xq_lt_q(r, q) tests whether r < q
108	* xq_gt_q(r, q) tests whether r > q
109	* xq_ge_q(r, q) tests whether r >= q
110	* xq_eq_q(r, q) tests whether r == q
111	* xq_neg_q(r, q) tests whether r != q
112	*/
113	static inline bool xq_le_q(xrational_t r, rational_t q) {	193,273✔
114	return xq_cmp_q(r, q) <= 0;	193,273✔
115	}
116
117	static inline bool xq_lt_q(xrational_t r, rational_t q) {	3,810,503✔
118	return xq_cmp_q(r, q) < 0;	3,810,503✔
119	}
120
121	static inline bool xq_ge_q(xrational_t r, rational_t q) {	3,884,805✔
122	return xq_cmp_q(r, q) >= 0;	3,884,805✔
123	}
124
125	static inline bool xq_gt_q(xrational_t r, rational_t q) {	158,175✔
126	return xq_cmp_q(r, q) > 0;	158,175✔
127	}
128
129	static inline bool xq_eq_q(xrational_t r, rational_t q) {	1,333✔
130	return xq_cmp_q(r, q) == 0;	1,333✔
131	}
132
133	static inline bool xq_neq_q(xrational_t r, rational_t q) {
134	return xq_cmp_q(r, q) != 0;
135	}
136
137	/*
138	* Check whether r is 0, +1, or -1
139	*/
140	static inline bool xq_is_zero(xrational_t *r) {
141	return q_is_zero(&r->main) && q_is_zero(&r->delta);
142	}
143
144	static inline bool xq_is_one(xrational_t *r) {
145	return q_is_one(&r->main) && q_is_zero(&r->delta);
146	}
147
148	static inline bool xq_is_minus_one(xrational_t *r) {
149	return q_is_minus_one(&r->main) && q_is_zero(&r->delta);
150	}
151
152
153	/*
154	* Check whether r is a rational or an integer
155	*/
156	static inline bool xq_is_rational(xrational_t *r) {	2,027✔
157	return q_is_zero(&r->delta);	2,027✔
158	}
159
160	static inline bool xq_is_integer(xrational_t *r) {	608,616✔
161	return q_is_zero(&r->delta) && q_is_integer(&r->main);	608,616✔
162	}
163
164
165
166	/*
167	* Get the sign of r
168	* - xq_sgn(r) = 0 if r = 0
169	* - xq_sgn(r) = -1 if r < 0
170	* - xq_sgn(r) = +1 if r > 0
171	*/
172	static inline int xq_sgn(xrational_t *r) {
173	if (q_is_zero(&r->main)) {
174	return q_sgn(&r->delta);
175	} else {
176	return q_sgn(&r->main);
177	}
178	}
179
180
181
182
183	/******************************************
184	* ASSIGNMENT AND ARITHMETIC OPERATIONS *
185	*****************************************/
186
187	/*
188	* Set r to 0 + 0.delta
189	*/
190	static inline void xq_init(xrational_t *r) {	1,860,841✔
191	q_init(&r->main);	1,860,841✔
192	q_init(&r->delta);	1,860,841✔
193	}	1,860,841✔
194
195
196	/*
197	* Clear r: free the gmp numbers attached to rx if any
198	* then set r to 0 + 0.delta
199	*/
200	static inline void xq_clear(xrational_t *r) {	53,420,547✔
201	q_clear(&r->main);	53,420,547✔
202	q_clear(&r->delta);	53,420,547✔
203	}	53,420,547✔
204
205
206
207
208	/*
209	* Assignment operations:
210	* - r must be initialized first to avoid memory leaks
211	*/
212
213	/*
214	* Assign r1 to r
215	*/
216	static inline void xq_set(xrational_t r, xrational_t r1) {	21,644,332✔
217	q_set(&r->main, &r1->main);	21,644,332✔
218	q_set(&r->delta, &r1->delta);	21,644,332✔
219	}	21,644,332✔
220
221	/*
222	* Assign -r1 to r
223	*/
224	static inline void xq_set_neg(xrational_t r, xrational_t r1) {
225	q_set_neg(&r->main, &r1->main);
226	q_set_neg(&r->delta, &r1->delta);
227	}
228
229	/*
230	* Assign a + 0.delta to r
231	*/
232	static inline void xq_set_q(xrational_t r, rational_t a) {	2,308,359✔
233	q_set(&r->main, a);	2,308,359✔
234	q_clear(&r->delta);	2,308,359✔
235	}	2,308,359✔
236
237	/*
238	* Assign a + delta to r
239	*/
240	static inline void xq_set_q_plus_delta(xrational_t r, rational_t a) {	136✔
241	q_set(&r->main, a);	136✔
242	q_set_one(&r->delta);	136✔
243	}	136✔
244
245	/*
246	* Assign a - delta to r
247	*/
248	static inline void xq_set_q_minus_delta(xrational_t r, rational_t a) {	153✔
249	q_set(&r->main, a);	153✔
250	q_set_minus_one(&r->delta);	153✔
251	}	153✔
252
253
254	/*
255	* Assign +/-1 + 0.delta to r
256	*/
257	static inline void xq_set_one(xrational_t *r) {	9,770✔
258	q_set_one(&r->main);	9,770✔
259	q_clear(&r->delta);	9,770✔
260	}	9,770✔
261
262	static inline void xq_set_minus_one(xrational_t *r) {
263	q_set_minus_one(&r->main);
264	q_clear(&r->delta);
265	}
266
267
268
269
270	/*
271	* OPERATIONS
272	*/
273
274	/*
275	* Add r2 to r1
276	*/
277	static inline void xq_add(xrational_t r1, xrational_t r2) {	492,686✔
278	q_add(&r1->main, &r2->main);	492,686✔
279	q_add(&r1->delta, &r2->delta);	492,686✔
280	}	492,686✔
281
282	/*
283	* Add a rational q2 to r1
284	*/
285	static inline void xq_add_q(xrational_t r1, rational_t q2) {	462,317✔
286	q_add(&r1->main, q2);	462,317✔
287	}	462,317✔
288
289	/*
290	* Subtract r2 from r1
291	*/
292	static inline void xq_sub(xrational_t r1, xrational_t r2) {	407,459✔
293	q_sub(&r1->main, &r2->main);	407,459✔
294	q_sub(&r1->delta, &r2->delta);	407,459✔
295	}	407,459✔
296
297	/*
298	* Subtract a rational q2 from r1
299	*/
300	static inline void xq_sub_q(xrational_t r1, rational_t q2) {
301	q_sub(&r1->main, q2);
302	}
303
304
305	/*
306	* Negate r
307	*/
308	static inline void xq_neg(xrational_t *r) {	723,264✔
309	q_neg(&r->main);	723,264✔
310	q_neg(&r->delta);	723,264✔
311	}	723,264✔
312
313	/*
314	* Multiply r by q
315	*/
316	static inline void xq_mul(xrational_t r, rational_t q) {	54,861✔
317	q_mul(&r->main, q);	54,861✔
318	q_mul(&r->delta, q);	54,861✔
319	}	54,861✔
320
321
322	/*
323	* Divide r by q
324	*/
325	static inline void xq_div(xrational_t r, rational_t q) {	2,923,795✔
326	q_div(&r->main, q);	2,923,795✔
327	q_div(&r->delta, q);	2,923,795✔
328	}	2,923,795✔
329
330
331
332	/*
333	* Add q * r2 to r1
334	*/
335	static inline void xq_addmul(xrational_t r1, xrational_t r2, rational_t *q) {	3,160,195✔
336	q_addmul(&r1->main, &r2->main, q);	3,160,195✔
337	q_addmul(&r1->delta, &r2->delta, q);	3,160,195✔
338	}	3,160,195✔
339
340	/*
341	* Subtract q * r2 from r1
342	*/
343	static inline void xq_submul(xrational_t r1, xrational_t r2, rational_t *q) {	17,457,567✔
344	q_submul(&r1->main, &r2->main, q);	17,457,567✔
345	q_submul(&r1->delta, &r2->delta, q);	17,457,567✔
346	}	17,457,567✔
347
348
349	/*
350	* Add q1 * q2 to r
351	*/
352	static inline void xq_addmul_q(xrational_t r, rational_t q1, rational_t *q2) {	793✔
353	q_addmul(&r->main, q1, q2);	793✔
354	}	793✔
355
356
357	/*
358	* Subtract q1 * q2 from r
359	*/
360	static inline void xq_submul_q(xrational_t r, rational_t q1, rational_t *q2) {
361	q_submul(&r->main, q1, q2);
362	}
363
364
365	/*
366	* Add +/-1 or +/-delta to r
367	*/
368	static inline void xq_add_one(xrational_t *r) {	×
369	q_add_one(&r->main);	×
370	}	×
371
372	static inline void xq_sub_one(xrational_t *r) {	376,383✔
373	q_sub_one(&r->main);	376,383✔
374	}	376,383✔
375
376	static inline void xq_add_delta(xrational_t *r) {	192,274✔
377	q_add_one(&r->delta);	192,274✔
378	}	192,274✔
379
380	static inline void xq_sub_delta(xrational_t *r) {	177,167✔
381	q_sub_one(&r->delta);	177,167✔
382	}	177,167✔
383
384
385
386
387	/*
388	* Round r to floor or ceiling
389	*/
390	extern void xq_ceil(xrational_t *r);
391	extern void xq_floor(xrational_t *r);
392
393
394
395	/*
396	* Print r on stream f
397	*/
398	extern void xq_print(FILE f, xrational_t r);
399
400
401	#endif /* __EXTENDED_RATIONALS_H */

SRI-CSL / yices2 / 12367760548

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