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.35

/src/solvers/cdcl/gates_hash_table.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/>.
 */

/*
 * HASH TABLE FOR BOOLEAN GATES
 */

/*
 * This provides support for encoding and hash-consing boolean combinators
 * (xor, or, and, iff, ite, etc.)
 * - Inputs and outputs of a gate are literals.
 * - Combinators may have several outputs (e.g., a single-bit adder)
 * - Push and pop operations are supported
 */

#ifndef __GATES_HASH_TABLE_H
#define __GATES_HASH_TABLE_H

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

#include "solvers/cdcl/smt_core_base_types.h"


/*
 * Logical gates and building blocks for bit-vector arithmetic
 * -----------------------------------------------------------
 *
 * XOR(a_1, ..., a_n)(b)  b = (xor a_1 ... a_n)
 *
 *  OR(a_1, ..., a_n)(b)  b = (or a_1 ... a_n)
 *
 * ITE(c, a1, a2)(b)      b = (ite c a1 a2)
 *
 *
 * Building block for comparators:
 *
 * CMP(a1, a2, c)(b)     b = ((a1 > a2) or (a_1 == a2 and c))
 *
 * Adders:
 *
 * HALFADD(a1, a2)(s, c)      s = (xor a1 a2)
 *                            c = (a1 and a2)
 *
 * FULLADD(a1, a2, c)(s, d)   s = (xor a1 a2 c)
 *                            d = (or (and a1 a2) (and a1 c) (and a2 c))
 *
 */
typedef enum gate_op {
  XOR_GATE,
  OR_GATE,
  ITE_GATE,
  CMP_GATE,
  HALFADD_GATE,
  FULLADD_GATE,
} gate_op_t;

#define GTAG_NUM_OPS (FULLADD_GATE + 1)



/*
 * Gate descriptor:
 * - 32bit tag encodes operator + indegree + outdegree
 * - if indegree is k and outdegree is j, then
 *      lit[0 ... k-1] are the input literals
 *      lit[k ... k+j-1] are the output literals
 * - each descriptor also includes a hash code = hash of tag + input literals
 */


/*
 * Tag structure
 * - 8 bits for the operator (bits 24 to 31)
 * - 8 bits for outdegree (bits 16 to 23)
 * - 16 bits for indegree (bits 0 to 15)
 */
#define GTAG_OPCODE_BITS 8
#define GTAG_ODEG_BITS   8
#define GTAG_IDEG_BITS   16

#define MAX_OPCODE     ((1<<GTAG_OPCODE_BITS)-1)
#define MAX_OUTDEGREE  ((uint32_t)((1<<GTAG_ODEG_BITS)-1))
#define MAX_INDEGREE   ((uint32_t)((1<<GTAG_IDEG_BITS)-1))

#define GTAG_GATE_SHIFT (GTAG_IDEG_BITS+GTAG_ODEG_BITS)
#define GTAG_ODEG_SHIFT GTAG_IDEG_BITS

#define GTAG_ODEG_MASK  MAX_OUTDEGREE
#define GTAG_IDEG_MASK  MAX_INDEGREE


static inline gate_op_t tag_combinator(uint32_t tag) {
  return (gate_op_t) (tag >> GTAG_GATE_SHIFT);
}

static inline uint32_t tag_outdegree(uint32_t tag) {
  return (tag >> GTAG_ODEG_SHIFT) & GTAG_ODEG_MASK;
}

static inline uint32_t tag_indegree(uint32_t tag) {
  return tag & GTAG_IDEG_MASK;
}

// clang gives warning for op <= MAX_OPCODE: coerced op to int to fix that
static inline uint32_t mk_gate_tag(gate_op_t op, uint32_t in_deg, uint32_t out_deg) {
  assert((int) op <= MAX_OPCODE && in_deg <= MAX_INDEGREE && out_deg <= MAX_OUTDEGREE);
  return (((uint32_t)op) << GTAG_GATE_SHIFT) | (out_deg << GTAG_ODEG_SHIFT) | in_deg;
}

static inline uint32_t orgate_tag(uint32_t in_deg) {
  return mk_gate_tag(OR_GATE, in_deg, 1);
}

static inline uint32_t xorgate_tag(uint32_t in_deg) {
  return mk_gate_tag(XOR_GATE, in_deg, 1);
}

static inline uint32_t itegate_tag(void) {
  return mk_gate_tag(ITE_GATE, 3, 1);
}

static inline uint32_t cmpgate_tag(void) {
  return mk_gate_tag(CMP_GATE, 3, 1);
}

static inline uint32_t halfaddgate_tag(void) {
  return mk_gate_tag(HALFADD_GATE, 2, 2);
}

static inline uint32_t fulladdgate_tag(void) {
  return mk_gate_tag(FULLADD_GATE, 3, 2);
}



/*
 * Descriptor of a boolean gate
 */
typedef struct boolgate_s {
  uint32_t hash;
  uint32_t tag;
  literal_t lit[0]; // real size depends on tag
} boolgate_t;


/*
 * List of boolean gates (for pop operation)
 */
typedef struct lnkgate_s lnkgate_t;

struct lnkgate_s {
  lnkgate_t *next;
  boolgate_t gate;
};



/*
 * Stack of lists for push/pop
 * - objects created at level k>0 are stored in a linked list
 * - on exit from level k (pop operation), all elements
 *   created in that level must be removed.
 * - for push/pop, we maintain a stack of list descriptors;
 *   each descriptor is a pair <level, list> (i.e., the list
 *   of objects created at that level).
 * - the descriptors are in data[0 ... nlists-1] with
 *      data[i].level < data[i+1].level
 *      data[i].list is not empty
 *      data[i].level <= current_level
 * - top_level is 0 if the stack is empty
 *   otherwise top_level = data[nlist-1].level
 * - nlist = the top of the list
 * - size = size of the data array
 */
typedef struct levlist_s {
  uint32_t level;
  lnkgate_t *list;
} levlist_t;

typedef struct levlist_stack_s {
  uint32_t current_level;
  uint32_t top_level;
  uint32_t nlists;
  uint32_t size;
  levlist_t *data;
} levlist_stack_t;


#define DEF_LEVLIST_STACK_SIZE 10
#define MAX_LEVLIST_STACK_SIZE (UINT32_MAX/sizeof(levlist_t))



/*
 * Hash table (similar to int_hash_table, etc.).
 */
typedef struct gate_htbl_s {
  boolgate_t **data;  // hash table proper
  uint32_t size;      // its size (power of 2)
  uint32_t nelems;    // number of elements
  uint32_t ndeleted;
  uint32_t resize_threshold;
  uint32_t cleanup_threshold;
} gate_htbl_t;


/*
 * Marker for deleted elements in data array
 * - data[i] = NULL if it's empty
 */
#define DELETED_GATE ((boolgate_t*) 1)

#define DEF_GATE_HTBL_SIZE 32
#define MAX_GATE_HTBL_SIZE (UINT32_MAX/sizeof(boolgate_t*))
#define GATE_HTBL_RESIZE_RATIO  0.6
#define GATE_HTBL_CLEANUP_RATIO 0.2




/*
 * Full hash_consing structure
 */
typedef struct gate_table_s {
  levlist_stack_t stack;
  gate_htbl_t htbl;
} gate_table_t;




/***********************
 *  CREATION/DELETION  *
 **********************/

/*
 * Initialize table: memory for stack and hash-table is not
 * allocated yet.
 */
extern void init_gate_table(gate_table_t *table);

/*
 * Delete all objects stored in the table and all allocated memory
 */
extern void delete_gate_table(gate_table_t *table);

/*
 * Empty the table and set current_level to 0
 */
extern void reset_gate_table(gate_table_t *table);

/*
 * Push
 */
static inline void gate_table_push(gate_table_t *table) {
  table->stack.current_level ++;
}

/*
 * Pop: delete all objects created at the current level
 * then decrement current_level. Should not be called at level 0.
 */
extern void gate_table_pop(gate_table_t *table);


/*
 * Set level: same effect as calling push n times
 */
static inline void gate_table_set_level(gate_table_t *table, uint32_t n) {
  assert(table->stack.current_level == 0);
  table->stack.current_level = n;
}



/***************************
 *  HASH-TABLE OPERATIONS  *
 **************************/

/*
 * Find a descriptor with the given tag and input literals
 * - the input literals are in a[0 ... n-1] where n = indegree(tag)
 * - return NULL if there's no matching record in the table
 */
extern boolgate_t *gate_table_find(gate_table_t *table, uint32_t tag, literal_t *a);

/*
 * Find or create a descriptor with the given tag/input literals
 * - if the descriptor is new, then its output are initialized to null_literal
 */
extern boolgate_t *gate_table_get(gate_table_t *table, uint32_t tag, literal_t *a);


/*
 * Find and get for (op a b) and (op a b c)
 */
extern boolgate_t *gate_table_find2(gate_table_t *table, uint32_t tag, literal_t a, literal_t b);
extern boolgate_t *gate_table_get2(gate_table_t *table, uint32_t tag, literal_t a, literal_t b);
extern boolgate_t *gate_table_find3(gate_table_t *table, uint32_t tag, literal_t a, literal_t b, literal_t c);
extern boolgate_t *gate_table_get3(gate_table_t *table, uint32_t tag, literal_t a, literal_t b, literal_t c);


/*
 * Short cuts: (or a[0] ... a[n-1]) and (xor a[0] ... a[n-1])
 */
static inline boolgate_t *gate_table_find_or(gate_table_t *table, uint32_t n, literal_t *a) {
  return gate_table_find(table, orgate_tag(n), a);
}
static inline boolgate_t *gate_table_find_xor(gate_table_t *table, uint32_t n, literal_t *a) {
  return gate_table_find(table, xorgate_tag(n), a);
}

static inline boolgate_t *gate_table_get_or(gate_table_t *table, uint32_t n, literal_t *a) {
  return gate_table_get(table, orgate_tag(n), a);
}
static inline boolgate_t *gate_table_get_xor(gate_table_t *table, uint32_t n, literal_t *a) {
  return gate_table_get(table, xorgate_tag(n), a);
}


/*
 * All binary and ternary gates
 */
static inline boolgate_t *gate_table_find_or2(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_find2(table, orgate_tag(2), a, b);
}

static inline boolgate_t *gate_table_find_xor2(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_find2(table, xorgate_tag(2), a, b);
}

static inline boolgate_t *gate_table_find_halfadd(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_find2(table, halfaddgate_tag(), a, b);
}

static inline boolgate_t *gate_table_find_or3(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_find3(table, orgate_tag(3), a, b, c);
}

static inline boolgate_t *gate_table_find_xor3(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_find3(table, xorgate_tag(3), a, b, c);
}

static inline boolgate_t *gate_table_find_ite(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_find3(table, itegate_tag(), a, b, c);
}

static inline boolgate_t *gate_table_find_cmp(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_find3(table, cmpgate_tag(), a, b, c);
}

static inline boolgate_t *gate_table_find_fulladd(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_find3(table, fulladdgate_tag(), a, b, c);
}



/*
 * All binary and ternary gates
 */
static inline boolgate_t *gate_table_get_or2(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_get2(table, orgate_tag(2), a, b);
}

static inline boolgate_t *gate_table_get_xor2(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_get2(table, xorgate_tag(2), a, b);
}

static inline boolgate_t *gate_table_get_halfadd(gate_table_t *table, literal_t a, literal_t b) {
  return gate_table_get2(table, halfaddgate_tag(), a, b);
}

static inline boolgate_t *gate_table_get_or3(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_get3(table, orgate_tag(3), a, b, c);
}

static inline boolgate_t *gate_table_get_xor3(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_get3(table, xorgate_tag(3), a, b, c);
}

static inline boolgate_t *gate_table_get_ite(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_get3(table, itegate_tag(), a, b, c);
}

static inline boolgate_t *gate_table_get_cmp(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_get3(table, cmpgate_tag(), a, b, c);
}

static inline boolgate_t *gate_table_get_fulladd(gate_table_t *table, literal_t a, literal_t b, literal_t c) {
  return gate_table_get3(table, fulladdgate_tag(), a, b, c);
}


/*
 * Support for scanning all the gates
 * - *index to scan from
 * - return the first gate found or NULL if there's no more gate
 * - update *index to the index that follows this gate
 *
 * To scan the table, use something like this:
 *
 *   uint32_t scan_index;
 *   boolgate_t *g;
 *
 *   scan_index = 0;
 *   g = gate_table_next(table, &scan_index);
 *   while (g != NULL) {
 *     ...
 *     g = gate_table_next(table, &scan_index);
 *   }
 */
extern boolgate_t *gate_table_next(const gate_table_t *table, uint32_t *index);


#endif /* __GATES_HASH_TABLE_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	* HASH TABLE FOR BOOLEAN GATES
21	*/
22
23	/*
24	* This provides support for encoding and hash-consing boolean combinators
25	* (xor, or, and, iff, ite, etc.)
26	* - Inputs and outputs of a gate are literals.
27	* - Combinators may have several outputs (e.g., a single-bit adder)
28	* - Push and pop operations are supported
29	*/
30
31	#ifndef __GATES_HASH_TABLE_H
32	#define __GATES_HASH_TABLE_H
33
34	#include <stdint.h>
35	#include <assert.h>
36
37	#include "solvers/cdcl/smt_core_base_types.h"
38
39
40	/*
41	* Logical gates and building blocks for bit-vector arithmetic
42	* -----------------------------------------------------------
43	*
44	* XOR(a_1, ..., a_n)(b) b = (xor a_1 ... a_n)
45	*
46	* OR(a_1, ..., a_n)(b) b = (or a_1 ... a_n)
47	*
48	* ITE(c, a1, a2)(b) b = (ite c a1 a2)
49	*
50	*
51	* Building block for comparators:
52	*
53	* CMP(a1, a2, c)(b) b = ((a1 > a2) or (a_1 == a2 and c))
54	*
55	* Adders:
56	*
57	* HALFADD(a1, a2)(s, c) s = (xor a1 a2)
58	* c = (a1 and a2)
59	*
60	* FULLADD(a1, a2, c)(s, d) s = (xor a1 a2 c)
61	* d = (or (and a1 a2) (and a1 c) (and a2 c))
62	*
63	*/
64	typedef enum gate_op {
65	XOR_GATE,
66	OR_GATE,
67	ITE_GATE,
68	CMP_GATE,
69	HALFADD_GATE,
70	FULLADD_GATE,
71	} gate_op_t;
72
73	#define GTAG_NUM_OPS (FULLADD_GATE + 1)
74
75
76
77	/*
78	* Gate descriptor:
79	* - 32bit tag encodes operator + indegree + outdegree
80	* - if indegree is k and outdegree is j, then
81	* lit[0 ... k-1] are the input literals
82	* lit[k ... k+j-1] are the output literals
83	* - each descriptor also includes a hash code = hash of tag + input literals
84	*/
85
86
87	/*
88	* Tag structure
89	* - 8 bits for the operator (bits 24 to 31)
90	* - 8 bits for outdegree (bits 16 to 23)
91	* - 16 bits for indegree (bits 0 to 15)
92	*/
93	#define GTAG_OPCODE_BITS 8
94	#define GTAG_ODEG_BITS 8
95	#define GTAG_IDEG_BITS 16
96
97	#define MAX_OPCODE ((1<<GTAG_OPCODE_BITS)-1)
98	#define MAX_OUTDEGREE ((uint32_t)((1<<GTAG_ODEG_BITS)-1))
99	#define MAX_INDEGREE ((uint32_t)((1<<GTAG_IDEG_BITS)-1))
100
101	#define GTAG_GATE_SHIFT (GTAG_IDEG_BITS+GTAG_ODEG_BITS)
102	#define GTAG_ODEG_SHIFT GTAG_IDEG_BITS
103
104	#define GTAG_ODEG_MASK MAX_OUTDEGREE
105	#define GTAG_IDEG_MASK MAX_INDEGREE
106
107
108	static inline gate_op_t tag_combinator(uint32_t tag) {	×
109	return (gate_op_t) (tag >> GTAG_GATE_SHIFT);	×
110	}
111
112	static inline uint32_t tag_outdegree(uint32_t tag) {	2,925,890✔
113	return (tag >> GTAG_ODEG_SHIFT) & GTAG_ODEG_MASK;	2,925,890✔
114	}
115
116	static inline uint32_t tag_indegree(uint32_t tag) {	7,442,514✔
117	return tag & GTAG_IDEG_MASK;	7,442,514✔
118	}
119
120	// clang gives warning for op <= MAX_OPCODE: coerced op to int to fix that
121	static inline uint32_t mk_gate_tag(gate_op_t op, uint32_t in_deg, uint32_t out_deg) {	4,429,051✔
122	assert((int) op <= MAX_OPCODE && in_deg <= MAX_INDEGREE && out_deg <= MAX_OUTDEGREE);
123	return (((uint32_t)op) << GTAG_GATE_SHIFT) \| (out_deg << GTAG_ODEG_SHIFT) \| in_deg;	4,429,051✔
124	}
125
126	static inline uint32_t orgate_tag(uint32_t in_deg) {	804,395✔
127	return mk_gate_tag(OR_GATE, in_deg, 1);	804,395✔
128	}
129
130	static inline uint32_t xorgate_tag(uint32_t in_deg) {	464,276✔
131	return mk_gate_tag(XOR_GATE, in_deg, 1);	464,276✔
132	}
133
134	static inline uint32_t itegate_tag(void) {	689,439✔
135	return mk_gate_tag(ITE_GATE, 3, 1);	689,439✔
136	}
137
138	static inline uint32_t cmpgate_tag(void) {	729,278✔
139	return mk_gate_tag(CMP_GATE, 3, 1);	729,278✔
140	}
141
142	static inline uint32_t halfaddgate_tag(void) {	122,644✔
143	return mk_gate_tag(HALFADD_GATE, 2, 2);	122,644✔
144	}
145
146	static inline uint32_t fulladdgate_tag(void) {	1,619,019✔
147	return mk_gate_tag(FULLADD_GATE, 3, 2);	1,619,019✔
148	}
149
150
151
152	/*
153	* Descriptor of a boolean gate
154	*/
155	typedef struct boolgate_s {
156	uint32_t hash;
157	uint32_t tag;
158	literal_t lit[0]; // real size depends on tag
159	} boolgate_t;
160
161
162	/*
163	* List of boolean gates (for pop operation)
164	*/
165	typedef struct lnkgate_s lnkgate_t;
166
167	struct lnkgate_s {
168	lnkgate_t *next;
169	boolgate_t gate;
170	};
171
172
173
174	/*
175	* Stack of lists for push/pop
176	* - objects created at level k>0 are stored in a linked list
177	* - on exit from level k (pop operation), all elements
178	* created in that level must be removed.
179	* - for push/pop, we maintain a stack of list descriptors;
180	* each descriptor is a pair <level, list> (i.e., the list
181	* of objects created at that level).
182	* - the descriptors are in data[0 ... nlists-1] with
183	* data[i].level < data[i+1].level
184	* data[i].list is not empty
185	* data[i].level <= current_level
186	* - top_level is 0 if the stack is empty
187	* otherwise top_level = data[nlist-1].level
188	* - nlist = the top of the list
189	* - size = size of the data array
190	*/
191	typedef struct levlist_s {
192	uint32_t level;
193	lnkgate_t *list;
194	} levlist_t;
195
196	typedef struct levlist_stack_s {
197	uint32_t current_level;
198	uint32_t top_level;
199	uint32_t nlists;
200	uint32_t size;
201	levlist_t *data;
202	} levlist_stack_t;
203
204
205	#define DEF_LEVLIST_STACK_SIZE 10
206	#define MAX_LEVLIST_STACK_SIZE (UINT32_MAX/sizeof(levlist_t))
207
208
209
210	/*
211	* Hash table (similar to int_hash_table, etc.).
212	*/
213	typedef struct gate_htbl_s {
214	boolgate_t **data; // hash table proper
215	uint32_t size; // its size (power of 2)
216	uint32_t nelems; // number of elements
217	uint32_t ndeleted;
218	uint32_t resize_threshold;
219	uint32_t cleanup_threshold;
220	} gate_htbl_t;
221
222
223	/*
224	* Marker for deleted elements in data array
225	* - data[i] = NULL if it's empty
226	*/
227	#define DELETED_GATE ((boolgate_t*) 1)
228
229	#define DEF_GATE_HTBL_SIZE 32
230	#define MAX_GATE_HTBL_SIZE (UINT32_MAX/sizeof(boolgate_t*))
231	#define GATE_HTBL_RESIZE_RATIO 0.6
232	#define GATE_HTBL_CLEANUP_RATIO 0.2
233
234
235
236
237	/*
238	* Full hash_consing structure
239	*/
240	typedef struct gate_table_s {
241	levlist_stack_t stack;
242	gate_htbl_t htbl;
243	} gate_table_t;
244
245
246
247
248	/***********************
249	* CREATION/DELETION *
250	**********************/
251
252	/*
253	* Initialize table: memory for stack and hash-table is not
254	* allocated yet.
255	*/
256	extern void init_gate_table(gate_table_t *table);
257
258	/*
259	* Delete all objects stored in the table and all allocated memory
260	*/
261	extern void delete_gate_table(gate_table_t *table);
262
263	/*
264	* Empty the table and set current_level to 0
265	*/
266	extern void reset_gate_table(gate_table_t *table);
267
268	/*
269	* Push
270	*/
271	static inline void gate_table_push(gate_table_t *table) {	8,478✔
272	table->stack.current_level ++;	8,478✔
273	}	8,478✔
274
275	/*
276	* Pop: delete all objects created at the current level
277	* then decrement current_level. Should not be called at level 0.
278	*/
279	extern void gate_table_pop(gate_table_t *table);
280
281
282	/*
283	* Set level: same effect as calling push n times
284	*/
285	static inline void gate_table_set_level(gate_table_t *table, uint32_t n) {
286	assert(table->stack.current_level == 0);
287	table->stack.current_level = n;
288	}
289
290
291
292	/***************************
293	* HASH-TABLE OPERATIONS *
294	**************************/
295
296	/*
297	* Find a descriptor with the given tag and input literals
298	* - the input literals are in a[0 ... n-1] where n = indegree(tag)
299	* - return NULL if there's no matching record in the table
300	*/
301	extern boolgate_t gate_table_find(gate_table_t table, uint32_t tag, literal_t *a);
302
303	/*
304	* Find or create a descriptor with the given tag/input literals
305	* - if the descriptor is new, then its output are initialized to null_literal
306	*/
307	extern boolgate_t gate_table_get(gate_table_t table, uint32_t tag, literal_t *a);
308
309
310	/*
311	* Find and get for (op a b) and (op a b c)
312	*/
313	extern boolgate_t gate_table_find2(gate_table_t table, uint32_t tag, literal_t a, literal_t b);
314	extern boolgate_t gate_table_get2(gate_table_t table, uint32_t tag, literal_t a, literal_t b);
315	extern boolgate_t gate_table_find3(gate_table_t table, uint32_t tag, literal_t a, literal_t b, literal_t c);
316	extern boolgate_t gate_table_get3(gate_table_t table, uint32_t tag, literal_t a, literal_t b, literal_t c);
317
318
319	/*
320	* Short cuts: (or a[0] ... a[n-1]) and (xor a[0] ... a[n-1])
321	*/
322	static inline boolgate_t gate_table_find_or(gate_table_t table, uint32_t n, literal_t *a) {
323	return gate_table_find(table, orgate_tag(n), a);
324	}
325	static inline boolgate_t gate_table_find_xor(gate_table_t table, uint32_t n, literal_t *a) {
326	return gate_table_find(table, xorgate_tag(n), a);
327	}
328
329	static inline boolgate_t gate_table_get_or(gate_table_t table, uint32_t n, literal_t *a) {	2,148✔
330	return gate_table_get(table, orgate_tag(n), a);	2,148✔
331	}
332	static inline boolgate_t gate_table_get_xor(gate_table_t table, uint32_t n, literal_t *a) {	222,195✔
333	return gate_table_get(table, xorgate_tag(n), a);	222,195✔
334	}
335
336
337	/*
338	* All binary and ternary gates
339	*/
340	static inline boolgate_t gate_table_find_or2(gate_table_t table, literal_t a, literal_t b) {
341	return gate_table_find2(table, orgate_tag(2), a, b);
342	}
343
344	static inline boolgate_t gate_table_find_xor2(gate_table_t table, literal_t a, literal_t b) {	230,773✔
345	return gate_table_find2(table, xorgate_tag(2), a, b);	230,773✔
346	}
347
348	static inline boolgate_t gate_table_find_halfadd(gate_table_t table, literal_t a, literal_t b) {	61,711✔
349	return gate_table_find2(table, halfaddgate_tag(), a, b);	61,711✔
350	}
351
352	static inline boolgate_t gate_table_find_or3(gate_table_t table, literal_t a, literal_t b, literal_t c) {
353	return gate_table_find3(table, orgate_tag(3), a, b, c);
354	}
355
356	static inline boolgate_t gate_table_find_xor3(gate_table_t table, literal_t a, literal_t b, literal_t c) {
357	return gate_table_find3(table, xorgate_tag(3), a, b, c);
358	}
359
360	static inline boolgate_t gate_table_find_ite(gate_table_t table, literal_t a, literal_t b, literal_t c) {	325,772✔
361	return gate_table_find3(table, itegate_tag(), a, b, c);	325,772✔
362	}
363
364	static inline boolgate_t gate_table_find_cmp(gate_table_t table, literal_t a, literal_t b, literal_t c) {
365	return gate_table_find3(table, cmpgate_tag(), a, b, c);
366	}
367
368	static inline boolgate_t gate_table_find_fulladd(gate_table_t table, literal_t a, literal_t b, literal_t c) {
369	return gate_table_find3(table, fulladdgate_tag(), a, b, c);
370	}
371
372
373
374	/*
375	* All binary and ternary gates
376	*/
377	static inline boolgate_t gate_table_get_or2(gate_table_t table, literal_t a, literal_t b) {	636,745✔
378	return gate_table_get2(table, orgate_tag(2), a, b);	636,745✔
379	}
380
381	static inline boolgate_t gate_table_get_xor2(gate_table_t table, literal_t a, literal_t b) {	3,170✔
382	return gate_table_get2(table, xorgate_tag(2), a, b);	3,170✔
383	}
384
385	static inline boolgate_t gate_table_get_halfadd(gate_table_t table, literal_t a, literal_t b) {	60,933✔
386	return gate_table_get2(table, halfaddgate_tag(), a, b);	60,933✔
387	}
388
389	static inline boolgate_t gate_table_get_or3(gate_table_t table, literal_t a, literal_t b, literal_t c) {
390	return gate_table_get3(table, orgate_tag(3), a, b, c);
391	}
392
393	static inline boolgate_t gate_table_get_xor3(gate_table_t table, literal_t a, literal_t b, literal_t c) {
394	return gate_table_get3(table, xorgate_tag(3), a, b, c);
395	}
396
397	static inline boolgate_t gate_table_get_ite(gate_table_t table, literal_t a, literal_t b, literal_t c) {	323,669✔
398	return gate_table_get3(table, itegate_tag(), a, b, c);	323,669✔
399	}
400
401	static inline boolgate_t gate_table_get_cmp(gate_table_t table, literal_t a, literal_t b, literal_t c) {	729,278✔
402	return gate_table_get3(table, cmpgate_tag(), a, b, c);	729,278✔
403	}
404
405	static inline boolgate_t gate_table_get_fulladd(gate_table_t table, literal_t a, literal_t b, literal_t c) {
406	return gate_table_get3(table, fulladdgate_tag(), a, b, c);
407	}
408
409
410	/*
411	* Support for scanning all the gates
412	* - *index to scan from
413	* - return the first gate found or NULL if there's no more gate
414	* - update *index to the index that follows this gate
415	*
416	* To scan the table, use something like this:
417	*
418	* uint32_t scan_index;
419	* boolgate_t *g;
420	*
421	* scan_index = 0;
422	* g = gate_table_next(table, &scan_index);
423	* while (g != NULL) {
424	* ...
425	* g = gate_table_next(table, &scan_index);
426	* }
427	*/
428	extern boolgate_t gate_table_next(const gate_table_t table, uint32_t *index);
429
430
431	#endif /* __GATES_HASH_TABLE_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