tclbdd

Check-in [f7a47671e9]
Login

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

Overview
Comment:Added ===, tautology, satisfiable methods (no tests yet). Replaced 'constant' and 'copy' with a single ':=' method.
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:f7a47671e987522b20074340a26eef2efc5fed97
User & Date: kennykb 2013-12-01 23:26:26
Context
2013-12-01
23:27
Removed pure-Tcl superclass for bdd: not sure where I was going with that. check-in: af2be65f95 user: kennykb tags: trunk
23:26
Added ===, tautology, satisfiable methods (no tests yet). Replaced 'constant' and 'copy' with a single ':=' method. check-in: f7a47671e9 user: kennykb tags: trunk
23:14
Implemented foreach_sat (no tests yet). Fixed a bug where restrict cannot handle variables out of sequence, and added a test case for same. Made the 8-queens example use foreach_sat to enumerate the solutions. check-in: 5b78565cad user: kennykb tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to generic/tclBdd.c.

   100    100   static void DeletePerInterpData(PerInterpData*);
   101    101   static int BddSystemConstructor(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   102    102   				int, Tcl_Obj* const[]);
   103    103   static int BddSystemBeadindexMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   104    104   				    int, Tcl_Obj* const[]);
   105    105   static int BddSystemBinopMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   106    106   				int, Tcl_Obj* const[]);
   107         -static int BddSystemConstantMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   108         -				   int, Tcl_Obj* const[]);
   109    107   static int BddSystemCopyMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   110    108   			       int, Tcl_Obj* const[]);
   111    109   static int BddSystemDumpMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   112    110   			       int, Tcl_Obj* const[]);
   113    111   static int BddSystemForeachSatMethod(ClientData, Tcl_Interp*, Tcl_ObjectContext,
   114    112   				     int, Tcl_Obj *const[]);
   115    113   static int ForeachSatPre(Tcl_Interp* interp, BddSystemData*,
................................................................................
   167    165   const static Tcl_MethodType BddSystemBinopMethodType = {
   168    166       TCL_OO_METHOD_VERSION_CURRENT, /* version */
   169    167       "binop",			   /* name */
   170    168       BddSystemBinopMethod,	   /* callProc */
   171    169       DeleteMethod,		   /* method delete proc */
   172    170       CloneMethod			   /* method clone proc */
   173    171   };				   /* common to all ten binary operators */
   174         -const static Tcl_MethodType BddSystemConstantMethodType = {
   175         -    TCL_OO_METHOD_VERSION_CURRENT, /* version */
   176         -    "constant",			   /* name */
   177         -    BddSystemConstantMethod,	   /* callProc */
   178         -    DeleteMethod,		   /* method delete proc */
   179         -    CloneMethod			   /* method clone proc */
   180         -};
   181    172   const static Tcl_MethodType BddSystemCopyMethodType = {
   182    173       TCL_OO_METHOD_VERSION_CURRENT, /* version */
   183    174       "copy",			   /* name */
   184    175       BddSystemCopyMethod,	   /* callProc */
   185    176       DeleteMethod,		   /* method delete proc */
   186    177       CloneMethod			   /* method clone proc */
   187    178   };
................................................................................
   245    236   /*
   246    237    * Method table for the BDD system object
   247    238    */
   248    239   
   249    240   MethodTableRow systemMethodTable[] = {
   250    241       { "!=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NE },
   251    242       { "&",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_AND },
          243  +    { ":=",        &BddSystemCopyMethodType,      NULL },
   252    244       { "<",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LT },
   253    245       { "<=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_LE },
   254    246       { "==",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_EQ },
   255    247       { ">",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GT },
   256    248       { ">=",        &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_GE },
   257    249       { "^",         &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_XOR },
   258    250       { "beadindex", &BddSystemBeadindexMethodType, NULL },
   259         -    { "constant",  &BddSystemConstantMethodType,  NULL },
   260         -    { "copy",      &BddSystemCopyMethodType,      NULL },
   261    251       { "dump",      &BddSystemDumpMethodType,      NULL },
   262    252       { "foreach_sat",
   263    253                      &BddSystemForeachSatMethodType,NULL },
   264    254       { "nand",      &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NAND },
   265    255       { "nor",       &BddSystemBinopMethodType,     (ClientData) BDD_BINOP_NOR },
   266    256       { "notnthvar", &BddSystemNotnthvarMethodType, NULL },
   267    257       { "nthvar",    &BddSystemNthvarMethodType,    NULL },
................................................................................
   553    543       }
   554    544       beadIndexResult = BDD_Apply(sdata->system, (BDD_BinOp) (size_t)clientData,
   555    545   				beadIndexOpd1, beadIndexOpd2);
   556    546       SetNamedExpression(sdata, objv[skipped], beadIndexResult);
   557    547       BDD_UnrefBead(sdata->system, beadIndexResult);
   558    548       return TCL_OK;
   559    549   }
   560         -
   561         -/*
   562         - *-----------------------------------------------------------------------------
   563         - *
   564         - * BddSystemConstantMethod --
   565         - *
   566         - *	Computes a constant expression in a system of BDD's and assigns
   567         - *	it a name
   568         - *
   569         - * Usage:
   570         - *	$system constant name value
   571         - *
   572         - * Parameters:
   573         - *	name - The name to assign
   574         - *	value - The Boolean value to give it
   575         - *
   576         - * Results:
   577         - *	None
   578         - *
   579         - * Side effects:
   580         - *	Assigns the given value to the name
   581         - *
   582         - *-----------------------------------------------------------------------------
   583         - */
   584         -
   585         -static int
   586         -BddSystemConstantMethod(
   587         -    ClientData clientData,	/* Operation to perform */
   588         -    Tcl_Interp* interp,		/* Tcl interpreter */
   589         -    Tcl_ObjectContext ctx,	/* Object context */
   590         -    int objc,			/* Parameter count */
   591         -    Tcl_Obj *const objv[])	/* Parameter vector */
   592         -{
   593         -    Tcl_Object thisObject = Tcl_ObjectContextObject(ctx);
   594         -				/* The current object */
   595         -    BddSystemData* sdata = (BddSystemData*)
   596         -	Tcl_ObjectGetMetadata(thisObject, &BddSystemDataType);
   597         -				/* The current system of expressions */
   598         -    int skipped = Tcl_ObjectContextSkippedArgs(ctx);
   599         -				/* The number of args used in method dispatch */
   600         -    int boolval;		/* Boolean value */
   601         -
   602         -    /* Check syntax */
   603         -
   604         -    if (objc != skipped+2) {
   605         -	Tcl_WrongNumArgs(interp, skipped, objv, "name value");
   606         -	return TCL_ERROR;
   607         -    }
   608         -    if (Tcl_GetBooleanFromObj(interp, objv[skipped+1], &boolval) != TCL_OK) {
   609         -	return TCL_ERROR;
   610         -    }
   611         -    SetNamedExpression(sdata, objv[skipped], (BDD_BeadIndex) boolval);
   612         -    return TCL_OK;
   613         -}
   614    550   
   615    551   /*
   616    552    *-----------------------------------------------------------------------------
   617    553    *
   618    554    * BddSystemCopyMethod --
   619    555    *
   620    556    *	Copies a named expression in a system of BDD's and assigns

Changes to library/tclbdd.tcl.

    10     10   #------------------------------------------------------------------------------
    11     11   
    12     12   namespace eval bdd {
    13     13       namespace export system
    14     14   }
    15     15   
    16     16   oo::class create bdd::SystemInt {
    17         -    variable beadseq
    18     17       constructor args {
    19     18       }
    20     19   }
    21     20   oo::class create bdd::system {
    22     21       superclass ::bdd::SystemInt
           22  +    method === {exprName1 exprName2} {
           23  +	expr {[my beadindex $exprName1] == [my beadindex exprName2]}
           24  +    }
           25  +    method satisfiable {exprName} {
           26  +	expr {[my beadindex $exprName] != 0}
           27  +    }
           28  +    method tautology {exprName} {
           29  +	expr {[my beadindex $exprname] == 1}
           30  +    }
    23     31   }

Changes to tests/bdd.test.

    81     81       -setup {bdd::system create sys}
    82     82       -body {list [catch {sys beadindex garbage} result] $result $::errorCode}
    83     83       -cleanup {rename sys {}}
    84     84       -result \
    85     85   	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
    86     86   }
    87     87   
    88         -test bdd-3.1 {constant - wrong # args} {*}{
           88  +test bdd-4.1 {:= - wrong # args} {*}{
    89     89       -setup {bdd::system create sys}
    90         -    -body {sys constant}
           90  +    -body {sys :=}
    91     91       -cleanup {rename sys {}}
    92     92       -returnCodes error
    93     93       -match glob
    94     94       -result {wrong # args: *}
    95     95   }
    96     96   
    97         -test bdd-3.2 {constant - bad value} {*}{
           97  +test bdd-4.2 {:= - can't find expr} {*}{
    98     98       -setup {bdd::system create sys}
    99         -    -body {sys constant rubbish garbage}
   100         -    -cleanup {rename sys {}}
   101         -    -returnCodes error
   102         -    -match glob
   103         -    -result {expected boolean value but got "garbage"}
   104         -}
   105         -
   106         -test bdd-3.3 {constant 0} {*}{
   107         -    -setup {bdd::system create sys}
   108         -    -body {sys constant zero false; sys beadindex zero}
   109         -    -cleanup {rename sys {}}
   110         -    -result 0
   111         -}
   112         -
   113         -test bdd-3.4 {constant 1} {*}{
   114         -    -setup {bdd::system create sys}
   115         -    -body {sys constant one true; sys beadindex one}
   116         -    -cleanup {rename sys {}}
   117         -    -result 1
   118         -}
   119         -
   120         -test bdd-4.1 {copy - wrong # args} {*}{
   121         -    -setup {bdd::system create sys; sys constant one true}
   122         -    -body {sys copy}
   123         -    -cleanup {rename sys {}}
   124         -    -returnCodes error
   125         -    -match glob
   126         -    -result {wrong # args: *}
   127         -}
   128         -
   129         -test bdd-4.2 {copy - can't find expr} {*}{
   130         -    -setup {bdd::system create sys; sys constant one true}
   131         -    -body {list [catch {sys copy yes garbage} result] $result $::errorCode}
           99  +    -body {list [catch {sys := yes garbage} result] $result $::errorCode}
   132    100       -cleanup {rename sys {}}
   133    101       -result \
   134    102   	{1 {expression named "garbage" not found} {BDD ExprNotFound garbage}}
   135    103   }
   136    104   
   137         -test bdd-4.3 {copy} {*}{
   138         -    -setup {bdd::system create sys; sys constant one true}
   139         -    -body {sys copy yes one; sys beadindex yes}
          105  +test bdd-4.3 {:=} {*}{
          106  +    -setup {bdd::system create sys}
          107  +    -body {sys := yes 1; sys beadindex yes}
   140    108       -cleanup {rename sys {}}
   141    109       -result 1
   142    110   }
   143    111   
   144    112   test bdd-5.1 {dump - wrong # args} {*}{
   145    113       -setup {bdd::system create sys}
   146    114       -body {sys dump}
................................................................................
   815    783       -setup {
   816    784   	bdd::system create sys
   817    785   	for {set i 0} {$i < 128} {incr i} {
   818    786   	    sys nthvar v$i $i
   819    787   	}
   820    788       }
   821    789       -body {
   822         -	sys copy r0 0
          790  +	sys := r0 0
   823    791   	for {set i 0} {$i < 128} {incr i 2} {
   824    792   	    sys ^ r0 r0 v$i
   825    793   	}
   826    794   	for {set i 1} {$i < 128} {incr i 2} {
   827    795   	    sys ^ r0 r0 v$i
   828    796   	}
   829    797   	list [dict size [sys dump r0]] [format %llx [sys satcount r0]]
................................................................................
  1024    992       -setup {
  1025    993   	bdd::system create sys
  1026    994   	for {set i 0} {$i < 64} {incr i} {
  1027    995   	    sys nthvar v$i $i; sys notnthvar !v$i $i
  1028    996   	}
  1029    997       }
  1030    998       -body {
  1031         -	sys copy solution 1
          999  +	sys := solution 1
  1032   1000   
  1033   1001   	# iterate through the cells
  1034   1002   
  1035   1003   	for {set row 0} {$row < 8} {incr row} {
  1036         -	    sys copy thisRowC 1
         1004  +	    sys := thisRowC 1
  1037   1005   	    for {set col 7} {$col >= 0} {incr col -1} {
  1038         -		sys copy cellC 1
         1006  +		sys := cellC 1
  1039   1007   		set q1 v[expr {8* $row + $col}]
  1040   1008   
  1041   1009   		# queen here <= no other queen in the same column
  1042   1010   
  1043         -		sys copy columnC 1
         1011  +		sys := columnC 1
  1044   1012   		for {set col2 7} {$col2 >= 0} {incr col2 -1} {
  1045   1013   		    if {$col2 != $col} {
  1046   1014   			set q2 v[expr {8 * $row + $col2}]
  1047   1015   			sys & columnC columnC !$q2
  1048   1016   		    }
  1049   1017   		}
  1050   1018   		sys <= columnC $q1 columnC
  1051   1019   		sys & cellC cellC columnC
  1052   1020   		
  1053   1021   		# queen here <= no other queen in the same row
  1054   1022   
  1055         -		sys copy rowC 1
         1023  +		sys := rowC 1
  1056   1024   		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
  1057   1025   		    if {$row2 != $row} {
  1058   1026   			set q2 v[expr {8 * $row2 + $col}]
  1059   1027   			sys & rowC rowC !$q2
  1060   1028   		    }
  1061   1029   		}
  1062   1030   		sys <= rowC $q1 rowC
  1063   1031   		sys & cellC cellC rowC
  1064   1032   
  1065   1033   		# queen here <= no other queen in the same diagonal
  1066   1034   
  1067         -		sys copy diag1C 1
  1068         -		sys copy diag2C 1
         1035  +		sys := diag1C 1
         1036  +		sys := diag2C 1
  1069   1037   		for {set row2 7} {$row2 >= 0} {incr row2 -1} {
  1070   1038   		    if {$row2 != $row} {
  1071   1039   			set col2 [expr {$col + $row2 - $row}]
  1072   1040   			if {$col2 >= 0 && $col2 < 8} {
  1073   1041   			    set q2 v[expr {8 * $row2 + $col2}]
  1074   1042   			    sys & diag1C diag1C !$q2
  1075   1043   			}
................................................................................
  1094   1062   	    # accumulate all constraints for a row into the solution
  1095   1063   
  1096   1064   	    sys & solution solution thisRowC
  1097   1065   	}
  1098   1066   		
  1099   1067   	# at least one queen in each column
  1100   1068   	for {set col 0} {$col < 8} {incr col} {
  1101         -	    sys copy columnC 0
         1069  +	    sys := columnC 0
  1102   1070   	    for {set row 0} {$row < 8} {incr row} {
  1103   1071   		set q v[expr {8*$row + $col}]
  1104   1072   		sys | columnC columnC $q
  1105   1073   	    }
  1106   1074   	    sys & solution solution columnC
  1107   1075   	}
  1108   1076   	sys foreach_sat A solution {
................................................................................
  1127   1095   	sys nthvar x 0; sys notnthvar !x 0
  1128   1096   	sys nthvar y 1; sys notnthvar !y 1
  1129   1097   	sys nthvar ci 2; sys notnthvar !ci 2
  1130   1098       }
  1131   1099       -body {
  1132   1100   
  1133   1101   	# specification is a truth table
  1134         -	sys copy spec_co 0
  1135         -	sys copy spec_z 0
         1102  +	sys := spec_co 0
         1103  +	sys := spec_z 0
  1136   1104   	foreach {x y ci co z} {
  1137   1105   	    0 0 0 0 0
  1138   1106   	    0 0 1 0 1
  1139   1107   	    0 1 0 0 1
  1140   1108   	    0 1 1 1 0
  1141   1109   
  1142   1110   	    1 0 0 0 1