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

83.33

/src/solvers/bv/bv_atomtable.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/>.
 */

/*
 * TABLE OF ATOMS FOR THE BITVECTOR SOLVER
 */

/*
 * Bit vector atoms are of three kinds:
 * - bveq x y
 * - bvge x y: x <= y, where x and y are interpreted
 *   as unsigned integers
 * - bvsge x y: x <= y, where x and y are as signed
 *   integers
 */

#ifndef __BV_ATOMTABLE_H
#define __BV_ATOMTABLE_H

#include <stdint.h>
#include <stdbool.h>
#include <stddef.h>
#include <assert.h>

#include "solvers/egraph/egraph_base_types.h"
#include "utils/int_hash_tables.h"


/*
 * Tags for atom types
 * - each atom maps an external boolean variable (in the core)
 *   to a constraint on two variables x and y.
 * - there are three kinds of atoms: eq, ge, sge
 */
typedef enum bvatm_tag {
  BVEQ_ATM,     // (x == y)
  BVUGE_ATM,    // (x >= y) unsigned
  BVSGE_ATM,    // (x >= y) signed
} bvatm_tag_t;



/*
 * ATOMS
 */

/*
 * Atom structure:
 * - the header encodes the tag + a mark
 * - lit is a literal in the core.
 *   if lit == true_literal, the atom is true at the toplevel
 *   if lit == false_literal, the atom is false at the toplevel
 *   otherwise the atom is attached to a boolean variable v
 *   in the core and lit is pos_lit(v).
 * - left/right are x and y
 */
typedef struct bvatm_s {
  uint32_t header;
  literal_t lit;
  thvar_t left;
  thvar_t right;
} bvatm_t;



/*
 * Access to tag and mark
 * - the two low order bits of the header contain the tag
 * - the next bit is the mark
 */
static inline bvatm_tag_t bvatm_tag(bvatm_t *atm) {
  return (bvatm_tag_t) (atm->header & 0x3);
}

static inline bool bvatm_is_eq(bvatm_t *atm) {
  return bvatm_tag(atm) == BVEQ_ATM;
}

static inline bool bvatm_is_ge(bvatm_t *atm) {
  return bvatm_tag(atm) == BVUGE_ATM;
}

static inline bool bvatm_is_sge(bvatm_t *atm) {
  return bvatm_tag(atm) == BVSGE_ATM;
}

static inline bool bvatm_is_marked(bvatm_t *atm) {
  return (atm->header & 0x4) != 0;
}

static inline void bvatm_set_mark(bvatm_t *atm) {
  atm->header |= 0x4;
}


/*
 * Boolean variable of atm
 * - if lit == null_literal, return null_bvar
 */
static inline bvar_t bvatm_bvar(bvatm_t *atm) {
  return var_of(atm->lit);
}


/*
 * Conversions between void* pointers and atom indices
 * - an atom index is packed into a void * pointer, with a two-bit tag
 *   to indicate that it's an bitvector atom (cf. egraph_base_types.h)
 * - there's no loss of data even if pointers are 32 bits (because
 *   the tag is 2bits and i is less than MAX_BVATOMTABLE_SIZE (i.e., 2^32/16)
 */
static inline void *bvatom_idx2tagged_ptr(int32_t i) {
  return tagged_bv_atom((void *)((size_t) (i << 2)));
}

static inline int32_t bvatom_tagged_ptr2idx(void *p) {
  return (int32_t)(((size_t) p) >> 2);
}




/*
 * ATOM TABLE
 */

/*
 * Atom descriptors are stored in array data
 * - natoms = number of atoms
 * - size = size of the data array
 */
typedef struct bv_atomtable_s {
  uint32_t natoms;
  uint32_t size;
  bvatm_t *data;

  int_htbl_t htbl;  // for hash consing
} bv_atomtable_t;


#define DEF_BVATOMTABLE_SIZE 100
#define MAX_BVATOMTABLE_SIZE (UINT32_MAX/sizeof(bvatm_t))




/*
 * OPERATIONS
 */

/*
 * Initialization
 * - use the default size
 * - the table is initially empty
 */
extern void init_bv_atomtable(bv_atomtable_t *table);


/*
 * Delete the table
 */
extern void delete_bv_atomtable(bv_atomtable_t *table);


/*
 * Empty the table
 */
extern void reset_bv_atomtable(bv_atomtable_t *table);


/*
 * Remove all atoms of index >= na
 */
extern void bv_atomtable_remove_atoms(bv_atomtable_t *table, uint32_t na);


/*
 * Constructors
 * - get_bv_atom(table, op, x, y): check whether atom (op x y) exists.
 *   If it does not create a new atom, with literal set to null_literal.
 *   Return the atom index.
 * - get_bveq_atom normalizes (eq x y) then calls get_bv_atom.
 */
extern int32_t get_bv_atom(bv_atomtable_t *table, bvatm_tag_t op, thvar_t x, thvar_t y);
extern int32_t get_bveq_atom(bv_atomtable_t *table, thvar_t x, thvar_t y);

static inline int32_t get_bvuge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {
  return get_bv_atom(table, BVUGE_ATM, x, y);
}

static inline int32_t get_bvsge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {
  return get_bv_atom(table, BVSGE_ATM, x, y);
}


/*
 * Search for an atom
 * - return the atom id if it exists
 * - return -1 otherwise
 */
extern int32_t find_bv_atom(bv_atomtable_t *table, bvatm_tag_t op, thvar_t x, thvar_t y);
extern int32_t find_bveq_atom(bv_atomtable_t *table, thvar_t x, thvar_t y);

static inline int32_t find_bvuge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {
  return find_bv_atom(table, BVUGE_ATM, x, y);
}

static inline int32_t find_bvsge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {
  return find_bv_atom(table, BVSGE_ATM, x, y);
}




/*
 * Get the descriptor of atom i
 */
static inline bvatm_t *bvatom_desc(bv_atomtable_t *atbl, int32_t i) {
  assert(0 <= i && i < atbl->natoms);
  return atbl->data + i;
}




#endif /* __BV_ATOMTABLE_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	* TABLE OF ATOMS FOR THE BITVECTOR SOLVER
21	*/
22
23	/*
24	* Bit vector atoms are of three kinds:
25	* - bveq x y
26	* - bvge x y: x <= y, where x and y are interpreted
27	* as unsigned integers
28	* - bvsge x y: x <= y, where x and y are as signed
29	* integers
30	*/
31
32	#ifndef __BV_ATOMTABLE_H
33	#define __BV_ATOMTABLE_H
34
35	#include <stdint.h>
36	#include <stdbool.h>
37	#include <stddef.h>
38	#include <assert.h>
39
40	#include "solvers/egraph/egraph_base_types.h"
41	#include "utils/int_hash_tables.h"
42
43
44	/*
45	* Tags for atom types
46	* - each atom maps an external boolean variable (in the core)
47	* to a constraint on two variables x and y.
48	* - there are three kinds of atoms: eq, ge, sge
49	*/
50	typedef enum bvatm_tag {
51	BVEQ_ATM, // (x == y)
52	BVUGE_ATM, // (x >= y) unsigned
53	BVSGE_ATM, // (x >= y) signed
54	} bvatm_tag_t;
55
56
57
58	/*
59	* ATOMS
60	*/
61
62	/*
63	* Atom structure:
64	* - the header encodes the tag + a mark
65	* - lit is a literal in the core.
66	* if lit == true_literal, the atom is true at the toplevel
67	* if lit == false_literal, the atom is false at the toplevel
68	* otherwise the atom is attached to a boolean variable v
69	* in the core and lit is pos_lit(v).
70	* - left/right are x and y
71	*/
72	typedef struct bvatm_s {
73	uint32_t header;
74	literal_t lit;
75	thvar_t left;
76	thvar_t right;
77	} bvatm_t;
78
79
80
81	/*
82	* Access to tag and mark
83	* - the two low order bits of the header contain the tag
84	* - the next bit is the mark
85	*/
86	static inline bvatm_tag_t bvatm_tag(bvatm_t *atm) {	890,101✔
87	return (bvatm_tag_t) (atm->header & 0x3);	890,101✔
88	}
89
90	static inline bool bvatm_is_eq(bvatm_t *atm) {	11✔
91	return bvatm_tag(atm) == BVEQ_ATM;	11✔
92	}
93
94	static inline bool bvatm_is_ge(bvatm_t *atm) {	3,212✔
95	return bvatm_tag(atm) == BVUGE_ATM;	3,212✔
96	}
97
98	static inline bool bvatm_is_sge(bvatm_t *atm) {	1,485✔
99	return bvatm_tag(atm) == BVSGE_ATM;	1,485✔
100	}
101
102	static inline bool bvatm_is_marked(bvatm_t *atm) {
103	return (atm->header & 0x4) != 0;
104	}
105
106	static inline void bvatm_set_mark(bvatm_t *atm) {
107	atm->header \|= 0x4;
108	}
109
110
111	/*
112	* Boolean variable of atm
113	* - if lit == null_literal, return null_bvar
114	*/
115	static inline bvar_t bvatm_bvar(bvatm_t *atm) {	×
116	return var_of(atm->lit);	×
117	}
118
119
120	/*
121	* Conversions between void* pointers and atom indices
122	* - an atom index is packed into a void * pointer, with a two-bit tag
123	* to indicate that it's an bitvector atom (cf. egraph_base_types.h)
124	* - there's no loss of data even if pointers are 32 bits (because
125	* the tag is 2bits and i is less than MAX_BVATOMTABLE_SIZE (i.e., 2^32/16)
126	*/
127	static inline void *bvatom_idx2tagged_ptr(int32_t i) {	20,904✔
128	return tagged_bv_atom((void *)((size_t) (i << 2)));	20,904✔
129	}
130
131	static inline int32_t bvatom_tagged_ptr2idx(void *p) {	×
132	return (int32_t)(((size_t) p) >> 2);	×
133	}
134
135
136
137
138	/*
139	* ATOM TABLE
140	*/
141
142	/*
143	* Atom descriptors are stored in array data
144	* - natoms = number of atoms
145	* - size = size of the data array
146	*/
147	typedef struct bv_atomtable_s {
148	uint32_t natoms;
149	uint32_t size;
150	bvatm_t *data;
151
152	int_htbl_t htbl; // for hash consing
153	} bv_atomtable_t;
154
155
156	#define DEF_BVATOMTABLE_SIZE 100
157	#define MAX_BVATOMTABLE_SIZE (UINT32_MAX/sizeof(bvatm_t))
158
159
160
161
162	/*
163	* OPERATIONS
164	*/
165
166	/*
167	* Initialization
168	* - use the default size
169	* - the table is initially empty
170	*/
171	extern void init_bv_atomtable(bv_atomtable_t *table);
172
173
174	/*
175	* Delete the table
176	*/
177	extern void delete_bv_atomtable(bv_atomtable_t *table);
178
179
180	/*
181	* Empty the table
182	*/
183	extern void reset_bv_atomtable(bv_atomtable_t *table);
184
185
186	/*
187	* Remove all atoms of index >= na
188	*/
189	extern void bv_atomtable_remove_atoms(bv_atomtable_t *table, uint32_t na);
190
191
192	/*
193	* Constructors
194	* - get_bv_atom(table, op, x, y): check whether atom (op x y) exists.
195	* If it does not create a new atom, with literal set to null_literal.
196	* Return the atom index.
197	* - get_bveq_atom normalizes (eq x y) then calls get_bv_atom.
198	*/
199	extern int32_t get_bv_atom(bv_atomtable_t *table, bvatm_tag_t op, thvar_t x, thvar_t y);
200	extern int32_t get_bveq_atom(bv_atomtable_t *table, thvar_t x, thvar_t y);
201
202	static inline int32_t get_bvuge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {	3,310✔
203	return get_bv_atom(table, BVUGE_ATM, x, y);	3,310✔
204	}
205
206	static inline int32_t get_bvsge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {	3,963✔
207	return get_bv_atom(table, BVSGE_ATM, x, y);	3,963✔
208	}
209
210
211	/*
212	* Search for an atom
213	* - return the atom id if it exists
214	* - return -1 otherwise
215	*/
216	extern int32_t find_bv_atom(bv_atomtable_t *table, bvatm_tag_t op, thvar_t x, thvar_t y);
217	extern int32_t find_bveq_atom(bv_atomtable_t *table, thvar_t x, thvar_t y);
218
219	static inline int32_t find_bvuge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {	1,654✔
220	return find_bv_atom(table, BVUGE_ATM, x, y);	1,654✔
221	}
222
223	static inline int32_t find_bvsge_atom(bv_atomtable_t *table, thvar_t x, thvar_t y) {	747✔
224	return find_bv_atom(table, BVSGE_ATM, x, y);	747✔
225	}
226
227
228
229
230	/*
231	* Get the descriptor of atom i
232	*/
233	static inline bvatm_t bvatom_desc(bv_atomtable_t atbl, int32_t i) {	42,240✔
234	assert(0 <= i && i < atbl->natoms);
235	return atbl->data + i;	42,240✔
236	}
237
238
239
240
241	#endif /* __BV_ATOMTABLE_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