Context Navigation

← Previous Revision
Latest Revision
Next Revision →
Blame
Revision Log

cuddEssent.c @ 100

Last change on this file since 100 was 13, checked in by cecile, 13 years ago
library glu 2.3
File size: 43.6 KB

Line
1	/CFile*********************************************************************
2
3	FileName [cuddEssent.c]
4
5	PackageName [cudd]
6
7	Synopsis [Functions for the detection of essential variables.]
8
9	Description [External procedures included in this file:
10	<ul>
11	<li> Cudd_FindEssential()
12	<li> Cudd_bddIsVarEssential()
13	<li> Cudd_FindTwoLiteralClauses()
14	<li> Cudd_ReadIthClause()
15	<li> Cudd_PrintTwoLiteralClauses()
16	<li> Cudd_tlcInfoFree()
17	</ul>
18	Static procedures included in this module:
19	<ul>
20	<li> ddFindEssentialRecur()
21	<li> ddFindTwoLiteralClausesRecur()
22	<li> computeClauses()
23	<li> computeClausesWithUniverse()
24	<li> emptyClauseSet()
25	<li> sentinelp()
26	<li> equalp()
27	<li> beforep()
28	<li> oneliteralp()
29	<li> impliedp()
30	<li> bitVectorAlloc()
31	<li> bitVectorClear()
32	<li> bitVectorFree()
33	<li> bitVectorRead()
34	<li> bitVectorSet()
35	<li> tlcInfoAlloc()
36	</ul>]
37
38	Author [Fabio Somenzi]
39
40	Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
41
42	All rights reserved.
43
44	Redistribution and use in source and binary forms, with or without
45	modification, are permitted provided that the following conditions
46	are met:
47
48	Redistributions of source code must retain the above copyright
49	notice, this list of conditions and the following disclaimer.
50
51	Redistributions in binary form must reproduce the above copyright
52	notice, this list of conditions and the following disclaimer in the
53	documentation and/or other materials provided with the distribution.
54
55	Neither the name of the University of Colorado nor the names of its
56	contributors may be used to endorse or promote products derived from
57	this software without specific prior written permission.
58
59	THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
60	"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
61	LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
62	FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
63	COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
64	INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
65	BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
66	LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
67	CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
68	LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
69	ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
70	POSSIBILITY OF SUCH DAMAGE.]
71
72	******************************************************************************/
73
74	#include "util.h"
75	#include "cuddInt.h"
76
77	/---------------------------------------------------------------------------/
78	/* Constant declarations */
79	/---------------------------------------------------------------------------/
80
81	/* These definitions are for the bit vectors. */
82	#if SIZEOF_LONG == 8
83	#define BPL 64
84	#define LOGBPL 6
85	#else
86	#define BPL 32
87	#define LOGBPL 5
88	#endif
89
90	/---------------------------------------------------------------------------/
91	/* Stucture declarations */
92	/---------------------------------------------------------------------------/
93
94	/* This structure holds the set of clauses for a node. Each clause consists
95	** of two literals. For one-literal clauses, the second lietral is FALSE.
96	** Each literal is composed of a variable and a phase. A variable is a node
97	** index, and requires sizeof(DdHalfWord) bytes. The constant literals use
98	** CUDD_MAXINDEX as variable indicator. Each phase is a bit: 0 for positive
99	** phase, and 1 for negative phase.
100	** Variables and phases are stored separately for the sake of compactness.
101	** The variables are stored in an array of DdHalfWord's terminated by a
102	** sentinel (a pair of zeroes). The phases are stored in a bit vector.
103	** The cnt field holds, at the end, the number of clauses.
104	** The clauses of the set are kept sorted. For each clause, the first literal
105	** is the one of least index. So, the clause with literals +2 and -4 is stored
106	** as (+2,-4). A one-literal clause with literal +3 is stored as
107	** (+3,-CUDD_MAXINDEX). Clauses are sorted in decreasing order as follows:
108	** (+5,-7)
109	** (+5,+6)
110	** (-5,+7)
111	** (-4,FALSE)
112	** (-4,+8)
113	** ...
114	** That is, one first looks at the variable of the first literal, then at the
115	** phase of the first litral, then at the variable of the second literal,
116	** and finally at the phase of the second literal.
117	*/
118	struct DdTlcInfo {
119	DdHalfWord *vars;
120	long *phases;
121	DdHalfWord cnt;
122	};
123
124	/* This structure is for temporary representation of sets of clauses. It is
125	** meant to be used in link lists, when the number of clauses is not yet
126	** known. The encoding of a clause is the same as in DdTlcInfo, though
127	** the phase information is not stored in a bit array. */
128	struct TlClause {
129	DdHalfWord v1, v2;
130	short p1, p2;
131	struct TlClause *next;
132	};
133
134	/---------------------------------------------------------------------------/
135	/* Type declarations */
136	/---------------------------------------------------------------------------/
137
138	typedef long BitVector;
139	typedef struct TlClause TlClause;
140
141	/---------------------------------------------------------------------------/
142	/* Variable declarations */
143	/---------------------------------------------------------------------------/
144
145	#ifndef lint
146	static char rcsid[] DD_UNUSED = "$Id: cuddEssent.c,v 1.24 2009/02/21 18:24:10 fabio Exp $";
147	#endif
148
149	static BitVector *Tolv;
150	static BitVector *Tolp;
151	static BitVector *Eolv;
152	static BitVector *Eolp;
153
154	/---------------------------------------------------------------------------/
155	/* Macro declarations */
156	/---------------------------------------------------------------------------/
157
158	/AutomaticStart***********************************************************/
159
160	/---------------------------------------------------------------------------/
161	/* Static function prototypes */
162	/---------------------------------------------------------------------------/
163
164	static DdNode * ddFindEssentialRecur (DdManager dd, DdNode f);
165	static DdTlcInfo * ddFindTwoLiteralClausesRecur (DdManager * dd, DdNode * f, st_table *table);
166	static DdTlcInfo * computeClauses (DdTlcInfo Tres, DdTlcInfo Eres, DdHalfWord label, int size);
167	static DdTlcInfo * computeClausesWithUniverse (DdTlcInfo *Cres, DdHalfWord label, short phase);
168	static DdTlcInfo * emptyClauseSet (void);
169	static int sentinelp (DdHalfWord var1, DdHalfWord var2);
170	static int equalp (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
171	static int beforep (DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b);
172	static int oneliteralp (DdHalfWord var);
173	static int impliedp (DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector olv, BitVector olp);
174	static BitVector * bitVectorAlloc (int size);
175	DD_INLINE static void bitVectorClear (BitVector *vector, int size);
176	static void bitVectorFree (BitVector *vector);
177	DD_INLINE static short bitVectorRead (BitVector *vector, int i);
178	DD_INLINE static void bitVectorSet (BitVector * vector, int i, short val);
179	static DdTlcInfo * tlcInfoAlloc (void);
180
181	/AutomaticEnd*************************************************************/
182
183
184	/---------------------------------------------------------------------------/
185	/* Definition of exported functions */
186	/---------------------------------------------------------------------------/
187
188
189	/Function******************************************************************
190
191	Synopsis [Finds the essential variables of a DD.]
192
193	Description [Returns the cube of the essential variables. A positive
194	literal means that the variable must be set to 1 for the function to be
195	1. A negative literal means that the variable must be set to 0 for the
196	function to be 1. Returns a pointer to the cube BDD if successful;
197	NULL otherwise.]
198
199	SideEffects [None]
200
201	SeeAlso [Cudd_bddIsVarEssential]
202
203	******************************************************************************/
204	DdNode *
205	Cudd_FindEssential(
206	DdManager * dd,
207	DdNode * f)
208	{
209	DdNode *res;
210
211	do {
212	dd->reordered = 0;
213	res = ddFindEssentialRecur(dd,f);
214	} while (dd->reordered == 1);
215	return(res);
216
217	} /* end of Cudd_FindEssential */
218
219
220	/Function******************************************************************
221
222	Synopsis [Determines whether a given variable is essential with a
223	given phase in a BDD.]
224
225	Description [Determines whether a given variable is essential with a
226	given phase in a BDD. Uses Cudd_bddIteConstant. Returns 1 if phase == 1
227	and f-->x_id, or if phase == 0 and f-->x_id'.]
228
229	SideEffects [None]
230
231	SeeAlso [Cudd_FindEssential]
232
233	******************************************************************************/
234	int
235	Cudd_bddIsVarEssential(
236	DdManager * manager,
237	DdNode * f,
238	int id,
239	int phase)
240	{
241	DdNode *var;
242	int res;
243
244	var = Cudd_bddIthVar(manager, id);
245
246	var = Cudd_NotCond(var,phase == 0);
247
248	res = Cudd_bddLeq(manager, f, var);
249
250	return(res);
251
252	} /* end of Cudd_bddIsVarEssential */
253
254
255	/Function******************************************************************
256
257	Synopsis [Finds the two literal clauses of a DD.]
258
259	Description [Returns the one- and two-literal clauses of a DD.
260	Returns a pointer to the structure holding the clauses if
261	successful; NULL otherwise. For a constant DD, the empty set of clauses
262	is returned. This is obviously correct for a non-zero constant. For the
263	constant zero, it is based on the assumption that only those clauses
264	containing variables in the support of the function are considered. Since
265	the support of a constant function is empty, no clauses are returned.]
266
267	SideEffects [None]
268
269	SeeAlso [Cudd_FindEssential]
270
271	******************************************************************************/
272	DdTlcInfo *
273	Cudd_FindTwoLiteralClauses(
274	DdManager * dd,
275	DdNode * f)
276	{
277	DdTlcInfo *res;
278	st_table *table;
279	st_generator *gen;
280	DdTlcInfo *tlc;
281	DdNode *node;
282	int size = dd->size;
283
284	if (Cudd_IsConstant(f)) {
285	res = emptyClauseSet();
286	return(res);
287	}
288	table = st_init_table(st_ptrcmp,st_ptrhash);
289	if (table == NULL) return(NULL);
290	Tolv = bitVectorAlloc(size);
291	if (Tolv == NULL) {
292	st_free_table(table);
293	return(NULL);
294	}
295	Tolp = bitVectorAlloc(size);
296	if (Tolp == NULL) {
297	st_free_table(table);
298	bitVectorFree(Tolv);
299	return(NULL);
300	}
301	Eolv = bitVectorAlloc(size);
302	if (Eolv == NULL) {
303	st_free_table(table);
304	bitVectorFree(Tolv);
305	bitVectorFree(Tolp);
306	return(NULL);
307	}
308	Eolp = bitVectorAlloc(size);
309	if (Eolp == NULL) {
310	st_free_table(table);
311	bitVectorFree(Tolv);
312	bitVectorFree(Tolp);
313	bitVectorFree(Eolv);
314	return(NULL);
315	}
316
317	res = ddFindTwoLiteralClausesRecur(dd,f,table);
318	/* Dispose of table contents and free table. */
319	st_foreach_item(table, gen, &node, &tlc) {
320	if (node != f) {
321	Cudd_tlcInfoFree(tlc);
322	}
323	}
324	st_free_table(table);
325	bitVectorFree(Tolv);
326	bitVectorFree(Tolp);
327	bitVectorFree(Eolv);
328	bitVectorFree(Eolp);
329
330	if (res != NULL) {
331	int i;
332	for (i = 0; !sentinelp(res->vars[i], res->vars[i+1]); i += 2);
333	res->cnt = i >> 1;
334	}
335
336	return(res);
337
338	} /* end of Cudd_FindTwoLiteralClauses */
339
340
341	/Function******************************************************************
342
343	Synopsis [Accesses the i-th clause of a DD.]
344
345	Description [Accesses the i-th clause of a DD given the clause set which
346	must be already computed. Returns 1 if successful; 0 if i is out of range,
347	or in case of error.]
348
349	SideEffects [the four components of a clause are returned as side effects.]
350
351	SeeAlso [Cudd_FindTwoLiteralClauses]
352
353	******************************************************************************/
354	int
355	Cudd_ReadIthClause(
356	DdTlcInfo * tlc,
357	int i,
358	DdHalfWord *var1,
359	DdHalfWord *var2,
360	int *phase1,
361	int *phase2)
362	{
363	if (tlc == NULL) return(0);
364	if (tlc->vars == NULL \|\| tlc->phases == NULL) return(0);
365	if (i < 0 \|\| (unsigned) i >= tlc->cnt) return(0);
366	var1 = tlc->vars[2i];
367	var2 = tlc->vars[2i+1];
368	phase1 = (int) bitVectorRead(tlc->phases, 2i);
369	phase2 = (int) bitVectorRead(tlc->phases, 2i+1);
370	return(1);
371
372	} /* end of Cudd_ReadIthClause */
373
374
375	/Function******************************************************************
376
377	Synopsis [Prints the two literal clauses of a DD.]
378
379	Description [Prints the one- and two-literal clauses. Returns 1 if
380	successful; 0 otherwise. The argument "names" can be NULL, in which case
381	the variable indices are printed.]
382
383	SideEffects [None]
384
385	SeeAlso [Cudd_FindTwoLiteralClauses]
386
387	******************************************************************************/
388	int
389	Cudd_PrintTwoLiteralClauses(
390	DdManager * dd,
391	DdNode * f,
392	char **names,
393	FILE *fp)
394	{
395	DdHalfWord *vars;
396	BitVector *phases;
397	int i;
398	DdTlcInfo *res = Cudd_FindTwoLiteralClauses(dd, f);
399	FILE *ifp = fp == NULL ? dd->out : fp;
400
401	if (res == NULL) return(0);
402	vars = res->vars;
403	phases = res->phases;
404	for (i = 0; !sentinelp(vars[i], vars[i+1]); i += 2) {
405	if (names != NULL) {
406	if (vars[i+1] == CUDD_MAXINDEX) {
407	(void) fprintf(ifp, "%s%s\n",
408	bitVectorRead(phases, i) ? "~" : " ",
409	names[vars[i]]);
410	} else {
411	(void) fprintf(ifp, "%s%s \| %s%s\n",
412	bitVectorRead(phases, i) ? "~" : " ",
413	names[vars[i]],
414	bitVectorRead(phases, i+1) ? "~" : " ",
415	names[vars[i+1]]);
416	}
417	} else {
418	if (vars[i+1] == CUDD_MAXINDEX) {
419	(void) fprintf(ifp, "%s%d\n",
420	bitVectorRead(phases, i) ? "~" : " ",
421	(int) vars[i]);
422	} else {
423	(void) fprintf(ifp, "%s%d \| %s%d\n",
424	bitVectorRead(phases, i) ? "~" : " ",
425	(int) vars[i],
426	bitVectorRead(phases, i+1) ? "~" : " ",
427	(int) vars[i+1]);
428	}
429	}
430	}
431	Cudd_tlcInfoFree(res);
432
433	return(1);
434
435	} /* end of Cudd_PrintTwoLiteralClauses */
436
437
438	/Function******************************************************************
439
440	Synopsis [Frees a DdTlcInfo Structure.]
441
442	Description [Frees a DdTlcInfo Structure as well as the memory pointed
443	by it.]
444
445	SideEffects [None]
446
447	SeeAlso []
448
449	******************************************************************************/
450	void
451	Cudd_tlcInfoFree(
452	DdTlcInfo * t)
453	{
454	if (t->vars != NULL) FREE(t->vars);
455	if (t->phases != NULL) FREE(t->phases);
456	FREE(t);
457
458	} /* end of Cudd_tlcInfoFree */
459
460
461	/---------------------------------------------------------------------------/
462	/* Definition of internal functions */
463	/---------------------------------------------------------------------------/
464
465
466	/---------------------------------------------------------------------------/
467	/* Definition of static functions */
468	/---------------------------------------------------------------------------/
469
470
471	/Function******************************************************************
472
473	Synopsis [Implements the recursive step of Cudd_FindEssential.]
474
475	Description [Implements the recursive step of Cudd_FindEssential.
476	Returns a pointer to the cube BDD if successful; NULL otherwise.]
477
478	SideEffects [None]
479
480	******************************************************************************/
481	static DdNode *
482	ddFindEssentialRecur(
483	DdManager * dd,
484	DdNode * f)
485	{
486	DdNode T, E, *F;
487	DdNode essT, essE, *res;
488	int index;
489	DdNode one, lzero, *azero;
490
491	one = DD_ONE(dd);
492	F = Cudd_Regular(f);
493	/* If f is constant the set of essential variables is empty. */
494	if (cuddIsConstant(F)) return(one);
495
496	res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
497	if (res != NULL) {
498	return(res);
499	}
500
501	lzero = Cudd_Not(one);
502	azero = DD_ZERO(dd);
503	/* Find cofactors: here f is non-constant. */
504	T = cuddT(F);
505	E = cuddE(F);
506	if (Cudd_IsComplement(f)) {
507	T = Cudd_Not(T); E = Cudd_Not(E);
508	}
509
510	index = F->index;
511	if (Cudd_IsConstant(T) && T != lzero && T != azero) {
512	/* if E is zero, index is essential, otherwise there are no
513	** essentials, because index is not essential and no other variable
514	** can be, since setting index = 1 makes the function constant and
515	** different from 0.
516	*/
517	if (E == lzero \|\| E == azero) {
518	res = dd->vars[index];
519	} else {
520	res = one;
521	}
522	} else if (T == lzero \|\| T == azero) {
523	if (Cudd_IsConstant(E)) { /* E cannot be zero here */
524	res = Cudd_Not(dd->vars[index]);
525	} else { /* E == non-constant */
526	/* find essentials in the else branch */
527	essE = ddFindEssentialRecur(dd,E);
528	if (essE == NULL) {
529	return(NULL);
530	}
531	cuddRef(essE);
532
533	/* add index to the set with negative phase */
534	res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
535	if (res == NULL) {
536	Cudd_RecursiveDeref(dd,essE);
537	return(NULL);
538	}
539	res = Cudd_Not(res);
540	cuddDeref(essE);
541	}
542	} else { /* T == non-const */
543	if (E == lzero \|\| E == azero) {
544	/* find essentials in the then branch */
545	essT = ddFindEssentialRecur(dd,T);
546	if (essT == NULL) {
547	return(NULL);
548	}
549	cuddRef(essT);
550
551	/* add index to the set with positive phase */
552	/* use And because essT may be complemented */
553	res = cuddBddAndRecur(dd,dd->vars[index],essT);
554	if (res == NULL) {
555	Cudd_RecursiveDeref(dd,essT);
556	return(NULL);
557	}
558	cuddDeref(essT);
559	} else if (!Cudd_IsConstant(E)) {
560	/* if E is a non-zero constant there are no essentials
561	** because T is non-constant.
562	*/
563	essT = ddFindEssentialRecur(dd,T);
564	if (essT == NULL) {
565	return(NULL);
566	}
567	if (essT == one) {
568	res = one;
569	} else {
570	cuddRef(essT);
571	essE = ddFindEssentialRecur(dd,E);
572	if (essE == NULL) {
573	Cudd_RecursiveDeref(dd,essT);
574	return(NULL);
575	}
576	cuddRef(essE);
577
578	/* res = intersection(essT, essE) */
579	res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
580	if (res == NULL) {
581	Cudd_RecursiveDeref(dd,essT);
582	Cudd_RecursiveDeref(dd,essE);
583	return(NULL);
584	}
585	cuddRef(res);
586	Cudd_RecursiveDeref(dd,essT);
587	Cudd_RecursiveDeref(dd,essE);
588	cuddDeref(res);
589	}
590	} else { /* E is a non-zero constant */
591	res = one;
592	}
593	}
594
595	cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
596	return(res);
597
598	} /* end of ddFindEssentialRecur */
599
600
601	/Function******************************************************************
602
603	Synopsis [Implements the recursive step of Cudd_FindTwoLiteralClauses.]
604
605	Description [Implements the recursive step of
606	Cudd_FindTwoLiteralClauses. The DD node is assumed to be not
607	constant. Returns a pointer to a set of clauses if successful; NULL
608	otherwise.]
609
610	SideEffects [None]
611
612	SeeAlso [Cudd_FindTwoLiteralClauses]
613
614	******************************************************************************/
615	static DdTlcInfo *
616	ddFindTwoLiteralClausesRecur(
617	DdManager * dd,
618	DdNode * f,
619	st_table *table)
620	{
621	DdNode T, E, *F;
622	DdNode one, lzero, *azero;
623	DdTlcInfo res, Tres, *Eres;
624	DdHalfWord index;
625
626	F = Cudd_Regular(f);
627
628	assert(!cuddIsConstant(F));
629
630	/* Check computed table. Separate entries are necessary for
631	** a node and its complement. We should update the counter here. */
632	if (st_lookup(table, f, &res)) {
633	return(res);
634	}
635
636	/* Easy access to the constants for BDDs and ADDs. */
637	one = DD_ONE(dd);
638	lzero = Cudd_Not(one);
639	azero = DD_ZERO(dd);
640
641	/* Find cofactors and variable labeling the top node. */
642	T = cuddT(F); E = cuddE(F);
643	if (Cudd_IsComplement(f)) {
644	T = Cudd_Not(T); E = Cudd_Not(E);
645	}
646	index = F->index;
647
648	if (Cudd_IsConstant(T) && T != lzero && T != azero) {
649	/* T is a non-zero constant. If E is zero, then this node's index
650	** is a one-literal clause. Otherwise, if E is a non-zero
651	** constant, there are no clauses for this node. Finally,
652	** if E is not constant, we recursively compute its clauses, and then
653	** merge using the empty set for T. */
654	if (E == lzero \|\| E == azero) {
655	/* Create the clause (index + 0). */
656	res = tlcInfoAlloc();
657	if (res == NULL) return(NULL);
658	res->vars = ALLOC(DdHalfWord,4);
659	if (res->vars == NULL) {
660	FREE(res);
661	return(NULL);
662	}
663	res->phases = bitVectorAlloc(2);
664	if (res->phases == NULL) {
665	FREE(res->vars);
666	FREE(res);
667	return(NULL);
668	}
669	res->vars[0] = index;
670	res->vars[1] = CUDD_MAXINDEX;
671	res->vars[2] = 0;
672	res->vars[3] = 0;
673	bitVectorSet(res->phases, 0, 0); /* positive phase */
674	bitVectorSet(res->phases, 1, 1); /* negative phase */
675	} else if (Cudd_IsConstant(E)) {
676	/* If E is a non-zero constant, no clauses. */
677	res = emptyClauseSet();
678	} else {
679	/* E is non-constant */
680	Tres = emptyClauseSet();
681	if (Tres == NULL) return(NULL);
682	Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
683	if (Eres == NULL) {
684	Cudd_tlcInfoFree(Tres);
685	return(NULL);
686	}
687	res = computeClauses(Tres, Eres, index, dd->size);
688	Cudd_tlcInfoFree(Tres);
689	}
690	} else if (T == lzero \|\| T == azero) {
691	/* T is zero. If E is a non-zero constant, then the
692	** complement of this node's index is a one-literal clause.
693	** Otherwise, if E is not constant, we recursively compute its
694	** clauses, and then merge using the universal set for T. */
695	if (Cudd_IsConstant(E)) { /* E cannot be zero here */
696	/* Create the clause (!index + 0). */
697	res = tlcInfoAlloc();
698	if (res == NULL) return(NULL);
699	res->vars = ALLOC(DdHalfWord,4);
700	if (res->vars == NULL) {
701	FREE(res);
702	return(NULL);
703	}
704	res->phases = bitVectorAlloc(2);
705	if (res->phases == NULL) {
706	FREE(res->vars);
707	FREE(res);
708	return(NULL);
709	}
710	res->vars[0] = index;
711	res->vars[1] = CUDD_MAXINDEX;
712	res->vars[2] = 0;
713	res->vars[3] = 0;
714	bitVectorSet(res->phases, 0, 1); /* negative phase */
715	bitVectorSet(res->phases, 1, 1); /* negative phase */
716	} else { /* E == non-constant */
717	Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
718	if (Eres == NULL) return(NULL);
719	res = computeClausesWithUniverse(Eres, index, 1);
720	}
721	} else { /* T == non-const */
722	Tres = ddFindTwoLiteralClausesRecur(dd, T, table);
723	if (Tres == NULL) return(NULL);
724	if (Cudd_IsConstant(E)) {
725	if (E == lzero \|\| E == azero) {
726	res = computeClausesWithUniverse(Tres, index, 0);
727	} else {
728	Eres = emptyClauseSet();
729	if (Eres == NULL) return(NULL);
730	res = computeClauses(Tres, Eres, index, dd->size);
731	Cudd_tlcInfoFree(Eres);
732	}
733	} else {
734	Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
735	if (Eres == NULL) return(NULL);
736	res = computeClauses(Tres, Eres, index, dd->size);
737	}
738	}
739
740	/* Cache results. */
741	if (st_add_direct(table, (char )f, (char )res) == ST_OUT_OF_MEM) {
742	FREE(res);
743	return(NULL);
744	}
745	return(res);
746
747	} /* end of ddFindTwoLiteralClausesRecur */
748
749
750	/Function******************************************************************
751
752	Synopsis [Computes the two-literal clauses for a node.]
753
754	Description [Computes the two-literal clauses for a node given the
755	clauses for its children and the label of the node. Returns a
756	pointer to a TclInfo structure if successful; NULL otherwise.]
757
758	SideEffects [None]
759
760	SeeAlso [computeClausesWithUniverse]
761
762	******************************************************************************/
763	static DdTlcInfo *
764	computeClauses(
765	DdTlcInfo Tres / list of clauses for T child */,
766	DdTlcInfo Eres / list of clauses for E child */,
767	DdHalfWord label /* variable labeling the current node */,
768	int size /* number of variables in the manager */)
769	{
770	DdHalfWord Tcv = Tres->vars; / variables of clauses for the T child */
771	BitVector Tcp = Tres->phases; / phases of clauses for the T child */
772	DdHalfWord Ecv = Eres->vars; / variables of clauses for the E child */
773	BitVector Ecp = Eres->phases; / phases of clauses for the E child */
774	DdHalfWord Vcv = NULL; / pointer to variables of the clauses for v */
775	BitVector Vcp = NULL; / pointer to phases of the clauses for v */
776	DdTlcInfo res = NULL; / the set of clauses to be returned */
777	int pt = 0; /* index in the list of clauses of T */
778	int pe = 0; /* index in the list of clauses of E */
779	int cv = 0; /* counter of the clauses for this node */
780	TlClause iclauses = NULL; / list of inherited clauses */
781	TlClause tclauses = NULL; / list of 1-literal clauses of T */
782	TlClause eclauses = NULL; / list of 1-literal clauses of E */
783	TlClause nclauses = NULL; / list of new (non-inherited) clauses */
784	TlClause lnclause = NULL; / pointer to last new clause */
785	TlClause newclause; / temporary pointer to new clauses */
786
787	/* Initialize sets of one-literal clauses. The one-literal clauses
788	** are stored redundantly. These sets allow constant-time lookup, which
789	** we need when we check for implication of a two-literal clause by a
790	** one-literal clause. The linked lists allow fast sequential
791	** processing. */
792	bitVectorClear(Tolv, size);
793	bitVectorClear(Tolp, size);
794	bitVectorClear(Eolv, size);
795	bitVectorClear(Eolp, size);
796
797	/* Initialize result structure. */
798	res = tlcInfoAlloc();
799	if (res == NULL) goto cleanup;
800
801	/* Scan the two input list. Extract inherited two-literal clauses
802	** and set aside one-literal clauses from each list. The incoming lists
803	** are sorted in the order defined by beforep. The three linked list
804	** produced by this loop are sorted in the reverse order because we
805	** always append to the front of the lists.
806	** The inherited clauses are those clauses (both one- and two-literal)
807	** that are common to both children; and the two-literal clauses of
808	** one child that are implied by a one-literal clause of the other
809	** child. */
810	while (!sentinelp(Tcv[pt], Tcv[pt+1]) \|\| !sentinelp(Ecv[pe], Ecv[pe+1])) {
811	if (equalp(Tcv[pt], bitVectorRead(Tcp, pt),
812	Tcv[pt+1], bitVectorRead(Tcp, pt+1),
813	Ecv[pe], bitVectorRead(Ecp, pe),
814	Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
815	/* Add clause to inherited list. */
816	newclause = ALLOC(TlClause,1);
817	if (newclause == NULL) goto cleanup;
818	newclause->v1 = Tcv[pt];
819	newclause->v2 = Tcv[pt+1];
820	newclause->p1 = bitVectorRead(Tcp, pt);
821	newclause->p2 = bitVectorRead(Tcp, pt+1);
822	newclause->next = iclauses;
823	iclauses = newclause;
824	pt += 2; pe += 2; cv++;
825	} else if (beforep(Tcv[pt], bitVectorRead(Tcp, pt),
826	Tcv[pt+1], bitVectorRead(Tcp, pt+1),
827	Ecv[pe], bitVectorRead(Ecp, pe),
828	Ecv[pe+1], bitVectorRead(Ecp, pe+1))) {
829	if (oneliteralp(Tcv[pt+1])) {
830	/* Add this one-literal clause to the T set. */
831	newclause = ALLOC(TlClause,1);
832	if (newclause == NULL) goto cleanup;
833	newclause->v1 = Tcv[pt];
834	newclause->v2 = CUDD_MAXINDEX;
835	newclause->p1 = bitVectorRead(Tcp, pt);
836	newclause->p2 = 1;
837	newclause->next = tclauses;
838	tclauses = newclause;
839	bitVectorSet(Tolv, Tcv[pt], 1);
840	bitVectorSet(Tolp, Tcv[pt], bitVectorRead(Tcp, pt));
841	} else {
842	if (impliedp(Tcv[pt], bitVectorRead(Tcp, pt),
843	Tcv[pt+1], bitVectorRead(Tcp, pt+1),
844	Eolv, Eolp)) {
845	/* Add clause to inherited list. */
846	newclause = ALLOC(TlClause,1);
847	if (newclause == NULL) goto cleanup;
848	newclause->v1 = Tcv[pt];
849	newclause->v2 = Tcv[pt+1];
850	newclause->p1 = bitVectorRead(Tcp, pt);
851	newclause->p2 = bitVectorRead(Tcp, pt+1);
852	newclause->next = iclauses;
853	iclauses = newclause;
854	cv++;
855	}
856	}
857	pt += 2;
858	} else { /* !beforep() */
859	if (oneliteralp(Ecv[pe+1])) {
860	/* Add this one-literal clause to the E set. */
861	newclause = ALLOC(TlClause,1);
862	if (newclause == NULL) goto cleanup;
863	newclause->v1 = Ecv[pe];
864	newclause->v2 = CUDD_MAXINDEX;
865	newclause->p1 = bitVectorRead(Ecp, pe);
866	newclause->p2 = 1;
867	newclause->next = eclauses;
868	eclauses = newclause;
869	bitVectorSet(Eolv, Ecv[pe], 1);
870	bitVectorSet(Eolp, Ecv[pe], bitVectorRead(Ecp, pe));
871	} else {
872	if (impliedp(Ecv[pe], bitVectorRead(Ecp, pe),
873	Ecv[pe+1], bitVectorRead(Ecp, pe+1),
874	Tolv, Tolp)) {
875	/* Add clause to inherited list. */
876	newclause = ALLOC(TlClause,1);
877	if (newclause == NULL) goto cleanup;
878	newclause->v1 = Ecv[pe];
879	newclause->v2 = Ecv[pe+1];
880	newclause->p1 = bitVectorRead(Ecp, pe);
881	newclause->p2 = bitVectorRead(Ecp, pe+1);
882	newclause->next = iclauses;
883	iclauses = newclause;
884	cv++;
885	}
886	}
887	pe += 2;
888	}
889	}
890
891	/* Add one-literal clauses for the label variable to the front of
892	** the two lists. */
893	newclause = ALLOC(TlClause,1);
894	if (newclause == NULL) goto cleanup;
895	newclause->v1 = label;
896	newclause->v2 = CUDD_MAXINDEX;
897	newclause->p1 = 0;
898	newclause->p2 = 1;
899	newclause->next = tclauses;
900	tclauses = newclause;
901	newclause = ALLOC(TlClause,1);
902	if (newclause == NULL) goto cleanup;
903	newclause->v1 = label;
904	newclause->v2 = CUDD_MAXINDEX;
905	newclause->p1 = 1;
906	newclause->p2 = 1;
907	newclause->next = eclauses;
908	eclauses = newclause;
909
910	/* Produce the non-inherited clauses. We preserve the "reverse"
911	** order of the two input lists by appending to the end of the
912	** list. In this way, iclauses and nclauses are consistent. */
913	while (tclauses != NULL && eclauses != NULL) {
914	if (beforep(eclauses->v1, eclauses->p1, eclauses->v2, eclauses->p2,
915	tclauses->v1, tclauses->p1, tclauses->v2, tclauses->p2)) {
916	TlClause *nextclause = tclauses->next;
917	TlClause *otherclauses = eclauses;
918	while (otherclauses != NULL) {
919	if (tclauses->v1 != otherclauses->v1) {
920	newclause = ALLOC(TlClause,1);
921	if (newclause == NULL) goto cleanup;
922	newclause->v1 = tclauses->v1;
923	newclause->v2 = otherclauses->v1;
924	newclause->p1 = tclauses->p1;
925	newclause->p2 = otherclauses->p1;
926	newclause->next = NULL;
927	if (nclauses == NULL) {
928	nclauses = newclause;
929	lnclause = newclause;
930	} else {
931	lnclause->next = newclause;
932	lnclause = newclause;
933	}
934	cv++;
935	}
936	otherclauses = otherclauses->next;
937	}
938	FREE(tclauses);
939	tclauses = nextclause;
940	} else {
941	TlClause *nextclause = eclauses->next;
942	TlClause *otherclauses = tclauses;
943	while (otherclauses != NULL) {
944	if (eclauses->v1 != otherclauses->v1) {
945	newclause = ALLOC(TlClause,1);
946	if (newclause == NULL) goto cleanup;
947	newclause->v1 = eclauses->v1;
948	newclause->v2 = otherclauses->v1;
949	newclause->p1 = eclauses->p1;
950	newclause->p2 = otherclauses->p1;
951	newclause->next = NULL;
952	if (nclauses == NULL) {
953	nclauses = newclause;
954	lnclause = newclause;
955	} else {
956	lnclause->next = newclause;
957	lnclause = newclause;
958	}
959	cv++;
960	}
961	otherclauses = otherclauses->next;
962	}
963	FREE(eclauses);
964	eclauses = nextclause;
965	}
966	}
967	while (tclauses != NULL) {
968	TlClause *nextclause = tclauses->next;
969	FREE(tclauses);
970	tclauses = nextclause;
971	}
972	while (eclauses != NULL) {
973	TlClause *nextclause = eclauses->next;
974	FREE(eclauses);
975	eclauses = nextclause;
976	}
977
978	/* Merge inherited and non-inherited clauses. Now that we know the
979	** total number, we allocate the arrays, and we fill them bottom-up
980	** to restore the proper ordering. */
981	Vcv = ALLOC(DdHalfWord, 2*(cv+1));
982	if (Vcv == NULL) goto cleanup;
983	if (cv > 0) {
984	Vcp = bitVectorAlloc(2*cv);
985	if (Vcp == NULL) goto cleanup;
986	} else {
987	Vcp = NULL;
988	}
989	res->vars = Vcv;
990	res->phases = Vcp;
991	/* Add sentinel. */
992	Vcv[2*cv] = 0;
993	Vcv[2*cv+1] = 0;
994	while (iclauses != NULL \|\| nclauses != NULL) {
995	TlClause *nextclause;
996	cv--;
997	if (nclauses == NULL \|\| (iclauses != NULL &&
998	beforep(nclauses->v1, nclauses->p1, nclauses->v2, nclauses->p2,
999	iclauses->v1, iclauses->p1, iclauses->v2, iclauses->p2))) {
1000	Vcv[2*cv] = iclauses->v1;
1001	Vcv[2*cv+1] = iclauses->v2;
1002	bitVectorSet(Vcp, 2*cv, iclauses->p1);
1003	bitVectorSet(Vcp, 2*cv+1, iclauses->p2);
1004	nextclause = iclauses->next;
1005	FREE(iclauses);
1006	iclauses = nextclause;
1007	} else {
1008	Vcv[2*cv] = nclauses->v1;
1009	Vcv[2*cv+1] = nclauses->v2;
1010	bitVectorSet(Vcp, 2*cv, nclauses->p1);
1011	bitVectorSet(Vcp, 2*cv+1, nclauses->p2);
1012	nextclause = nclauses->next;
1013	FREE(nclauses);
1014	nclauses = nextclause;
1015	}
1016	}
1017	assert(cv == 0);
1018
1019	return(res);
1020
1021	cleanup:
1022	if (res != NULL) Cudd_tlcInfoFree(res);
1023	while (iclauses != NULL) {
1024	TlClause *nextclause = iclauses->next;
1025	FREE(iclauses);
1026	iclauses = nextclause;
1027	}
1028	while (nclauses != NULL) {
1029	TlClause *nextclause = nclauses->next;
1030	FREE(nclauses);
1031	nclauses = nextclause;
1032	}
1033	while (tclauses != NULL) {
1034	TlClause *nextclause = tclauses->next;
1035	FREE(tclauses);
1036	tclauses = nextclause;
1037	}
1038	while (eclauses != NULL) {
1039	TlClause *nextclause = eclauses->next;
1040	FREE(eclauses);
1041	eclauses = nextclause;
1042	}
1043
1044	return(NULL);
1045
1046	} /* end of computeClauses */
1047
1048
1049	/Function******************************************************************
1050
1051	Synopsis [Computes the two-literal clauses for a node.]
1052
1053	Description [Computes the two-literal clauses for a node with a zero
1054	child, given the clauses for its other child and the label of the
1055	node. Returns a pointer to a TclInfo structure if successful; NULL
1056	otherwise.]
1057
1058	SideEffects [None]
1059
1060	SeeAlso [computeClauses]
1061
1062	******************************************************************************/
1063	static DdTlcInfo *
1064	computeClausesWithUniverse(
1065	DdTlcInfo Cres / list of clauses for child */,
1066	DdHalfWord label /* variable labeling the current node */,
1067	short phase /* 0 if E child is zero; 1 if T child is zero */)
1068	{
1069	DdHalfWord Ccv = Cres->vars; / variables of clauses for child */
1070	BitVector Ccp = Cres->phases; / phases of clauses for child */
1071	DdHalfWord Vcv = NULL; / pointer to the variables of the clauses for v */
1072	BitVector Vcp = NULL; / pointer to the phases of the clauses for v */
1073	DdTlcInfo res = NULL; / the set of clauses to be returned */
1074	int i;
1075
1076	/* Initialize result. */
1077	res = tlcInfoAlloc();
1078	if (res == NULL) goto cleanup;
1079	/* Count entries for new list and allocate accordingly. */
1080	for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2);
1081	/* At this point, i is twice the number of clauses in the child's
1082	** list. We need four more entries for this node: 2 for the one-literal
1083	** clause for the label, and 2 for the sentinel. */
1084	Vcv = ALLOC(DdHalfWord,i+4);
1085	if (Vcv == NULL) goto cleanup;
1086	Vcp = bitVectorAlloc(i+4);
1087	if (Vcp == NULL) goto cleanup;
1088	res->vars = Vcv;
1089	res->phases = Vcp;
1090	/* Copy old list into new. */
1091	for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2) {
1092	Vcv[i] = Ccv[i];
1093	Vcv[i+1] = Ccv[i+1];
1094	bitVectorSet(Vcp, i, bitVectorRead(Ccp, i));
1095	bitVectorSet(Vcp, i+1, bitVectorRead(Ccp, i+1));
1096	}
1097	/* Add clause corresponding to label. */
1098	Vcv[i] = label;
1099	bitVectorSet(Vcp, i, phase);
1100	i++;
1101	Vcv[i] = CUDD_MAXINDEX;
1102	bitVectorSet(Vcp, i, 1);
1103	i++;
1104	/* Add sentinel. */
1105	Vcv[i] = 0;
1106	Vcv[i+1] = 0;
1107	bitVectorSet(Vcp, i, 0);
1108	bitVectorSet(Vcp, i+1, 0);
1109
1110	return(res);
1111
1112	cleanup:
1113	/* Vcp is guaranteed to be NULL here. Hence, we do not try to free it. */
1114	if (Vcv != NULL) FREE(Vcv);
1115	if (res != NULL) Cudd_tlcInfoFree(res);
1116
1117	return(NULL);
1118
1119	} /* end of computeClausesWithUniverse */
1120
1121
1122	/Function******************************************************************
1123
1124	Synopsis [Returns an enpty set of clauses.]
1125
1126	Description [Returns a pointer to an empty set of clauses if
1127	successful; NULL otherwise. No bit vector for the phases is
1128	allocated.]
1129
1130	SideEffects [None]
1131
1132	SeeAlso []
1133
1134	******************************************************************************/
1135	static DdTlcInfo *
1136	emptyClauseSet(void)
1137	{
1138	DdTlcInfo *eset;
1139
1140	eset = ALLOC(DdTlcInfo,1);
1141	if (eset == NULL) return(NULL);
1142	eset->vars = ALLOC(DdHalfWord,2);
1143	if (eset->vars == NULL) {
1144	FREE(eset);
1145	return(NULL);
1146	}
1147	/* Sentinel */
1148	eset->vars[0] = 0;
1149	eset->vars[1] = 0;
1150	eset->phases = NULL; /* does not matter */
1151	eset->cnt = 0;
1152	return(eset);
1153
1154	} /* end of emptyClauseSet */
1155
1156
1157	/Function******************************************************************
1158
1159	Synopsis [Returns true iff the argument is the sentinel clause.]
1160
1161	Description [Returns true iff the argument is the sentinel clause.
1162	A sentinel clause has both variables equal to 0.]
1163
1164	SideEffects [None]
1165
1166	SeeAlso []
1167
1168	******************************************************************************/
1169	static int
1170	sentinelp(
1171	DdHalfWord var1,
1172	DdHalfWord var2)
1173	{
1174	return(var1 == 0 && var2 == 0);
1175
1176	} /* end of sentinelp */
1177
1178
1179	/Function******************************************************************
1180
1181	Synopsis [Returns true iff the two arguments are identical clauses.]
1182
1183	Description [Returns true iff the two arguments are identical
1184	clauses. Since literals are sorted, we only need to compare
1185	literals in the same position.]
1186
1187	SideEffects [None]
1188
1189	SeeAlso [beforep]
1190
1191	******************************************************************************/
1192	static int
1193	equalp(
1194	DdHalfWord var1a,
1195	short phase1a,
1196	DdHalfWord var1b,
1197	short phase1b,
1198	DdHalfWord var2a,
1199	short phase2a,
1200	DdHalfWord var2b,
1201	short phase2b)
1202	{
1203	return(var1a == var2a && phase1a == phase2a &&
1204	var1b == var2b && phase1b == phase2b);
1205
1206	} /* end of equalp */
1207
1208
1209	/Function******************************************************************
1210
1211	Synopsis [Returns true iff the first argument precedes the second in
1212	the clause order.]
1213
1214	Description [Returns true iff the first argument precedes the second
1215	in the clause order. A clause precedes another if its first lieral
1216	precedes the first literal of the other, or if the first literals
1217	are the same, and its second literal precedes the second literal of
1218	the other clause. A literal precedes another if it has a higher
1219	index, of if it has the same index, but it has lower phase. Phase 0
1220	is the positive phase, and it is lower than Phase 1 (negative
1221	phase).]
1222
1223	SideEffects [None]
1224
1225	SeeAlso [equalp]
1226
1227	******************************************************************************/
1228	static int
1229	beforep(
1230	DdHalfWord var1a,
1231	short phase1a,
1232	DdHalfWord var1b,
1233	short phase1b,
1234	DdHalfWord var2a,
1235	short phase2a,
1236	DdHalfWord var2b,
1237	short phase2b)
1238	{
1239	return(var1a > var2a \|\| (var1a == var2a &&
1240	(phase1a < phase2a \|\| (phase1a == phase2a &&
1241	(var1b > var2b \|\| (var1b == var2b && phase1b < phase2b))))));
1242
1243	} /* end of beforep */
1244
1245
1246	/Function******************************************************************
1247
1248	Synopsis [Returns true iff the argument is a one-literal clause.]
1249
1250	Description [Returns true iff the argument is a one-literal clause.
1251	A one-litaral clause has the constant FALSE as second literal.
1252	Since the constant TRUE is never used, it is sufficient to test for
1253	a constant.]
1254
1255	SideEffects [None]
1256
1257	SeeAlso []
1258
1259	******************************************************************************/
1260	static int
1261	oneliteralp(
1262	DdHalfWord var)
1263	{
1264	return(var == CUDD_MAXINDEX);
1265
1266	} /* end of oneliteralp */
1267
1268
1269	/Function******************************************************************
1270
1271	Synopsis [Returns true iff either literal of a clause is in a set of
1272	literals.]
1273
1274	Description [Returns true iff either literal of a clause is in a set
1275	of literals. The first four arguments specify the clause. The
1276	remaining two arguments specify the literal set.]
1277
1278	SideEffects [None]
1279
1280	SeeAlso []
1281
1282	******************************************************************************/
1283	static int
1284	impliedp(
1285	DdHalfWord var1,
1286	short phase1,
1287	DdHalfWord var2,
1288	short phase2,
1289	BitVector *olv,
1290	BitVector *olp)
1291	{
1292	return((bitVectorRead(olv, var1) &&
1293	bitVectorRead(olp, var1) == phase1) \|\|
1294	(bitVectorRead(olv, var2) &&
1295	bitVectorRead(olp, var2) == phase2));
1296
1297	} /* end of impliedp */
1298
1299
1300	/Function******************************************************************
1301
1302	Synopsis [Allocates a bit vector.]
1303
1304	Description [Allocates a bit vector. The parameter size gives the
1305	number of bits. This procedure allocates enough long's to hold the
1306	specified number of bits. Returns a pointer to the allocated vector
1307	if successful; NULL otherwise.]
1308
1309	SideEffects [None]
1310
1311	SeeAlso [bitVectorClear bitVectorFree]
1312
1313	******************************************************************************/
1314	static BitVector *
1315	bitVectorAlloc(
1316	int size)
1317	{
1318	int allocSize;
1319	BitVector *vector;
1320
1321	/* Find out how many long's we need.
1322	** There are sizeof(long) * 8 bits in a long.
1323	** The ceiling of the ratio of two integers m and n is given
1324	** by ((n-1)/m)+1. Putting all this together, we get... */
1325	allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1326	vector = ALLOC(BitVector, allocSize);
1327	if (vector == NULL) return(NULL);
1328	/* Clear the whole array. */
1329	(void) memset(vector, 0, allocSize * sizeof(BitVector));
1330	return(vector);
1331
1332	} /* end of bitVectorAlloc */
1333
1334
1335	/Function******************************************************************
1336
1337	Synopsis [Clears a bit vector.]
1338
1339	Description [Clears a bit vector. The parameter size gives the
1340	number of bits.]
1341
1342	SideEffects [None]
1343
1344	SeeAlso [bitVectorAlloc]
1345
1346	******************************************************************************/
1347	DD_INLINE
1348	static void
1349	bitVectorClear(
1350	BitVector *vector,
1351	int size)
1352	{
1353	int allocSize;
1354
1355	/* Find out how many long's we need.
1356	** There are sizeof(long) * 8 bits in a long.
1357	** The ceiling of the ratio of two integers m and n is given
1358	** by ((n-1)/m)+1. Putting all this together, we get... */
1359	allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1360	/* Clear the whole array. */
1361	(void) memset(vector, 0, allocSize * sizeof(BitVector));
1362	return;
1363
1364	} /* end of bitVectorClear */
1365
1366
1367	/Function******************************************************************
1368
1369	Synopsis [Frees a bit vector.]
1370
1371	Description [Frees a bit vector.]
1372
1373	SideEffects [None]
1374
1375	SeeAlso [bitVectorAlloc]
1376
1377	******************************************************************************/
1378	static void
1379	bitVectorFree(
1380	BitVector *vector)
1381	{
1382	FREE(vector);
1383
1384	} /* end of bitVectorFree */
1385
1386
1387	/Function******************************************************************
1388
1389	Synopsis [Returns the i-th entry of a bit vector.]
1390
1391	Description [Returns the i-th entry of a bit vector.]
1392
1393	SideEffects [None]
1394
1395	SeeAlso [bitVectorSet]
1396
1397	******************************************************************************/
1398	DD_INLINE
1399	static short
1400	bitVectorRead(
1401	BitVector *vector,
1402	int i)
1403	{
1404	int word, bit;
1405	short result;
1406
1407	if (vector == NULL) return((short) 0);
1408
1409	word = i >> LOGBPL;
1410	bit = i & (BPL - 1);
1411	result = (short) ((vector[word] >> bit) & 1L);
1412	return(result);
1413
1414	} /* end of bitVectorRead */
1415
1416
1417	/Function******************************************************************
1418
1419	Synopsis [Sets the i-th entry of a bit vector to a value.]
1420
1421	Description [Sets the i-th entry of a bit vector to a value.]
1422
1423	SideEffects [None]
1424
1425	SeeAlso [bitVectorRead]
1426
1427	******************************************************************************/
1428	DD_INLINE
1429	static void
1430	bitVectorSet(
1431	BitVector * vector,
1432	int i,
1433	short val)
1434	{
1435	int word, bit;
1436
1437	word = i >> LOGBPL;
1438	bit = i & (BPL - 1);
1439	vector[word] &= ~(1L << bit);
1440	vector[word] \|= (((long) val) << bit);
1441
1442	} /* end of bitVectorSet */
1443
1444
1445	/Function******************************************************************
1446
1447	Synopsis [Allocates a DdTlcInfo Structure.]
1448
1449	Description [Returns a pointer to a DdTlcInfo Structure if successful;
1450	NULL otherwise.]
1451
1452	SideEffects [None]
1453
1454	SeeAlso [Cudd_tlcInfoFree]
1455
1456	******************************************************************************/
1457	static DdTlcInfo *
1458	tlcInfoAlloc(void)
1459	{
1460	DdTlcInfo *res = ALLOC(DdTlcInfo,1);
1461	if (res == NULL) return(NULL);
1462	res->vars = NULL;
1463	res->phases = NULL;
1464	res->cnt = 0;
1465	return(res);
1466
1467	} /* end of tlcInfoAlloc */

Note: See TracBrowser for help on using the repository browser.

Context Navigation

source: vis_dev/glu-2.3/src/cuBdd/cuddEssent.c @ 100

Download in other formats: