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

97.22

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

/*
 * NEORATIONAL NUMBERS
 */

#ifndef __RATIONALS_H
#define __RATIONALS_H

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

#include "terms/mpq_aux.h"
#include "utils/memalloc.h"


/*
 * INTERNAL REPRESENTATION
 */

/*
 * A neorational is a union of size 64 bits.
 *
 * if the least bit is 1 it represents a
 * pointer to a gmp number.
 *
 * if the least bit is zero it is a struct consisting of a 32 bit
 * signed numerator, and a 31 bit unsigned denominator.
 */
typedef struct {
#ifdef WORDS_BIGENDIAN
  int32_t  num;
  uint32_t den;
#else
  uint32_t den;
  int32_t  num;
#endif
} rat32_t;

typedef struct {
  intptr_t gmp;
} ratgmp_t;


typedef union rational { rat32_t s; ratgmp_t p; } rational_t;   //s for struct; p for pointer

#define IS_RAT32  0x0
#define IS_RATGMP 0x1
/* the test for unicity in the denominator occurs frequently. the denominator is one if it is 2 :-) */
#define ONE_DEN   0x2


/*
 * Initialization: allocate and initialize
 * global variables.
 */
extern void init_rationals(void);


/*
 * Cleanup: free memory
 */
extern void cleanup_rationals(void);


/*
 * Set r to 0/1, Must be called before any operation on r.
 */
static inline void q_init(rational_t *r) {
  r->s.num = 0;
  r->s.den = ONE_DEN;
}


/*
 * Tests and conversions to/from gmp and rat32
 *
 * NOTE: the type mpq_ptr is defined in gmp.h. It's a pointer
 * to the internal structure representing a gmp number.
 */
static inline bool is_rat32(const rational_t *r) {
  return (r->p.gmp & IS_RATGMP) != IS_RATGMP;
}

static inline bool is_ratgmp(const rational_t *r) {
  return (r->p.gmp & IS_RATGMP) == IS_RATGMP;
}

static inline mpq_ptr get_gmp(const rational_t *r) {
  assert(is_ratgmp(r));  
  return (mpq_ptr) (r->p.gmp ^ IS_RATGMP);
}

static inline mpz_ptr get_gmp_num(const rational_t *r) {
  assert(is_ratgmp(r));
  return mpq_numref(get_gmp(r));
}

static inline mpz_ptr get_gmp_den(const rational_t *r) {
  assert(is_ratgmp(r));
  return mpq_denref(get_gmp(r));
}

static inline int32_t get_num(const rational_t *r) {
  assert(is_rat32(r));  
  return r->s.num;
}

static inline uint32_t get_den(const rational_t *r) {
  assert(is_rat32(r));
  return r->s.den >> 1;
}

static inline void set_ratgmp(rational_t *r, mpq_ptr gmp){
  r->p.gmp = ((intptr_t) gmp) | IS_RATGMP;
}

/*
 * Free mpq number attached to r if any, then set r to 0/1.
 * Must be called before r is deleted to prevent memory leaks.
 */
extern void q_clear(rational_t *r);

/*
 * If r is represented as a gmp rational, convert it
 * to a pair of integers if possible.
 * If it's possible the gmp number is freed.
 */
extern void q_normalize(rational_t *r);


/*
 * ASSIGNMENT
 */

/*
 * Assign +1 or -1 to r
 */
static inline void q_set_one(rational_t *r) {
  q_clear(r);
  r->s.num = 1;
}

static inline void q_set_minus_one(rational_t *r) {
  q_clear(r);
  r->s.num = -1;
}

/*
 * Assignment operations: all set the value of the first argument (r or r1).
 * - in q_set_int32 and q_set_int64, num/den is normalized first
 *   (common factors are removed) and den must be non-zero
 * - in q_set_mpq, q must be canonicalized first
 *   (a copy of q is made)
 * - q_set copies r2 into r1 (if r2 is a gmp number,
 *   then a new gmp number is allocated with the same value
 *   and assigned to r1)
 * - q_set_neg assigns the opposite of r2 to r1
 * - q_set_abs assigns the absolute value of r2 to r1
 */
extern void q_set_int32(rational_t *r, int32_t num, uint32_t den);
extern void q_set_int64(rational_t *r, int64_t num, uint64_t den);
extern void q_set32(rational_t *r, int32_t num);
extern void q_set64(rational_t *r, int64_t num);

extern void q_set_mpq(rational_t *r, const mpq_t q);
extern void q_set_mpz(rational_t *r, const mpz_t z);
extern void q_set(rational_t *r1, const rational_t *r2);
extern void q_set_neg(rational_t *r1, const rational_t *r2);
extern void q_set_abs(rational_t *r1, const rational_t *r2);

/*
 * Copy r2 into r1: share the gmp index if r2
 * is a gmp number. Then clear r2.
 * This can be used without calling q_init(r1).
 */
static inline void q_copy_and_clear(rational_t *r1, rational_t *r2) {
  *r1 = *r2;
  r2->s.num = 0;
  r2->s.den = ONE_DEN;
}

/*
 * Swap values of r1 and r2
 */
static inline void q_swap(rational_t *r1, rational_t *r2) {
  rational_t aux;

  aux = *r1;
  *r1 = *r2;
  *r2 = aux;
}

/*
 * Copy the numerator or denominator of r2 into r1
 */
extern void q_get_num(rational_t *r1, const rational_t *r2);
extern void q_get_den(rational_t *r1, const rational_t *r2);

/*
 * String parsing:
 * - set_from_string uses the GMP format with base 10:
 *       <optional_sign> <numerator>/<denominator>
 *       <optional_sign> <number>
 *
 * - set_from_string_base uses the GMP format with base b
 *
 * - set_from_float_string uses a floating point format:
 *   <optional sign> <integer part> . <fractional part>
 *   <optional sign> <integer part> <exp> <optional sign> <integer>
 *   <optional sign> <integer part> . <fractional part> <exp> <optional sign> <integer>
 *
 * where <optional sign> is + or - or nothing
 *       <exp> is either 'e' or 'E'
 *
 * The functions return -1 if the format is wrong and leave r unchanged.
 * The functions q_set_from_string and q_set_from_string_base return -2
 * if the denominator is 0.
 * Otherwise, the functions return 0 and the parsed value is stored in r.
 */
extern int q_set_from_string(rational_t *r, const char *s);
extern int q_set_from_string_base(rational_t *r, const char *s, int32_t b);
extern int q_set_from_float_string(rational_t *r, const char *s);

/*
 * ARITHMETIC: ALL OPERATIONS MODIFY THE FIRST ARGUMENT
 */

/*
 * Arithmetic operations:
 * - all operate on the first argument:
 *    q_add: add r2 to r1
 *    q_sub: subtract r2 from r1
 *    q_mul: set r1 to r1 * r2
 *    q_div: set r1 to r1/r2 (r2 must be nonzero)
 *    q_neg: negate r
 *    q_inv: invert r (r must be nonzero)
 *    q_addmul: add r2 * r3 to r1
 *    q_submul: subtract r2 * r3 from r1
 *    q_addone: add 1 to r1
 *    q_subone: subtract 1 from r1
 * - lcm/gcd operations (r1 and r2 must be integers)
 *    q_lcm: store lcm(r1, r2) into r1
 *    q_gcd: store gcd(r1, r2) into r1 (r1 and r2 must not be zero)
 * - floor and ceiling are also in-place operations:
 *    q_floor: store largest integer <= r into r
 *    q_ceil: store smaller integer >= r into r
 */
extern void q_add(rational_t *r1, const rational_t *r2);
extern void q_sub(rational_t *r1, const rational_t *r2);
extern void q_mul(rational_t *r1, const rational_t *r2);
extern void q_div(rational_t *r1, const rational_t *r2);
extern void q_neg(rational_t *r);
extern void q_inv(rational_t *r);

extern void q_addmul(rational_t *r1, const rational_t *r2, const rational_t *r3);
extern void q_submul(rational_t *r1, const rational_t *r2, const rational_t *r3);
extern void q_add_one(rational_t *r1);
extern void q_sub_one(rational_t *r1);

extern void q_lcm(rational_t *r1, const rational_t *r2);
extern void q_gcd(rational_t *r1, const rational_t *r2);

extern void q_floor(rational_t *r);
extern void q_ceil(rational_t *r);

extern void q_inv_mod(rational_t *r, const rational_t *mod);


/*
 * Exponentiation:
 * - q_mulexp(r1, r2, n): multiply r1 by r2^n
 */
extern void q_mulexp(rational_t *r1, const rational_t *r2, uint32_t n);


/*
 * Integer division and remainder
 * - r1 and r2 must both be integer
 * - r2 must be positive.
 * - Consider normalizing r2 before
 *
 * q_integer_div(r1, r2) stores the quotient of r1 divided by r2 into r1
 * q_integer_rem(r1, r2) stores the remainder into r1
 *
 * This implements the usual definition of division (unlike C).
 * If r = remainder and q = quotient then we have
 *    0 <= r < r2 and  r1 = q * r2 + r
 */
extern void q_integer_div(rational_t *r1, const rational_t *r2);
extern void q_integer_rem(rational_t *r1, const rational_t *r2);


/*
 * Generalized LCM: compute the smallest non-negative rational q
 * such that q/r1 is an integer and q/r2 is an integer.
 * - r1 and r2 can be arbitrary rationals.
 * - the result is stored in r1
 */
extern void q_generalized_lcm(rational_t *r1, const rational_t *r2);

/*
 * Generalized GCD: compute the largest positive rational q
 * such that r1/q and r2/q are both integer.
 * - the result is stored in r1
 */
extern void q_generalized_gcd(rational_t *r1, const rational_t *r2);



/*
 * SMT2 Versions of division and mod
 *
 * Intended semantics for div and mod:
 * - if y > 0 then div(x, y) is floor(x/y)
 * - if y < 0 then div(x, y) is ceil(x/y)
 * - 0 <= mod(x, y) < y
 * - x = y * div(x, y) + mod(x, y)
 * These operations are defined for any x and non-zero y.
 * The terms x and y are not required to be integers.
 *
 * - q_smt2_div(q, x, y) stores (div x y) in q
 * - q_smt2_mod(q, x, y) stores (mod x y) in q
 *
 * For both functions, y must not be zero.
 */
extern void q_smt2_div(rational_t *q, const rational_t *x, const rational_t *y);
extern void q_smt2_mod(rational_t *q, const rational_t *x, const rational_t *y);


/*
 * TESTS: DO NOT MODIFY THE ARGUMENT(S)
 */

/*
 * Sign of r: q_sgn(r) = 0 if r = 0
 *            q_sgn(r) = +1 if r > 0
 *            q_sgn(r) = -1 if r < 0
 */
static inline int q_sgn(const rational_t *r) {
  if (is_ratgmp(r)) {
    return mpq_sgn(get_gmp(r));
  } else {
    return (r->s.num < 0 ? -1 : (r->s.num > 0));
  }
}


/*
 * Compare r1 and r2:
 * - returns a negative number if r1 < r2
 * - returns 0 if r1 = r2
 * - returns a positive number if r1 > r2
 */
extern int q_cmp(const rational_t *r1, const rational_t *r2);


/*
 * Compare r1 and num/den
 * - den must be nonzero
 * - returns a negative number if r1 < num/den
 * - returns 0 if r1 = num/den
 * - returns a positive number if r1 > num/den
 */
extern int q_cmp_int32(const rational_t *r1, int32_t num, uint32_t den);
extern int q_cmp_int64(const rational_t *r1, int64_t num, uint64_t den);


/*
 * Variants of q_cmp:
 * - q_le(r1, r2) is nonzero iff r1 <= r2
 * - q_lt(r1, r2) is nonzero iff r1 < r2
 * - q_gt(r1, r2) is nonzero iff r1 > r2
 * - q_ge(r1, r2) is nonzero iff r1 >= r2
 * - q_eq(r1, r2) is nonzero iff r1 = r2
 * - q_neq(r1, r2) is nonzero iff r1 != r2
 */
static inline bool q_le(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) <= 0;
}

static inline bool q_lt(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) < 0;
}

static inline bool q_ge(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) >= 0;
}

static inline bool q_gt(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) > 0;
}

static inline bool q_eq(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) == 0;
}

static inline bool q_neq(const rational_t *r1, const rational_t *r2) {
  return q_cmp(r1, r2) != 0;
}


/*
 * Check whether r1 and r2 are opposite (i.e., r1 + r2 = 0)
 */
extern bool q_opposite(const rational_t *r1, const rational_t *r2);


/*
 * Tests on rational r
 */
static inline bool q_is_zero(const rational_t *r) {
  return is_ratgmp(r) ? mpq_is_zero(get_gmp(r)) : r->s.num == 0;
}

static inline bool q_is_nonzero(const rational_t *r) {
  return is_ratgmp(r) ? mpq_is_nonzero(get_gmp(r)) : r->s.num != 0;
}

static inline bool q_is_one(const rational_t *r) {
  return (r->s.den == ONE_DEN && r->s.num == 1) ||
    (is_ratgmp(r) && mpq_is_one(get_gmp(r)));
}

static inline bool q_is_minus_one(const rational_t *r) {
  return (r->s.den == ONE_DEN && r->s.num == -1) ||
    (is_ratgmp(r) && mpq_is_minus_one(get_gmp(r)));
}

static inline bool q_is_pos(const rational_t *r) {
  return (is_rat32(r) ?  r->s.num > 0 : mpq_is_pos(get_gmp(r)));
}

static inline bool q_is_nonneg(const rational_t *r) {
  return (is_rat32(r) ?  r->s.num >= 0 : mpq_is_nonneg(get_gmp(r)));
}

static inline bool q_is_neg(const rational_t *r) {
  return (is_rat32(r) ?  r->s.num < 0 : mpq_is_neg(get_gmp(r)));
}

static inline bool q_is_nonpos(const rational_t *r) {
  return (is_rat32(r) ?  r->s.num <= 0 : mpq_is_nonpos(get_gmp(r)));
}

static inline bool q_is_integer(const rational_t *r) {
  return (is_rat32(r) && r->s.den == ONE_DEN) || (is_ratgmp(r) && mpq_is_integer(get_gmp(r)));
}



/*
 * DIVISIBILITY TESTS
 */

/*
 * Check whether r1 divides r2: both must be integers
 * - r1 must be non-zero
 * - side effect: r1 is normalized
 */
extern bool q_integer_divides(rational_t *r1, const rational_t *r2);


/*
 * General divisibility check: return true iff r2/r1 is an integer
 * - r1 must be non-zero
 */
extern bool q_divides(const rational_t *r1, const rational_t *r2);


/*
 * SMT2 version:
 * - if t1 is non-zero, return true iff (r2/r1) is an integer
 * - if t1 is zero, return true iff r2 is zero
 */
extern bool q_smt2_divides(const rational_t *r1, const rational_t *r2);


/*
 * Tests on integer rational r mod m
 */
static inline bool q_is_zero_mod(const rational_t *r, const rational_t *m) {
  assert(q_is_integer(r) && q_is_integer(m) && q_is_pos(m));
  return q_integer_divides((rational_t *)m, r);
}

static inline bool q_is_nonzero_mod(const rational_t *r, const rational_t *m) {
  return !q_is_zero_mod(r, m);
}


/*
 * CONVERSIONS TO INTEGERS
 */

/*
 * Check whether r is a small integer (use with care: this
 * ignores the case where r is a small integer that happens
 * to be represented as a gmp rational).
 * Call q_normalize(r) first if there's a doubt.
 */
static inline bool q_is_smallint(rational_t *r) {  
  return r->s.den == ONE_DEN;
}

/*
 * Convert r to an integer, provided q_is_smallint(r) is true
 */
static inline int32_t q_get_smallint(rational_t *r) {
  return get_num(r);
}


/*
 * Conversions: all functions attempt to convert r into an integer or
 * a pair of integers (num/den). If the conversion is not possible
 * the functions return false. Otherwise, the result is true and the
 * value is returned in v or num/den.
 */
extern bool q_get32(rational_t *r, int32_t *v);
extern bool q_get64(rational_t *r, int64_t *v);
extern bool q_get_int32(rational_t *r, int32_t *num, uint32_t *den);
extern bool q_get_int64(rational_t *r, int64_t *num, uint64_t *den);


/*
 * Similar to the conversion functions above but just check
 * whether the conversions are possible.
 */
extern bool q_is_int32(rational_t *r);   // r is a/1 where a is int32
extern bool q_is_int64(rational_t *r);   // r is a/1 where a is int64
extern bool q_fits_int32(rational_t *r); // r is a/b where a is int32, b is uint32
extern bool q_fits_int64(rational_t *r); // r is a/b where a is int64, b is uint64



/*
 * Size estimate
 * - this returns approximately the number of bits to represent r's numerator
 * - this may not be exact (typically rounded up to a multiple of 32)
 * - also if r is really really big, this function may return
 *   UINT32_MAX (not very likely!)
 */
extern uint32_t q_size(rational_t *r);


/*
 * CONVERSION TO GMP OBJECTS
 */

/*
 * Store r into the GMP integer z.
 * - return false if r is not a integer, true otherwise
 */
extern bool q_get_mpz(const rational_t *r, mpz_t z);


/*
 * Store r into q
 */
extern void q_get_mpq(const rational_t *r, mpq_t q);


/*
 * Convert to a floating point number
 */
extern double q_get_double(rational_t *r);



/*
 * PRINT
 */

/*
 * Print r on stream f.
 * q_print_abs prints the absolute value
 */
extern void q_print(FILE *f, const rational_t *r);
extern void q_print_abs(FILE *f, const rational_t *r);


/*
 * HASH FUNCTION
 */

/*
 * Hash functions: return a hash of numerator or denominator.
 * - hash_numerator(r) = numerator MOD bigprime
 * - hash_denominator(r) = denominator MOD bigprime
 * where bigprime is the largest prime number smaller than 2^32.
 */
extern uint32_t q_hash_numerator(const rational_t *r);
extern uint32_t q_hash_denominator(const rational_t *r);
extern void q_hash_decompose(const rational_t *r, uint32_t *h_num, uint32_t *h_den);




/*
 * RATIONAL ARRAYS
 */

#define MAX_RATIONAL_ARRAY_SIZE (UINT32_MAX/sizeof(rational_t))

/*
 * Create and initialize an array of n rationals.
 */
extern rational_t *new_rational_array(uint32_t n);

/*
 * Delete an array created by the previous function
 * - n must be the size of a
 */
extern void free_rational_array(rational_t *a, uint32_t n);





#endif /* __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	* NEORATIONAL NUMBERS
21	*/
22
23	#ifndef __RATIONALS_H
24	#define __RATIONALS_H
25
26	#include <assert.h>
27	#include <stdio.h>
28	#include <stdint.h>
29	#include <stdbool.h>
30	#include <gmp.h>
31
32	#include "terms/mpq_aux.h"
33	#include "utils/memalloc.h"
34
35
36	/*
37	* INTERNAL REPRESENTATION
38	*/
39
40	/*
41	* A neorational is a union of size 64 bits.
42	*
43	* if the least bit is 1 it represents a
44	* pointer to a gmp number.
45	*
46	* if the least bit is zero it is a struct consisting of a 32 bit
47	* signed numerator, and a 31 bit unsigned denominator.
48	*/
49	typedef struct {
50	#ifdef WORDS_BIGENDIAN
51	int32_t num;
52	uint32_t den;
53	#else
54	uint32_t den;
55	int32_t num;
56	#endif
57	} rat32_t;
58
59	typedef struct {
60	intptr_t gmp;
61	} ratgmp_t;
62
63
64	typedef union rational { rat32_t s; ratgmp_t p; } rational_t; //s for struct; p for pointer
65
66	#define IS_RAT32 0x0
67	#define IS_RATGMP 0x1
68	/* the test for unicity in the denominator occurs frequently. the denominator is one if it is 2 :-) */
69	#define ONE_DEN 0x2
70
71
72	/*
73	* Initialization: allocate and initialize
74	* global variables.
75	*/
76	extern void init_rationals(void);
77
78
79	/*
80	* Cleanup: free memory
81	*/
82	extern void cleanup_rationals(void);
83
84
85	/*
86	* Set r to 0/1, Must be called before any operation on r.
87	*/
88	static inline void q_init(rational_t *r) {	120,360,891✔
89	r->s.num = 0;	120,360,891✔
90	r->s.den = ONE_DEN;	120,360,891✔
91	}	120,360,891✔
92
93
94	/*
95	* Tests and conversions to/from gmp and rat32
96	*
97	* NOTE: the type mpq_ptr is defined in gmp.h. It's a pointer
98	* to the internal structure representing a gmp number.
99	*/
100	static inline bool is_rat32(const rational_t *r) {	38,263,931✔
101	return (r->p.gmp & IS_RATGMP) != IS_RATGMP;	38,263,931✔
102	}
103
104	static inline bool is_ratgmp(const rational_t *r) {	1,592,526,293✔
105	return (r->p.gmp & IS_RATGMP) == IS_RATGMP;	1,592,526,293✔
106	}
107
108	static inline mpq_ptr get_gmp(const rational_t *r) {	54,689,248✔
109	assert(is_ratgmp(r));
110	return (mpq_ptr) (r->p.gmp ^ IS_RATGMP);	54,689,248✔
111	}
112
113	static inline mpz_ptr get_gmp_num(const rational_t *r) {	486✔
114	assert(is_ratgmp(r));
115	return mpq_numref(get_gmp(r));	486✔
116	}
117
118	static inline mpz_ptr get_gmp_den(const rational_t *r) {
119	assert(is_ratgmp(r));
120	return mpq_denref(get_gmp(r));
121	}
122
123	static inline int32_t get_num(const rational_t *r) {	478,768,797✔
124	assert(is_rat32(r));
125	return r->s.num;	478,768,797✔
126	}
127
128	static inline uint32_t get_den(const rational_t *r) {	493,410,248✔
129	assert(is_rat32(r));
130	return r->s.den >> 1;	493,410,248✔
131	}
132
133	static inline void set_ratgmp(rational_t *r, mpq_ptr gmp){	6,461,797✔
134	r->p.gmp = ((intptr_t) gmp) \| IS_RATGMP;	6,461,797✔
135	}	6,461,797✔
136
137	/*
138	* Free mpq number attached to r if any, then set r to 0/1.
139	* Must be called before r is deleted to prevent memory leaks.
140	*/
141	extern void q_clear(rational_t *r);
142
143	/*
144	* If r is represented as a gmp rational, convert it
145	* to a pair of integers if possible.
146	* If it's possible the gmp number is freed.
147	*/
148	extern void q_normalize(rational_t *r);
149
150
151	/*
152	* ASSIGNMENT
153	*/
154
155	/*
156	* Assign +1 or -1 to r
157	*/
158	static inline void q_set_one(rational_t *r) {	602,402✔
159	q_clear(r);	602,402✔
160	r->s.num = 1;	602,402✔
161	}	602,402✔
162
163	static inline void q_set_minus_one(rational_t *r) {	191,354✔
164	q_clear(r);	191,354✔
165	r->s.num = -1;	191,354✔
166	}	191,354✔
167
168	/*
169	* Assignment operations: all set the value of the first argument (r or r1).
170	* - in q_set_int32 and q_set_int64, num/den is normalized first
171	* (common factors are removed) and den must be non-zero
172	* - in q_set_mpq, q must be canonicalized first
173	* (a copy of q is made)
174	* - q_set copies r2 into r1 (if r2 is a gmp number,
175	* then a new gmp number is allocated with the same value
176	* and assigned to r1)
177	* - q_set_neg assigns the opposite of r2 to r1
178	* - q_set_abs assigns the absolute value of r2 to r1
179	*/
180	extern void q_set_int32(rational_t *r, int32_t num, uint32_t den);
181	extern void q_set_int64(rational_t *r, int64_t num, uint64_t den);
182	extern void q_set32(rational_t *r, int32_t num);
183	extern void q_set64(rational_t *r, int64_t num);
184
185	extern void q_set_mpq(rational_t *r, const mpq_t q);
186	extern void q_set_mpz(rational_t *r, const mpz_t z);
187	extern void q_set(rational_t r1, const rational_t r2);
188	extern void q_set_neg(rational_t r1, const rational_t r2);
189	extern void q_set_abs(rational_t r1, const rational_t r2);
190
191	/*
192	* Copy r2 into r1: share the gmp index if r2
193	* is a gmp number. Then clear r2.
194	* This can be used without calling q_init(r1).
195	*/
196	static inline void q_copy_and_clear(rational_t r1, rational_t r2) {	2,574,087✔
197	r1 = r2;	2,574,087✔
198	r2->s.num = 0;	2,574,087✔
199	r2->s.den = ONE_DEN;	2,574,087✔
200	}	2,574,087✔
201
202	/*
203	* Swap values of r1 and r2
204	*/
205	static inline void q_swap(rational_t r1, rational_t r2) {
206	rational_t aux;
207
208	aux = *r1;
209	r1 = r2;
210	*r2 = aux;
211	}
212
213	/*
214	* Copy the numerator or denominator of r2 into r1
215	*/
216	extern void q_get_num(rational_t r1, const rational_t r2);
217	extern void q_get_den(rational_t r1, const rational_t r2);
218
219	/*
220	* String parsing:
221	* - set_from_string uses the GMP format with base 10:
222	* <optional_sign> <numerator>/<denominator>
223	* <optional_sign> <number>
224	*
225	* - set_from_string_base uses the GMP format with base b
226	*
227	* - set_from_float_string uses a floating point format:
228	* <optional sign> <integer part> . <fractional part>
229	* <optional sign> <integer part> <exp> <optional sign> <integer>
230	* <optional sign> <integer part> . <fractional part> <exp> <optional sign> <integer>
231	*
232	* where <optional sign> is + or - or nothing
233	* <exp> is either 'e' or 'E'
234	*
235	* The functions return -1 if the format is wrong and leave r unchanged.
236	* The functions q_set_from_string and q_set_from_string_base return -2
237	* if the denominator is 0.
238	* Otherwise, the functions return 0 and the parsed value is stored in r.
239	*/
240	extern int q_set_from_string(rational_t r, const char s);
241	extern int q_set_from_string_base(rational_t r, const char s, int32_t b);
242	extern int q_set_from_float_string(rational_t r, const char s);
243
244	/*
245	* ARITHMETIC: ALL OPERATIONS MODIFY THE FIRST ARGUMENT
246	*/
247
248	/*
249	* Arithmetic operations:
250	* - all operate on the first argument:
251	* q_add: add r2 to r1
252	* q_sub: subtract r2 from r1
253	* q_mul: set r1 to r1 * r2
254	* q_div: set r1 to r1/r2 (r2 must be nonzero)
255	* q_neg: negate r
256	* q_inv: invert r (r must be nonzero)
257	* q_addmul: add r2 * r3 to r1
258	* q_submul: subtract r2 * r3 from r1
259	* q_addone: add 1 to r1
260	* q_subone: subtract 1 from r1
261	* - lcm/gcd operations (r1 and r2 must be integers)
262	* q_lcm: store lcm(r1, r2) into r1
263	* q_gcd: store gcd(r1, r2) into r1 (r1 and r2 must not be zero)
264	* - floor and ceiling are also in-place operations:
265	* q_floor: store largest integer <= r into r
266	* q_ceil: store smaller integer >= r into r
267	*/
268	extern void q_add(rational_t r1, const rational_t r2);
269	extern void q_sub(rational_t r1, const rational_t r2);
270	extern void q_mul(rational_t r1, const rational_t r2);
271	extern void q_div(rational_t r1, const rational_t r2);
272	extern void q_neg(rational_t *r);
273	extern void q_inv(rational_t *r);
274
275	extern void q_addmul(rational_t r1, const rational_t r2, const rational_t *r3);
276	extern void q_submul(rational_t r1, const rational_t r2, const rational_t *r3);
277	extern void q_add_one(rational_t *r1);
278	extern void q_sub_one(rational_t *r1);
279
280	extern void q_lcm(rational_t r1, const rational_t r2);
281	extern void q_gcd(rational_t r1, const rational_t r2);
282
283	extern void q_floor(rational_t *r);
284	extern void q_ceil(rational_t *r);
285
286	extern void q_inv_mod(rational_t r, const rational_t mod);
287
288
289	/*
290	* Exponentiation:
291	* - q_mulexp(r1, r2, n): multiply r1 by r2^n
292	*/
293	extern void q_mulexp(rational_t r1, const rational_t r2, uint32_t n);
294
295
296	/*
297	* Integer division and remainder
298	* - r1 and r2 must both be integer
299	* - r2 must be positive.
300	* - Consider normalizing r2 before
301	*
302	* q_integer_div(r1, r2) stores the quotient of r1 divided by r2 into r1
303	* q_integer_rem(r1, r2) stores the remainder into r1
304	*
305	* This implements the usual definition of division (unlike C).
306	* If r = remainder and q = quotient then we have
307	* 0 <= r < r2 and r1 = q * r2 + r
308	*/
309	extern void q_integer_div(rational_t r1, const rational_t r2);
310	extern void q_integer_rem(rational_t r1, const rational_t r2);
311
312
313	/*
314	* Generalized LCM: compute the smallest non-negative rational q
315	* such that q/r1 is an integer and q/r2 is an integer.
316	* - r1 and r2 can be arbitrary rationals.
317	* - the result is stored in r1
318	*/
319	extern void q_generalized_lcm(rational_t r1, const rational_t r2);
320
321	/*
322	* Generalized GCD: compute the largest positive rational q
323	* such that r1/q and r2/q are both integer.
324	* - the result is stored in r1
325	*/
326	extern void q_generalized_gcd(rational_t r1, const rational_t r2);
327
328
329
330	/*
331	* SMT2 Versions of division and mod
332	*
333	* Intended semantics for div and mod:
334	* - if y > 0 then div(x, y) is floor(x/y)
335	* - if y < 0 then div(x, y) is ceil(x/y)
336	* - 0 <= mod(x, y) < y
337	* - x = y * div(x, y) + mod(x, y)
338	* These operations are defined for any x and non-zero y.
339	* The terms x and y are not required to be integers.
340	*
341	* - q_smt2_div(q, x, y) stores (div x y) in q
342	* - q_smt2_mod(q, x, y) stores (mod x y) in q
343	*
344	* For both functions, y must not be zero.
345	*/
346	extern void q_smt2_div(rational_t q, const rational_t x, const rational_t *y);
347	extern void q_smt2_mod(rational_t q, const rational_t x, const rational_t *y);
348
349
350	/*
351	* TESTS: DO NOT MODIFY THE ARGUMENT(S)
352	*/
353
354	/*
355	* Sign of r: q_sgn(r) = 0 if r = 0
356	* q_sgn(r) = +1 if r > 0
357	* q_sgn(r) = -1 if r < 0
358	*/
359	static inline int q_sgn(const rational_t *r) {	48,505,712✔
360	if (is_ratgmp(r)) {	48,505,712✔
361	return mpq_sgn(get_gmp(r));	1,150,228✔
362	} else {
363	return (r->s.num < 0 ? -1 : (r->s.num > 0));	47,355,484✔
364	}
365	}
366
367
368	/*
369	* Compare r1 and r2:
370	* - returns a negative number if r1 < r2
371	* - returns 0 if r1 = r2
372	* - returns a positive number if r1 > r2
373	*/
374	extern int q_cmp(const rational_t r1, const rational_t r2);
375
376
377	/*
378	* Compare r1 and num/den
379	* - den must be nonzero
380	* - returns a negative number if r1 < num/den
381	* - returns 0 if r1 = num/den
382	* - returns a positive number if r1 > num/den
383	*/
384	extern int q_cmp_int32(const rational_t *r1, int32_t num, uint32_t den);
385	extern int q_cmp_int64(const rational_t *r1, int64_t num, uint64_t den);
386
387
388	/*
389	* Variants of q_cmp:
390	* - q_le(r1, r2) is nonzero iff r1 <= r2
391	* - q_lt(r1, r2) is nonzero iff r1 < r2
392	* - q_gt(r1, r2) is nonzero iff r1 > r2
393	* - q_ge(r1, r2) is nonzero iff r1 >= r2
394	* - q_eq(r1, r2) is nonzero iff r1 = r2
395	* - q_neq(r1, r2) is nonzero iff r1 != r2
396	*/
397	static inline bool q_le(const rational_t r1, const rational_t r2) {	2,168✔
398	return q_cmp(r1, r2) <= 0;	2,168✔
399	}
400
401	static inline bool q_lt(const rational_t r1, const rational_t r2) {	3,411,469✔
402	return q_cmp(r1, r2) < 0;	3,411,469✔
403	}
404
405	static inline bool q_ge(const rational_t r1, const rational_t r2) {	51,019✔
406	return q_cmp(r1, r2) >= 0;	51,019✔
407	}
408
409	static inline bool q_gt(const rational_t r1, const rational_t r2) {	121,891✔
410	return q_cmp(r1, r2) > 0;	121,891✔
411	}
412
413	static inline bool q_eq(const rational_t r1, const rational_t r2) {	2,844,039✔
414	return q_cmp(r1, r2) == 0;	2,844,039✔
415	}
416
417	static inline bool q_neq(const rational_t r1, const rational_t r2) {	343,843✔
418	return q_cmp(r1, r2) != 0;	343,843✔
419	}
420
421
422	/*
423	* Check whether r1 and r2 are opposite (i.e., r1 + r2 = 0)
424	*/
425	extern bool q_opposite(const rational_t r1, const rational_t r2);
426
427
428	/*
429	* Tests on rational r
430	*/
431	static inline bool q_is_zero(const rational_t *r) {	314,855,982✔
432	return is_ratgmp(r) ? mpq_is_zero(get_gmp(r)) : r->s.num == 0;	314,855,982✔
433	}
434
435	static inline bool q_is_nonzero(const rational_t *r) {	1,552,204✔
436	return is_ratgmp(r) ? mpq_is_nonzero(get_gmp(r)) : r->s.num != 0;	1,552,204✔
437	}
438
439	static inline bool q_is_one(const rational_t *r) {	9,872,201✔
440	return (r->s.den == ONE_DEN && r->s.num == 1) \|\|	17,137,996✔
441	(is_ratgmp(r) && mpq_is_one(get_gmp(r)));	7,265,795✔
442	}
443
444	static inline bool q_is_minus_one(const rational_t *r) {	6,892,300✔
445	return (r->s.den == ONE_DEN && r->s.num == -1) \|\|	11,231,658✔
446	(is_ratgmp(r) && mpq_is_minus_one(get_gmp(r)));	4,339,358✔
447	}
448
449	static inline bool q_is_pos(const rational_t *r) {	22,539,469✔
450	return (is_rat32(r) ? r->s.num > 0 : mpq_is_pos(get_gmp(r)));	22,539,469✔
451	}
452
453	static inline bool q_is_nonneg(const rational_t *r) {	163,090✔
454	return (is_rat32(r) ? r->s.num >= 0 : mpq_is_nonneg(get_gmp(r)));	163,090✔
455	}
456
457	static inline bool q_is_neg(const rational_t *r) {	2,191,760✔
458	return (is_rat32(r) ? r->s.num < 0 : mpq_is_neg(get_gmp(r)));	2,191,760✔
459	}
460
461	static inline bool q_is_nonpos(const rational_t *r) {	×
462	return (is_rat32(r) ? r->s.num <= 0 : mpq_is_nonpos(get_gmp(r)));	×
463	}
464
465	static inline bool q_is_integer(const rational_t *r) {	4,177,168✔
466	return (is_rat32(r) && r->s.den == ONE_DEN) \|\| (is_ratgmp(r) && mpq_is_integer(get_gmp(r)));	4,177,168✔
467	}
468
469
470
471	/*
472	* DIVISIBILITY TESTS
473	*/
474
475	/*
476	* Check whether r1 divides r2: both must be integers
477	* - r1 must be non-zero
478	* - side effect: r1 is normalized
479	*/
480	extern bool q_integer_divides(rational_t r1, const rational_t r2);
481
482
483	/*
484	* General divisibility check: return true iff r2/r1 is an integer
485	* - r1 must be non-zero
486	*/
487	extern bool q_divides(const rational_t r1, const rational_t r2);
488
489
490	/*
491	* SMT2 version:
492	* - if t1 is non-zero, return true iff (r2/r1) is an integer
493	* - if t1 is zero, return true iff r2 is zero
494	*/
495	extern bool q_smt2_divides(const rational_t r1, const rational_t r2);
496
497
498	/*
499	* Tests on integer rational r mod m
500	*/
501	static inline bool q_is_zero_mod(const rational_t r, const rational_t m) {
502	assert(q_is_integer(r) && q_is_integer(m) && q_is_pos(m));
503	return q_integer_divides((rational_t *)m, r);
504	}
505
506	static inline bool q_is_nonzero_mod(const rational_t r, const rational_t m) {
507	return !q_is_zero_mod(r, m);
508	}
509
510
511	/*
512	* CONVERSIONS TO INTEGERS
513	*/
514
515	/*
516	* Check whether r is a small integer (use with care: this
517	* ignores the case where r is a small integer that happens
518	* to be represented as a gmp rational).
519	* Call q_normalize(r) first if there's a doubt.
520	*/
521	static inline bool q_is_smallint(rational_t *r) {	11,146✔
522	return r->s.den == ONE_DEN;	11,146✔
523	}
524
525	/*
526	* Convert r to an integer, provided q_is_smallint(r) is true
527	*/
528	static inline int32_t q_get_smallint(rational_t *r) {	10,954✔
529	return get_num(r);	10,954✔
530	}
531
532
533	/*
534	* Conversions: all functions attempt to convert r into an integer or
535	* a pair of integers (num/den). If the conversion is not possible
536	* the functions return false. Otherwise, the result is true and the
537	* value is returned in v or num/den.
538	*/
539	extern bool q_get32(rational_t r, int32_t v);
540	extern bool q_get64(rational_t r, int64_t v);
541	extern bool q_get_int32(rational_t r, int32_t num, uint32_t *den);
542	extern bool q_get_int64(rational_t r, int64_t num, uint64_t *den);
543
544
545	/*
546	* Similar to the conversion functions above but just check
547	* whether the conversions are possible.
548	*/
549	extern bool q_is_int32(rational_t *r); // r is a/1 where a is int32
550	extern bool q_is_int64(rational_t *r); // r is a/1 where a is int64
551	extern bool q_fits_int32(rational_t *r); // r is a/b where a is int32, b is uint32
552	extern bool q_fits_int64(rational_t *r); // r is a/b where a is int64, b is uint64
553
554
555
556	/*
557	* Size estimate
558	* - this returns approximately the number of bits to represent r's numerator
559	* - this may not be exact (typically rounded up to a multiple of 32)
560	* - also if r is really really big, this function may return
561	* UINT32_MAX (not very likely!)
562	*/
563	extern uint32_t q_size(rational_t *r);
564
565
566	/*
567	* CONVERSION TO GMP OBJECTS
568	*/
569
570	/*
571	* Store r into the GMP integer z.
572	* - return false if r is not a integer, true otherwise
573	*/
574	extern bool q_get_mpz(const rational_t *r, mpz_t z);
575
576
577	/*
578	* Store r into q
579	*/
580	extern void q_get_mpq(const rational_t *r, mpq_t q);
581
582
583	/*
584	* Convert to a floating point number
585	*/
586	extern double q_get_double(rational_t *r);
587
588
589
590	/*
591	* PRINT
592	*/
593
594	/*
595	* Print r on stream f.
596	* q_print_abs prints the absolute value
597	*/
598	extern void q_print(FILE f, const rational_t r);
599	extern void q_print_abs(FILE f, const rational_t r);
600
601
602	/*
603	* HASH FUNCTION
604	*/
605
606	/*
607	* Hash functions: return a hash of numerator or denominator.
608	* - hash_numerator(r) = numerator MOD bigprime
609	* - hash_denominator(r) = denominator MOD bigprime
610	* where bigprime is the largest prime number smaller than 2^32.
611	*/
612	extern uint32_t q_hash_numerator(const rational_t *r);
613	extern uint32_t q_hash_denominator(const rational_t *r);
614	extern void q_hash_decompose(const rational_t r, uint32_t h_num, uint32_t *h_den);
615
616
617
618
619	/*
620	* RATIONAL ARRAYS
621	*/
622
623	#define MAX_RATIONAL_ARRAY_SIZE (UINT32_MAX/sizeof(rational_t))
624
625	/*
626	* Create and initialize an array of n rationals.
627	*/
628	extern rational_t *new_rational_array(uint32_t n);
629
630	/*
631	* Delete an array created by the previous function
632	* - n must be the size of a
633	*/
634	extern void free_rational_array(rational_t *a, uint32_t n);
635
636
637
638
639
640	#endif /* __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