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 POLYNOMIALS WITH 64BIT COEFFICIENTS
21 */
22
23 /*
24 * Polynomials with small bit-vector coefficients
25 * represented as arrays of monomials. This can be
26 * used for bit-vector polynomials with bitsize between
27 * 1 and 64.
28 *
29 * Each monomial is a pair <coeff, variable>
30 * - coeff is a bit-vector constant, stored as a 64bit integer.
31 * - variable is a 32bit integer.
32 *
33 * Most operations require the polynomial object to be normalized:
34 * - the monomials must be sorted and all the coefficients must
35 * be non-zero and reduced modulo 2^bitsize.
36 * - the last monomials must be an end marker (var = max_idx)
37 *
38 * Most related operations are defined in bvarith64_buffers.c.
39 */
40
41 #ifndef __BV64_POLYNOMIALS_H
42 #define __BV64_POLYNOMIALS_H
43
44 #include <stdint.h>
45 #include <stdbool.h>
46
47 #include "terms/polynomial_common.h"
48 #include "utils/memalloc.h"
49
50 /*
51 * Polynomial structure:
52 * - bitsize = number of bits (must be between 1 and 64)
53 * - nterms = number of monomials
54 * - mono = array of (nterms + 1) monomials
55 * Polynomials are normalized:
56 * - the coefficients are non zero.
57 * - the monomials are sorted.
58 * - mono[nterms].var contains the end marker max_idx
59 */
60
61 // monomial
62 typedef struct {
63 int32_t var;
64 uint64_t coeff;
65 } bvmono64_t;
66
67 // polynomial
68 typedef struct {
69 uint32_t nterms;
70 uint32_t bitsize;
71 bvmono64_t mono[0]; // actual size = nterms + 1
72 } bvpoly64_t;
73
74
75 /*
76 * Maximal number of terms in a polynomial
77 */
78 #define MAX_BVPOLY64_SIZE (((UINT32_MAX-sizeof(bvpoly64_t))/sizeof(bvmono64_t))-1)
79
80
81 /*
82 * Seed used in the hash function
83 */
84 #define HASH_BVPOLY64_SEED ((uint32_t) 0xfe4dea20)
85
86
87 /*
88 * Allocate a bit-vector polynomial
89 * - n = number of terms (excluding the end marker)
90 * - n must be less than MAX_BVPOLY64_SIZE
91 * - size = bitsize (must be positive and no more than 64)
92 * The coefficients and variables are not initialized,
93 * except the end marker.
94 */
95 extern bvpoly64_t *alloc_bvpoly64(uint32_t n, uint32_t size);
96
97
98 /*
99 * Free p
100 */
free_bvpoly64(bvpoly64_t * p)101 static inline void free_bvpoly64(bvpoly64_t *p) {
102 safe_free(p);
103 }
104
105
106 /*
107 * Hash code of p
108 */
109 extern uint32_t hash_bvpoly64(bvpoly64_t *p);
110
111
112 /*
113 * Return the main variable of p (i.e., last variable)
114 * - return null_idx if p is zero
115 * - return const_idx is p is a constant
116 */
117 extern int32_t bvpoly64_main_var(bvpoly64_t *p);
118
119
120 /*
121 * Check whether p1 and p2 are equal
122 * - p1 and p2 must be normalized
123 */
124 extern bool equal_bvpoly64(bvpoly64_t *p1, bvpoly64_t *p2);
125
126
127 /*
128 * Check for simple disequality: return true if (p1 - p2) is a non-zero
129 * constant bitvector.
130 * - p1 and p2 must have the same bitsize and must be normalized
131 */
132 extern bool disequal_bvpoly64(bvpoly64_t *p1, bvpoly64_t *p2);
133
134
135 /*
136 * Check whether p is equal to k + x for a non-zero constant k and a variable x
137 */
138 extern bool bvpoly64_is_const_plus_var(bvpoly64_t *p, int32_t x);
139
140
141
142
143 #endif /* __BV64_POLYNOMIALS_H */
144