Context Navigation

source: vis_dev/glu-2.1/src/cuBdd/cuddEssent.c @ 13

Last change on this file since 13 was 8, checked in by cecile, 13 years ago
src glu
File size: 43.8 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.21 2004/08/13 18:04:48 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, int size);
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 >= 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, dd->size);
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, dd->size);
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	int size /* number of variables in the manager */)
1069	{
1070	DdHalfWord Ccv = Cres->vars; / variables of clauses for child */
1071	BitVector Ccp = Cres->phases; / phases of clauses for child */
1072	DdHalfWord Vcv = NULL; / pointer to the variables of the clauses for v */
1073	BitVector Vcp = NULL; / pointer to the phases of the clauses for v */
1074	DdTlcInfo res = NULL; / the set of clauses to be returned */
1075	int i;
1076
1077	/* Initialize result. */
1078	res = tlcInfoAlloc();
1079	if (res == NULL) goto cleanup;
1080	/* Count entries for new list and allocate accordingly. */
1081	for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2);
1082	/* At this point, i is twice the number of clauses in the child's
1083	** list. We need four more entries for this node: 2 for the one-literal
1084	** clause for the label, and 2 for the sentinel. */
1085	Vcv = ALLOC(DdHalfWord,i+4);
1086	if (Vcv == NULL) goto cleanup;
1087	Vcp = bitVectorAlloc(i+4);
1088	if (Vcp == NULL) goto cleanup;
1089	res->vars = Vcv;
1090	res->phases = Vcp;
1091	/* Copy old list into new. */
1092	for (i = 0; !sentinelp(Ccv[i], Ccv[i+1]); i += 2) {
1093	Vcv[i] = Ccv[i];
1094	Vcv[i+1] = Ccv[i+1];
1095	bitVectorSet(Vcp, i, bitVectorRead(Ccp, i));
1096	bitVectorSet(Vcp, i+1, bitVectorRead(Ccp, i+1));
1097	}
1098	/* Add clause corresponding to label. */
1099	Vcv[i] = label;
1100	bitVectorSet(Vcp, i, phase);
1101	i++;
1102	Vcv[i] = CUDD_MAXINDEX;
1103	bitVectorSet(Vcp, i, 1);
1104	i++;
1105	/* Add sentinel. */
1106	Vcv[i] = 0;
1107	Vcv[i+1] = 0;
1108	bitVectorSet(Vcp, i, 0);
1109	bitVectorSet(Vcp, i+1, 0);
1110
1111	return(res);
1112
1113	cleanup:
1114	if (Vcv != NULL) FREE(Vcv);
1115	if (Vcp != NULL) bitVectorFree(Vcp);
1116	if (res != NULL) Cudd_tlcInfoFree(res);
1117
1118	return(NULL);
1119
1120	} /* end of computeClausesWithUniverse */
1121
1122
1123	/Function******************************************************************
1124
1125	Synopsis [Returns an enpty set of clauses.]
1126
1127	Description [Returns a pointer to an empty set of clauses if
1128	successful; NULL otherwise. No bit vector for the phases is
1129	allocated.]
1130
1131	SideEffects [None]
1132
1133	SeeAlso []
1134
1135	******************************************************************************/
1136	static DdTlcInfo *
1137	emptyClauseSet(void)
1138	{
1139	DdTlcInfo *eset;
1140
1141	eset = ALLOC(DdTlcInfo,1);
1142	if (eset == NULL) return(NULL);
1143	eset->vars = ALLOC(DdHalfWord,2);
1144	if (eset->vars == NULL) {
1145	FREE(eset);
1146	return(NULL);
1147	}
1148	/* Sentinel */
1149	eset->vars[0] = 0;
1150	eset->vars[1] = 0;
1151	eset->phases = NULL; /* does not matter */
1152	eset->cnt = 0;
1153	return(eset);
1154
1155	} /* end of emptyClauseSet */
1156
1157
1158	/Function******************************************************************
1159
1160	Synopsis [Returns true iff the argument is the sentinel clause.]
1161
1162	Description [Returns true iff the argument is the sentinel clause.
1163	A sentinel clause has both variables equal to 0.]
1164
1165	SideEffects [None]
1166
1167	SeeAlso []
1168
1169	******************************************************************************/
1170	static int
1171	sentinelp(
1172	DdHalfWord var1,
1173	DdHalfWord var2)
1174	{
1175	return(var1 == 0 && var2 == 0);
1176
1177	} /* end of sentinelp */
1178
1179
1180	/Function******************************************************************
1181
1182	Synopsis [Returns true iff the two arguments are identical clauses.]
1183
1184	Description [Returns true iff the two arguments are identical
1185	clauses. Since literals are sorted, we only need to compare
1186	literals in the same position.]
1187
1188	SideEffects [None]
1189
1190	SeeAlso [beforep]
1191
1192	******************************************************************************/
1193	static int
1194	equalp(
1195	DdHalfWord var1a,
1196	short phase1a,
1197	DdHalfWord var1b,
1198	short phase1b,
1199	DdHalfWord var2a,
1200	short phase2a,
1201	DdHalfWord var2b,
1202	short phase2b)
1203	{
1204	return(var1a == var2a && phase1a == phase2a &&
1205	var1b == var2b && phase1b == phase2b);
1206
1207	} /* end of equalp */
1208
1209
1210	/Function******************************************************************
1211
1212	Synopsis [Returns true iff the first argument precedes the second in
1213	the clause order.]
1214
1215	Description [Returns true iff the first argument precedes the second
1216	in the clause order. A clause precedes another if its first lieral
1217	precedes the first literal of the other, or if the first literals
1218	are the same, and its second literal precedes the second literal of
1219	the other clause. A literal precedes another if it has a higher
1220	index, of if it has the same index, but it has lower phase. Phase 0
1221	is the positive phase, and it is lower than Phase 1 (negative
1222	phase).]
1223
1224	SideEffects [None]
1225
1226	SeeAlso [equalp]
1227
1228	******************************************************************************/
1229	static int
1230	beforep(
1231	DdHalfWord var1a,
1232	short phase1a,
1233	DdHalfWord var1b,
1234	short phase1b,
1235	DdHalfWord var2a,
1236	short phase2a,
1237	DdHalfWord var2b,
1238	short phase2b)
1239	{
1240	return(var1a > var2a \|\| (var1a == var2a &&
1241	(phase1a < phase2a \|\| (phase1a == phase2a &&
1242	(var1b > var2b \|\| (var1b == var2b && phase1b < phase2b))))));
1243
1244	} /* end of beforep */
1245
1246
1247	/Function******************************************************************
1248
1249	Synopsis [Returns true iff the argument is a one-literal clause.]
1250
1251	Description [Returns true iff the argument is a one-literal clause.
1252	A one-litaral clause has the constant FALSE as second literal.
1253	Since the constant TRUE is never used, it is sufficient to test for
1254	a constant.]
1255
1256	SideEffects [None]
1257
1258	SeeAlso []
1259
1260	******************************************************************************/
1261	static int
1262	oneliteralp(
1263	DdHalfWord var)
1264	{
1265	return(var == CUDD_MAXINDEX);
1266
1267	} /* end of oneliteralp */
1268
1269
1270	/Function******************************************************************
1271
1272	Synopsis [Returns true iff either literal of a clause is in a set of
1273	literals.]
1274
1275	Description [Returns true iff either literal of a clause is in a set
1276	of literals. The first four arguments specify the clause. The
1277	remaining two arguments specify the literal set.]
1278
1279	SideEffects [None]
1280
1281	SeeAlso []
1282
1283	******************************************************************************/
1284	static int
1285	impliedp(
1286	DdHalfWord var1,
1287	short phase1,
1288	DdHalfWord var2,
1289	short phase2,
1290	BitVector *olv,
1291	BitVector *olp)
1292	{
1293	return((bitVectorRead(olv, var1) &&
1294	bitVectorRead(olp, var1) == phase1) \|\|
1295	(bitVectorRead(olv, var2) &&
1296	bitVectorRead(olp, var2) == phase2));
1297
1298	} /* end of impliedp */
1299
1300
1301	/Function******************************************************************
1302
1303	Synopsis [Allocates a bit vector.]
1304
1305	Description [Allocates a bit vector. The parameter size gives the
1306	number of bits. This procedure allocates enough long's to hold the
1307	specified number of bits. Returns a pointer to the allocated vector
1308	if successful; NULL otherwise.]
1309
1310	SideEffects [None]
1311
1312	SeeAlso [bitVectorClear bitVectorFree]
1313
1314	******************************************************************************/
1315	static BitVector *
1316	bitVectorAlloc(
1317	int size)
1318	{
1319	int allocSize;
1320	BitVector *vector;
1321
1322	/* Find out how many long's we need.
1323	** There are sizeof(long) * 8 bits in a long.
1324	** The ceiling of the ratio of two integers m and n is given
1325	** by ((n-1)/m)+1. Putting all this together, we get... */
1326	allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1327	vector = ALLOC(BitVector, allocSize);
1328	if (vector == NULL) return(NULL);
1329	/* Clear the whole array. */
1330	(void) memset(vector, 0, allocSize * sizeof(BitVector));
1331	return(vector);
1332
1333	} /* end of bitVectorAlloc */
1334
1335
1336	/Function******************************************************************
1337
1338	Synopsis [Clears a bit vector.]
1339
1340	Description [Clears a bit vector. The parameter size gives the
1341	number of bits.]
1342
1343	SideEffects [None]
1344
1345	SeeAlso [bitVectorAlloc]
1346
1347	******************************************************************************/
1348	DD_INLINE
1349	static void
1350	bitVectorClear(
1351	BitVector *vector,
1352	int size)
1353	{
1354	int allocSize;
1355
1356	/* Find out how many long's we need.
1357	** There are sizeof(long) * 8 bits in a long.
1358	** The ceiling of the ratio of two integers m and n is given
1359	** by ((n-1)/m)+1. Putting all this together, we get... */
1360	allocSize = ((size - 1) / (sizeof(BitVector) * 8)) + 1;
1361	/* Clear the whole array. */
1362	(void) memset(vector, 0, allocSize * sizeof(BitVector));
1363	return;
1364
1365	} /* end of bitVectorClear */
1366
1367
1368	/Function******************************************************************
1369
1370	Synopsis [Frees a bit vector.]
1371
1372	Description [Frees a bit vector.]
1373
1374	SideEffects [None]
1375
1376	SeeAlso [bitVectorAlloc]
1377
1378	******************************************************************************/
1379	static void
1380	bitVectorFree(
1381	BitVector *vector)
1382	{
1383	FREE(vector);
1384
1385	} /* end of bitVectorFree */
1386
1387
1388	/Function******************************************************************
1389
1390	Synopsis [Returns the i-th entry of a bit vector.]
1391
1392	Description [Returns the i-th entry of a bit vector.]
1393
1394	SideEffects [None]
1395
1396	SeeAlso [bitVectorSet]
1397
1398	******************************************************************************/
1399	DD_INLINE
1400	static short
1401	bitVectorRead(
1402	BitVector *vector,
1403	int i)
1404	{
1405	int word, bit;
1406	short result;
1407
1408	if (vector == NULL) return((short) 0);
1409
1410	word = i >> LOGBPL;
1411	bit = i & (BPL - 1);
1412	result = (short) ((vector[word] >> bit) & 1L);
1413	return(result);
1414
1415	} /* end of bitVectorRead */
1416
1417
1418	/Function******************************************************************
1419
1420	Synopsis [Sets the i-th entry of a bit vector to a value.]
1421
1422	Description [Sets the i-th entry of a bit vector to a value.]
1423
1424	SideEffects [None]
1425
1426	SeeAlso [bitVectorRead]
1427
1428	******************************************************************************/
1429	DD_INLINE
1430	static void
1431	bitVectorSet(
1432	BitVector * vector,
1433	int i,
1434	short val)
1435	{
1436	int word, bit;
1437
1438	word = i >> LOGBPL;
1439	bit = i & (BPL - 1);
1440	vector[word] &= ~(1L << bit);
1441	vector[word] \|= (((long) val) << bit);
1442
1443	} /* end of bitVectorSet */
1444
1445
1446	/Function******************************************************************
1447
1448	Synopsis [Allocates a DdTlcInfo Structure.]
1449
1450	Description [Returns a pointer to a DdTlcInfo Structure if successful;
1451	NULL otherwise.]
1452
1453	SideEffects [None]
1454
1455	SeeAlso [Cudd_tlcInfoFree]
1456
1457	******************************************************************************/
1458	static DdTlcInfo *
1459	tlcInfoAlloc(void)
1460	{
1461	DdTlcInfo *res = ALLOC(DdTlcInfo,1);
1462	if (res == NULL) return(NULL);
1463	res->vars = NULL;
1464	res->phases = NULL;
1465	res->cnt = 0;
1466	return(res);
1467
1468	} /* end of tlcInfoAlloc */

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

Download in other formats: