tclbdd

Check-in [7771be216c]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added GarbageCollect for memory debugging Modified all tests to gc at the end and report # of nodes in use for leak checking. Added Tcl binding for ApplyAndQuantify Modified unset to take an arbitrary number of names.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:7771be216cb69d0eb23ea5c34e0a10d34e82670a
User & Date: kbk 2013-12-11 02:34:53
Context
2013-12-11
03:01
test appquant check-in: b7045d44bb user: kbk tags: trunk
02:34
Added GarbageCollect for memory debugging Modified all tests to gc at the end and report # of nodes in use for leak checking. Added Tcl binding for ApplyAndQuantify Modified unset to take an arbitrary number of names. check-in: 7771be216c user: kbk tags: trunk
2013-12-10
13:32
Flesh out BDD_ApplyAndQuantify. Needs Tcl wrapper. check-in: 33b0644fb3 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Changes to generic/bdd.c.

781
782
783
784
785
786
787




























































788
789
790
791
792
793
794
...
879
880
881
882
883
884
885



886
887
888
889
890
891
892
....
1834
1835
1836
1837
1838
1839
1840

1841
1842
1843
1844
1845

1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858

1859
1860
1861
1862
1863
1864
1865
....
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949

    return bead;
}
 
/*
 *-----------------------------------------------------------------------------
 *




























































 * BDD_MakeBead --
 *
 *	Searches for a bead in the hash table and constructs one if it is
 *	not found.
 *
 * Results:
 *	Returns the index of the bead.
................................................................................
    BDD_BeadIndex bead)		/* Index of the bead being unreferened */
{
    Bead* beads = sysPtr->beads;
				/* Bead table */

    if (bead <= 1) return;




    if (--(beads[bead].refCount) == 0) {

	/* Remove the bead from the hash table */
	RemoveFromHash(sysPtr, bead);
	
	/* Mark the bead as freed. */
	beads[bead].level = ~(BDD_VariableIndex) 0;
................................................................................

	    if (level < *v) {
		/*
		 * The current variable in the expression is unquantified.
		 * Recurse into the subexpressions, and recombine with
		 * a simple IF-THEN_ELSE
		 */

		l = ApplyAndQuantify(sysPtr, n, v, low1, low2);
		h = ApplyAndQuantify(sysPtr, n, v, high1, high2);
		result = BDD_MakeBead(sysPtr, level, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);

		
	    } else if (level == *v) {
		/*
		 * The current variable in the expression is quantified.
		 * Recurse into the subexpressions at the next variable,
		 * and combine by applying the quantifier.
		 */
		l = ApplyAndQuantify(sysPtr, n-1, v+1, low1, low2);
		h = ApplyAndQuantify(sysPtr, n-1, v+1, high1, high2);
		sysPtr->applyOp = sysPtr->quantifier;
		result = Apply(sysPtr, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);

		
	    } else {
		/*
		 * The current variable in the quantifier is unused.
		 * Advance to the next one.
		 * FIXME This is wrong for a UNIQUE quantifier
		 */
................................................................................
 *
 * This procedure performs simultaneous composition. The result is
 * different from consecutive composition calls on the individual variables:
 *
 * compose(x1&x2&x3, (x1->x2,x2->x3,x3->x1)) == (x2&x3&x1)
 * compose(x1&x2&x3, x1->x2) == x2&x2&x3 == x2&x3
 * compose(x2&x3, x2->x3) == x3&x3 == x3
x * compose(x3, x3->x1) == x1
 *
 * If all the variables need to be replaced with constants, then Restrict
 * is much faster than Compose at generating the replaced BDD.
 *
 *-----------------------------------------------------------------------------
 */








>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
>
>







 







>





>













>







 







|







781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
...
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
....
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
....
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015

    return bead;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_GarbageCollect --
 *
 *	Garbage collects the unused beads in the system.
 *
 * Results:
 *	Returns the count of allocated beads after garbage collection.
 *
 * This function ordinarily should not be called. Free beads are
 * garbage-collected incrementally. Freed beads also remain in the
 * cache from BDD_MakeBead and can be recycled without new memory
 * allocation if new beads with the same attributes are requested.
 * This function is primarily provided for testing the library to
 * ensure that the operations remain free of memory leaks.
 *
 *-----------------------------------------------------------------------------
 */

BDD_BeadIndex
BDD_GarbageCollect(
    BDD_System* sysPtr)		/* System of BDD's */
{
    BDD_BeadIndex garbage = 0;
    Bead* beads = sysPtr->beads;
    BDD_BeadIndex bead;
    BDD_BeadIndex count = sysPtr->beadsAlloc;

    /* 
     * Allocate beads until no free beads remain. This will force any
     * weakly referenced beads to be recycled.
     */
    while (sysPtr->unusedBead != 0) {
	bead = AddBead(sysPtr, ~(BDD_VariableIndex)0, (BDD_BeadIndex)0, 
		       (BDD_BeadIndex)0);
	sysPtr->beads[bead].next = garbage;
	garbage = bead;
    }

    /* 
     * Free the beads again, counting them. Any beads not counted are
     * "in use".
     */
    while (garbage != 0) {
	bead = garbage;
	garbage = sysPtr->beads[bead].next;
	if (sysPtr->unusedBead == 0) {
	    beads[bead].next = 0;
	} else {
	    beads[bead].next = beads[sysPtr->unusedBead].next;
	    beads[sysPtr->unusedBead].next = bead;
	}
	sysPtr->unusedBead = bead;
	--count;
    }

    return count;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BDD_MakeBead --
 *
 *	Searches for a bead in the hash table and constructs one if it is
 *	not found.
 *
 * Results:
 *	Returns the index of the bead.
................................................................................
    BDD_BeadIndex bead)		/* Index of the bead being unreferened */
{
    Bead* beads = sysPtr->beads;
				/* Bead table */

    if (bead <= 1) return;

    if (beads[bead].refCount == 0) {
	Tcl_Panic("unref free bead!");
    }
    if (--(beads[bead].refCount) == 0) {

	/* Remove the bead from the hash table */
	RemoveFromHash(sysPtr, bead);
	
	/* Mark the bead as freed. */
	beads[bead].level = ~(BDD_VariableIndex) 0;
................................................................................

	    if (level < *v) {
		/*
		 * The current variable in the expression is unquantified.
		 * Recurse into the subexpressions, and recombine with
		 * a simple IF-THEN_ELSE
		 */

		l = ApplyAndQuantify(sysPtr, n, v, low1, low2);
		h = ApplyAndQuantify(sysPtr, n, v, high1, high2);
		result = BDD_MakeBead(sysPtr, level, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);
		break;
		
	    } else if (level == *v) {
		/*
		 * The current variable in the expression is quantified.
		 * Recurse into the subexpressions at the next variable,
		 * and combine by applying the quantifier.
		 */
		l = ApplyAndQuantify(sysPtr, n-1, v+1, low1, low2);
		h = ApplyAndQuantify(sysPtr, n-1, v+1, high1, high2);
		sysPtr->applyOp = sysPtr->quantifier;
		result = Apply(sysPtr, l, h);
		BDD_UnrefBead(sysPtr, l);
		BDD_UnrefBead(sysPtr, h);
		break;
		
	    } else {
		/*
		 * The current variable in the quantifier is unused.
		 * Advance to the next one.
		 * FIXME This is wrong for a UNIQUE quantifier
		 */
................................................................................
 *
 * This procedure performs simultaneous composition. The result is
 * different from consecutive composition calls on the individual variables:
 *
 * compose(x1&x2&x3, (x1->x2,x2->x3,x3->x1)) == (x2&x3&x1)
 * compose(x1&x2&x3, x1->x2) == x2&x2&x3 == x2&x3
 * compose(x2&x3, x2->x3) == x3&x3 == x3
 * compose(x3, x3->x1) == x1
 *
 * If all the variables need to be replaced with constants, then Restrict
 * is much faster than Compose at generating the replaced BDD.
 *
 *-----------------------------------------------------------------------------
 */

Changes to generic/bdd.h.

127
128
129
130
131
132
133

134
135
136
137
138
139
140
extern BDDAPI BDD_BeadIndex BDD_MakeBead(BDD_System* sysPtr,
					 BDD_VariableIndex level,
					 BDD_BeadIndex low,
					 BDD_BeadIndex high);
extern BDDAPI void BDD_IncrBeadRefCount(BDD_System* sysPtr, 
					BDD_BeadIndex bead);
extern BDDAPI void BDD_UnrefBead(BDD_System* sysPtr, BDD_BeadIndex bead);

extern BDDAPI BDD_BeadIndex BDD_NthVariable(BDD_System* sysPtr,
					    BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_NotNthVariable(BDD_System* sysPtr,
					       BDD_VariableIndex n);
extern BDDAPI int BDD_Literal(BDD_System* sysPtr, BDD_BeadIndex expr,
			      BDD_ValueAssignment* assignPtr);
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);







>







127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
extern BDDAPI BDD_BeadIndex BDD_MakeBead(BDD_System* sysPtr,
					 BDD_VariableIndex level,
					 BDD_BeadIndex low,
					 BDD_BeadIndex high);
extern BDDAPI void BDD_IncrBeadRefCount(BDD_System* sysPtr, 
					BDD_BeadIndex bead);
extern BDDAPI void BDD_UnrefBead(BDD_System* sysPtr, BDD_BeadIndex bead);
extern BDDAPI BDD_BeadIndex BDD_GarbageCollect(BDD_System* sysPtr);
extern BDDAPI BDD_BeadIndex BDD_NthVariable(BDD_System* sysPtr,
					    BDD_VariableIndex n);
extern BDDAPI BDD_BeadIndex BDD_NotNthVariable(BDD_System* sysPtr,
					       BDD_VariableIndex n);
extern BDDAPI int BDD_Literal(BDD_System* sysPtr, BDD_BeadIndex expr,
			      BDD_ValueAssignment* assignPtr);
extern BDDAPI BDD_BeadIndex BDD_Negate(BDD_System* sysPtr, BDD_BeadIndex u);

Changes to generic/tclBdd.c.

81
82
83
84
85
86
87
















88
89
90
91
92
93
94
..
97
98
99
100
101
102
103


104
105
106
107
108
109
110
...
113
114
115
116
117
118
119


120
121
122
123
124
125
126
...
158
159
160
161
162
163
164







165
166
167
168
169
170
171
...
197
198
199
200
201
202
203







204
205
206
207
208
209
210
...
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
...
288
289
290
291
292
293
294

295
296
297
298
299
300
301
...
305
306
307
308
309
310
311






















312
313
314
315
316
317
318
...
332
333
334
335
336
337
338

339




340
341
342
343
344
345
346
...
384
385
386
387
388
389
390













391
392
393
394
395
396
397
...
525
526
527
528
529
530
531








































































































532
533
534
535
536
537
538
....
1061
1062
1063
1064
1065
1066
1067















































1068
1069
1070
1071
1072
1073
1074
....
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
....
1587
1588
1589
1590
1591
1592
1593

1594
1595
1596

1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
 */
typedef struct MethodTableRow {
    const char* name;		/* Name of the method */
    const Tcl_MethodType* type;	/* Type of the method */
    ClientData clientData;	/* Client data */
} MethodTableRow;

















/*
 * Static functions defined within this file
 */

static void SetNamedExpression(BddSystemData*, Tcl_Obj*, BDD_BeadIndex);
static Tcl_HashEntry* FindHashEntryForNamedExpression(Tcl_Interp*,
						      BddSystemData*,
................................................................................
			       BDD_BeadIndex*);
static int UnsetNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*);
static int CompareValueAssignments(const void* a, const void* b);
static int CompareVariableIndices(const void* a, const void* b);
static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);


static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemComposeMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemCopyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
			       int, Tcl_Obj* const[]);
static int BddSystemForeachSatMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
			 Tcl_Obj* varName, Tcl_Obj* script,
			 BDD_AllSatState* stateVector);
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);


static int BddSystemNegateMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemNotnthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemNthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "CONSTRUCTOR",		   /* name */
    BddSystemConstructor,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};








const static Tcl_MethodType BddSystemBeadindexMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "beadindex",		   /* name */
    BddSystemBeadindexMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemForeachSatMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "foreach_sat",		   /* name */
    BddSystemForeachSatMethod,	   /* callProc */







    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemNegateMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "negate",			   /* name */
    BddSystemNegateMethod,	   /* callProc */
................................................................................
    CloneMethod			   /* method clone proc */
};

/*
 * Method table for the BDD system object
 */

MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },
    { "&3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_AND },
    { ":=",        &BddSystemCopyMethodType,      NULL },
    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
................................................................................
    { "even3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_EVEN },
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },

    { "median" ,   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_MEDIAN },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nand3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                          NULL }
};






















 
/*
 *-----------------------------------------------------------------------------
 *
 * Tclbdd_Init --
 *
 *	Initialize the 'bdd' package
................................................................................

    PerInterpData* pidata;	/* Per-interpreter data for the package */
    Tcl_Obj** literals;		/* Literal pool */
    Tcl_Object curClassObject;	/* Tcl_Object representing a class being
				   initialized */
    Tcl_Class curClass;		/* Tcl_Class representing a class being
				   initialized */

    MethodTableRow* methodPtr;	/* Current row in the method table */




    int i;

    if (Tcl_InitStubs(interp, TCL_VERSION, 0) == NULL) {
	return TCL_ERROR;
    }
    if (Tcl_TomMath_InitStubs(interp, TCL_VERSION) == NULL) {
	return TCL_ERROR;
................................................................................
					  &BddSystemConstructorType,
					  (ClientData) pidata));
    IncrPerInterpRefCount(pidata);
    for (methodPtr = systemMethodTable; methodPtr->name != NULL; ++methodPtr) {
	Tcl_NewMethod(interp, curClass, Tcl_NewStringObj(methodPtr->name, -1),
		      1, methodPtr->type, methodPtr->clientData);
    }













    /* Provide the package */

    if (Tcl_PkgProvideEx(interp, PACKAGE_NAME, PACKAGE_VERSION,
			 ( ClientData) NULL) == TCL_ERROR) {
	DecrPerInterpRefCount(pidata);
	return TCL_ERROR;
    }
................................................................................
    if (FindNamedExpression(interp, sdata, objv[skipped],
			    &beadIndex) != TCL_OK) {
	return TCL_ERROR;
    }
    Tcl_SetObjResult(interp, Tcl_NewWideIntObj(beadIndex));
    return TCL_OK;
}








































































































 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemBinopMethod --
 *
 *	Computes a binary operation between two expressions in a BDD system
................................................................................
    DecrBddSystemDataRefCount(sdata);
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *















































 * BddSystemNegateMethod --
 *
 *	Computes the negation of a named expression in a system of
 *	BDD's and assigns it a name
 *
 * Usage:
 *	$system negate result operand
................................................................................
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemUnsetMethod --
 *
 *	Forgets a named expression
 *
 * Usage:
 *	$system unset name
 *
 * Parameters:
 *	name - Name of the expression
 *
................................................................................
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */


    /* Check syntax */


    if (objc != skipped+1) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name");
	return TCL_ERROR;
    }
    UnsetNamedExpression(interp, sdata, objv[skipped]);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * CloneBddSystemObject --







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
>







 







>
>







 







>
>
>
>
>
>
>







 







>
>
>
>
>
>
>







 







|







 







>







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
|
>
>
>
>







 







>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







|







 







>
|
<
<
>
|
<
<

<







81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
...
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
...
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
...
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
...
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
...
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
...
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
...
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
...
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
...
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
...
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
....
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
....
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
....
1813
1814
1815
1816
1817
1818
1819
1820
1821


1822
1823


1824

1825
1826
1827
1828
1829
1830
1831
 */
typedef struct MethodTableRow {
    const char* name;		/* Name of the method */
    const Tcl_MethodType* type;	/* Type of the method */
    ClientData clientData;	/* Client data */
} MethodTableRow;

/*
 * Row in a quantifier table
 */
typedef struct QuantifierTableRow {
    const char* name;		/* Name of the quantifier */
    BDD_Quantifier quant;	/* Quantifier */
} QuantifierTableRow;

/*
 * Row in a binary operator table
 */
typedef struct BinOpTableRow {
    const char* name;		/* Name of the operator */
    BDD_BinOp op;		/* Operator */
} BinOpTableRow;

/*
 * Static functions defined within this file
 */

static void SetNamedExpression(BddSystemData*, Tcl_Obj*, BDD_BeadIndex);
static Tcl_HashEntry* FindHashEntryForNamedExpression(Tcl_Interp*,
						      BddSystemData*,
................................................................................
			       BDD_BeadIndex*);
static int UnsetNamedExpression(Tcl_Interp*, BddSystemData*, Tcl_Obj*);
static int CompareValueAssignments(const void* a, const void* b);
static int CompareVariableIndices(const void* a, const void* b);
static void DeletePerInterpData(PerInterpData*);
static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemAppquantMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				   int, Tcl_Obj* const[]);
static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				int, Tcl_Obj* const[]);
static int BddSystemComposeMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				  int, Tcl_Obj* const[]);
static int BddSystemCopyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
			       int, Tcl_Obj* const[]);
static int BddSystemForeachSatMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				     int, Tcl_Obj *const[]);
static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
			 Tcl_Obj* varName, Tcl_Obj* script,
			 BDD_AllSatState* stateVector);
static int ForeachSatPost(ClientData data[4], Tcl_Interp*, int);
static int BddSystemGCMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
			     int, Tcl_Obj *const[]);
static int BddSystemNegateMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemNotnthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				    int, Tcl_Obj* const[]);
static int BddSystemNthvarMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
				 int, Tcl_Obj* const[]);
static int BddSystemQuantifyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
................................................................................
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "CONSTRUCTOR",		   /* name */
    BddSystemConstructor,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};

const static Tcl_MethodType BddSystemAppquantMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "appquant",			   /* name */
    BddSystemAppquantMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemBeadindexMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "beadindex",		   /* name */
    BddSystemBeadindexMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
................................................................................
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemForeachSatMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "foreach_sat",		   /* name */
    BddSystemForeachSatMethod,	   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemGCMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "gc",			   /* name */
    BddSystemGCMethod,		   /* callProc */
    DeleteMethod,		   /* method delete proc */
    CloneMethod			   /* method clone proc */
};
const static Tcl_MethodType BddSystemNegateMethodType = {
    TCL_OO_METHOD_VERSION_CURRENT, /* version */
    "negate",			   /* name */
    BddSystemNegateMethod,	   /* callProc */
................................................................................
    CloneMethod			   /* method clone proc */
};

/*
 * Method table for the BDD system object
 */

const static MethodTableRow systemMethodTable[] = {
    { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
    { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },
    { "&3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_AND },
    { ":=",        &BddSystemCopyMethodType,      NULL },
    { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
    { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
    { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
................................................................................
    { "even3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_EVEN },
    { "exists",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_EXISTS },
    { "forall",	   &BddSystemQuantifyMethodType,  
      					        (ClientData) BDD_QUANT_FORALL },
    { "foreach_sat",
                   &BddSystemForeachSatMethodType,NULL },
    { "gc",        &BddSystemGCMethodType,        NULL },
    { "median" ,   &BddSystemTernopMethodType, (ClientData) BDD_TERNOP_MEDIAN },
    { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
    { "nand3",     &BddSystemTernopMethodType,   (ClientData) BDD_TERNOP_NAND },
    { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
    { "nor3",      &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_NOR },
    { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
    { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
    { "twoof3",    &BddSystemTernopMethodType,  (ClientData) BDD_TERNOP_TWOOF },
    { "unset",     &BddSystemUnsetMethodType,     NULL },
    { "|",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_OR },
    { "|3",        &BddSystemTernopMethodType,    (ClientData) BDD_TERNOP_OR },
    { "~",         &BddSystemNegateMethodType,    NULL },
    { NULL,	   NULL,                          NULL }
};

const static QuantifierTableRow QuantifierTable[] = {
    {  "exists", BDD_QUANT_EXISTS  },
    {  "forall", BDD_QUANT_FORALL  },
    /* "unique", BDD_QUANT_UNIQUE */
    {  NULL,     0                 }
};

const static BinOpTableRow BinOpTable[] = {
    { "!=",   BDD_BINOP_NE   },
    { "&",    BDD_BINOP_AND  },
    { "<",    BDD_BINOP_LT   },
    { "<=",   BDD_BINOP_LE   },
    { "==",   BDD_BINOP_EQ   },
    { ">",    BDD_BINOP_GT   },
    { ">=",   BDD_BINOP_GE   },
    { "^",    BDD_BINOP_XOR  },
    { "nand", BDD_BINOP_NAND },
    { "nor",  BDD_BINOP_NOR  },
    { "|",    BDD_BINOP_OR   },
    { NULL,   0              }
};
 
/*
 *-----------------------------------------------------------------------------
 *
 * Tclbdd_Init --
 *
 *	Initialize the 'bdd' package
................................................................................

    PerInterpData* pidata;	/* Per-interpreter data for the package */
    Tcl_Obj** literals;		/* Literal pool */
    Tcl_Object curClassObject;	/* Tcl_Object representing a class being
				   initialized */
    Tcl_Class curClass;		/* Tcl_Class representing a class being
				   initialized */
    const MethodTableRow* methodPtr;
				/* Current row in the method table */
    const QuantifierTableRow* quantPtr;
				/* Current row in the quantifier table */
    const BinOpTableRow* opPtr;	/* Current row in the operator table */
    Tcl_Obj* nameObj;		/* Name of an "apply-and-quantify" method */
    int i;

    if (Tcl_InitStubs(interp, TCL_VERSION, 0) == NULL) {
	return TCL_ERROR;
    }
    if (Tcl_TomMath_InitStubs(interp, TCL_VERSION) == NULL) {
	return TCL_ERROR;
................................................................................
					  &BddSystemConstructorType,
					  (ClientData) pidata));
    IncrPerInterpRefCount(pidata);
    for (methodPtr = systemMethodTable; methodPtr->name != NULL; ++methodPtr) {
	Tcl_NewMethod(interp, curClass, Tcl_NewStringObj(methodPtr->name, -1),
		      1, methodPtr->type, methodPtr->clientData);
    }
    for (quantPtr = QuantifierTable; quantPtr->name != NULL; ++quantPtr) {
	for (opPtr = BinOpTable; opPtr->name != NULL; ++opPtr) {
	    nameObj = Tcl_NewStringObj(quantPtr->name, -1);
	    Tcl_AppendToObj(nameObj, "_", -1);
	    Tcl_AppendToObj(nameObj, opPtr->name, -1);
	    Tcl_IncrRefCount(nameObj);
	    Tcl_NewMethod(interp, curClass, nameObj, 1,
			  &BddSystemAppquantMethodType,
			  (ClientData) (size_t) ((quantPtr->quant<<4)
						 | (opPtr->op)));
	}
    }

    /* Provide the package */

    if (Tcl_PkgProvideEx(interp, PACKAGE_NAME, PACKAGE_VERSION,
			 ( ClientData) NULL) == TCL_ERROR) {
	DecrPerInterpRefCount(pidata);
	return TCL_ERROR;
    }
................................................................................
    if (FindNamedExpression(interp, sdata, objv[skipped],
			    &beadIndex) != TCL_OK) {
	return TCL_ERROR;
    }
    Tcl_SetObjResult(interp, Tcl_NewWideIntObj(beadIndex));
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemAppquantMethod --
 *
 *	Applies a binary operation to a pair of BDD's, then applies a
 *	quantification over a set of variables to the result.
 *
 * Usage:
 *	$system ${quant}_${op} $result $vars $expr1 $expr2
 *
 * Parameters:
 *	system - System of BDD's
 *	quant  - 'exists' or 'forall' according to which quantification
 *               is desired
 *	op     - One of the binary operators !=, &, <, <=, ==, >. >=,
 *               ^, nand, nor, and |
 *      result - Name to be assigned to the resulting BDD.
 *	vars   - List of names of variables to quantify over
 *	expr1  - Left operand
 *	expr2  - Rught operand
 */

static int
BddSystemAppquantMethod(
    ClientData clientData,	/* unused */
    Tcl_Interp* interp,		/* Tcl interpreter */
    Tcl_ObjectContext ctx,	/* Object context */
    int objc,			/* Parameter count */
    Tcl_Obj *const objv[])	/* Parameter vector */
{
    BDD_Quantifier q = (BDD_Quantifier) ((size_t)clientData >> 4);
				/* The quantifier to apply */
    BDD_BinOp op = (BDD_BinOp) ((size_t) clientData & 0xF);
				/* The operation to apply */
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */
    BDD_BeadIndex u1;		/* The left operand */
    BDD_BeadIndex u2;		/* The right operand */
    int varc;			/* Count of supplied variable names */
    Tcl_Obj** varv;		/* List of variable names supplied */
    BDD_VariableIndex* v;	/* Variables to quantify */
    BDD_BeadIndex literalIndex;	/* Index of the current variable as a BDD */
    BDD_ValueAssignment a;	/* Current quantified variable */
    Tcl_Obj* errorMessage;	/* Error message for a failed execution */
    BDD_BeadIndex result;	/* Result of the operation */
    BDD_VariableIndex i;

    /* Check syntax */

    if (objc != skipped+4) {
	Tcl_WrongNumArgs(interp, skipped, objv, "name vars expr");
	return TCL_ERROR;
    }
    if (FindNamedExpression(interp, sdata, objv[skipped+2],
			    &u1) != TCL_OK
	|| FindNamedExpression(interp, sdata, objv[skipped+3],
			       &u2) != TCL_OK) {
	return TCL_ERROR;
    }
    if (Tcl_ListObjGetElements(interp, objv[skipped+1],
			       &varc, &varv) != TCL_OK) {
	return TCL_ERROR;
    }
    v = ckalloc(varc * sizeof(BDD_VariableIndex));
    for (i = 0; i < varc; ++i) {
	if (FindNamedExpression(interp, sdata, varv[i],
				&literalIndex) != TCL_OK) {
	    ckfree(v);
	    return TCL_ERROR;
	}
	if (!BDD_Literal(sdata->system, literalIndex, &a)
	    || (a.value == 0)) {
	    errorMessage = Tcl_ObjPrintf("%s is not a variable",
					 Tcl_GetString(varv[i]));
	    Tcl_SetObjResult(interp, errorMessage);
	    Tcl_SetErrorCode(interp, "BDD", "NotVariable",
			     Tcl_GetString(varv[i]), NULL);
	    ckfree(v);
	    return TCL_ERROR;
	}	    
	v[i] = a.var;
    }

    /*
     * Order the literals
     */
    qsort(v, varc, sizeof(BDD_VariableIndex), CompareVariableIndices);

    /*
     * Do the combined operation and quantification
     */
    result = BDD_ApplyAndQuantify(sdata->system, q, varc, v, op, u1, u2);
    ckfree(v);
    SetNamedExpression(sdata, objv[skipped], result);
    BDD_UnrefBead(sdata->system, result);
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemBinopMethod --
 *
 *	Computes a binary operation between two expressions in a BDD system
................................................................................
    DecrBddSystemDataRefCount(sdata);
    return result;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemGCMethod --
 *
 *	Asks the BDD engine to perform a garbage collection.
 *
 * Usage:
 *	$system gc
 *
 * Parameters:
 *	system - System of BDD's.
 *
 * Results:
 *	Returns the number of allocated beads after the garbage collection.
 *
 *-----------------------------------------------------------------------------
 */

static int
BddSystemGCMethod(
    ClientData clientData,	/* Operation to perform */
    Tcl_Interp* interp,		/* Tcl interpreter */
    Tcl_ObjectContext ctx,	/* Object context */
    int objc,			/* Parameter count */
    Tcl_Obj *const objv[])	/* Parameter vector */
{
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */
    BDD_BeadIndex beadCount;	/* Number of allocated beads after GC */
    
    if (objc != skipped) {
	Tcl_WrongNumArgs(interp, skipped, objv, "");
	return TCL_ERROR;
    }

    beadCount = BDD_GarbageCollect(sdata->system);

    Tcl_SetObjResult(interp, Tcl_NewWideIntObj(beadCount));
    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemNegateMethod --
 *
 *	Computes the negation of a named expression in a system of
 *	BDD's and assigns it a name
 *
 * Usage:
 *	$system negate result operand
................................................................................
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * BddSystemUnsetMethod --
 *
 *	Forgets a set of named expressions
 *
 * Usage:
 *	$system unset name
 *
 * Parameters:
 *	name - Name of the expression
 *
................................................................................
    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
				/* The current object */
    BddSystemData* sdata = (BddSystemData*)
	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
				/* The current system of expressions */
    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
				/* The number of args used in method dispatch */
    int i;
    


    for (i = skipped; i < objc; ++i) {
	UnsetNamedExpression(NULL, sdata, objv[i]);


    }

    return TCL_OK;
}
 
/*
 *-----------------------------------------------------------------------------
 *
 * CloneBddSystemObject --

Changes to tests/bdd.test.

147
148
149
150
151
152
153

154




155
156
157
158
159
160



161




162
163
164
165
166
167
168
169


170


171
172
173
174
175
176
177
178
179
180
...
188
189
190
191
192
193
194

195


196
197
198
199
200
201
202
203
204

205
206
207
208
209
210
211
212
213
214

215
216
217
218
219
220
221
222
223
224
...
238
239
240
241
242
243
244


245


246
247
248
249
250
251
252
253
254
...
258
259
260
261
262
263
264


265


266
267
268
269
270
271
272
273
274


275


276
277
278
279
280
281
282
283
284
...
322
323
324
325
326
327
328


329
330
331
332
333
334
335
336
337
338
339
...
344
345
346
347
348
349
350


351
352
353
354
355
356
357
358
359
360
361
...
366
367
368
369
370
371
372


373
374
375
376
377
378
379
380
381
382
383
...
388
389
390
391
392
393
394


395
396
397
398
399
400
401
402
403
404
405
...
410
411
412
413
414
415
416


417
418
419
420
421
422
423
424
425
426
427
...
428
429
430
431
432
433
434
435
436
437
438


439
440
441
442
443
444
445
446
447
448
449
...
454
455
456
457
458
459
460


461
462
463
464
465
466
467
468
469
470
471
...
476
477
478
479
480
481
482


483
484
485
486
487
488
489
490
491
492
493
...
498
499
500
501
502
503
504


505
506
507
508
509
510
511
512
513
514
515
...
520
521
522
523
524
525
526


527
528
529
530
531
532
533
534
535
536
537
...
547
548
549
550
551
552
553
554



555
556
557
558
559
560
561
562
563
564
565
566
567
568
569


570
571
572
573
574
575
576
577
578
...
579
580
581
582
583
584
585
586


587
588
589
590
591
592
593
594
595
...
596
597
598
599
600
601
602
603


604
605
606
607
608
609
610
611
612
...
614
615
616
617
618
619
620
621


622
623
624
625
626
627
628
629
630
...
632
633
634
635
636
637
638
639


640
641
642
643
644
645
646
647
648
...
650
651
652
653
654
655
656
657


658
659
660
661
662
663
664
665
666
...
677
678
679
680
681
682
683

684

685
686
687
688
689
690

691

692
693
694
695
696
697
698


699
700
701
702
703
704
705


706
707
708
709
710
711
712


713
714
715
716
717
718
719
720
721
722
723
724
725

726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744

745
746
747
748
749
750
751
752
753
754
755
756
...
767
768
769
770
771
772
773
774


775
776
777
778
779
780
781
782
783
784
785
786
...
790
791
792
793
794
795
796

797





798
799
800
801
802
803
804
805
806
807
808
809
...
872
873
874
875
876
877
878
879


880
881
882
883
884
885
886
887
888
889
...
890
891
892
893
894
895
896
897


898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914


915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931


932
933
934
935
936
937
938
939
940
941
...
942
943
944
945
946
947
948
949


950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968


969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985


986
987
988
989
990
991
992
993
994
995
....
1072
1073
1074
1075
1076
1077
1078


1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
....
1095
1096
1097
1098
1099
1100
1101


1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
....
1118
1119
1120
1121
1122
1123
1124


1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
....
1146
1147
1148
1149
1150
1151
1152
1153



1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183


1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207

1208
1209
1210
1211
1212
1213
1214
1215
1216
1217


1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
....
1411
1412
1413
1414
1415
1416
1417


1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
....
1430
1431
1432
1433
1434
1435
1436


1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
....
1454
1455
1456
1457
1458
1459
1460


1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
....
1478
1479
1480
1481
1482
1483
1484


1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
....
1500
1501
1502
1503
1504
1505
1506
1507


1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
....
1522
1523
1524
1525
1526
1527
1528
1529


1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
....
1573
1574
1575
1576
1577
1578
1579

1580
1581



1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597

1598
1599



1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
....
1613
1614
1615
1616
1617
1618
1619
1620


1621
1622
1623
1624
1625
1626
1627
1628
1629
....
1641
1642
1643
1644
1645
1646
1647
1648


1649
1650
1651
1652
1653
1654
1655
1656
1657
....
1669
1670
1671
1672
1673
1674
1675
1676


1677
1678
1679

1680
1681
1682
1683
1684
1685
1686
....
1691
1692
1693
1694
1695
1696
1697
1698


1699
1700
1701
1702
1703
1704
1705
1706
1707
....
1714
1715
1716
1717
1718
1719
1720
1721


1722
1723
1724
1725
1726
1727
1728
1729
1730
....
1736
1737
1738
1739
1740
1741
1742
1743


1744
1745
1746

1747
1748
1749
1750
1751
1752
1753
....
1759
1760
1761
1762
1763
1764
1765
1766


1767
1768
1769
1770
1771
1772
1773
1774
1775
....
1786
1787
1788
1789
1790
1791
1792
1793


1794
1795
1796
1797
1798
1799
1800
1801
1802
....
1813
1814
1815
1816
1817
1818
1819
1820


1821
1822
1823
1824
1825
1826
1827
1828
1829
....
1835
1836
1837
1838
1839
1840
1841
1842


1843
1844
1845
1846
1847
1848
1849
1850
1851
....
1858
1859
1860
1861
1862
1863
1864
1865


1866
1867
1868
1869
1870
1871
1872
1873
1874
....
1885
1886
1887
1888
1889
1890
1891
1892


1893
1894
1895
1896
1897
1898
1899
1900
1901
....
1907
1908
1909
1910
1911
1912
1913
1914


1915
1916
1917
1918
1919
1920
1921
1922
1923
....
1957
1958
1959
1960
1961
1962
1963
1964

1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979

1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993

1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007

2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023


2024
2025
2026
2027
2028
2029
2030
2031
2032
2033
....
2034
2035
2036
2037
2038
2039
2040
2041


2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
....
2052
2053
2054
2055
2056
2057
2058
2059


2060
2061
2062
2063
2064
2065
2066
2067
2068
2069
....
2070
2071
2072
2073
2074
2075
2076
2077


2078
2079
2080
2081
2082
2083
2084
2085
2086
2087
....
2093
2094
2095
2096
2097
2098
2099


2100
2101
2102
2103
2104
2105
2106
2107
2108
2109
2110
....
2114
2115
2116
2117
2118
2119
2120
2121
2122
2123
2124


2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141


2142
2143
2144
2145
2146
2147
2148
2149
2150
....
2155
2156
2157
2158
2159
2160
2161
2162


2163
2164
2165
2166
2167
2168
2169
2170
2171
....
2176
2177
2178
2179
2180
2181
2182
2183


2184
2185
2186
2187
2188
2189
2190
2191
2192
2193
2194
2195
2196
2197
2198
2199
2200
2201
2202
2203


2204
2205
2206



























































2207
2208
2209
2210
2211
2212
2213
....
2231
2232
2233
2234
2235
2236
2237

2238
2239
2240
2241
2242
2243
2244
2245
2246
2247
2248
2249

2250
2251
2252
2253
2254
2255
2256
....
2264
2265
2266
2267
2268
2269
2270

2271
2272
2273

2274
2275
2276
2277

2278
2279
2280
2281
2282

2283
2284
2285
2286
2287
2288
2289
2290
2291
2292

2293


2294
2295
2296
2297
2298
2299
2300
2301
2302








2303
2304
2305
2306
2307
2308
2309
2310
2311
2312
2313
2314
....
2359
2360
2361
2362
2363
2364
2365
2366



2367
2368
2369
2370
2371
2372
2373
2374
2375
2376
2377
    -cleanup {rename sys {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}

test bdd-6.3 {nthvar - var 0} {
    -setup {bdd::system create sys}

    -body {sys nthvar a 0; sys dump a}




    -cleanup {rename sys {}}
    -result {2 {0 0 1} 0 {1 0 0} 1 {1 1 1}}
}

test bdd-6.4 {nthvar - two vars} {
    -setup {bdd::system create sys}



    -body {sys nthvar a 0; sys nthvar b 1; list [sys dump b] [sys dump a]}




    -cleanup {rename sys {}}
    -result {{3 {1 0 1} 0 {2 0 0} 1 {2 1 1}} {2 {0 0 1} 0 {2 0 0} 1 {2 1 1}}}
}

test bdd-6.5 {nthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 0


	list [sys beadindex a] [sys beadindex b] [sys beadindex c]


    }
    -cleanup {rename sys {}}
    -result {2 3 2}
}

test bdd-7.1 {notnthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys notnthvar}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
    -cleanup {rename sys {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}

test bdd-7.3 {notnthvar - var 0} {
    -setup {bdd::system create sys}

    -body {sys notnthvar !a 0; sys dump !a}


    -cleanup {rename sys {}}
    -result {2 {0 1 0} 1 {1 1 1} 0 {1 0 0}}
}

test bdd-7.4 {notnthvar - two vars} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1
	list [sys dump !b] [sys dump !a]

    }
    -cleanup {rename sys {}}
    -result {{3 {1 1 0} 1 {2 1 1} 0 {2 0 0}} {2 {0 1 0} 1 {2 1 1} 0 {2 0 0}}}
}

test bdd-7.5 {nthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1; sys notnthvar !c 0
	list [sys beadindex !a] [sys beadindex !b] [sys beadindex !c]

    }
    -cleanup {rename sys {}}
    -result {2 3 2}
}

test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
}

test bdd-8.3 {negate 0} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }


    -body {sys ~ b 0; sys beadindex b}


    -cleanup {rename sys {}}
    -result 1
}

test bdd-8.4 {negate 1} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
................................................................................
}

test bdd-8.5 {negate a} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }


    -body {sys ~ b a; expr {[sys beadindex b] == [sys beadindex !a]}}


    -cleanup {rename sys {}}
    -result 1
}

test bdd-8.5 {negate !a} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }


    -body {sys ~ b !a; expr {[sys beadindex b] == [sys beadindex a]}}


    -cleanup {rename sys {}}
    -result 1
}

test bdd-9.1 {binop - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nand}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys nor c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys nor c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys nor c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {0001 0010 0100 1000}
}

test bdd-9.5 {binary < operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys < c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys < c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys < c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {0100 1000 0001 0010}
}

test bdd-9.6 {binary > operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys > c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys > c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys > c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {0010 0001 1000 0100}
}

test bdd-9.7 {binary ^ operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {0110 1001 1001 0110}
}

test bdd-9.8 {binary nand operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys nand c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys nand c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys nand c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {0111 1011 1101 1110}
}
test bdd-9.9 {binary & operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
................................................................................
    -body {
	set tables {}
	sys & c !a !b
	lappend tables [truthtable [sys dump c] 2]
	sys & c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys & c !a b

	lappend tables [truthtable [sys dump c] 2]
	sys & c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {1000 0100 0010 0001}
}

test bdd-9.10 {binary == operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys == c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys == c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys == c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result  {1001 0110 0110 1001}
}

test bdd-9.11 {binary <= operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys <= c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys <= c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys <= c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {1101 1110 0111 1011}
}

test bdd-9.12 {binary >= operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys >= c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys >= c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys >= c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {1011 0111 1110 1101}
}

test bdd-9.13 {binary | operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys | c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys | c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys | c a b
	lappend tables [truthtable [sys dump c] 2]


	set tables
    }
    -cleanup {rename sys {}}
    -result {1110 1101 1011 0111}
}

test bdd-10.1 {syllogism in the mode of barbara} {
    -setup {
	bdd::system create sys
	sys nthvar man(x) 0
	sys nthvar mortal(x) 1
................................................................................
	sys <= test1 minor conclusion;    # does the minor premise imply
	;			          # the conclusion?
	sys <= test2 conjunct conclusion; # is the syllogism valid?
	list \
	    [expr {[sys beadindex test0] == 1}] \
	    [expr {[sys beadindex test1] == 1}] \
	    [expr {[sys beadindex test2] == 1}] \
	    [truthtable [sys dump conjunct] 3]



    } 
    -cleanup {rename sys {}}
    -result {0 0 1 10110001}
}

test bdd-11.1 {demorgan} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys & c a b
	sys nor d !a !b
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-11.2 {demorgan} {
    -setup {
................................................................................
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys | c a b
	sys nand d !a !b
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-11.3 {demorgan} {
    -setup {
................................................................................
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys ^ c a b
	sys ^ d !a !b
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-11.4 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys & c a b
	sys | d !a !b
	sys ~ d d
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-11.5 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys | c a b
	sys & d !a !b
	sys ~ d d
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-11.6 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys ^ c a b
	sys == d !a !b
	sys ~ d d
	expr {[sys beadindex c] == [sys beadindex d]}


    }
    -result 1
    -cleanup {
	rename sys {}
   }
}

test bdd-12.1 {satcount - wrong # args} {
    -setup {bdd::system create sys}
................................................................................
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-12.3 {satcount - zero} {
    -setup {bdd::system create sys}

    -body {sys satcount 0}

    -cleanup {rename sys {}}
    -result 0
}
    
test bdd-12.4 {satcount - no vars} {
    -setup {bdd::system create sys}

    -body {sys satcount 1}

    -cleanup {rename sys {}}
    -result 1
}

test bdd-12.5 {satcount - one var} {
    -setup {bdd::system create sys; sys nthvar a 0}
    -body {sys satcount 1}


    -cleanup {rename sys {}}
    -result 2
}

test bdd-12.6 {satcount - two vars} {
    -setup {bdd::system create sys; sys nthvar a 1}
    -body {sys satcount 1}


    -cleanup {rename sys {}}
    -result 4
}

test bdd-12.7 {satcount - three vars} {
    -setup {bdd::system create sys; sys nthvar a 2}
    -body {sys satcount 1}


    -cleanup {rename sys {}}
    -result 8
}

test bdd-12.8 {satcount - one var of three} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
	list [sys satcount a] [sys satcount b] [sys satcount c]

    }
    -cleanup {
	rename sys {}
    }
    -result {4 4 4}
}

test bdd-12.9 {satcount - two vars of three} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
	sys | r1 a b
	sys | r2 a c
	sys | r3 b c
	list [sys satcount r1] [sys satcount r2] [sys satcount r3]

    }
    -cleanup {
	rename sys {}
    }
    -result {6 6 6}
}

test bdd-12.10 {satcount - complex expr} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys & r2 c d
	sys | r2 r2 e
	sys & r1 r1 r2
	sys | r2 f g
	sys | r2 r2 h
	sys & r1 r1 r2
	sys ~ r2 r1
	list [sys satcount r1] [sys satcount r2]


    }
    -cleanup {
	rename sys {}
    }
    -result {210 302}
}

test bdd-12.11 {satcount - parity tree} {
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 128} {incr i} {
	    sys nthvar v$i $i
................................................................................
	sys := r0 0
	for {set i 0} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	for {set i 1} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}

	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]





    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000}
}

test bdd-13.1 {restrict - wrong # args} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2
	expr {[sys beadindex r1] == [sys beadindex r2]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.6 {restrict by literal} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 !b
	sys ^ r3 a c 
	expr {[sys beadindex r1] == [sys beadindex r3]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.7 {restrict by two literals} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 a c
	expr {[sys beadindex r1] == [sys beadindex b]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.8 {restrict by two disordered literals} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 c a
	expr {[sys beadindex r1] == [sys beadindex b]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-13.9 {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys nthvar c 2
    }
    -body {
	sys & r1 a b
	sys & r1 r1 c
	sys restrict r1 r1 a b
	sys restrict r2 r1 c
	sys beadindex r2


    }
    -cleanup {
	rename sys {}
    }
    -result 1
}

test bdd-13.10 {restrict zero} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 0 a c
	sys beadindex r1


    }
    -cleanup {rename sys {}}
    -result 0
}

test bdd-13.11 {restrict one} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 1 a c
	sys beadindex r1


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-14.1 {foreach_sat - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
................................................................................
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    lappend result $x
	}


	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1} {0 0 1 1 2 1} {0 1}}
}

test bdd-14.7 {foreach_sat - continue} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
................................................................................
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    if {[dict exists $x 3]} continue
	    lappend result $x
	}


	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 1 2 1} {0 1}}
}

test bdd-14.8 {foreach_sat - break} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
................................................................................
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    if {![dict exists $x 3]} break
	    lappend result $x
	}


	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1}}
}

test bdd-14.9 {foreach_sat - return} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	proc bdd-14.9 {} {
................................................................................
	}
    }
    -body {
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	bdd-14.9



    }
    -cleanup {
	rename sys {}
	rename bdd-14.9 {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1}}
}

test bdd-14.10 {foreach_sat - error} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
    -body {
	set result {}
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	list \
	    [catch {
		sys foreach_sat x z {
		    if {![dict exists $x 3]} {
			error testing
		    }
		    lappend result $x
		}
	    } result] \
	    $result \
	    $::errorInfo


    }
    -cleanup {
	rename sys {}
    }
    -match glob
    -result {1 testing {testing
    while executing
"error testing"
   ('foreach_sat' body, line 3)
    invoked from within
*}}
}

test bdd-14.11 {foreach_sat - unusual return} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
    -body {
	set result {}
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d

	list \
	    [catch {
		sys foreach_sat x z {
		    if {![dict exists $x 3]} {
			return -code 6 -level 0 testing
		    }
		    lappend result $x
		}
	    } result] \
	    $result


    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing}
}

test bdd-15.1.1 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
................................................................................
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys exists z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}


	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1}
}

test bdd-15.8.2 {quantifiers - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys forall z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}


	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1}
}

test bdd-15.9.1 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys exists z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}


	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1}
}

test bdd-15.9.2 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys forall z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}


	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1}
}

test bdd-15.10 {existential quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
................................................................................
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys | ye a b
	sys | ye ye c
	sys | ye ye d
	sys exists ze {e f} expr
	expr {[sys beadindex ze] == [sys beadindex ye]}


    }
    -cleanup {rename sys {}}
    -result {1}
}

test bdd-15.11 {universal quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
................................................................................
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys & yu a b
	sys & yu yu c
	sys & yu yu d
	sys forall zu {e f} expr
	expr {[sys beadindex zu] == [sys beadindex yu]}


    }
    -cleanup {rename sys {}}
    -result {1}
}

foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.1-$operation "$operation - wrong # args" {*}{
	-setup {
................................................................................
    test bdd-16.3-$operation {$operation - bad second expr} {*}{
	-setup {
	    bdd::system create sys
	    sys nthvar a 0; sys notnthvar !a 0
	    sys nthvar b 0; sys notnthvar !b 0
	    sys nthvar c 0; sys notnthvar !c 0
	}

	-body {list [catch {sys $operation z a garbage c} result] \
		   $result $::errorCode}



	-cleanup {rename sys {}}
	-result \
	    {1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
    }
}

foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.4-$operation {$operation - bad third expr} {*}{
	-setup {
	    bdd::system create sys
	    sys nthvar a 0; sys notnthvar !a 0
	    sys nthvar b 0; sys notnthvar !b 0
	    sys nthvar c 0; sys notnthvar !c 0
	}

	-body {list [catch {sys $operation z a b garbage} result] \
		   $result $::errorCode}



	-cleanup {rename sys {}}
	-result \
	    {1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
    }
}

test bdd-16.5 {ternary nor} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & r c f
    }
    -body {
	sys nor3 y p q r
	sys | t p q
	sys | t t r
	sys ~ z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.6 {ternary oneof} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & z z !r
	sys & t !p q
	sys & t t !r
	sys | z z t
	sys & t !p !q
	sys & t t r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.7 {ternary twoof} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & z z !r
	sys & t p !q
	sys & t t r
	sys | z z t
	sys & t !p q
	sys & t t r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}

}

test bdd-16.7 {ternary even} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
	sys nthvar d 3; sys nthvar e 4; sys nthvar f 5;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys even3 y p q r
	sys ^ z p q
	sys ^ z z !r
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.8 {ternary differ} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !r r
    }
    -body {
	sys differ3 y p q r
	sys &3 z p q r
	sys &3 t !p !q !r
	sys nor z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.9 {ternary nand} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys nand3 y p q r
	sys &3 z p q r
	sys ~ z z
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}

}

test bdd-16.10 {ternary concurrence} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
	sys nthvar d 3; sys nthvar e 4; sys nthvar f 5;
................................................................................
	sys ~ !r r
    }
    -body {
	sys concur3 y p q r
	sys &3 z p q r
	sys &3 t !p !q !r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.11 {ternary - borrow bit of subtraction} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z !p !q  r
	sys &3 t !p  q !r
	sys | z z t
	sys &3 t !p  q  r
	sys | z z t
	sys &3 t  p  q  r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.12 {ternary - borrow bit of subtraction} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z !p !q  r
	sys &3 t !p  q !r
	sys | z z t
	sys &3 t !p  q  r
	sys | z z t
	sys &3 t  p  q  r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.13 {ternary - xor} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys ^3 y p q r
	sys ^ z p q
	sys ^ z z r
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.14 {ternary - ?:} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !r r
    }
    -body {
	sys ?: y p q r
	sys & z p q
	sys & t !p r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.15 {ternary - median} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z p q !r
	sys &3 t p !q r
	sys | z z t
	sys &3 t !p q r
	sys | z z t
	sys &3 t p q r
	sys | z z t
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-16.16 {ternary - or} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys |3 y p q r
	sys | z p q
	sys | z z r
	expr {[sys beadindex y] == [sys beadindex z]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-17.1 {compose - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
................................................................................

test bdd-17.4 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
    }
    -body {
	list [catch {sys compose x a garbage 0} result] $result $::errorCode

    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-17.5 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys & c a b
    }
    -body {
	list [catch {sys compose x a c 0} result] $result $::errorCode

    }
    -cleanup {rename sys {}}
    -result \
	{1 {c is not a variable} {BDD NotVariable c}}
}

test bdd-17.6 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys notnthvar !b 1
    }
    -body {
	list [catch {sys compose x a !b 0} result] $result $::errorCode

    }
    -cleanup {rename sys {}}
    -result \
	{1 {!b is not a variable} {BDD NotVariable !b}}
}

test bdd-17.7 {compose - bad replacement expr} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
    }
    -body {
	list [catch {sys compose x a b garbage} result] $result $::errorCode

    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-17.8 {compose - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys & c a b
    }
    -body {
	sys compose d c
	expr {[sys beadindex d] == [sys beadindex c]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-17.9 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c p 0
	expr {[sys beadindex d] == [sys beadindex c]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-17.10 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c q 0
	expr {[sys beadindex d] == [sys beadindex c]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-17.10 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c r 0
	expr {[sys beadindex d] == [sys beadindex c]}


    }
    -cleanup {rename sys {}}
    -result 1
}

test bdd-17.11 {compose - replace with constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	    {
		sys compose z c {*}$s
		if {[sys beadindex z] != [sys beadindex $y]} {
		    lappend trouble "a&b\[[lindex $s 1]/[lindex $s 0]] " \
			"should be $y"
		}
	    }


	join $trouble \n
    }
    -cleanup {rename sys {}}
    -result {}
}

test bdd-17.12 {compose - replace with variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0; sys notnthvar !p 0
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & c a b
    }
    -body {
	set trouble {} 
	foreach x {p a q b r} {
	    sys compose d c a $x
	    sys & e $x b
	    if {[sys beadindex d] != [sys beadindex d]} {
		lappend trouble "a&$x should be the same as (a&b)\[$x/b]"
	    }
	}


	join $trouble \n
    }
    -cleanup {rename sys {}}
    -result {}
}

test bdd-17.13 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
	sys nthvar b 2; sys notnthvar !b 2
	sys < c a b
	sys < y b a
    } 
    -body {
	sys compose z c a b b a
	expr {[sys beadindex z] == [sys beadindex y]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-17.14 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & x x t
	sys <= y b c
	sys <= t c a
	sys & y y t
    } 
    -body {
	sys compose z x a b b c c a
	expr {[sys beadindex z] == [sys beadindex y]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-17.15 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & x x t
	sys <= y c a
	sys <= t a b
	sys & y y t
    } 
    -body {
	sys compose z x b a c b a c
	expr {[sys beadindex z] == [sys beadindex y]}


    }
    -result 1
    -cleanup {rename sys {}}
}

test bdd-17.15 {compose - more complex substitution} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
	sys nthvar d 3
	sys | x a b
	sys & t a b
	sys & u c d
	sys | y t u
    } 
    -body {
	sys compose z x a t b u
	expr {[sys beadindex z] == [sys beadindex y]}


    }
    -result 1
    -cleanup {rename sys {}}



























































}

test bdd-21.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
................................................................................
		    if {$col2 != $col} {
			set q2 v[expr {8 * $row + $col2}]
			sys & columnC columnC !$q2
		    }
		}
		sys <= columnC $q1 columnC
		sys & cellC cellC columnC

		
		# queen here <= no other queen in the same row

		sys := rowC 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set q2 v[expr {8 * $row2 + $col}]
			sys & rowC rowC !$q2
		    }
		}
		sys <= rowC $q1 rowC
		sys & cellC cellC rowC


		# queen here <= no other queen in the same diagonal

		sys := diag1C 1
		sys := diag2C 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
................................................................................
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag2C diag2C !$q2
			}
		    }
		}
		sys <= diag1C $q1 diag1C
		sys & cellC cellC diag1C


		sys <= diag2C $q1 diag2C
		sys & cellC cellC diag2C


		# accumulate into the constraint set for the row

		sys & thisRowC thisRowC cellC

	    }

	    # accumulate all constraints for a row into the solution

	    sys & solution solution thisRowC

	}
		
	# at least one queen in each column
	for {set col 0} {$col < 8} {incr col} {
	    sys := columnC 0
	    for {set row 0} {$row < 8} {incr row} {
		set q v[expr {8*$row + $col}]
		sys | columnC columnC $q
	    }
	    sys & solution solution columnC

	}


	sys foreach_sat A solution {
	    set sol [lrepeat 8 {}]
	    foreach {var value} $A {
		if {$value} {
		    lset sol [expr {$var/8}] [expr {$var%8}]
		}
	    }
	    lappend sols [join $sol {}]
	}








	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-21.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
................................................................................
	sys & gate1 x y
	sys ^ gate2 x y
	sys & gate3 gate2 ci
	sys ^ z gate2 ci
	sys | co gate1 gate3

	list [expr {[sys beadindex co] == [sys beadindex spec_co]}] \
	    [expr {[sys beadindex z] == [sys beadindex spec_z]}]



    }
    -cleanup {rename sys {}}
    -result {1 1}
}
		
cleanupTests
return

# Local Variables:
# mode: tcl
# End:







>
|
>
>
>
>

|




>
>
>
|
>
>
>
>

|





|
>
>
|
>
>


|







 







>
|
>
>

|






|
>


|






|
>


|







 







>
>
|
>
>

|







 







>
>
|
>
>

|







>
>
|
>
>

|







 







>
>



|







 







>
>



|







 







>
>



|







 







>
>



|







 







>
>



|







 







<



>
>



|







 







>
>



|







 







>
>



|







 







>
>



|







 







>
>



|







 







|
>
>
>


|











|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







>
|
>

|




>
|
>

|




|
>
>

|




|
>
>

|




|
>
>

|










|
>




|













|
>




|







 







|
>
>




|







 







>
|
>
>
>
>
>




|







 







|
>
>


|







 







|
>
>


|













|
>
>


|













|
>
>


|







 







|
>
>




|













|
>
>


|













|
>
>


|







 







>
>





|







 







>
>





|







 







>
>





|







 







|
>
>
>





|













|
|
|
|
|
|
|
|
|
|
|
>
>










|













>
|
|
|
|
|
|
|
|
|
|
>
>




|







 







>
>



|







 







>
>



|







 







>
>



|







 







>
>



|







 







|
>
>


|







 







|
>
>


|







 







>
|
|
>
>
>


|













>
|
|
>
>
>


|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

<

>







 







|
>
>

|







 







|
>
>

|







 







|
>
>

<

>







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>
>

|







 







|
>



|










|
>



|









|
>



|









|
>



|











|
>
>


|







 







|
>
>


|







 







|
>
>


|







 







|
>
>


|







 







>
>



|







 







|



>
>



|












|
>
>

|







 







|
>
>

|







 







|
>
>

|



|













|
>
>

|

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>












>







 







>



>




>





>










>

>
>









>
>
>
>
>
>
>
>




|







 







|
>
>
>


|

|






147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
...
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
...
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
...
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
...
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
...
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
...
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
...
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
...
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
...
471
472
473
474
475
476
477

478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
...
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
...
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
...
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
...
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
...
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
...
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
...
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
...
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
...
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
...
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
...
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
...
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
...
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
...
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
...
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
....
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
....
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
....
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
....
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
....
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
....
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
....
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
....
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
....
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
....
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
....
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
....
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
....
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
....
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
....
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818

1819
1820
1821
1822
1823
1824
1825
1826
1827
....
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
....
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
....
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891

1892
1893
1894
1895
1896
1897
1898
1899
1900
....
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
....
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
....
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
....
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
....
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
2024
2025
2026
2027
2028
2029
2030
2031
....
2042
2043
2044
2045
2046
2047
2048
2049
2050
2051
2052
2053
2054
2055
2056
2057
2058
2059
2060
....
2066
2067
2068
2069
2070
2071
2072
2073
2074
2075
2076
2077
2078
2079
2080
2081
2082
2083
2084
....
2118
2119
2120
2121
2122
2123
2124
2125
2126
2127
2128
2129
2130
2131
2132
2133
2134
2135
2136
2137
2138
2139
2140
2141
2142
2143
2144
2145
2146
2147
2148
2149
2150
2151
2152
2153
2154
2155
2156
2157
2158
2159
2160
2161
2162
2163
2164
2165
2166
2167
2168
2169
2170
2171
2172
2173
2174
2175
2176
2177
2178
2179
2180
2181
2182
2183
2184
2185
2186
2187
2188
2189
2190
2191
2192
2193
2194
2195
2196
2197
2198
2199
2200
....
2201
2202
2203
2204
2205
2206
2207
2208
2209
2210
2211
2212
2213
2214
2215
2216
2217
2218
2219
2220
....
2221
2222
2223
2224
2225
2226
2227
2228
2229
2230
2231
2232
2233
2234
2235
2236
2237
2238
2239
2240
....
2241
2242
2243
2244
2245
2246
2247
2248
2249
2250
2251
2252
2253
2254
2255
2256
2257
2258
2259
2260
....
2266
2267
2268
2269
2270
2271
2272
2273
2274
2275
2276
2277
2278
2279
2280
2281
2282
2283
2284
2285
....
2289
2290
2291
2292
2293
2294
2295
2296
2297
2298
2299
2300
2301
2302
2303
2304
2305
2306
2307
2308
2309
2310
2311
2312
2313
2314
2315
2316
2317
2318
2319
2320
2321
2322
2323
2324
2325
2326
2327
2328
2329
....
2334
2335
2336
2337
2338
2339
2340
2341
2342
2343
2344
2345
2346
2347
2348
2349
2350
2351
2352
....
2357
2358
2359
2360
2361
2362
2363
2364
2365
2366
2367
2368
2369
2370
2371
2372
2373
2374
2375
2376
2377
2378
2379
2380
2381
2382
2383
2384
2385
2386
2387
2388
2389
2390
2391
2392
2393
2394
2395
2396
2397
2398
2399
2400
2401
2402
2403
2404
2405
2406
2407
2408
2409
2410
2411
2412
2413
2414
2415
2416
2417
2418
2419
2420
2421
2422
2423
2424
2425
2426
2427
2428
2429
2430
2431
2432
2433
2434
2435
2436
2437
2438
2439
2440
2441
2442
2443
2444
2445
2446
2447
2448
2449
2450
2451
2452
2453
2454
2455
2456
2457
....
2475
2476
2477
2478
2479
2480
2481
2482
2483
2484
2485
2486
2487
2488
2489
2490
2491
2492
2493
2494
2495
2496
2497
2498
2499
2500
2501
2502
....
2510
2511
2512
2513
2514
2515
2516
2517
2518
2519
2520
2521
2522
2523
2524
2525
2526
2527
2528
2529
2530
2531
2532
2533
2534
2535
2536
2537
2538
2539
2540
2541
2542
2543
2544
2545
2546
2547
2548
2549
2550
2551
2552
2553
2554
2555
2556
2557
2558
2559
2560
2561
2562
2563
2564
2565
2566
2567
2568
2569
2570
2571
2572
2573
2574
2575
....
2620
2621
2622
2623
2624
2625
2626
2627
2628
2629
2630
2631
2632
2633
2634
2635
2636
2637
2638
2639
2640
2641
    -cleanup {rename sys {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}

test bdd-6.3 {nthvar - var 0} {
    -setup {bdd::system create sys}
    -body {
	sys nthvar a 0
	set result [list [sys dump a]]
	sys unset a
	lappend result [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{2 {0 0 1} 0 {1 0 0} 1 {1 1 1}} 2}
}

test bdd-6.4 {nthvar - two vars} {
    -setup {bdd::system create sys}
    -body {
	sys nthvar a 0
	sys nthvar b 1
	set result [list [sys dump b] [sys dump a]]
	sys unset a
	sys unset b
	lappend result [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{3 {1 0 1} 0 {2 0 0} 1 {2 1 1}} {2 {0 0 1} 0 {2 0 0} 1 {2 1 1}} 2}
}

test bdd-6.5 {nthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys nthvar a 0;
	sys nthvar b 1;
	sys nthvar c 0
	list [sys beadindex a] [sys beadindex b] [sys beadindex c] \
	    [sys unset a] [sys unset b] [sys unset c] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}

test bdd-7.1 {notnthvar - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys notnthvar}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
    -cleanup {rename sys {}}
    -returnCodes error
    -result {expected integer but got "garbage"}
}

test bdd-7.3 {notnthvar - var 0} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; 
	list [sys dump !a] [sys unset !a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{2 {0 1 0} 1 {1 1 1} 0 {1 0 0}} {} 2}
}

test bdd-7.4 {notnthvar - two vars} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1
	list [sys dump !b] [sys dump !a] \
	    [sys unset !b] [sys unset !a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {{3 {1 1 0} 1 {2 1 1} 0 {2 0 0}} {2 {0 1 0} 1 {2 1 1} 0 {2 0 0}} {} {} 2}
}

test bdd-7.5 {nthvar - redundant var (tests duplicate BDD_MakeBead)} {
    -setup {bdd::system create sys}
    -body {
	sys notnthvar !a 0; sys notnthvar !b 1; sys notnthvar !c 0
	list [sys beadindex !a] [sys beadindex !b] [sys beadindex !c] \
	    [sys unset !a] [sys unset !b] [sys unset !c] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 3 2 {} {} {} 2}
}

test bdd-8.1 {negate - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys ~}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
}

test bdd-8.3 {negate 0} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
    -body {
	sys ~ b 0; 
	list [sys beadindex b] \
	    [sys unset b] [sys unset !a] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} {} {} 2}
}

test bdd-8.4 {negate 1} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
................................................................................
}

test bdd-8.5 {negate a} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
    -body {
	sys ~ b a; 
	list [expr {[sys beadindex b] == [sys beadindex !a]}] \
	    [sys unset b] [sys unset !a] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} {} {} 2}
}

test bdd-8.5 {negate !a} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
    }
    -body {
	sys ~ b !a; 
	list [expr {[sys beadindex b] == [sys beadindex a]}] \
	    [sys unset b] [sys unset !a] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} {} {} 2}
}

test bdd-9.1 {binop - wrong # args} {
    -setup {bdd::system create sys}
    -body {sys nand}
    -cleanup {rename sys {}}
    -returnCodes error
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys nor c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys nor c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys nor c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {0001 0010 0100 1000 2}
}

test bdd-9.5 {binary < operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys < c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys < c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys < c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {0100 1000 0001 0010 2}
}

test bdd-9.6 {binary > operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys > c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys > c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys > c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {0010 0001 1000 0100 2}
}

test bdd-9.7 {binary ^ operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys ^ c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {0110 1001 1001 0110 2}
}

test bdd-9.8 {binary nand operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys nand c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys nand c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys nand c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {0111 1011 1101 1110 2}
}
test bdd-9.9 {binary & operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
................................................................................
    -body {
	set tables {}
	sys & c !a !b
	lappend tables [truthtable [sys dump c] 2]
	sys & c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys & c !a b

	lappend tables [truthtable [sys dump c] 2]
	sys & c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1000 0100 0010 0001 2}
}

test bdd-9.10 {binary == operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys == c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys == c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys == c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result  {1001 0110 0110 1001 2}
}

test bdd-9.11 {binary <= operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys <= c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys <= c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys <= c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1101 1110 0111 1011 2}
}

test bdd-9.12 {binary >= operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys >= c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys >= c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys >= c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1011 0111 1110 1101 2}
}

test bdd-9.13 {binary | operator} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	lappend tables [truthtable [sys dump c] 2]
	sys | c a !b
	lappend tables [truthtable [sys dump c] 2]
	sys | c !a b
	lappend tables [truthtable [sys dump c] 2]
	sys | c a b
	lappend tables [truthtable [sys dump c] 2]
	sys unset a !a b !b c
	lappend tables [sys gc]
	set tables
    }
    -cleanup {rename sys {}}
    -result {1110 1101 1011 0111 2}
}

test bdd-10.1 {syllogism in the mode of barbara} {
    -setup {
	bdd::system create sys
	sys nthvar man(x) 0
	sys nthvar mortal(x) 1
................................................................................
	sys <= test1 minor conclusion;    # does the minor premise imply
	;			          # the conclusion?
	sys <= test2 conjunct conclusion; # is the syllogism valid?
	list \
	    [expr {[sys beadindex test0] == 1}] \
	    [expr {[sys beadindex test1] == 1}] \
	    [expr {[sys beadindex test2] == 1}] \
	    [truthtable [sys dump conjunct] 3] \
	    [sys unset test2 test1 test0 conclusion conjunct minor major \
		 socrates(x) mortal(x) man(x)] \
	    [sys gc]
    } 
    -cleanup {rename sys {}}
    -result {0 0 1 10110001 {} 2}
}

test bdd-11.1 {demorgan} {
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys & c a b
	sys nor d !a !b
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-11.2 {demorgan} {
    -setup {
................................................................................
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys | c a b
	sys nand d !a !b
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-11.3 {demorgan} {
    -setup {
................................................................................
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys ^ c a b
	sys ^ d !a !b
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-11.4 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys & c a b
	sys | d !a !b
	sys ~ d d
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-11.5 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys | c a b
	sys & d !a !b
	sys ~ d d
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-11.6 {demorgan} {
    -setup {
................................................................................
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
    }
    -body {
	sys ^ c a b
	sys == d !a !b
	sys ~ d d
	list [expr {[sys beadindex c] == [sys beadindex d]}] \
	    [sys unset d c !b b !a a] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {
	rename sys {}
   }
}

test bdd-12.1 {satcount - wrong # args} {
    -setup {bdd::system create sys}
................................................................................
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
}

test bdd-12.3 {satcount - zero} {
    -setup {bdd::system create sys}
    -body {
	list [sys satcount 0] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {0 2}
}
    
test bdd-12.4 {satcount - no vars} {
    -setup {bdd::system create sys}
    -body {
	list [sys satcount 1] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 2}
}

test bdd-12.5 {satcount - one var} {
    -setup {bdd::system create sys; sys nthvar a 0}
    -body {
	list [sys satcount 1] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {2 {} 2}
}

test bdd-12.6 {satcount - two vars} {
    -setup {bdd::system create sys; sys nthvar a 1}
    -body {
	list [sys satcount 1] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {4 {} 2}
}

test bdd-12.7 {satcount - three vars} {
    -setup {bdd::system create sys; sys nthvar a 2}
    -body {
	list [sys satcount 1] [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result {8 {} 2}
}

test bdd-12.8 {satcount - one var of three} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
	list [sys satcount a] [sys satcount b] [sys satcount c] \
	    [sys unset c b a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {4 4 4 {} 2}
}

test bdd-12.9 {satcount - two vars of three} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
    }
    -body {
	sys | r1 a b
	sys | r2 a c
	sys | r3 b c
	list [sys satcount r1] [sys satcount r2] [sys satcount r3] \
	    [sys unset r3 r2 r1 c b a] [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {6 6 6 {} 2}
}

test bdd-12.10 {satcount - complex expr} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys & r2 c d
	sys | r2 r2 e
	sys & r1 r1 r2
	sys | r2 f g
	sys | r2 r2 h
	sys & r1 r1 r2
	sys ~ r2 r1
	list [sys satcount r1] [sys satcount r2] \
	    [sys unset r2 r1 j h g f e d c b a] \
	    [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {210 302 {} 2}
}

test bdd-12.11 {satcount - parity tree} {
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 128} {incr i} {
	    sys nthvar v$i $i
................................................................................
	sys := r0 0
	for {set i 0} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	for {set i 1} {$i < 128} {incr i 2} {
	    sys ^ r0 r0 v$i
	}
	set result [list [dict size [sys dump r0]] \
			[format %llx [sys satcount r0]]]
	sys unset r0
	for {set i 0} {$i < 128} {incr i} {
	    sys unset v$i
	}
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {257 80000000000000000000000000000000 2}
}

test bdd-13.1 {restrict - wrong # args} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2
	list [expr {[sys beadindex r1] == [sys beadindex r2]}] \
	    [sys unset r1 r2 c !c b !b a !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-13.6 {restrict by literal} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 !b
	sys ^ r3 a c 
	list [expr {[sys beadindex r1] == [sys beadindex r3]}] \
	    [sys unset r3 r2 r1 !c c !b b !a a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-13.7 {restrict by two literals} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 a c
	list [expr {[sys beadindex r1] == [sys beadindex b]}] \
	    [sys unset r2 r1 !c c !b b !a a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-13.8 {restrict by two disordered literals} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 r2 c a
	list [expr {[sys beadindex r1] == [sys beadindex b]}] \
	    [sys unset r2 r1 c !c b !b a !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-13.9 {restrict - reduce to constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
	sys nthvar c 2
    }
    -body {
	sys & r1 a b
	sys & r1 r1 c
	sys restrict r1 r1 a b
	sys restrict r2 r1 c
	list [sys beadindex r2] \
	    [sys unset r2 r1 c b a] \
	    [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {1 {} 2}
}

test bdd-13.10 {restrict zero} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 0 a c
	list [sys beadindex r1] \
	    [sys unset r2 c !c b !b a !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {0 {} 2}
}

test bdd-13.11 {restrict one} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys ^ r2 c b
	sys ^ r2  a r2
    }
    -body {
	sys restrict r1 1 a c
	list [sys beadindex r1] \
	    [sys unset r1 r2 c b a !c !b !a] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-14.1 {foreach_sat - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
................................................................................
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    lappend result $x
	}
	sys unset z y a b c d
	lappend result [sys gc]
	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1} {0 0 1 1 2 1} {0 1} 2}
}

test bdd-14.7 {foreach_sat - continue} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
................................................................................
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    if {[dict exists $x 3]} continue
	    lappend result $x
	}
	sys unset z y a b c d
	lappend result [sys gc]
	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 1 2 1} {0 1} 2}
}

test bdd-14.8 {foreach_sat - break} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
................................................................................
	sys & y b c
	sys | z z y
	sys | z z d
	sys foreach_sat x z {
	    if {![dict exists $x 3]} break
	    lappend result $x
	}
	sys unset z y a b c d
	lappend result [sys gc]
	set result
    }
    -cleanup {
	rename sys {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1} 2}
}

test bdd-14.9 {foreach_sat - return} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	proc bdd-14.9 {} {
................................................................................
	}
    }
    -body {
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	set result [bdd-14.9]
	sys unset z y a b c d
	lappend result [sys gc]
	set result
    }
    -cleanup {
	rename sys {}
	rename bdd-14.9 {}
    }
    -result {{0 0 1 0 3 1} {0 0 1 1 2 0 3 1} 2}
}

test bdd-14.10 {foreach_sat - error} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
    -body {
	set result {}
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	set result [list \
			[catch {
			    sys foreach_sat x z {
				if {![dict exists $x 3]} {
				    error testing
				}
				lappend result $x
			    }
			} result] \
			$result \
			$::errorInfo]
	sys unset z y a b c d
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -match glob
    -result {1 testing {testing
    while executing
"error testing"
   ('foreach_sat' body, line 3)
    invoked from within
*} 2}
}

test bdd-14.11 {foreach_sat - unusual return} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
    }
    -body {
	set result {}
	sys := z a
	sys & y b c
	sys | z z y
	sys | z z d
	set result \
	    [list \
		 [catch {
		     sys foreach_sat x z {
			 if {![dict exists $x 3]} {
			     return -code 6 -level 0 testing
			 }
			 lappend result $x
		     }
		 } result] \
		 $result]
	sys unset y z a b c d
	lappend result [sys gc]
    }
    -cleanup {
	rename sys {}
    }
    -result {6 testing 2}
}

test bdd-15.1.1 {quantifiers - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
    -body {
................................................................................
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys exists z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}
	sys unset z c b a
	lappend result [sys gc]
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 2}
}

test bdd-15.8.2 {quantifiers - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
................................................................................
    }
    -body {
	set result {}
	foreach ex {0 1 a b c} {
	    sys forall z {} $ex
	    lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	}
	sys unset z c a b
	lappend result [sys gc]
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 2}
}

test bdd-15.9.1 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys exists z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}
	sys unset z p q r a b c
	lappend result [sys gc]
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2}
}

test bdd-15.9.2 {quantifiers - irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	set result {}
	foreach v {p q r} {
	    foreach ex {0 1 a b c} {
		sys forall z $v $ex
		lappend result [expr {[sys beadindex z] == [sys beadindex $ex]}]
	    }
	}
	sys unset z p q r a b c
	lappend result [sys gc]
	set result
    }
    -cleanup {rename sys {}}
    -result {1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2}
}

test bdd-15.10 {existential quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
................................................................................
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys | ye a b
	sys | ye ye c
	sys | ye ye d
	sys exists ze {e f} expr
	list [expr {[sys beadindex ze] == [sys beadindex ye]}] \
	    [sys unset ye ze term expr a b c d e f !e !f] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-15.11 {universal quantifier} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2; sys nthvar d 3
	sys nthvar e 4; sys notnthvar !e 4
................................................................................
	sys & term  e  f; sys & term term d; sys | expr expr term
    }
    -body {
	sys & yu a b
	sys & yu yu c
	sys & yu yu d
	sys forall zu {e f} expr
	list [expr {[sys beadindex zu] == [sys beadindex yu]}] \
	    [sys unset zu yu expr term e !e f !f a b c d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.1-$operation "$operation - wrong # args" {*}{
	-setup {
................................................................................
    test bdd-16.3-$operation {$operation - bad second expr} {*}{
	-setup {
	    bdd::system create sys
	    sys nthvar a 0; sys notnthvar !a 0
	    sys nthvar b 0; sys notnthvar !b 0
	    sys nthvar c 0; sys notnthvar !c 0
	}
	-body {
	    list [catch {sys $operation z a garbage c} result] \
		$result $::errorCode \
		[sys unset a !a b !b c !c] \
		[sys gc]
	     }
	-cleanup {rename sys {}}
	-result \
	    {1 {expression named "garbage" not found} {BDD ExprNotFound garbage} {} 2}
    }
}

foreach operation {
    &3 ^3 ?: borrow concur3 differ3 even3 median nand3 nor3 oneof3 twoof3 |3
} {
    test bdd-16.4-$operation {$operation - bad third expr} {*}{
	-setup {
	    bdd::system create sys
	    sys nthvar a 0; sys notnthvar !a 0
	    sys nthvar b 0; sys notnthvar !b 0
	    sys nthvar c 0; sys notnthvar !c 0
	}
	-body {
	    list [catch {sys $operation z a b garbage} result] \
		$result $::errorCode \
		[sys unset a b c !a !b !c] \
		[sys gc]
	}
	-cleanup {rename sys {}}
	-result \
	    {1 {expression named "garbage" not found} {BDD ExprNotFound garbage} {} 2}
    }
}

test bdd-16.5 {ternary nor} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & r c f
    }
    -body {
	sys nor3 y p q r
	sys | t p q
	sys | t t r
	sys ~ z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y t p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.6 {ternary oneof} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & z z !r
	sys & t !p q
	sys & t t !r
	sys | z z t
	sys & t !p !q
	sys & t t r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.7 {ternary twoof} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys & z z !r
	sys & t p !q
	sys & t t r
	sys | z z t
	sys & t !p q
	sys & t t r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y t p q r !p !q !r a b c d e f] \
	    [sys gc]
    }

    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-16.7 {ternary even} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
	sys nthvar d 3; sys nthvar e 4; sys nthvar f 5;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys even3 y p q r
	sys ^ z p q
	sys ^ z z !r
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.8 {ternary differ} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !r r
    }
    -body {
	sys differ3 y p q r
	sys &3 z p q r
	sys &3 t !p !q !r
	sys nor z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset y z t p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.9 {ternary nand} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys nand3 y p q r
	sys &3 z p q r
	sys ~ z z
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }

    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-16.10 {ternary concurrence} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
	sys nthvar d 3; sys nthvar e 4; sys nthvar f 5;
................................................................................
	sys ~ !r r
    }
    -body {
	sys concur3 y p q r
	sys &3 z p q r
	sys &3 t !p !q !r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y !p !q !r p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.11 {ternary - borrow bit of subtraction} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z !p !q  r
	sys &3 t !p  q !r
	sys | z z t
	sys &3 t !p  q  r
	sys | z z t
	sys &3 t  p  q  r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.12 {ternary - borrow bit of subtraction} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z !p !q  r
	sys &3 t !p  q !r
	sys | z z t
	sys &3 t !p  q  r
	sys | z z t
	sys &3 t  p  q  r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.13 {ternary - xor} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys ^3 y p q r
	sys ^ z p q
	sys ^ z z r
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.14 {ternary - ?:} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !r r
    }
    -body {
	sys ?: y p q r
	sys & z p q
	sys & t !p r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y !p !q !r p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.15 {ternary - median} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys &3 z p q !r
	sys &3 t p !q r
	sys | z z t
	sys &3 t !p q r
	sys | z z t
	sys &3 t p q r
	sys | z z t
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z t y p q r !p !q !r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-16.16 {ternary - or} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys nthvar b 1; sys nthvar c 2;
................................................................................
	sys ~ !q q
	sys ~ !r r
    }
    -body {
	sys |3 y p q r
	sys | z p q
	sys | z z r
	list [expr {[sys beadindex y] == [sys beadindex z]}] \
	    [sys unset z y !p !q !r p q r a b c d e f] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-17.1 {compose - wrong # args} {*}{
    -setup {
	bdd::system create sys
    }
................................................................................

test bdd-17.4 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
    }
    -body {
	list [catch {sys compose x a garbage 0} result] $result $::errorCode \
	    [sys unset a] [sys gc]
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage} {} 2}
}

test bdd-17.5 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys & c a b
    }
    -body {
	list [catch {sys compose x a c 0} result] $result $::errorCode \
	    [sys unset a b c] [sys gc]
    }
    -cleanup {rename sys {}}
    -result \
	{1 {c is not a variable} {BDD NotVariable c} {} 2}
}

test bdd-17.6 {compose - bad var} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys notnthvar !b 1
    }
    -body {
	list [catch {sys compose x a !b 0} result] $result $::errorCode \
	    [sys unset a !b] [sys gc]
    }
    -cleanup {rename sys {}}
    -result \
	{1 {!b is not a variable} {BDD NotVariable !b} {} 2}
}

test bdd-17.7 {compose - bad replacement expr} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
    }
    -body {
	list [catch {sys compose x a b garbage} result] $result $::errorCode \
	    [sys unset a b] [sys gc]
    }
    -cleanup {rename sys {}}
    -result \
	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage} {} 2}
}

test bdd-17.8 {compose - do nothing gracefully} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys & c a b
    }
    -body {
	sys compose d c
	list [expr {[sys beadindex d] == [sys beadindex c]}] \
	    [sys unset a b c d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-17.9 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c p 0
	list [expr {[sys beadindex d] == [sys beadindex c]}] \
	    [sys unset a b c d p q r] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-17.10 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c q 0
	list [expr {[sys beadindex d] == [sys beadindex c]}] \
	    [sys unset a b c p q r d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-17.10 {compose with irrelevant variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0
	sys nthvar a 1
................................................................................
	sys nthvar q 2
	sys nthvar b 3
	sys nthvar r 4
	sys & c a b
    }
    -body {
	sys compose d c r 0
	list [expr {[sys beadindex d] == [sys beadindex c]}] \
	    [sys unset a b c p q r d] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-17.11 {compose - replace with constant} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
................................................................................
	    {
		sys compose z c {*}$s
		if {[sys beadindex z] != [sys beadindex $y]} {
		    lappend trouble "a&b\[[lindex $s 1]/[lindex $s 0]] " \
			"should be $y"
		}
	    }
	sys unset a !a b !b c z
	lappend trouble [sys gc]
	join $trouble \n
    }
    -cleanup {rename sys {}}
    -result 2
}

test bdd-17.12 {compose - replace with variable} {*}{
    -setup {
	bdd::system create sys
	sys nthvar p 0; sys notnthvar !p 0
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & c a b
    }
    -body {
	set trouble {} 
	foreach x {p a q b r} {
	    sys compose d c a $x
	    sys & e $x b
	    if {[sys beadindex d] != [sys beadindex e]} {
		lappend trouble "a&$x should be the same as (a&b)\[$x/b]"
	    }
	}
	sys unset a b c p q r !a !b !c !p !q !r d e
	lappend trouble [sys gc]
	join $trouble \n
    }
    -cleanup {rename sys {}}
    -result {2}
}

test bdd-17.13 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
	sys nthvar b 2; sys notnthvar !b 2
	sys < c a b
	sys < y b a
    } 
    -body {
	sys compose z c a b b a
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset z y c a b !a !b] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-17.14 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & x x t
	sys <= y b c
	sys <= t c a
	sys & y y t
    } 
    -body {
	sys compose z x a b b c c a
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset z y t x a b c !a !b !c] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-17.15 {compose - interchange variables} {
    -setup {
	bdd::system create sys
	sys nthvar a 1; sys notnthvar !a 1
................................................................................
	sys & x x t
	sys <= y c a
	sys <= t a b
	sys & y y t
    } 
    -body {
	sys compose z x b a c b a c
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset z t y x a b c !a !b !c] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

test bdd-17.16 {compose - more complex substitution} {
    -setup {
	bdd::system create sys
	sys nthvar a 0
	sys nthvar b 1
	sys nthvar c 2
	sys nthvar d 3
	sys | x a b
	sys & t a b
	sys & u c d
	sys | y t u
    } 
    -body {
	sys compose z x a t b u
	list [expr {[sys beadindex z] == [sys beadindex y]}] \
	    [sys unset x y z t u a b c d] \
	    [sys gc]
    }
    -result {1 {} 2}
    -cleanup {rename sys {}}
}

# FIXME tests for appquant

test bdd-18.n {relational product} {*}{
    -setup {
	bdd::system create sys
	sys nthvar a 0; sys notnthvar !a 0
	sys nthvar b 1; sys notnthvar !b 1
	sys nthvar c 2; sys notnthvar !c 2
	sys nthvar d 3; sys notnthvar !d 3
	sys nthvar e 4; sys notnthvar !e 4
	sys nthvar f 5; sys notnthvar !f 5
	sys nthvar g 6; sys notnthvar !g 6
	sys nthvar h 7; sys notnthvar !h 7

	sys &3 p a !b !c
	sys & p p !d
	sys &3 expr1 p !e !f
	sys &3 expr2 p !g !h

	sys &3 p !a b !c
	sys & p p !d
	sys &3 term1 p !e f
	sys &3 term2 p !g h
	sys | expr1 expr1 term1
	sys | expr2 expr2 term2

	sys &3 p !a !b c
	sys & p p !d
	sys &3 term1 p e !f
	sys &3 term2 p g !h
	sys | expr1 expr1 term1
	sys | expr2 expr2 term2

	sys &3 p !a !b !c
	sys & p p d
	sys &3 term1 p e f
	sys &3 term2 p g h
	sys | expr1 expr1 term1
	sys | expr2 expr2 term2

	sys unset p term1 term2

	sys == result_sb e g
	sys == term f h
	sys & result_sb result_sb term
	sys unset term

    }
    -body {
	sys exists_& result_is {a b c d} expr1 expr2
	list [expr {[sys beadindex result_is] == [sys beadindex result_sb]}] \
	    [sys unset result_is result_sb expr1 expr2 \
		 a b c d e f g h !a !b !c !d !e !f !g !h] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 {} 2}
}

test bdd-21.1 {eight queens} {*}{
    -setup {
	bdd::system create sys
	for {set i 0} {$i < 64} {incr i} {
	    sys nthvar v$i $i; sys notnthvar !v$i $i
................................................................................
		    if {$col2 != $col} {
			set q2 v[expr {8 * $row + $col2}]
			sys & columnC columnC !$q2
		    }
		}
		sys <= columnC $q1 columnC
		sys & cellC cellC columnC
		sys unset columnC
		
		# queen here <= no other queen in the same row

		sys := rowC 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
			set q2 v[expr {8 * $row2 + $col}]
			sys & rowC rowC !$q2
		    }
		}
		sys <= rowC $q1 rowC
		sys & cellC cellC rowC
		sys unset rowC

		# queen here <= no other queen in the same diagonal

		sys := diag1C 1
		sys := diag2C 1
		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
		    if {$row2 != $row} {
................................................................................
			    set q2 v[expr {8 * $row2 + $col2}]
			    sys & diag2C diag2C !$q2
			}
		    }
		}
		sys <= diag1C $q1 diag1C
		sys & cellC cellC diag1C
		sys unset diag1C

		sys <= diag2C $q1 diag2C
		sys & cellC cellC diag2C
		sys unset diag2C

		# accumulate into the constraint set for the row

		sys & thisRowC thisRowC cellC
		sys unset cellC
	    }

	    # accumulate all constraints for a row into the solution

	    sys & solution solution thisRowC
	    sys unset thisRowC
	}
		
	# at least one queen in each column
	for {set col 0} {$col < 8} {incr col} {
	    sys := columnC 0
	    for {set row 0} {$row < 8} {incr row} {
		set q v[expr {8*$row + $col}]
		sys | columnC columnC $q
	    }
	    sys & solution solution columnC
	    sys unset columnC
	}

	# enumerate solutions
	sys foreach_sat A solution {
	    set sol [lrepeat 8 {}]
	    foreach {var value} $A {
		if {$value} {
		    lset sol [expr {$var/8}] [expr {$var%8}]
		}
	    }
	    lappend sols [join $sol {}]
	}

	# clean up
	sys unset solution
	for {set i 0} {$i < 64} {incr i} {
	    sys unset v$i !v$i
	}
	lappend sols [sys gc]

	lreverse $sols

    }
    -cleanup {rename sys {}}
    -result {2 04752613 05726314 06357142 06471352 13572064 14602753 14630752 15063724 15720364 16257403 16470352 17502463 20647135 24170635 24175360 24603175 24730615 25147063 25160374 25164073 25307461 25317460 25703641 25704613 25713064 26174035 26175304 27360514 30471625 30475261 31475026 31625704 31625740 31640752 31746025 31750246 35041726 35716024 35720641 36074152 36271405 36415027 36420571 37025164 37046152 37420615 40357162 40731625 40752613 41357206 41362750 41506372 41703625 42057136 42061753 42736051 46027531 46031752 46137025 46152037 46152073 46302751 47302516 47306152 50417263 51602473 51603742 52064713 52073164 52074136 52460317 52470316 52613704 52617403 52630714 53047162 53174602 53602417 53607142 57130642 60275314 61307425 61520374 62057413 62714053 63147025 63175024 64205713 71306425 71420635 72051463 73025164}
}

test bdd-21.2 {verification of a full adder} {
    -setup {
	bdd::system create sys
	sys nthvar x 0; sys notnthvar !x 0
	sys nthvar y 1; sys notnthvar !y 1
................................................................................
	sys & gate1 x y
	sys ^ gate2 x y
	sys & gate3 gate2 ci
	sys ^ z gate2 ci
	sys | co gate1 gate3

	list [expr {[sys beadindex co] == [sys beadindex spec_co]}] \
	    [expr {[sys beadindex z] == [sys beadindex spec_z]}] \
	    [sys unset x y ci !x !y !ci spec_co spec_z input \
		 gate1 gate2 gate3 z co] \
	    [sys gc]
    }
    -cleanup {rename sys {}}
    -result {1 1 {} 2}
}

cleanupTests
return

# Local Variables:
# mode: tcl
# End: