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

93.22

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

/*
 * XOR/OR/NOT graph used to represent intermediate bit-vector expressions.
 *
 * We need a new representation to replace BDDs. The BDDs blow
 * up on several benchmarks.
 *
 * Update: January 29, 2009.
 * - Tests show that flattening the nodes is dangerous. It can consume
 *   a lot of memory and the node table blows up on one QF_BV benchmark.
 * - Since flattening does not work, it makes sense to simplify the
 *   data structures. All OR and XOR nodes are now binary nodes.
 *
 * February 09, 2009:
 * - Added sets of variables to each node
 *
 * April 2010:
 * - adjusted this module to the new term representations
 * - added a new node type (select k i) for bit-select
 * - added a map field to support conversion from bit representation
 *   to boolean terms
 * - removed the vsets
 */

#ifndef __BIT_EXPR_H
#define __BIT_EXPR_H

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

#include "utils/indexed_table.h"
#include "utils/int_hash_tables.h"
#include "utils/int_vectors.h"


/*
 * The graph is stored as a table of nodes
 * - each node is identified by a 30 bit index in the table
 * - negations are encoded by attaching a polarity bit to a node index:
 *   a node occurrence u_i is a 32 bit integer formatted as
 *     [0|node index|polarity bit]
 *   polarity 0 means positive occurrence
 *   polarity 1 means negative occurrence
 * - there are five types of nodes
 *   - the constant node: 0
 *   - variable node: (term-idx i) where i is an integer
 *   - select node: (select k i) where k and i are integers
 *   - OR nodes: (OR a b)
 *   - XOR nodes: (XOR a b)
 *   where a and b are node occurrences
 *
 * (term-idx i) is intended to denote boolean term i in the term table
 *
 * (select k i) is intended to be bit k of term i where i
 * is a bitvector term in the term table.
 *
 * The constant, variable, and select nodes are the leaf nodes
 * in the DAG. The OR and XOR nodes are non-leaf nodes.
 */

/*
 * Tags identifying the node type
 */
typedef enum {
  UNUSED_NODE,    // deleted node
  CONSTANT_NODE,  // 0 = true
  VARIABLE_NODE,
  SELECT_NODE,
  OR_NODE,
  XOR_NODE,
} node_kind_t;


/*
 * Bit type = 32bit integers
 */
typedef int32_t bit_t;
typedef int32_t node_t;


/*
 * Conversion from node index to bit
 */
static inline bit_t pos_bit(node_t x) {
  return (x<<1)|0;
}

static inline bit_t neg_bit(node_t x) {
  return (x<<1)|1;
}

// sign = 0 or 1 (0 means positive, 1 means negative)
static inline bit_t mk_bit(node_t x, uint32_t sign) {
  assert((sign & ~1) == 0);
  return (x<<1)|sign;
}

static inline bool bit_is_pos(bit_t x) {
  return (x & 1) == 0;
}

static inline bool bit_is_neg(bit_t x) {
  return (x & 1) != 0;
}

static inline node_t node_of_bit(bit_t x) {
  return (x >> 1);
}

// sign = 1 --> negative bit, sign = 0 --> positive bit
static inline uint32_t sign_of_bit(bit_t x) {
  return ((uint32_t) x) & 1;
}

// force the sign bit to 0 (convert (neg_bit(b) to pos_bit(b))
static inline bit_t unsigned_bit(bit_t x) {
  return (x & ~1);
}

// check whether x == (not y)
static inline bool opposite_bits(bit_t x, bit_t y) {
  return (x ^ y) == 1;
}



/*
 * Predefined nodes and bits
 */
enum {
  null_node = -1,
  constant_node = 0,

  null_bit = -1,
  true_bit = 0,
  false_bit = 1,
};




/*
 * Node descriptor:
 * - either an integer (for a variable node)
 * - of a pair index, var (for a select node)
 * - or a pair of bits (for a binary node).
 */
typedef struct select_node_s {
  uint32_t index;
  int32_t var;
} select_node_t;

typedef struct node_desc_s {
  union {
    indexed_table_elem_t elem;
    int32_t var;
    select_node_t sel;
    bit_t c[2];
  };
  int32_t map;
  uint8_t kind;
} node_desc_t;



/*
 * Global table of nodes. For each node k, we keep
 * - kind[k] = UNUSED/CONSTANT/VARIABLE/OR/XOR
 * - desc[k] = descriptor
 * - map[k] = integer (used in conversion from bits to Boolean terms)
 *   map[k] is set to -1 when the node is created
 *   map[k] is the term corresponding to node k after conversion to terms
 *    (cf. bit_term_conversion)
 *
 * Free list: the UNUSED nodes are stored in a free list
 * - table->free_list = index of the first node in that list
 * - for an UNUSED node i, table->desc[i].var = next node in the free list
 *
 * Auxiliary structures:
 * - vector for simplifying OR and XOR
 * - hash table for hash consing of OR and XOR nodes
 *
 * Garbage collection:
 * - crude technique: we keep a global reference counter for the whole
 *   node table. The counter is the number of external objects that refer
 *   to nodes in the table.
 * - when the counter is zero we reset the whole table
 */
typedef struct node_table_s {
  indexed_table_t nodes;

  uint32_t ref_counter;

  ivector_t aux_buffer;
  int_htbl_t htbl;
} node_table_t;


#define DEF_NODE_TABLE_SIZE 1000
#define MAX_NODE_TABLE_SIZE (UINT32_MAX/sizeof(node_desc_t))





/*
 * INITIALIZATION/NODE CONSTRUCTION
 */


/*
 * Initialize node table
 * - n = initial size
 * - if n = 0, the default size is used
 * Also create the constant node
 */
extern void init_node_table(node_table_t *table, uint32_t n);

/*
 * Delete the full node table
 */
extern void delete_node_table(node_table_t *table);

/*
 * Empty the table (but keep the constant node)
 */
extern void reset_node_table(node_table_t *table);

static inline uint32_t node_table_nelems(const node_table_t *table) {
  return indexed_table_nelems(&table->nodes);
}


/*
 * CONSTRUCTORS
 */

/*
 * Create a variable node
 * - p = external term index
 */
extern bit_t node_table_alloc_var(node_table_t *table, int32_t p);


/*
 * Create a select node:
 * - k = index
 * - p = external term
 */
extern bit_t node_table_alloc_select(node_table_t *table, uint32_t k, int32_t p);


/*
 * Construct (not x)
 */
static inline bit_t bit_not(bit_t b) {
  return b ^ 1;
}

/*
 * Create a constant bit of value equal to tt
 */
static inline bit_t bit_constant(bool tt) {
  return false_bit - ((uint32_t) tt);
}

/*
 * Conversion of constant bit to integers:
 * - true_bit --> 1, false_bit --> 0
 */
static inline uint32_t bit_const_value(bit_t b) {
  assert(b == true_bit || b == false_bit);
  return b ^ 1;
}


/*
 * Main constructors: don't do much simplification
 */
extern bit_t bit_or2(node_table_t *table, bit_t b1, bit_t b2);
extern bit_t bit_xor2(node_table_t *table, bit_t b1, bit_t b2);

// Variant implementations: simplify more
extern bit_t bit_or2simplify(node_table_t *table, bit_t b1, bit_t b2);
extern bit_t bit_xor2simplify(node_table_t *table, bit_t b1, bit_t b2);


/*
 * Derived operations:
 * (and b1 b2) = ~(or ~b1 ~b2)
 *  (eq b1 b2) = ~(xor b1 b2)
 */
static inline bit_t bit_and2(node_table_t *table, bit_t b1, bit_t b2) {
  return bit_not(bit_or2(table, bit_not(b1), bit_not(b2)));
}

static inline bit_t bit_eq2(node_table_t *table, bit_t b1, bit_t b2) {
  return bit_not(bit_xor2(table, b1, b2));
}

static inline bit_t bit_and2simplify(node_table_t *table, bit_t b1, bit_t b2) {
  return bit_not(bit_or2simplify(table, bit_not(b1), bit_not(b2)));
}

static inline bit_t bit_eq2simplify(node_table_t *table, bit_t b1, bit_t b2) {
  return bit_not(bit_xor2simplify(table, b1, b2));
}



/*
 * N-ary constructors
 * (bit_or  b[0] ... b[n-1])
 * (bit_and b[0] ... b[n-1])
 * (bit_xor b[0] ... b[n-1])
 */
extern bit_t bit_or(node_table_t *table, bit_t *b, uint32_t n);
extern bit_t bit_and(node_table_t *table, bit_t *b, uint32_t n);
extern bit_t bit_xor(node_table_t *table, bit_t *b, uint32_t n);





/*
 * GARBAGE COLLECTION
 */
// increment the reference counter
static inline void node_table_incref(node_table_t *table) {
  table->ref_counter ++;
}

// decrement the reference counter
// if it becomes zero, empty the table.
extern void node_table_decref(node_table_t *table);


// force the reference counter to zero: use this before an explicit call to reset
static inline void node_table_clear_refcount(node_table_t *table) {
  table->ref_counter = 0;
}




/*
 * ACCESS TO THE TABLE
 */
static inline bool valid_node(node_table_t *table, node_t x) {
  return 0 <= x && x < node_table_nelems(table);
}

static inline node_desc_t *node_table_elem(node_table_t *table, node_t x) {
  return indexed_table_elem(node_desc_t, &table->nodes, x);
}

static inline node_kind_t node_kind(node_table_t *table, node_t x) {
  assert(valid_node(table, x));
  return node_table_elem(table, x)->kind;
}

static inline bool good_node(node_table_t *table, node_t x) {
  return valid_node(table, x) && node_kind(table, x) != UNUSED_NODE;
}

static inline bool is_constant_node(node_table_t *table, node_t x) {
  return node_kind(table, x) == CONSTANT_NODE;
}

static inline bool is_variable_node(node_table_t *table, node_t x) {
  return node_kind(table, x) == VARIABLE_NODE;
}

static inline bool is_select_node(node_table_t *table, node_t x) {
  return node_kind(table, x) == SELECT_NODE;
}

static inline bool is_or_node(node_table_t *table, node_t x) {
  return node_kind(table, x) == OR_NODE;
}

static inline bool is_xor_node(node_table_t *table, node_t x) {
  return node_kind(table, x) == XOR_NODE;
}

static inline bool is_leaf_node(node_table_t *table, node_t x) {
  node_kind_t k;
  k = node_kind(table, x);
  return k == CONSTANT_NODE || k == VARIABLE_NODE || k == SELECT_NODE;
}

static inline bool is_nonleaf_node(node_table_t *table, node_t x) {
  node_kind_t k;
  k = node_kind(table, x);
  return k == OR_NODE || k == XOR_NODE;
}



/*
 * Get or set map[x] for a node x
 * - the default value for map[x] is -1.
 */
static inline int32_t map_of_node(node_table_t *table, node_t x) {
  assert(good_node(table, x));
  return node_table_elem(table, x)->map;
}

static inline void set_map_of_node(node_table_t *table, node_t x, int32_t v) {
  assert(good_node(table, x));
  node_table_elem(table, x)->map = v;
}



/*
 * Variable of a variable node x
 */
static inline int32_t var_of_node(node_table_t *table, node_t x) {
  assert(is_variable_node(table, x));
  return node_table_elem(table, x)->var;
}


/*
 * Variable and index of a select node x
 */
static inline select_node_t *select_of_node(node_table_t *table, node_t x) {
  assert(is_select_node(table, x));
  return &node_table_elem(table, x)->sel;
}

static inline int32_t var_of_select_node(node_table_t *table, node_t x) {
  return select_of_node(table, x)->var;
}

static inline uint32_t index_of_select_node(node_table_t *table, node_t x) {
  return select_of_node(table, x)->index;
}



/*
 * Children of node x = array of 2 bits
 * - x must be a non-leaf node
 */
static inline bit_t *children_of_node(node_table_t *table, node_t x) {
  assert(is_nonleaf_node(table, x));
  return node_table_elem(table, x)->c;
}

// child 0 or 1
static inline bit_t child_of_node(node_table_t *table, node_t x, uint32_t k) {
  assert(k < 2);
  return children_of_node(table, x)[k];
}

// left child = child 0, right child = child 1
static inline bit_t left_child_of_node(node_table_t *table, node_t x) {
  return child_of_node(table, x, 0);
}

static inline bit_t right_child_of_node(node_table_t *table, node_t x) {
  return child_of_node(table, x, 1);
}


/*
 * Check whether bit-expression b is a constant
 */
static inline bool bit_is_const(bit_t b) {
  return node_of_bit(b) == constant_node;
}


#endif /* __BIT_EXPR_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	* XOR/OR/NOT graph used to represent intermediate bit-vector expressions.
21	*
22	* We need a new representation to replace BDDs. The BDDs blow
23	* up on several benchmarks.
24	*
25	* Update: January 29, 2009.
26	* - Tests show that flattening the nodes is dangerous. It can consume
27	* a lot of memory and the node table blows up on one QF_BV benchmark.
28	* - Since flattening does not work, it makes sense to simplify the
29	* data structures. All OR and XOR nodes are now binary nodes.
30	*
31	* February 09, 2009:
32	* - Added sets of variables to each node
33	*
34	* April 2010:
35	* - adjusted this module to the new term representations
36	* - added a new node type (select k i) for bit-select
37	* - added a map field to support conversion from bit representation
38	* to boolean terms
39	* - removed the vsets
40	*/
41
42	#ifndef __BIT_EXPR_H
43	#define __BIT_EXPR_H
44
45	#include <stdint.h>
46	#include <stdbool.h>
47	#include <assert.h>
48
49	#include "utils/indexed_table.h"
50	#include "utils/int_hash_tables.h"
51	#include "utils/int_vectors.h"
52
53
54	/*
55	* The graph is stored as a table of nodes
56	* - each node is identified by a 30 bit index in the table
57	* - negations are encoded by attaching a polarity bit to a node index:
58	* a node occurrence u_i is a 32 bit integer formatted as
59	* [0\|node index\|polarity bit]
60	* polarity 0 means positive occurrence
61	* polarity 1 means negative occurrence
62	* - there are five types of nodes
63	* - the constant node: 0
64	* - variable node: (term-idx i) where i is an integer
65	* - select node: (select k i) where k and i are integers
66	* - OR nodes: (OR a b)
67	* - XOR nodes: (XOR a b)
68	* where a and b are node occurrences
69	*
70	* (term-idx i) is intended to denote boolean term i in the term table
71	*
72	* (select k i) is intended to be bit k of term i where i
73	* is a bitvector term in the term table.
74	*
75	* The constant, variable, and select nodes are the leaf nodes
76	* in the DAG. The OR and XOR nodes are non-leaf nodes.
77	*/
78
79	/*
80	* Tags identifying the node type
81	*/
82	typedef enum {
83	UNUSED_NODE, // deleted node
84	CONSTANT_NODE, // 0 = true
85	VARIABLE_NODE,
86	SELECT_NODE,
87	OR_NODE,
88	XOR_NODE,
89	} node_kind_t;
90
91
92	/*
93	* Bit type = 32bit integers
94	*/
95	typedef int32_t bit_t;
96	typedef int32_t node_t;
97
98
99	/*
100	* Conversion from node index to bit
101	*/
102	static inline bit_t pos_bit(node_t x) {	4,099,382✔
103	return (x<<1)\|0;	4,099,382✔
104	}
105
106	static inline bit_t neg_bit(node_t x) {
107	return (x<<1)\|1;
108	}
109
110	// sign = 0 or 1 (0 means positive, 1 means negative)
111	static inline bit_t mk_bit(node_t x, uint32_t sign) {	13,410✔
112	assert((sign & ~1) == 0);
113	return (x<<1)\|sign;	13,410✔
114	}
115
116	static inline bool bit_is_pos(bit_t x) {	3,991,998✔
117	return (x & 1) == 0;	3,991,998✔
118	}
119
120	static inline bool bit_is_neg(bit_t x) {	×
121	return (x & 1) != 0;	×
122	}
123
124	static inline node_t node_of_bit(bit_t x) {	15,506,343✔
125	return (x >> 1);	15,506,343✔
126	}
127
128	// sign = 1 --> negative bit, sign = 0 --> positive bit
129	static inline uint32_t sign_of_bit(bit_t x) {	153,141✔
130	return ((uint32_t) x) & 1;	153,141✔
131	}
132
133	// force the sign bit to 0 (convert (neg_bit(b) to pos_bit(b))
134	static inline bit_t unsigned_bit(bit_t x) {
135	return (x & ~1);
136	}
137
138	// check whether x == (not y)
139	static inline bool opposite_bits(bit_t x, bit_t y) {	116,552✔
140	return (x ^ y) == 1;	116,552✔
141	}
142
143
144
145	/*
146	* Predefined nodes and bits
147	*/
148	enum {
149	null_node = -1,
150	constant_node = 0,
151
152	null_bit = -1,
153	true_bit = 0,
154	false_bit = 1,
155	};
156
157
158
159
160	/*
161	* Node descriptor:
162	* - either an integer (for a variable node)
163	* - of a pair index, var (for a select node)
164	* - or a pair of bits (for a binary node).
165	*/
166	typedef struct select_node_s {
167	uint32_t index;
168	int32_t var;
169	} select_node_t;
170
171	typedef struct node_desc_s {
172	union {
173	indexed_table_elem_t elem;
174	int32_t var;
175	select_node_t sel;
176	bit_t c[2];
177	};
178	int32_t map;
179	uint8_t kind;
180	} node_desc_t;
181
182
183
184	/*
185	* Global table of nodes. For each node k, we keep
186	* - kind[k] = UNUSED/CONSTANT/VARIABLE/OR/XOR
187	* - desc[k] = descriptor
188	* - map[k] = integer (used in conversion from bits to Boolean terms)
189	* map[k] is set to -1 when the node is created
190	* map[k] is the term corresponding to node k after conversion to terms
191	* (cf. bit_term_conversion)
192	*
193	* Free list: the UNUSED nodes are stored in a free list
194	* - table->free_list = index of the first node in that list
195	* - for an UNUSED node i, table->desc[i].var = next node in the free list
196	*
197	* Auxiliary structures:
198	* - vector for simplifying OR and XOR
199	* - hash table for hash consing of OR and XOR nodes
200	*
201	* Garbage collection:
202	* - crude technique: we keep a global reference counter for the whole
203	* node table. The counter is the number of external objects that refer
204	* to nodes in the table.
205	* - when the counter is zero we reset the whole table
206	*/
207	typedef struct node_table_s {
208	indexed_table_t nodes;
209
210	uint32_t ref_counter;
211
212	ivector_t aux_buffer;
213	int_htbl_t htbl;
214	} node_table_t;
215
216
217	#define DEF_NODE_TABLE_SIZE 1000
218	#define MAX_NODE_TABLE_SIZE (UINT32_MAX/sizeof(node_desc_t))
219
220
221
222
223
224	/*
225	* INITIALIZATION/NODE CONSTRUCTION
226	*/
227
228
229	/*
230	* Initialize node table
231	* - n = initial size
232	* - if n = 0, the default size is used
233	* Also create the constant node
234	*/
235	extern void init_node_table(node_table_t *table, uint32_t n);
236
237	/*
238	* Delete the full node table
239	*/
240	extern void delete_node_table(node_table_t *table);
241
242	/*
243	* Empty the table (but keep the constant node)
244	*/
245	extern void reset_node_table(node_table_t *table);
246
247	static inline uint32_t node_table_nelems(const node_table_t *table) {
248	return indexed_table_nelems(&table->nodes);
249	}
250
251
252	/*
253	* CONSTRUCTORS
254	*/
255
256	/*
257	* Create a variable node
258	* - p = external term index
259	*/
260	extern bit_t node_table_alloc_var(node_table_t *table, int32_t p);
261
262
263	/*
264	* Create a select node:
265	* - k = index
266	* - p = external term
267	*/
268	extern bit_t node_table_alloc_select(node_table_t *table, uint32_t k, int32_t p);
269
270
271	/*
272	* Construct (not x)
273	*/
274	static inline bit_t bit_not(bit_t b) {	778,969✔
275	return b ^ 1;	778,969✔
276	}
277
278	/*
279	* Create a constant bit of value equal to tt
280	*/
281	static inline bit_t bit_constant(bool tt) {	922,100✔
282	return false_bit - ((uint32_t) tt);	922,100✔
283	}
284
285	/*
286	* Conversion of constant bit to integers:
287	* - true_bit --> 1, false_bit --> 0
288	*/
289	static inline uint32_t bit_const_value(bit_t b) {	2,295,683✔
290	assert(b == true_bit \|\| b == false_bit);
291	return b ^ 1;	2,295,683✔
292	}
293
294
295	/*
296	* Main constructors: don't do much simplification
297	*/
298	extern bit_t bit_or2(node_table_t *table, bit_t b1, bit_t b2);
299	extern bit_t bit_xor2(node_table_t *table, bit_t b1, bit_t b2);
300
301	// Variant implementations: simplify more
302	extern bit_t bit_or2simplify(node_table_t *table, bit_t b1, bit_t b2);
303	extern bit_t bit_xor2simplify(node_table_t *table, bit_t b1, bit_t b2);
304
305
306	/*
307	* Derived operations:
308	* (and b1 b2) = ~(or ~b1 ~b2)
309	* (eq b1 b2) = ~(xor b1 b2)
310	*/
311	static inline bit_t bit_and2(node_table_t *table, bit_t b1, bit_t b2) {
312	return bit_not(bit_or2(table, bit_not(b1), bit_not(b2)));
313	}
314
315	static inline bit_t bit_eq2(node_table_t *table, bit_t b1, bit_t b2) {
316	return bit_not(bit_xor2(table, b1, b2));
317	}
318
319	static inline bit_t bit_and2simplify(node_table_t *table, bit_t b1, bit_t b2) {	146,599✔
320	return bit_not(bit_or2simplify(table, bit_not(b1), bit_not(b2)));	146,599✔
321	}
322
323	static inline bit_t bit_eq2simplify(node_table_t *table, bit_t b1, bit_t b2) {	3,664✔
324	return bit_not(bit_xor2simplify(table, b1, b2));	3,664✔
325	}
326
327
328
329	/*
330	* N-ary constructors
331	* (bit_or b[0] ... b[n-1])
332	* (bit_and b[0] ... b[n-1])
333	* (bit_xor b[0] ... b[n-1])
334	*/
335	extern bit_t bit_or(node_table_t table, bit_t b, uint32_t n);
336	extern bit_t bit_and(node_table_t table, bit_t b, uint32_t n);
337	extern bit_t bit_xor(node_table_t table, bit_t b, uint32_t n);
338
339
340
341
342
343	/*
344	* GARBAGE COLLECTION
345	*/
346	// increment the reference counter
347	static inline void node_table_incref(node_table_t *table) {	354,383✔
348	table->ref_counter ++;	354,383✔
349	}	354,383✔
350
351	// decrement the reference counter
352	// if it becomes zero, empty the table.
353	extern void node_table_decref(node_table_t *table);
354
355
356	// force the reference counter to zero: use this before an explicit call to reset
357	static inline void node_table_clear_refcount(node_table_t *table) {
358	table->ref_counter = 0;
359	}
360
361
362
363
364	/*
365	* ACCESS TO THE TABLE
366	*/
367	static inline bool valid_node(node_table_t *table, node_t x) {
368	return 0 <= x && x < node_table_nelems(table);
369	}
370
371	static inline node_desc_t node_table_elem(node_table_t table, node_t x) {	32,436,582✔
372	return indexed_table_elem(node_desc_t, &table->nodes, x);	32,436,582✔
373	}
374
375	static inline node_kind_t node_kind(node_table_t *table, node_t x) {	4,518,163✔
376	assert(valid_node(table, x));
377	return node_table_elem(table, x)->kind;	4,518,163✔
378	}
379
380	static inline bool good_node(node_table_t *table, node_t x) {
381	return valid_node(table, x) && node_kind(table, x) != UNUSED_NODE;
382	}
383
384	static inline bool is_constant_node(node_table_t *table, node_t x) {
385	return node_kind(table, x) == CONSTANT_NODE;
386	}
387
388	static inline bool is_variable_node(node_table_t *table, node_t x) {
389	return node_kind(table, x) == VARIABLE_NODE;
390	}
391
392	static inline bool is_select_node(node_table_t *table, node_t x) {	2,258,467✔
393	return node_kind(table, x) == SELECT_NODE;	2,258,467✔
394	}
395
396	static inline bool is_or_node(node_table_t *table, node_t x) {
397	return node_kind(table, x) == OR_NODE;
398	}
399
400	static inline bool is_xor_node(node_table_t *table, node_t x) {
401	return node_kind(table, x) == XOR_NODE;
402	}
403
404	static inline bool is_leaf_node(node_table_t *table, node_t x) {
405	node_kind_t k;
406	k = node_kind(table, x);
407	return k == CONSTANT_NODE \|\| k == VARIABLE_NODE \|\| k == SELECT_NODE;
408	}
409
410	static inline bool is_nonleaf_node(node_table_t *table, node_t x) {	209,650✔
411	node_kind_t k;
412	k = node_kind(table, x);	209,650✔
413	return k == OR_NODE \|\| k == XOR_NODE;	209,650✔
414	}
415
416
417
418	/*
419	* Get or set map[x] for a node x
420	* - the default value for map[x] is -1.
421	*/
422	static inline int32_t map_of_node(node_table_t *table, node_t x) {	8,153,887✔
423	assert(good_node(table, x));
424	return node_table_elem(table, x)->map;	8,153,887✔
425	}
426
427	static inline void set_map_of_node(node_table_t *table, node_t x, int32_t v) {	3,620,166✔
428	assert(good_node(table, x));
429	node_table_elem(table, x)->map = v;	3,620,166✔
430	}	3,620,166✔
431
432
433
434	/*
435	* Variable of a variable node x
436	*/
437	static inline int32_t var_of_node(node_table_t *table, node_t x) {	×
438	assert(is_variable_node(table, x));
439	return node_table_elem(table, x)->var;	×
440	}
441
442
443	/*
444	* Variable and index of a select node x
445	*/
446	static inline select_node_t select_of_node(node_table_t table, node_t x) {	8,118,039✔
447	assert(is_select_node(table, x));
448	return &node_table_elem(table, x)->sel;	8,118,039✔
449	}
450
451	static inline int32_t var_of_select_node(node_table_t *table, node_t x) {	4,016,473✔
452	return select_of_node(table, x)->var;	4,016,473✔
453	}
454
455	static inline uint32_t index_of_select_node(node_table_t *table, node_t x) {	4,101,566✔
456	return select_of_node(table, x)->index;	4,101,566✔
457	}
458
459
460
461	/*
462	* Children of node x = array of 2 bits
463	* - x must be a non-leaf node
464	*/
465	static inline bit_t children_of_node(node_table_t table, node_t x) {	161,892✔
466	assert(is_nonleaf_node(table, x));
467	return node_table_elem(table, x)->c;	161,892✔
468	}
469
470	// child 0 or 1
471	static inline bit_t child_of_node(node_table_t *table, node_t x, uint32_t k) {	101,862✔
472	assert(k < 2);
473	return children_of_node(table, x)[k];	101,862✔
474	}
475
476	// left child = child 0, right child = child 1
477	static inline bit_t left_child_of_node(node_table_t *table, node_t x) {	50,931✔
478	return child_of_node(table, x, 0);	50,931✔
479	}
480
481	static inline bit_t right_child_of_node(node_table_t *table, node_t x) {	50,931✔
482	return child_of_node(table, x, 1);	50,931✔
483	}
484
485
486	/*
487	* Check whether bit-expression b is a constant
488	*/
489	static inline bool bit_is_const(bit_t b) {	3,010,553✔
490	return node_of_bit(b) == constant_node;	3,010,553✔
491	}
492
493
494	#endif /* __BIT_EXPR_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