Merge BuDDy 2.3.
* examples/calculator/, examples/internal/: Were renamed as ... * examples/bddcalc/, examples/bddtest/: ... these. * configure.ac: Adjust version and output Makefiles. * examples/Makefile.am (SUBDIRS): Adjust subdir renaming. * examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were renamed as ... * examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these. * examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust accordingly. * src/Makefile.am (AM_CPPFLAGS): Define VERSION.
This commit is contained in:
Alexandre Duret-Lutz
parent
9ce6888872
commit
f1c3af808f
18 changed files with 0 additions and 6730 deletions
|
|
@ -1,24 +0,0 @@
|
||||||
include ../Makefile.def
|
|
||||||
EXTRA_DIST = \
|
|
||||||
readme \
|
|
||||||
example.cal \
|
|
||||||
examples/c432.cal \
|
|
||||||
examples/c499.cal \
|
|
||||||
examples/c1355.cal \
|
|
||||||
examples/c1908.cal \
|
|
||||||
examples/c2670.cal \
|
|
||||||
examples/c3540.cal \
|
|
||||||
examples/readme
|
|
||||||
|
|
||||||
AM_YFLAGS = -d
|
|
||||||
|
|
||||||
BUILT_SOURCES = parser.h
|
|
||||||
|
|
||||||
check_PROGRAMS = bddcalc
|
|
||||||
bddcalc_SOURCES = \
|
|
||||||
hashtbl.h \
|
|
||||||
hashtbl.cxx \
|
|
||||||
lexer.lxx \
|
|
||||||
parser.yxx \
|
|
||||||
parser_.h \
|
|
||||||
slist.h
|
|
||||||
|
|
@ -1,10 +0,0 @@
|
||||||
initial 100 100;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
a b c;
|
|
||||||
|
|
||||||
actions
|
|
||||||
t1 = (a | b) & c;
|
|
||||||
t2 = (a & c) | (b & c);
|
|
||||||
t3 = t1 <> t2;
|
|
||||||
tautology t3;
|
|
||||||
|
|
@ -1,818 +0,0 @@
|
||||||
/* BDD Calculator data file */
|
|
||||||
|
|
||||||
initial 10000 10000;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
_1gat _8gat _15gat _22gat _29gat _36gat _43gat _50gat _57gat _64gat
|
|
||||||
_71gat _78gat _85gat _92gat _99gat _106gat _113gat _120gat _127gat _134gat
|
|
||||||
_141gat _148gat _155gat _162gat _169gat _176gat _183gat _190gat _197gat _204gat
|
|
||||||
_211gat _218gat _225gat _226gat _227gat _228gat _229gat _230gat _231gat _232gat
|
|
||||||
_233gat ;
|
|
||||||
|
|
||||||
actions
|
|
||||||
autoreorder 0 sift;
|
|
||||||
|
|
||||||
t2 = _1gat;
|
|
||||||
t3 = _29gat;
|
|
||||||
t4 = t2 nand t3;
|
|
||||||
t5 = t2 nand t4;
|
|
||||||
t6 = t3 nand t4;
|
|
||||||
t7 = t5 nand t6;
|
|
||||||
t8 = _57gat;
|
|
||||||
t9 = _85gat;
|
|
||||||
t10 = t8 nand t9;
|
|
||||||
t11 = t8 nand t10;
|
|
||||||
t12 = t9 nand t10;
|
|
||||||
t13 = t11 nand t12;
|
|
||||||
t14 = t7 nand t13;
|
|
||||||
t15 = t7 nand t14;
|
|
||||||
t16 = t13 nand t14;
|
|
||||||
t17 = t15 nand t16;
|
|
||||||
t18 = _225gat;
|
|
||||||
t19 = _233gat;
|
|
||||||
t20 = t18 and t19;
|
|
||||||
t21 = _113gat;
|
|
||||||
t22 = _120gat;
|
|
||||||
t23 = t21 nand t22;
|
|
||||||
t24 = t21 nand t23;
|
|
||||||
t25 = t22 nand t23;
|
|
||||||
t26 = t24 nand t25;
|
|
||||||
t27 = _127gat;
|
|
||||||
t28 = _134gat;
|
|
||||||
t29 = t27 nand t28;
|
|
||||||
t30 = t27 nand t29;
|
|
||||||
t31 = t28 nand t29;
|
|
||||||
t32 = t30 nand t31;
|
|
||||||
t33 = t26 nand t32;
|
|
||||||
t34 = t26 nand t33;
|
|
||||||
t35 = t32 nand t33;
|
|
||||||
t36 = t34 nand t35;
|
|
||||||
t37 = _141gat;
|
|
||||||
t38 = _148gat;
|
|
||||||
t39 = t37 nand t38;
|
|
||||||
t40 = t37 nand t39;
|
|
||||||
t41 = t38 nand t39;
|
|
||||||
t42 = t40 nand t41;
|
|
||||||
t43 = _155gat;
|
|
||||||
t44 = _162gat;
|
|
||||||
t45 = t43 nand t44;
|
|
||||||
t46 = t43 nand t45;
|
|
||||||
t47 = t44 nand t45;
|
|
||||||
t48 = t46 nand t47;
|
|
||||||
t49 = t42 nand t48;
|
|
||||||
t50 = t42 nand t49;
|
|
||||||
t51 = t48 nand t49;
|
|
||||||
t52 = t50 nand t51;
|
|
||||||
t53 = t36 nand t52;
|
|
||||||
t54 = t36 nand t53;
|
|
||||||
t55 = t52 nand t53;
|
|
||||||
t56 = t54 nand t55;
|
|
||||||
t57 = t20 nand t56;
|
|
||||||
t58 = t20 nand t57;
|
|
||||||
t59 = t56 nand t57;
|
|
||||||
t60 = t58 nand t59;
|
|
||||||
t61 = t17 nand t60;
|
|
||||||
t62 = t17 nand t61;
|
|
||||||
t63 = t60 nand t61;
|
|
||||||
t64 = t62 nand t63;
|
|
||||||
t65 = t28 nand t44;
|
|
||||||
t66 = t28 nand t65;
|
|
||||||
t67 = t44 nand t65;
|
|
||||||
t68 = t66 nand t67;
|
|
||||||
t69 = _190gat;
|
|
||||||
t70 = _218gat;
|
|
||||||
t71 = t69 nand t70;
|
|
||||||
t72 = t69 nand t71;
|
|
||||||
t73 = t70 nand t71;
|
|
||||||
t74 = t72 nand t73;
|
|
||||||
t75 = t68 nand t74;
|
|
||||||
t76 = t68 nand t75;
|
|
||||||
t77 = t74 nand t75;
|
|
||||||
t78 = t76 nand t77;
|
|
||||||
t79 = _232gat;
|
|
||||||
t80 = t79 and t19;
|
|
||||||
t81 = _36gat;
|
|
||||||
t82 = t3 nand t81;
|
|
||||||
t83 = t3 nand t82;
|
|
||||||
t84 = t81 nand t82;
|
|
||||||
t85 = t83 nand t84;
|
|
||||||
t86 = _43gat;
|
|
||||||
t87 = _50gat;
|
|
||||||
t88 = t86 nand t87;
|
|
||||||
t89 = t86 nand t88;
|
|
||||||
t90 = t87 nand t88;
|
|
||||||
t91 = t89 nand t90;
|
|
||||||
t92 = t85 nand t91;
|
|
||||||
t93 = t85 nand t92;
|
|
||||||
t94 = t91 nand t92;
|
|
||||||
t95 = t93 nand t94;
|
|
||||||
t96 = _92gat;
|
|
||||||
t97 = t9 nand t96;
|
|
||||||
t98 = t9 nand t97;
|
|
||||||
t99 = t96 nand t97;
|
|
||||||
t100 = t98 nand t99;
|
|
||||||
t101 = _99gat;
|
|
||||||
t102 = _106gat;
|
|
||||||
t103 = t101 nand t102;
|
|
||||||
t104 = t101 nand t103;
|
|
||||||
t105 = t102 nand t103;
|
|
||||||
t106 = t104 nand t105;
|
|
||||||
t107 = t100 nand t106;
|
|
||||||
t108 = t100 nand t107;
|
|
||||||
t109 = t106 nand t107;
|
|
||||||
t110 = t108 nand t109;
|
|
||||||
t111 = t95 nand t110;
|
|
||||||
t112 = t95 nand t111;
|
|
||||||
t113 = t110 nand t111;
|
|
||||||
t114 = t112 nand t113;
|
|
||||||
t115 = t80 nand t114;
|
|
||||||
t116 = t80 nand t115;
|
|
||||||
t117 = t114 nand t115;
|
|
||||||
t118 = t116 nand t117;
|
|
||||||
t119 = t78 nand t118;
|
|
||||||
t120 = t78 nand t119;
|
|
||||||
t121 = t118 nand t119;
|
|
||||||
t122 = t120 nand t121;
|
|
||||||
t123 = not t122;
|
|
||||||
t124 = t27 nand t43;
|
|
||||||
t125 = t27 nand t124;
|
|
||||||
t126 = t43 nand t124;
|
|
||||||
t127 = t125 nand t126;
|
|
||||||
t128 = _183gat;
|
|
||||||
t129 = _211gat;
|
|
||||||
t130 = t128 nand t129;
|
|
||||||
t131 = t128 nand t130;
|
|
||||||
t132 = t129 nand t130;
|
|
||||||
t133 = t131 nand t132;
|
|
||||||
t134 = t127 nand t133;
|
|
||||||
t135 = t127 nand t134;
|
|
||||||
t136 = t133 nand t134;
|
|
||||||
t137 = t135 nand t136;
|
|
||||||
t138 = _231gat;
|
|
||||||
t139 = t138 and t19;
|
|
||||||
t140 = _8gat;
|
|
||||||
t141 = t2 nand t140;
|
|
||||||
t142 = t2 nand t141;
|
|
||||||
t143 = t140 nand t141;
|
|
||||||
t144 = t142 nand t143;
|
|
||||||
t145 = _15gat;
|
|
||||||
t146 = _22gat;
|
|
||||||
t147 = t145 nand t146;
|
|
||||||
t148 = t145 nand t147;
|
|
||||||
t149 = t146 nand t147;
|
|
||||||
t150 = t148 nand t149;
|
|
||||||
t151 = t144 nand t150;
|
|
||||||
t152 = t144 nand t151;
|
|
||||||
t153 = t150 nand t151;
|
|
||||||
t154 = t152 nand t153;
|
|
||||||
t155 = _64gat;
|
|
||||||
t156 = t8 nand t155;
|
|
||||||
t157 = t8 nand t156;
|
|
||||||
t158 = t155 nand t156;
|
|
||||||
t159 = t157 nand t158;
|
|
||||||
t160 = _71gat;
|
|
||||||
t161 = _78gat;
|
|
||||||
t162 = t160 nand t161;
|
|
||||||
t163 = t160 nand t162;
|
|
||||||
t164 = t161 nand t162;
|
|
||||||
t165 = t163 nand t164;
|
|
||||||
t166 = t159 nand t165;
|
|
||||||
t167 = t159 nand t166;
|
|
||||||
t168 = t165 nand t166;
|
|
||||||
t169 = t167 nand t168;
|
|
||||||
t170 = t154 nand t169;
|
|
||||||
t171 = t154 nand t170;
|
|
||||||
t172 = t169 nand t170;
|
|
||||||
t173 = t171 nand t172;
|
|
||||||
t174 = t139 nand t173;
|
|
||||||
t175 = t139 nand t174;
|
|
||||||
t176 = t173 nand t174;
|
|
||||||
t177 = t175 nand t176;
|
|
||||||
t178 = t137 nand t177;
|
|
||||||
t179 = t137 nand t178;
|
|
||||||
t180 = t177 nand t178;
|
|
||||||
t181 = t179 nand t180;
|
|
||||||
t182 = t21 nand t37;
|
|
||||||
t183 = t21 nand t182;
|
|
||||||
t184 = t37 nand t182;
|
|
||||||
t185 = t183 nand t184;
|
|
||||||
t186 = _169gat;
|
|
||||||
t187 = _197gat;
|
|
||||||
t188 = t186 nand t187;
|
|
||||||
t189 = t186 nand t188;
|
|
||||||
t190 = t187 nand t188;
|
|
||||||
t191 = t189 nand t190;
|
|
||||||
t192 = t185 nand t191;
|
|
||||||
t193 = t185 nand t192;
|
|
||||||
t194 = t191 nand t192;
|
|
||||||
t195 = t193 nand t194;
|
|
||||||
t196 = _229gat;
|
|
||||||
t197 = t196 and t19;
|
|
||||||
t198 = t154 nand t95;
|
|
||||||
t199 = t154 nand t198;
|
|
||||||
t200 = t95 nand t198;
|
|
||||||
t201 = t199 nand t200;
|
|
||||||
t202 = t197 nand t201;
|
|
||||||
t203 = t197 nand t202;
|
|
||||||
t204 = t201 nand t202;
|
|
||||||
t205 = t203 nand t204;
|
|
||||||
t206 = t195 nand t205;
|
|
||||||
t207 = t195 nand t206;
|
|
||||||
t208 = t205 nand t206;
|
|
||||||
t209 = t207 nand t208;
|
|
||||||
t210 = t22 nand t38;
|
|
||||||
t211 = t22 nand t210;
|
|
||||||
t212 = t38 nand t210;
|
|
||||||
t213 = t211 nand t212;
|
|
||||||
t214 = _176gat;
|
|
||||||
t215 = _204gat;
|
|
||||||
t216 = t214 nand t215;
|
|
||||||
t217 = t214 nand t216;
|
|
||||||
t218 = t215 nand t216;
|
|
||||||
t219 = t217 nand t218;
|
|
||||||
t220 = t213 nand t219;
|
|
||||||
t221 = t213 nand t220;
|
|
||||||
t222 = t219 nand t220;
|
|
||||||
t223 = t221 nand t222;
|
|
||||||
t224 = _230gat;
|
|
||||||
t225 = t224 and t19;
|
|
||||||
t226 = t169 nand t110;
|
|
||||||
t227 = t169 nand t226;
|
|
||||||
t228 = t110 nand t226;
|
|
||||||
t229 = t227 nand t228;
|
|
||||||
t230 = t225 nand t229;
|
|
||||||
t231 = t225 nand t230;
|
|
||||||
t232 = t229 nand t230;
|
|
||||||
t233 = t231 nand t232;
|
|
||||||
t234 = t223 nand t233;
|
|
||||||
t235 = t223 nand t234;
|
|
||||||
t236 = t233 nand t234;
|
|
||||||
t237 = t235 nand t236;
|
|
||||||
t238 = not t237;
|
|
||||||
t239 = t209 and t238;
|
|
||||||
t240 = t181 and t239;
|
|
||||||
t241 = t123 and t240;
|
|
||||||
t242 = t145 nand t86;
|
|
||||||
t243 = t145 nand t242;
|
|
||||||
t244 = t86 nand t242;
|
|
||||||
t245 = t243 nand t244;
|
|
||||||
t246 = t160 nand t101;
|
|
||||||
t247 = t160 nand t246;
|
|
||||||
t248 = t101 nand t246;
|
|
||||||
t249 = t247 nand t248;
|
|
||||||
t250 = t245 nand t249;
|
|
||||||
t251 = t245 nand t250;
|
|
||||||
t252 = t249 nand t250;
|
|
||||||
t253 = t251 nand t252;
|
|
||||||
t254 = _227gat;
|
|
||||||
t255 = t254 and t19;
|
|
||||||
t256 = t186 nand t214;
|
|
||||||
t257 = t186 nand t256;
|
|
||||||
t258 = t214 nand t256;
|
|
||||||
t259 = t257 nand t258;
|
|
||||||
t260 = t128 nand t69;
|
|
||||||
t261 = t128 nand t260;
|
|
||||||
t262 = t69 nand t260;
|
|
||||||
t263 = t261 nand t262;
|
|
||||||
t264 = t259 nand t263;
|
|
||||||
t265 = t259 nand t264;
|
|
||||||
t266 = t263 nand t264;
|
|
||||||
t267 = t265 nand t266;
|
|
||||||
t268 = t36 nand t267;
|
|
||||||
t269 = t36 nand t268;
|
|
||||||
t270 = t267 nand t268;
|
|
||||||
t271 = t269 nand t270;
|
|
||||||
t272 = t255 nand t271;
|
|
||||||
t273 = t255 nand t272;
|
|
||||||
t274 = t271 nand t272;
|
|
||||||
t275 = t273 nand t274;
|
|
||||||
t276 = t253 nand t275;
|
|
||||||
t277 = t253 nand t276;
|
|
||||||
t278 = t275 nand t276;
|
|
||||||
t279 = t277 nand t278;
|
|
||||||
t280 = not t279;
|
|
||||||
t281 = not t64;
|
|
||||||
t282 = t140 nand t81;
|
|
||||||
t283 = t140 nand t282;
|
|
||||||
t284 = t81 nand t282;
|
|
||||||
t285 = t283 nand t284;
|
|
||||||
t286 = t155 nand t96;
|
|
||||||
t287 = t155 nand t286;
|
|
||||||
t288 = t96 nand t286;
|
|
||||||
t289 = t287 nand t288;
|
|
||||||
t290 = t285 nand t289;
|
|
||||||
t291 = t285 nand t290;
|
|
||||||
t292 = t289 nand t290;
|
|
||||||
t293 = t291 nand t292;
|
|
||||||
t294 = _226gat;
|
|
||||||
t295 = t294 and t19;
|
|
||||||
t296 = t187 nand t215;
|
|
||||||
t297 = t187 nand t296;
|
|
||||||
t298 = t215 nand t296;
|
|
||||||
t299 = t297 nand t298;
|
|
||||||
t300 = t129 nand t70;
|
|
||||||
t301 = t129 nand t300;
|
|
||||||
t302 = t70 nand t300;
|
|
||||||
t303 = t301 nand t302;
|
|
||||||
t304 = t299 nand t303;
|
|
||||||
t305 = t299 nand t304;
|
|
||||||
t306 = t303 nand t304;
|
|
||||||
t307 = t305 nand t306;
|
|
||||||
t308 = t267 nand t307;
|
|
||||||
t309 = t267 nand t308;
|
|
||||||
t310 = t307 nand t308;
|
|
||||||
t311 = t309 nand t310;
|
|
||||||
t312 = t295 nand t311;
|
|
||||||
t313 = t295 nand t312;
|
|
||||||
t314 = t311 nand t312;
|
|
||||||
t315 = t313 nand t314;
|
|
||||||
t316 = t293 nand t315;
|
|
||||||
t317 = t293 nand t316;
|
|
||||||
t318 = t315 nand t316;
|
|
||||||
t319 = t317 nand t318;
|
|
||||||
t320 = t281 and t319;
|
|
||||||
t321 = t280 and t320;
|
|
||||||
t322 = t146 nand t87;
|
|
||||||
t323 = t146 nand t322;
|
|
||||||
t324 = t87 nand t322;
|
|
||||||
t325 = t323 nand t324;
|
|
||||||
t326 = t161 nand t102;
|
|
||||||
t327 = t161 nand t326;
|
|
||||||
t328 = t102 nand t326;
|
|
||||||
t329 = t327 nand t328;
|
|
||||||
t330 = t325 nand t329;
|
|
||||||
t331 = t325 nand t330;
|
|
||||||
t332 = t329 nand t330;
|
|
||||||
t333 = t331 nand t332;
|
|
||||||
t334 = _228gat;
|
|
||||||
t335 = t334 and t19;
|
|
||||||
t336 = t52 nand t307;
|
|
||||||
t337 = t52 nand t336;
|
|
||||||
t338 = t307 nand t336;
|
|
||||||
t339 = t337 nand t338;
|
|
||||||
t340 = t335 nand t339;
|
|
||||||
t341 = t335 nand t340;
|
|
||||||
t342 = t339 nand t340;
|
|
||||||
t343 = t341 nand t342;
|
|
||||||
t344 = t333 nand t343;
|
|
||||||
t345 = t333 nand t344;
|
|
||||||
t346 = t343 nand t344;
|
|
||||||
t347 = t345 nand t346;
|
|
||||||
t348 = not t347;
|
|
||||||
t349 = t321 and t348;
|
|
||||||
t350 = not t319;
|
|
||||||
t351 = t281 and t350;
|
|
||||||
t352 = t280 and t351;
|
|
||||||
t353 = t352 and t347;
|
|
||||||
t354 = t279 and t351;
|
|
||||||
t355 = t354 and t348;
|
|
||||||
t356 = t353 or t355;
|
|
||||||
t357 = t349 or t356;
|
|
||||||
t358 = t64 and t350;
|
|
||||||
t359 = t280 and t358;
|
|
||||||
t360 = t359 and t348;
|
|
||||||
t361 = t357 or t360;
|
|
||||||
t362 = t241 and t361;
|
|
||||||
t363 = t64 and t362;
|
|
||||||
t364 = t2 nand t363;
|
|
||||||
t365 = t2 nand t364;
|
|
||||||
t366 = t363 nand t364;
|
|
||||||
t367 = t365 nand t366;
|
|
||||||
t368 = t281 and t280;
|
|
||||||
t369 = t368 and t348;
|
|
||||||
t370 = t351 and t280;
|
|
||||||
t371 = t351 and t348;
|
|
||||||
t372 = t370 or t371;
|
|
||||||
t373 = t369 or t372;
|
|
||||||
t374 = t350 and t280;
|
|
||||||
t375 = t374 and t348;
|
|
||||||
t376 = t373 or t375;
|
|
||||||
t377 = t241 and t376;
|
|
||||||
t378 = t64 and t377;
|
|
||||||
t379 = t2 nand t378;
|
|
||||||
t380 = t2 nand t379;
|
|
||||||
t381 = t378 nand t379;
|
|
||||||
t382 = t380 nand t381;
|
|
||||||
t383 = t367 biimp t382;
|
|
||||||
t384 = t319 and t362;
|
|
||||||
t385 = t140 nand t384;
|
|
||||||
t386 = t140 nand t385;
|
|
||||||
t387 = t384 nand t385;
|
|
||||||
t388 = t386 nand t387;
|
|
||||||
t389 = t319 and t377;
|
|
||||||
t390 = t140 nand t389;
|
|
||||||
t391 = t140 nand t390;
|
|
||||||
t392 = t389 nand t390;
|
|
||||||
t393 = t391 nand t392;
|
|
||||||
t394 = t388 biimp t393;
|
|
||||||
t466 = not t209;
|
|
||||||
t467 = t466 and t237;
|
|
||||||
t468 = t181 and t467;
|
|
||||||
t469 = t123 and t468;
|
|
||||||
t470 = t469 and t361;
|
|
||||||
t494 = t279 and t470;
|
|
||||||
t495 = t160 nand t494;
|
|
||||||
t496 = t160 nand t495;
|
|
||||||
t497 = t494 nand t495;
|
|
||||||
t498 = t496 nand t497;
|
|
||||||
t476 = t469 and t376;
|
|
||||||
t499 = t279 and t476;
|
|
||||||
t500 = t160 nand t499;
|
|
||||||
t501 = t160 nand t500;
|
|
||||||
t502 = t499 nand t500;
|
|
||||||
t503 = t501 nand t502;
|
|
||||||
t504 = t498 biimp t503;
|
|
||||||
t505 = t347 and t470;
|
|
||||||
t506 = t161 nand t505;
|
|
||||||
t507 = t161 nand t506;
|
|
||||||
t508 = t505 nand t506;
|
|
||||||
t509 = t507 nand t508;
|
|
||||||
t510 = t347 and t476;
|
|
||||||
t511 = t161 nand t510;
|
|
||||||
t512 = t161 nand t511;
|
|
||||||
t513 = t510 nand t511;
|
|
||||||
t514 = t512 nand t513;
|
|
||||||
t515 = t509 biimp t514;
|
|
||||||
t417 = not t181;
|
|
||||||
t516 = t417 and t467;
|
|
||||||
t517 = t122 and t516;
|
|
||||||
t518 = t517 and t361;
|
|
||||||
t519 = t64 and t518;
|
|
||||||
t520 = t9 nand t519;
|
|
||||||
t521 = t9 nand t520;
|
|
||||||
t522 = t519 nand t520;
|
|
||||||
t523 = t521 nand t522;
|
|
||||||
t524 = t517 and t376;
|
|
||||||
t525 = t64 and t524;
|
|
||||||
t526 = t9 nand t525;
|
|
||||||
t527 = t9 nand t526;
|
|
||||||
t528 = t525 nand t526;
|
|
||||||
t529 = t527 nand t528;
|
|
||||||
t530 = t523 biimp t529;
|
|
||||||
t531 = t319 and t518;
|
|
||||||
t532 = t96 nand t531;
|
|
||||||
t533 = t96 nand t532;
|
|
||||||
t534 = t531 nand t532;
|
|
||||||
t535 = t533 nand t534;
|
|
||||||
t536 = t319 and t524;
|
|
||||||
t537 = t96 nand t536;
|
|
||||||
t538 = t96 nand t537;
|
|
||||||
t539 = t536 nand t537;
|
|
||||||
t540 = t538 nand t539;
|
|
||||||
t541 = t535 biimp t540;
|
|
||||||
t542 = t279 and t518;
|
|
||||||
t543 = t101 nand t542;
|
|
||||||
t544 = t101 nand t543;
|
|
||||||
t545 = t542 nand t543;
|
|
||||||
t546 = t544 nand t545;
|
|
||||||
t547 = t279 and t524;
|
|
||||||
t548 = t101 nand t547;
|
|
||||||
t549 = t101 nand t548;
|
|
||||||
t550 = t547 nand t548;
|
|
||||||
t551 = t549 nand t550;
|
|
||||||
t552 = t546 biimp t551;
|
|
||||||
t553 = t347 and t518;
|
|
||||||
t554 = t102 nand t553;
|
|
||||||
t555 = t102 nand t554;
|
|
||||||
t556 = t553 nand t554;
|
|
||||||
t557 = t555 nand t556;
|
|
||||||
t558 = t347 and t524;
|
|
||||||
t559 = t102 nand t558;
|
|
||||||
t560 = t102 nand t559;
|
|
||||||
t561 = t558 nand t559;
|
|
||||||
t562 = t560 nand t561;
|
|
||||||
t563 = t557 biimp t562;
|
|
||||||
t564 = t279 and t358;
|
|
||||||
t565 = t348 and t564;
|
|
||||||
t566 = t516 and t123;
|
|
||||||
t567 = t466 and t238;
|
|
||||||
t568 = t417 and t567;
|
|
||||||
t569 = t568 and t122;
|
|
||||||
t570 = t181 and t567;
|
|
||||||
t571 = t570 and t123;
|
|
||||||
t572 = t569 or t571;
|
|
||||||
t573 = t566 or t572;
|
|
||||||
t418 = t417 and t239;
|
|
||||||
t574 = t418 and t123;
|
|
||||||
t575 = t573 or t574;
|
|
||||||
t576 = t565 and t575;
|
|
||||||
t577 = t209 and t576;
|
|
||||||
t578 = t21 nand t577;
|
|
||||||
t579 = t21 nand t578;
|
|
||||||
t580 = t577 nand t578;
|
|
||||||
t581 = t579 nand t580;
|
|
||||||
t582 = t466 and t417;
|
|
||||||
t583 = t582 and t123;
|
|
||||||
t584 = t567 and t417;
|
|
||||||
t585 = t567 and t123;
|
|
||||||
t586 = t584 or t585;
|
|
||||||
t587 = t583 or t586;
|
|
||||||
t588 = t238 and t417;
|
|
||||||
t589 = t588 and t123;
|
|
||||||
t590 = t587 or t589;
|
|
||||||
t591 = t565 and t590;
|
|
||||||
t592 = t209 and t591;
|
|
||||||
t593 = t21 nand t592;
|
|
||||||
t594 = t21 nand t593;
|
|
||||||
t595 = t592 nand t593;
|
|
||||||
t596 = t594 nand t595;
|
|
||||||
t597 = t581 biimp t596;
|
|
||||||
t598 = t237 and t576;
|
|
||||||
t599 = t22 nand t598;
|
|
||||||
t600 = t22 nand t599;
|
|
||||||
t601 = t598 nand t599;
|
|
||||||
t602 = t600 nand t601;
|
|
||||||
t603 = t237 and t591;
|
|
||||||
t604 = t22 nand t603;
|
|
||||||
t605 = t22 nand t604;
|
|
||||||
t606 = t603 nand t604;
|
|
||||||
t607 = t605 nand t606;
|
|
||||||
t608 = t602 biimp t607;
|
|
||||||
t609 = t181 and t576;
|
|
||||||
t610 = t27 nand t609;
|
|
||||||
t611 = t27 nand t610;
|
|
||||||
t612 = t609 nand t610;
|
|
||||||
t613 = t611 nand t612;
|
|
||||||
t614 = t181 and t591;
|
|
||||||
t615 = t27 nand t614;
|
|
||||||
t616 = t27 nand t615;
|
|
||||||
t617 = t614 nand t615;
|
|
||||||
t618 = t616 nand t617;
|
|
||||||
t619 = t613 biimp t618;
|
|
||||||
t620 = t122 and t576;
|
|
||||||
t621 = t28 nand t620;
|
|
||||||
t622 = t28 nand t621;
|
|
||||||
t623 = t620 nand t621;
|
|
||||||
t624 = t622 nand t623;
|
|
||||||
t625 = t122 and t591;
|
|
||||||
t626 = t28 nand t625;
|
|
||||||
t627 = t28 nand t626;
|
|
||||||
t628 = t625 nand t626;
|
|
||||||
t629 = t627 nand t628;
|
|
||||||
t630 = t624 biimp t629;
|
|
||||||
t395 = t279 and t362;
|
|
||||||
t396 = t145 nand t395;
|
|
||||||
t397 = t145 nand t396;
|
|
||||||
t398 = t395 nand t396;
|
|
||||||
t399 = t397 nand t398;
|
|
||||||
t400 = t279 and t377;
|
|
||||||
t401 = t145 nand t400;
|
|
||||||
t402 = t145 nand t401;
|
|
||||||
t403 = t400 nand t401;
|
|
||||||
t404 = t402 nand t403;
|
|
||||||
t405 = t399 biimp t404;
|
|
||||||
t631 = t347 and t359;
|
|
||||||
t632 = t631 and t575;
|
|
||||||
t633 = t209 and t632;
|
|
||||||
t634 = t37 nand t633;
|
|
||||||
t635 = t37 nand t634;
|
|
||||||
t636 = t633 nand t634;
|
|
||||||
t637 = t635 nand t636;
|
|
||||||
t638 = t631 and t590;
|
|
||||||
t639 = t209 and t638;
|
|
||||||
t640 = t37 nand t639;
|
|
||||||
t641 = t37 nand t640;
|
|
||||||
t642 = t639 nand t640;
|
|
||||||
t643 = t641 nand t642;
|
|
||||||
t644 = t637 biimp t643;
|
|
||||||
t645 = t237 and t632;
|
|
||||||
t646 = t38 nand t645;
|
|
||||||
t647 = t38 nand t646;
|
|
||||||
t648 = t645 nand t646;
|
|
||||||
t649 = t647 nand t648;
|
|
||||||
t650 = t237 and t638;
|
|
||||||
t651 = t38 nand t650;
|
|
||||||
t652 = t38 nand t651;
|
|
||||||
t653 = t650 nand t651;
|
|
||||||
t654 = t652 nand t653;
|
|
||||||
t655 = t649 biimp t654;
|
|
||||||
t656 = t181 and t632;
|
|
||||||
t657 = t43 nand t656;
|
|
||||||
t658 = t43 nand t657;
|
|
||||||
t659 = t656 nand t657;
|
|
||||||
t660 = t658 nand t659;
|
|
||||||
t661 = t181 and t638;
|
|
||||||
t662 = t43 nand t661;
|
|
||||||
t663 = t43 nand t662;
|
|
||||||
t664 = t661 nand t662;
|
|
||||||
t665 = t663 nand t664;
|
|
||||||
t666 = t660 biimp t665;
|
|
||||||
t667 = t122 and t632;
|
|
||||||
t668 = t44 nand t667;
|
|
||||||
t669 = t44 nand t668;
|
|
||||||
t670 = t667 nand t668;
|
|
||||||
t671 = t669 nand t670;
|
|
||||||
t672 = t122 and t638;
|
|
||||||
t673 = t44 nand t672;
|
|
||||||
t674 = t44 nand t673;
|
|
||||||
t675 = t672 nand t673;
|
|
||||||
t676 = t674 nand t675;
|
|
||||||
t677 = t671 biimp t676;
|
|
||||||
t678 = t279 and t320;
|
|
||||||
t679 = t348 and t678;
|
|
||||||
t680 = t679 and t575;
|
|
||||||
t681 = t209 and t680;
|
|
||||||
t682 = t186 nand t681;
|
|
||||||
t683 = t186 nand t682;
|
|
||||||
t684 = t681 nand t682;
|
|
||||||
t685 = t683 nand t684;
|
|
||||||
t686 = t679 and t590;
|
|
||||||
t687 = t209 and t686;
|
|
||||||
t688 = t186 nand t687;
|
|
||||||
t689 = t186 nand t688;
|
|
||||||
t690 = t687 nand t688;
|
|
||||||
t691 = t689 nand t690;
|
|
||||||
t692 = t685 biimp t691;
|
|
||||||
t693 = t237 and t680;
|
|
||||||
t694 = t214 nand t693;
|
|
||||||
t695 = t214 nand t694;
|
|
||||||
t696 = t693 nand t694;
|
|
||||||
t697 = t695 nand t696;
|
|
||||||
t698 = t237 and t686;
|
|
||||||
t699 = t214 nand t698;
|
|
||||||
t700 = t214 nand t699;
|
|
||||||
t701 = t698 nand t699;
|
|
||||||
t702 = t700 nand t701;
|
|
||||||
t703 = t697 biimp t702;
|
|
||||||
t704 = t181 and t680;
|
|
||||||
t705 = t128 nand t704;
|
|
||||||
t706 = t128 nand t705;
|
|
||||||
t707 = t704 nand t705;
|
|
||||||
t708 = t706 nand t707;
|
|
||||||
t709 = t181 and t686;
|
|
||||||
t710 = t128 nand t709;
|
|
||||||
t711 = t128 nand t710;
|
|
||||||
t712 = t709 nand t710;
|
|
||||||
t713 = t711 nand t712;
|
|
||||||
t714 = t708 biimp t713;
|
|
||||||
t715 = t122 and t680;
|
|
||||||
t716 = t69 nand t715;
|
|
||||||
t717 = t69 nand t716;
|
|
||||||
t718 = t715 nand t716;
|
|
||||||
t719 = t717 nand t718;
|
|
||||||
t720 = t122 and t686;
|
|
||||||
t721 = t69 nand t720;
|
|
||||||
t722 = t69 nand t721;
|
|
||||||
t723 = t720 nand t721;
|
|
||||||
t724 = t722 nand t723;
|
|
||||||
t725 = t719 biimp t724;
|
|
||||||
t726 = t347 and t321;
|
|
||||||
t727 = t726 and t575;
|
|
||||||
t728 = t209 and t727;
|
|
||||||
t729 = t187 nand t728;
|
|
||||||
t730 = t187 nand t729;
|
|
||||||
t731 = t728 nand t729;
|
|
||||||
t732 = t730 nand t731;
|
|
||||||
t733 = t726 and t590;
|
|
||||||
t734 = t209 and t733;
|
|
||||||
t735 = t187 nand t734;
|
|
||||||
t736 = t187 nand t735;
|
|
||||||
t737 = t734 nand t735;
|
|
||||||
t738 = t736 nand t737;
|
|
||||||
t739 = t732 biimp t738;
|
|
||||||
t740 = t237 and t727;
|
|
||||||
t741 = t215 nand t740;
|
|
||||||
t742 = t215 nand t741;
|
|
||||||
t743 = t740 nand t741;
|
|
||||||
t744 = t742 nand t743;
|
|
||||||
t745 = t237 and t733;
|
|
||||||
t746 = t215 nand t745;
|
|
||||||
t747 = t215 nand t746;
|
|
||||||
t748 = t745 nand t746;
|
|
||||||
t749 = t747 nand t748;
|
|
||||||
t750 = t744 biimp t749;
|
|
||||||
t406 = t347 and t362;
|
|
||||||
t407 = t146 nand t406;
|
|
||||||
t408 = t146 nand t407;
|
|
||||||
t409 = t406 nand t407;
|
|
||||||
t410 = t408 nand t409;
|
|
||||||
t411 = t347 and t377;
|
|
||||||
t412 = t146 nand t411;
|
|
||||||
t413 = t146 nand t412;
|
|
||||||
t414 = t411 nand t412;
|
|
||||||
t415 = t413 nand t414;
|
|
||||||
t416 = t410 biimp t415;
|
|
||||||
t751 = t181 and t727;
|
|
||||||
t752 = t129 nand t751;
|
|
||||||
t753 = t129 nand t752;
|
|
||||||
t754 = t751 nand t752;
|
|
||||||
t755 = t753 nand t754;
|
|
||||||
t756 = t181 and t733;
|
|
||||||
t757 = t129 nand t756;
|
|
||||||
t758 = t129 nand t757;
|
|
||||||
t759 = t756 nand t757;
|
|
||||||
t760 = t758 nand t759;
|
|
||||||
t761 = t755 biimp t760;
|
|
||||||
t762 = t122 and t727;
|
|
||||||
t763 = t70 nand t762;
|
|
||||||
t764 = t70 nand t763;
|
|
||||||
t765 = t762 nand t763;
|
|
||||||
t766 = t764 nand t765;
|
|
||||||
t767 = t122 and t733;
|
|
||||||
t768 = t70 nand t767;
|
|
||||||
t769 = t70 nand t768;
|
|
||||||
t770 = t767 nand t768;
|
|
||||||
t771 = t769 nand t770;
|
|
||||||
t772 = t766 biimp t771;
|
|
||||||
t419 = t122 and t418;
|
|
||||||
t420 = t419 and t361;
|
|
||||||
t421 = t64 and t420;
|
|
||||||
t422 = t3 nand t421;
|
|
||||||
t423 = t3 nand t422;
|
|
||||||
t424 = t421 nand t422;
|
|
||||||
t425 = t423 nand t424;
|
|
||||||
t426 = t419 and t376;
|
|
||||||
t427 = t64 and t426;
|
|
||||||
t428 = t3 nand t427;
|
|
||||||
t429 = t3 nand t428;
|
|
||||||
t430 = t427 nand t428;
|
|
||||||
t431 = t429 nand t430;
|
|
||||||
t432 = t425 biimp t431;
|
|
||||||
t433 = t319 and t420;
|
|
||||||
t434 = t81 nand t433;
|
|
||||||
t435 = t81 nand t434;
|
|
||||||
t436 = t433 nand t434;
|
|
||||||
t437 = t435 nand t436;
|
|
||||||
t438 = t319 and t426;
|
|
||||||
t439 = t81 nand t438;
|
|
||||||
t440 = t81 nand t439;
|
|
||||||
t441 = t438 nand t439;
|
|
||||||
t442 = t440 nand t441;
|
|
||||||
t443 = t437 biimp t442;
|
|
||||||
t444 = t279 and t420;
|
|
||||||
t445 = t86 nand t444;
|
|
||||||
t446 = t86 nand t445;
|
|
||||||
t447 = t444 nand t445;
|
|
||||||
t448 = t446 nand t447;
|
|
||||||
t449 = t279 and t426;
|
|
||||||
t450 = t86 nand t449;
|
|
||||||
t451 = t86 nand t450;
|
|
||||||
t452 = t449 nand t450;
|
|
||||||
t453 = t451 nand t452;
|
|
||||||
t454 = t448 biimp t453;
|
|
||||||
t455 = t347 and t420;
|
|
||||||
t456 = t87 nand t455;
|
|
||||||
t457 = t87 nand t456;
|
|
||||||
t458 = t455 nand t456;
|
|
||||||
t459 = t457 nand t458;
|
|
||||||
t460 = t347 and t426;
|
|
||||||
t461 = t87 nand t460;
|
|
||||||
t462 = t87 nand t461;
|
|
||||||
t463 = t460 nand t461;
|
|
||||||
t464 = t462 nand t463;
|
|
||||||
t465 = t459 biimp t464;
|
|
||||||
t471 = t64 and t470;
|
|
||||||
t472 = t8 nand t471;
|
|
||||||
t473 = t8 nand t472;
|
|
||||||
t474 = t471 nand t472;
|
|
||||||
t475 = t473 nand t474;
|
|
||||||
t477 = t64 and t476;
|
|
||||||
t478 = t8 nand t477;
|
|
||||||
t479 = t8 nand t478;
|
|
||||||
t480 = t477 nand t478;
|
|
||||||
t481 = t479 nand t480;
|
|
||||||
t482 = t475 biimp t481;
|
|
||||||
t483 = t319 and t470;
|
|
||||||
t484 = t155 nand t483;
|
|
||||||
t485 = t155 nand t484;
|
|
||||||
t486 = t483 nand t484;
|
|
||||||
t487 = t485 nand t486;
|
|
||||||
t488 = t319 and t476;
|
|
||||||
t489 = t155 nand t488;
|
|
||||||
t490 = t155 nand t489;
|
|
||||||
t491 = t488 nand t489;
|
|
||||||
t492 = t490 nand t491;
|
|
||||||
t493 = t487 biimp t492;
|
|
||||||
|
|
||||||
tautology t383;
|
|
||||||
tautology t394;
|
|
||||||
tautology t504;
|
|
||||||
tautology t515;
|
|
||||||
tautology t530;
|
|
||||||
tautology t541;
|
|
||||||
tautology t552;
|
|
||||||
tautology t563;
|
|
||||||
tautology t597;
|
|
||||||
tautology t608;
|
|
||||||
tautology t619;
|
|
||||||
tautology t630;
|
|
||||||
tautology t405;
|
|
||||||
tautology t644;
|
|
||||||
tautology t655;
|
|
||||||
tautology t666;
|
|
||||||
tautology t677;
|
|
||||||
tautology t692;
|
|
||||||
tautology t703;
|
|
||||||
tautology t714;
|
|
||||||
tautology t725;
|
|
||||||
tautology t739;
|
|
||||||
tautology t750;
|
|
||||||
tautology t416;
|
|
||||||
tautology t761;
|
|
||||||
tautology t772;
|
|
||||||
tautology t432;
|
|
||||||
tautology t443;
|
|
||||||
tautology t454;
|
|
||||||
tautology t465;
|
|
||||||
tautology t482;
|
|
||||||
tautology t493;
|
|
||||||
|
|
@ -1,531 +0,0 @@
|
||||||
/* BDD Calculator data file */
|
|
||||||
|
|
||||||
initial 8000 10000;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
_101 _104 _107 _110 _113 _116 _119 _122 _125 _128
|
|
||||||
_131 _134 _137 _140 _143 _146 _210 _214 _217 _221
|
|
||||||
_224 _227 _234 _237 _469 _472 _475 _478 _898 _900
|
|
||||||
_902 _952 _953 ;
|
|
||||||
|
|
||||||
actions
|
|
||||||
autoreorder 0 sift;
|
|
||||||
|
|
||||||
t2 = _952;
|
|
||||||
t3 = not t2;
|
|
||||||
t4 = _953;
|
|
||||||
t5 = not t4;
|
|
||||||
t6 = _146;
|
|
||||||
t7 = not t6;
|
|
||||||
t8 = _143;
|
|
||||||
t9 = not t8;
|
|
||||||
t10 = not t9;
|
|
||||||
t11 = t7 nand t10;
|
|
||||||
t12 = not t7;
|
|
||||||
t13 = t9 nand t12;
|
|
||||||
t14 = t11 nand t13;
|
|
||||||
t15 = _128;
|
|
||||||
t16 = not t15;
|
|
||||||
t17 = not t16;
|
|
||||||
t18 = t14 nand t17;
|
|
||||||
t19 = not t14;
|
|
||||||
t20 = t16 nand t19;
|
|
||||||
t21 = t18 nand t20;
|
|
||||||
t22 = _125;
|
|
||||||
t23 = not t22;
|
|
||||||
t24 = not t23;
|
|
||||||
t25 = t21 nand t24;
|
|
||||||
t26 = not t21;
|
|
||||||
t27 = t23 nand t26;
|
|
||||||
t28 = t25 nand t27;
|
|
||||||
t29 = _224;
|
|
||||||
t30 = t29 and t5;
|
|
||||||
t31 = not t30;
|
|
||||||
t32 = t28 nand t31;
|
|
||||||
t33 = not t28;
|
|
||||||
t34 = t30 nand t33;
|
|
||||||
t35 = t32 nand t34;
|
|
||||||
t36 = not t35;
|
|
||||||
t37 = _107;
|
|
||||||
t38 = not t37;
|
|
||||||
t39 = _104;
|
|
||||||
t40 = not t39;
|
|
||||||
t41 = not t40;
|
|
||||||
t42 = t38 nand t41;
|
|
||||||
t43 = not t38;
|
|
||||||
t44 = t40 nand t43;
|
|
||||||
t45 = t42 nand t44;
|
|
||||||
t46 = _101;
|
|
||||||
t47 = not t46;
|
|
||||||
t48 = not t47;
|
|
||||||
t49 = t45 nand t48;
|
|
||||||
t50 = not t45;
|
|
||||||
t51 = t47 nand t50;
|
|
||||||
t52 = t49 nand t51;
|
|
||||||
t53 = not t52;
|
|
||||||
t54 = _119;
|
|
||||||
t55 = not t54;
|
|
||||||
t56 = _116;
|
|
||||||
t57 = not t56;
|
|
||||||
t58 = not t57;
|
|
||||||
t59 = t55 nand t58;
|
|
||||||
t60 = not t55;
|
|
||||||
t61 = t57 nand t60;
|
|
||||||
t62 = t59 nand t61;
|
|
||||||
t63 = _113;
|
|
||||||
t64 = not t63;
|
|
||||||
t65 = not t64;
|
|
||||||
t66 = t62 nand t65;
|
|
||||||
t67 = not t62;
|
|
||||||
t68 = t64 nand t67;
|
|
||||||
t69 = t66 nand t68;
|
|
||||||
t70 = not t69;
|
|
||||||
t71 = t53 nand t70;
|
|
||||||
t72 = not t53;
|
|
||||||
t73 = t69 nand t72;
|
|
||||||
t74 = t71 nand t73;
|
|
||||||
t75 = _122;
|
|
||||||
t76 = not t75;
|
|
||||||
t77 = _110;
|
|
||||||
t78 = not t77;
|
|
||||||
t79 = not t78;
|
|
||||||
t80 = t76 nand t79;
|
|
||||||
t81 = not t76;
|
|
||||||
t82 = t78 nand t81;
|
|
||||||
t83 = t80 nand t82;
|
|
||||||
t84 = not t83;
|
|
||||||
t85 = not t84;
|
|
||||||
t86 = t74 nand t85;
|
|
||||||
t87 = not t74;
|
|
||||||
t88 = t84 nand t87;
|
|
||||||
t89 = t86 nand t88;
|
|
||||||
t90 = not t89;
|
|
||||||
t91 = t36 nand t90;
|
|
||||||
t92 = not t36;
|
|
||||||
t93 = t89 nand t92;
|
|
||||||
t94 = t91 nand t93;
|
|
||||||
t95 = not t94;
|
|
||||||
t96 = _902;
|
|
||||||
t97 = not t96;
|
|
||||||
t98 = t95 nand t97;
|
|
||||||
t99 = _210;
|
|
||||||
t100 = _237;
|
|
||||||
t101 = not t100;
|
|
||||||
t102 = t101 nand t97;
|
|
||||||
t103 = t99 nand t102;
|
|
||||||
t104 = not t103;
|
|
||||||
t105 = t98 nand t104;
|
|
||||||
t106 = not t98;
|
|
||||||
t107 = t103 nand t106;
|
|
||||||
t108 = t105 nand t107;
|
|
||||||
t109 = not t108;
|
|
||||||
t110 = _140;
|
|
||||||
t111 = not t110;
|
|
||||||
t112 = not t111;
|
|
||||||
t113 = t78 nand t112;
|
|
||||||
t114 = t111 nand t79;
|
|
||||||
t115 = t113 nand t114;
|
|
||||||
t116 = _227;
|
|
||||||
t117 = t116 and t5;
|
|
||||||
t118 = not t117;
|
|
||||||
t119 = t115 nand t118;
|
|
||||||
t120 = not t115;
|
|
||||||
t121 = t117 nand t120;
|
|
||||||
t122 = t119 nand t121;
|
|
||||||
t123 = not t26;
|
|
||||||
t124 = t52 nand t123;
|
|
||||||
t125 = t26 nand t53;
|
|
||||||
t126 = t124 nand t125;
|
|
||||||
t127 = _137;
|
|
||||||
t128 = not t127;
|
|
||||||
t129 = _134;
|
|
||||||
t130 = not t129;
|
|
||||||
t131 = not t130;
|
|
||||||
t132 = t128 nand t131;
|
|
||||||
t133 = not t128;
|
|
||||||
t134 = t130 nand t133;
|
|
||||||
t135 = t132 nand t134;
|
|
||||||
t136 = _131;
|
|
||||||
t137 = not t136;
|
|
||||||
t138 = not t137;
|
|
||||||
t139 = t135 nand t138;
|
|
||||||
t140 = not t135;
|
|
||||||
t141 = t137 nand t140;
|
|
||||||
t142 = t139 nand t141;
|
|
||||||
t143 = not t142;
|
|
||||||
t144 = not t143;
|
|
||||||
t145 = t126 nand t144;
|
|
||||||
t146 = not t126;
|
|
||||||
t147 = t143 nand t146;
|
|
||||||
t148 = t145 nand t147;
|
|
||||||
t149 = not t148;
|
|
||||||
t150 = not t149;
|
|
||||||
t151 = t122 nand t150;
|
|
||||||
t152 = not t122;
|
|
||||||
t153 = t149 nand t152;
|
|
||||||
t154 = t151 nand t153;
|
|
||||||
t155 = t154 nand t97;
|
|
||||||
t156 = _469;
|
|
||||||
t157 = not t156;
|
|
||||||
t158 = not t157;
|
|
||||||
t159 = t155 nand t158;
|
|
||||||
t160 = not t155;
|
|
||||||
t161 = t157 nand t160;
|
|
||||||
t162 = t159 nand t161;
|
|
||||||
t163 = not t162;
|
|
||||||
t164 = _214;
|
|
||||||
t165 = t164 nand t102;
|
|
||||||
t166 = t99 and t101;
|
|
||||||
t167 = t166 and t5;
|
|
||||||
t168 = not t167;
|
|
||||||
t169 = t47 nand t168;
|
|
||||||
t170 = t167 nand t48;
|
|
||||||
t171 = t169 nand t170;
|
|
||||||
t172 = not t171;
|
|
||||||
t173 = t143 nand t26;
|
|
||||||
t174 = t21 nand t144;
|
|
||||||
t175 = t173 nand t174;
|
|
||||||
t176 = not t70;
|
|
||||||
t177 = t175 nand t176;
|
|
||||||
t178 = not t175;
|
|
||||||
t179 = t70 nand t178;
|
|
||||||
t180 = t177 nand t179;
|
|
||||||
t181 = not t180;
|
|
||||||
t182 = not t181;
|
|
||||||
t183 = t172 nand t182;
|
|
||||||
t184 = not t172;
|
|
||||||
t185 = t181 nand t184;
|
|
||||||
t186 = t183 nand t185;
|
|
||||||
t187 = t186 nand t97;
|
|
||||||
t188 = _472;
|
|
||||||
t189 = not t188;
|
|
||||||
t190 = not t189;
|
|
||||||
t191 = t187 nand t190;
|
|
||||||
t192 = not t187;
|
|
||||||
t193 = t189 nand t192;
|
|
||||||
t194 = t191 nand t193;
|
|
||||||
t195 = not t194;
|
|
||||||
t196 = t23 nand t112;
|
|
||||||
t197 = t111 nand t24;
|
|
||||||
t198 = t196 nand t197;
|
|
||||||
t199 = t198 nand t12;
|
|
||||||
t200 = not t198;
|
|
||||||
t201 = t7 nand t200;
|
|
||||||
t202 = t199 nand t201;
|
|
||||||
t203 = t164 and t101;
|
|
||||||
t204 = t203 and t5;
|
|
||||||
t205 = not t204;
|
|
||||||
t206 = t9 nand t205;
|
|
||||||
t207 = t204 nand t10;
|
|
||||||
t208 = t206 nand t207;
|
|
||||||
t209 = t208 nand t138;
|
|
||||||
t210 = not t208;
|
|
||||||
t211 = t137 nand t210;
|
|
||||||
t212 = t209 nand t211;
|
|
||||||
t213 = not t212;
|
|
||||||
t214 = t202 nand t213;
|
|
||||||
t215 = not t202;
|
|
||||||
t216 = t212 nand t215;
|
|
||||||
t217 = t214 nand t216;
|
|
||||||
t218 = t76 nand t65;
|
|
||||||
t219 = t64 nand t81;
|
|
||||||
t220 = t218 nand t219;
|
|
||||||
t221 = t220 nand t41;
|
|
||||||
t222 = not t220;
|
|
||||||
t223 = t40 nand t222;
|
|
||||||
t224 = t221 nand t223;
|
|
||||||
t225 = not t224;
|
|
||||||
t226 = t217 nand t225;
|
|
||||||
t227 = not t217;
|
|
||||||
t228 = t224 nand t227;
|
|
||||||
t229 = t226 nand t228;
|
|
||||||
t230 = t229 nand t97;
|
|
||||||
t231 = _475;
|
|
||||||
t232 = not t231;
|
|
||||||
t233 = not t232;
|
|
||||||
t234 = t230 nand t233;
|
|
||||||
t235 = not t230;
|
|
||||||
t236 = t232 nand t235;
|
|
||||||
t237 = t234 nand t236;
|
|
||||||
t238 = not t237;
|
|
||||||
t239 = t16 nand t60;
|
|
||||||
t240 = t55 nand t17;
|
|
||||||
t241 = t239 nand t240;
|
|
||||||
t242 = t241 nand t79;
|
|
||||||
t243 = not t241;
|
|
||||||
t244 = t78 nand t243;
|
|
||||||
t245 = t242 nand t244;
|
|
||||||
t246 = not t245;
|
|
||||||
t247 = not t246;
|
|
||||||
t248 = t215 nand t247;
|
|
||||||
t249 = not t215;
|
|
||||||
t250 = t246 nand t249;
|
|
||||||
t251 = t248 nand t250;
|
|
||||||
t252 = _221;
|
|
||||||
t253 = _234;
|
|
||||||
t254 = t252 and t253;
|
|
||||||
t255 = t254 and t5;
|
|
||||||
t256 = t255 nand t133;
|
|
||||||
t257 = not t255;
|
|
||||||
t258 = t128 nand t257;
|
|
||||||
t259 = t256 nand t258;
|
|
||||||
t260 = not t259;
|
|
||||||
t261 = not t260;
|
|
||||||
t262 = t251 nand t261;
|
|
||||||
t263 = not t251;
|
|
||||||
t264 = t260 nand t263;
|
|
||||||
t265 = t262 nand t264;
|
|
||||||
t266 = t265 nand t97;
|
|
||||||
t267 = _217;
|
|
||||||
t268 = t253 nand t97;
|
|
||||||
t269 = t267 nand t268;
|
|
||||||
t270 = not t269;
|
|
||||||
t271 = t266 nand t270;
|
|
||||||
t272 = not t266;
|
|
||||||
t273 = t269 nand t272;
|
|
||||||
t274 = t271 nand t273;
|
|
||||||
t275 = not t274;
|
|
||||||
t276 = t76 nand t58;
|
|
||||||
t277 = t57 nand t81;
|
|
||||||
t278 = t276 nand t277;
|
|
||||||
t279 = t278 nand t43;
|
|
||||||
t280 = not t278;
|
|
||||||
t281 = t38 nand t280;
|
|
||||||
t282 = t279 nand t281;
|
|
||||||
t283 = t9 nand t17;
|
|
||||||
t284 = t16 nand t10;
|
|
||||||
t285 = t283 nand t284;
|
|
||||||
t286 = t285 nand t131;
|
|
||||||
t287 = not t285;
|
|
||||||
t288 = t130 nand t287;
|
|
||||||
t289 = t286 nand t288;
|
|
||||||
t290 = not t289;
|
|
||||||
t291 = t282 nand t290;
|
|
||||||
t292 = not t282;
|
|
||||||
t293 = t289 nand t292;
|
|
||||||
t294 = t291 nand t293;
|
|
||||||
t295 = t267 and t253;
|
|
||||||
t296 = t295 and t5;
|
|
||||||
t297 = not t296;
|
|
||||||
t298 = t294 nand t297;
|
|
||||||
t299 = not t294;
|
|
||||||
t300 = t296 nand t299;
|
|
||||||
t301 = t298 nand t300;
|
|
||||||
t302 = t301 nand t97;
|
|
||||||
t303 = _478;
|
|
||||||
t304 = not t303;
|
|
||||||
t305 = not t304;
|
|
||||||
t306 = t302 nand t305;
|
|
||||||
t307 = not t302;
|
|
||||||
t308 = t304 nand t307;
|
|
||||||
t309 = t306 nand t308;
|
|
||||||
t310 = not t309;
|
|
||||||
t311 = t275 and t310;
|
|
||||||
t312 = t238 and t311;
|
|
||||||
t313 = t195 and t312;
|
|
||||||
t314 = t165 and t313;
|
|
||||||
t315 = t163 and t314;
|
|
||||||
t316 = t109 and t315;
|
|
||||||
t317 = t252 nand t268;
|
|
||||||
t318 = t316 nand t317;
|
|
||||||
t319 = t5 and t318;
|
|
||||||
t320 = t3 and t319;
|
|
||||||
t321 = t320 and t3;
|
|
||||||
t322 = t2 and t319;
|
|
||||||
t323 = t310 and t238;
|
|
||||||
t324 = t274 and t194;
|
|
||||||
t325 = t165 and t108;
|
|
||||||
t326 = t317 and t163;
|
|
||||||
t327 = t325 and t326;
|
|
||||||
t328 = t324 and t327;
|
|
||||||
t329 = t323 and t328;
|
|
||||||
t330 = _898;
|
|
||||||
t331 = not t330;
|
|
||||||
t332 = t331 and t96;
|
|
||||||
t333 = t4 and t332;
|
|
||||||
t334 = t253 nand t100;
|
|
||||||
t335 = t333 nand t334;
|
|
||||||
t336 = t2 and t5;
|
|
||||||
t337 = t336 nand t334;
|
|
||||||
t338 = t335 nand t337;
|
|
||||||
t339 = t329 nand t338;
|
|
||||||
t340 = t309 and t238;
|
|
||||||
t341 = t275 and t194;
|
|
||||||
t342 = t341 and t327;
|
|
||||||
t343 = t340 and t342;
|
|
||||||
t344 = t343 nand t338;
|
|
||||||
t345 = t310 and t237;
|
|
||||||
t346 = t345 and t342;
|
|
||||||
t347 = t346 nand t338;
|
|
||||||
t348 = t274 and t195;
|
|
||||||
t349 = t317 and t162;
|
|
||||||
t350 = t325 and t349;
|
|
||||||
t351 = t348 and t350;
|
|
||||||
t352 = t323 and t351;
|
|
||||||
t353 = t352 nand t338;
|
|
||||||
t354 = t275 and t195;
|
|
||||||
t355 = t354 and t350;
|
|
||||||
t356 = t340 and t355;
|
|
||||||
t357 = t356 nand t338;
|
|
||||||
t358 = t341 and t350;
|
|
||||||
t359 = t323 and t358;
|
|
||||||
t360 = t359 nand t338;
|
|
||||||
t361 = t345 and t355;
|
|
||||||
t362 = t361 nand t338;
|
|
||||||
t363 = t360 and t362;
|
|
||||||
t364 = t357 and t363;
|
|
||||||
t365 = t353 and t364;
|
|
||||||
t366 = t347 and t365;
|
|
||||||
t367 = t344 and t366;
|
|
||||||
t368 = t339 and t367;
|
|
||||||
t369 = t309 and t237;
|
|
||||||
t370 = t354 and t327;
|
|
||||||
t371 = t369 and t370;
|
|
||||||
t372 = t371 nand t338;
|
|
||||||
t373 = t368 and t372;
|
|
||||||
t374 = t369 and t358;
|
|
||||||
t375 = _900;
|
|
||||||
t376 = not t375;
|
|
||||||
t377 = t376 and t96;
|
|
||||||
t378 = t4 and t377;
|
|
||||||
t379 = t378 nand t334;
|
|
||||||
t380 = t379 nand t337;
|
|
||||||
t381 = t374 nand t380;
|
|
||||||
t382 = t165 and t109;
|
|
||||||
t383 = t382 and t349;
|
|
||||||
t384 = t348 and t383;
|
|
||||||
t385 = t345 and t384;
|
|
||||||
t386 = t385 nand t380;
|
|
||||||
t387 = t324 and t383;
|
|
||||||
t388 = t323 and t387;
|
|
||||||
t389 = t388 nand t380;
|
|
||||||
t390 = t341 and t383;
|
|
||||||
t391 = t340 and t390;
|
|
||||||
t392 = t391 nand t380;
|
|
||||||
t393 = t345 and t390;
|
|
||||||
t394 = t393 nand t380;
|
|
||||||
t395 = t348 and t327;
|
|
||||||
t396 = t345 and t395;
|
|
||||||
t397 = t396 nand t380;
|
|
||||||
t398 = t324 and t350;
|
|
||||||
t399 = t340 and t398;
|
|
||||||
t400 = t399 nand t380;
|
|
||||||
t401 = t397 and t400;
|
|
||||||
t402 = t394 and t401;
|
|
||||||
t403 = t392 and t402;
|
|
||||||
t404 = t389 and t403;
|
|
||||||
t405 = t386 and t404;
|
|
||||||
t406 = t381 and t405;
|
|
||||||
t407 = t345 and t398;
|
|
||||||
t408 = t407 nand t380;
|
|
||||||
t409 = t406 and t408;
|
|
||||||
t410 = t373 and t409;
|
|
||||||
t411 = not t317;
|
|
||||||
t412 = t411 and t163;
|
|
||||||
t413 = t382 and t412;
|
|
||||||
t414 = t354 and t413;
|
|
||||||
t415 = t323 and t414;
|
|
||||||
t416 = t336 and t334;
|
|
||||||
t417 = t415 nand t416;
|
|
||||||
t418 = t382 and t326;
|
|
||||||
t419 = t348 and t418;
|
|
||||||
t420 = t323 and t419;
|
|
||||||
t421 = t420 nand t416;
|
|
||||||
t422 = t354 and t418;
|
|
||||||
t423 = t340 and t422;
|
|
||||||
t424 = t423 nand t416;
|
|
||||||
t425 = t345 and t422;
|
|
||||||
t426 = t425 nand t416;
|
|
||||||
t427 = t341 and t418;
|
|
||||||
t428 = t323 and t427;
|
|
||||||
t429 = t428 nand t416;
|
|
||||||
t430 = t323 and t370;
|
|
||||||
t431 = t430 nand t416;
|
|
||||||
t432 = t354 and t383;
|
|
||||||
t433 = t323 and t432;
|
|
||||||
t434 = t433 nand t416;
|
|
||||||
t435 = t431 and t434;
|
|
||||||
t436 = t429 and t435;
|
|
||||||
t437 = t426 and t436;
|
|
||||||
t438 = t424 and t437;
|
|
||||||
t439 = t421 and t438;
|
|
||||||
t440 = t417 and t439;
|
|
||||||
t441 = not t165;
|
|
||||||
t442 = t441 and t109;
|
|
||||||
t443 = t442 and t326;
|
|
||||||
t444 = t354 and t443;
|
|
||||||
t445 = t323 and t444;
|
|
||||||
t446 = t445 nand t416;
|
|
||||||
t447 = t440 and t446;
|
|
||||||
t448 = t410 and t447;
|
|
||||||
t449 = t322 and t448;
|
|
||||||
t450 = t321 nor t449;
|
|
||||||
t451 = t319 and t3;
|
|
||||||
t452 = t382 and t163;
|
|
||||||
t453 = t354 and t452;
|
|
||||||
t454 = t323 and t453;
|
|
||||||
t455 = t454 nand t334;
|
|
||||||
t456 = t420 nand t334;
|
|
||||||
t457 = t423 nand t334;
|
|
||||||
t458 = t425 nand t334;
|
|
||||||
t459 = t428 nand t334;
|
|
||||||
t460 = t430 nand t334;
|
|
||||||
t461 = t433 nand t334;
|
|
||||||
t462 = t460 and t461;
|
|
||||||
t463 = t459 and t462;
|
|
||||||
t464 = t458 and t463;
|
|
||||||
t465 = t457 and t464;
|
|
||||||
t466 = t456 and t465;
|
|
||||||
t467 = t455 and t466;
|
|
||||||
t468 = t109 and t326;
|
|
||||||
t469 = t354 and t468;
|
|
||||||
t470 = t323 and t469;
|
|
||||||
t471 = t470 nand t334;
|
|
||||||
t472 = t467 and t471;
|
|
||||||
t473 = t410 and t472;
|
|
||||||
t474 = t319 and t473;
|
|
||||||
t475 = t451 nor t474;
|
|
||||||
t476 = t450 biimp t475;
|
|
||||||
t477 = t35 nand t90;
|
|
||||||
t478 = t89 nand t36;
|
|
||||||
t479 = t477 nand t478;
|
|
||||||
t480 = t99 and t102;
|
|
||||||
t481 = t480 and t96;
|
|
||||||
t482 = t373 nand t409;
|
|
||||||
t483 = t481 and t482;
|
|
||||||
t484 = not t483;
|
|
||||||
t485 = t479 nand t484;
|
|
||||||
t486 = not t479;
|
|
||||||
t487 = t483 nand t486;
|
|
||||||
t488 = t485 nand t487;
|
|
||||||
t489 = t3 nand t4;
|
|
||||||
t490 = t488 and t489;
|
|
||||||
t491 = t99 and t96;
|
|
||||||
t492 = t491 and t482;
|
|
||||||
t493 = not t492;
|
|
||||||
t494 = t479 nand t493;
|
|
||||||
t495 = t492 nand t486;
|
|
||||||
t496 = t494 nand t495;
|
|
||||||
t497 = t496 and t489;
|
|
||||||
t498 = t490 biimp t497;
|
|
||||||
t499 = t267 and t268;
|
|
||||||
t500 = t499 and t96;
|
|
||||||
t501 = t500 and t482;
|
|
||||||
t502 = not t501;
|
|
||||||
t503 = t265 nand t502;
|
|
||||||
t504 = not t265;
|
|
||||||
t505 = t501 nand t504;
|
|
||||||
t506 = t503 nand t505;
|
|
||||||
t507 = t489 and t506;
|
|
||||||
t508 = t267 and t96;
|
|
||||||
t509 = t508 and t482;
|
|
||||||
t510 = not t509;
|
|
||||||
t511 = t265 nand t510;
|
|
||||||
t512 = t509 nand t504;
|
|
||||||
t513 = t511 nand t512;
|
|
||||||
t514 = t489 and t513;
|
|
||||||
t515 = t507 biimp t514;
|
|
||||||
|
|
||||||
tautology t476;
|
|
||||||
tautology t498;
|
|
||||||
tautology t515;
|
|
||||||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -1,260 +0,0 @@
|
||||||
/* BDD Calculator data file */
|
|
||||||
|
|
||||||
initial 10000 10000;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
_1gat _4gat _8gat _11gat _14gat _17gat _21gat _24gat _27gat _30gat
|
|
||||||
_34gat _37gat _40gat _43gat _47gat _50gat _53gat _56gat _60gat _63gat
|
|
||||||
_66gat _69gat _73gat _76gat _79gat _82gat _86gat _89gat _92gat _95gat
|
|
||||||
_99gat _102gat _105gat _108gat _112gat _115gat ;
|
|
||||||
|
|
||||||
actions
|
|
||||||
autoreorder 0 win2ite;
|
|
||||||
|
|
||||||
t2 = _8gat;
|
|
||||||
t3 = _89gat;
|
|
||||||
t4 = not t3;
|
|
||||||
t5 = _95gat;
|
|
||||||
t6 = t4 nand t5;
|
|
||||||
t7 = _76gat;
|
|
||||||
t8 = not t7;
|
|
||||||
t9 = _82gat;
|
|
||||||
t10 = t8 nand t9;
|
|
||||||
t11 = _63gat;
|
|
||||||
t12 = not t11;
|
|
||||||
t13 = _69gat;
|
|
||||||
t14 = t12 nand t13;
|
|
||||||
t15 = _50gat;
|
|
||||||
t16 = not t15;
|
|
||||||
t17 = _56gat;
|
|
||||||
t18 = t16 nand t17;
|
|
||||||
t19 = _37gat;
|
|
||||||
t20 = not t19;
|
|
||||||
t21 = _43gat;
|
|
||||||
t22 = t20 nand t21;
|
|
||||||
t23 = _24gat;
|
|
||||||
t24 = not t23;
|
|
||||||
t25 = _30gat;
|
|
||||||
t26 = t24 nand t25;
|
|
||||||
t27 = _1gat;
|
|
||||||
t28 = not t27;
|
|
||||||
t29 = _4gat;
|
|
||||||
t30 = t28 nand t29;
|
|
||||||
t31 = _11gat;
|
|
||||||
t32 = not t31;
|
|
||||||
t33 = _17gat;
|
|
||||||
t34 = t32 nand t33;
|
|
||||||
t35 = t30 and t34;
|
|
||||||
t36 = t26 and t35;
|
|
||||||
t37 = t22 and t36;
|
|
||||||
t38 = t18 and t37;
|
|
||||||
t39 = t14 and t38;
|
|
||||||
t40 = t10 and t39;
|
|
||||||
t41 = t6 and t40;
|
|
||||||
t42 = _102gat;
|
|
||||||
t43 = not t42;
|
|
||||||
t44 = _108gat;
|
|
||||||
t45 = t43 nand t44;
|
|
||||||
t46 = t41 and t45;
|
|
||||||
t47 = not t46;
|
|
||||||
t48 = t47 xor t6;
|
|
||||||
t49 = _99gat;
|
|
||||||
t50 = not t5;
|
|
||||||
t51 = t49 nor t50;
|
|
||||||
t52 = t48 nand t51;
|
|
||||||
t53 = t47 xor t10;
|
|
||||||
t54 = _86gat;
|
|
||||||
t55 = not t9;
|
|
||||||
t56 = t54 nor t55;
|
|
||||||
t57 = t53 nand t56;
|
|
||||||
t58 = t47 xor t14;
|
|
||||||
t59 = _73gat;
|
|
||||||
t60 = not t13;
|
|
||||||
t61 = t59 nor t60;
|
|
||||||
t62 = t58 nand t61;
|
|
||||||
t63 = t47 xor t18;
|
|
||||||
t64 = _60gat;
|
|
||||||
t65 = not t17;
|
|
||||||
t66 = t64 nor t65;
|
|
||||||
t67 = t63 nand t66;
|
|
||||||
t68 = t47 xor t22;
|
|
||||||
t69 = _47gat;
|
|
||||||
t70 = not t21;
|
|
||||||
t71 = t69 nor t70;
|
|
||||||
t72 = t68 nand t71;
|
|
||||||
t73 = t47 xor t26;
|
|
||||||
t74 = _34gat;
|
|
||||||
t75 = not t25;
|
|
||||||
t76 = t74 nor t75;
|
|
||||||
t77 = t73 nand t76;
|
|
||||||
t78 = t47 xor t30;
|
|
||||||
t79 = not t29;
|
|
||||||
t80 = t2 nor t79;
|
|
||||||
t81 = t78 nand t80;
|
|
||||||
t82 = t47 xor t34;
|
|
||||||
t83 = _21gat;
|
|
||||||
t84 = not t33;
|
|
||||||
t85 = t83 nor t84;
|
|
||||||
t86 = t82 nand t85;
|
|
||||||
t87 = t81 and t86;
|
|
||||||
t88 = t77 and t87;
|
|
||||||
t89 = t72 and t88;
|
|
||||||
t90 = t67 and t89;
|
|
||||||
t91 = t62 and t90;
|
|
||||||
t92 = t57 and t91;
|
|
||||||
t93 = t52 and t92;
|
|
||||||
t94 = t47 xor t45;
|
|
||||||
t95 = _112gat;
|
|
||||||
t96 = not t44;
|
|
||||||
t97 = t95 nor t96;
|
|
||||||
t98 = t94 nand t97;
|
|
||||||
t99 = t93 and t98;
|
|
||||||
t100 = not t99;
|
|
||||||
t101 = t2 nand t100;
|
|
||||||
t102 = t27 nand t47;
|
|
||||||
t103 = t29 and t102;
|
|
||||||
t104 = t101 and t103;
|
|
||||||
t105 = _14gat;
|
|
||||||
t106 = t100 xor t52;
|
|
||||||
t107 = _105gat;
|
|
||||||
t108 = t107 nor t50;
|
|
||||||
t109 = t48 nand t108;
|
|
||||||
t110 = not t109;
|
|
||||||
t111 = t106 nand t110;
|
|
||||||
t112 = t100 xor t57;
|
|
||||||
t113 = _92gat;
|
|
||||||
t114 = t113 nor t55;
|
|
||||||
t115 = t53 nand t114;
|
|
||||||
t116 = not t115;
|
|
||||||
t117 = t112 nand t116;
|
|
||||||
t118 = t100 xor t62;
|
|
||||||
t119 = _79gat;
|
|
||||||
t120 = t119 nor t60;
|
|
||||||
t121 = t58 nand t120;
|
|
||||||
t122 = not t121;
|
|
||||||
t123 = t118 nand t122;
|
|
||||||
t124 = t100 xor t67;
|
|
||||||
t125 = _66gat;
|
|
||||||
t126 = t125 nor t65;
|
|
||||||
t127 = t63 nand t126;
|
|
||||||
t128 = not t127;
|
|
||||||
t129 = t124 nand t128;
|
|
||||||
t130 = t100 xor t72;
|
|
||||||
t131 = _53gat;
|
|
||||||
t132 = t131 nor t70;
|
|
||||||
t133 = t68 nand t132;
|
|
||||||
t134 = not t133;
|
|
||||||
t135 = t130 nand t134;
|
|
||||||
t136 = t100 xor t77;
|
|
||||||
t137 = _40gat;
|
|
||||||
t138 = t137 nor t75;
|
|
||||||
t139 = t73 nand t138;
|
|
||||||
t140 = not t139;
|
|
||||||
t141 = t136 nand t140;
|
|
||||||
t142 = t100 xor t81;
|
|
||||||
t143 = t105 nor t79;
|
|
||||||
t144 = t78 nand t143;
|
|
||||||
t145 = not t144;
|
|
||||||
t146 = t142 nand t145;
|
|
||||||
t147 = t100 xor t86;
|
|
||||||
t148 = _27gat;
|
|
||||||
t149 = t148 nor t84;
|
|
||||||
t150 = t82 nand t149;
|
|
||||||
t151 = not t150;
|
|
||||||
t152 = t147 nand t151;
|
|
||||||
t153 = t146 and t152;
|
|
||||||
t154 = t141 and t153;
|
|
||||||
t155 = t135 and t154;
|
|
||||||
t156 = t129 and t155;
|
|
||||||
t157 = t123 and t156;
|
|
||||||
t158 = t117 and t157;
|
|
||||||
t159 = t111 and t158;
|
|
||||||
t160 = t100 xor t98;
|
|
||||||
t161 = _115gat;
|
|
||||||
t162 = t161 nor t96;
|
|
||||||
t163 = t94 nand t162;
|
|
||||||
t164 = not t163;
|
|
||||||
t165 = t160 nand t164;
|
|
||||||
t166 = t159 and t165;
|
|
||||||
t167 = not t166;
|
|
||||||
t168 = t105 nand t167;
|
|
||||||
t169 = t104 nand t168;
|
|
||||||
t170 = not t169;
|
|
||||||
t171 = t167 nand t107;
|
|
||||||
t172 = t47 nand t3;
|
|
||||||
t173 = t100 nand t49;
|
|
||||||
t174 = t172 and t173;
|
|
||||||
t175 = t171 and t174;
|
|
||||||
t176 = t175 nand t5;
|
|
||||||
t177 = t167 nand t113;
|
|
||||||
t178 = t47 nand t7;
|
|
||||||
t179 = t100 nand t54;
|
|
||||||
t180 = t178 and t179;
|
|
||||||
t181 = t177 and t180;
|
|
||||||
t182 = t181 nand t9;
|
|
||||||
t183 = t167 nand t119;
|
|
||||||
t184 = t47 nand t11;
|
|
||||||
t185 = t100 nand t59;
|
|
||||||
t186 = t184 and t185;
|
|
||||||
t187 = t183 and t186;
|
|
||||||
t188 = t187 nand t13;
|
|
||||||
t189 = t167 nand t125;
|
|
||||||
t190 = t47 nand t15;
|
|
||||||
t191 = t100 nand t64;
|
|
||||||
t192 = t190 and t191;
|
|
||||||
t193 = t189 and t192;
|
|
||||||
t194 = t193 nand t17;
|
|
||||||
t195 = t167 nand t131;
|
|
||||||
t196 = t47 nand t19;
|
|
||||||
t197 = t100 nand t69;
|
|
||||||
t198 = t196 and t197;
|
|
||||||
t199 = t195 and t198;
|
|
||||||
t200 = t199 nand t21;
|
|
||||||
t201 = t167 nand t148;
|
|
||||||
t202 = t47 nand t31;
|
|
||||||
t203 = t100 nand t83;
|
|
||||||
t204 = t202 and t203;
|
|
||||||
t205 = t201 and t204;
|
|
||||||
t206 = t205 nand t33;
|
|
||||||
t207 = t167 nand t137;
|
|
||||||
t208 = t47 nand t23;
|
|
||||||
t209 = t100 nand t74;
|
|
||||||
t210 = t208 and t209;
|
|
||||||
t211 = t207 and t210;
|
|
||||||
t212 = t211 nand t25;
|
|
||||||
t213 = t206 and t212;
|
|
||||||
t214 = t200 and t213;
|
|
||||||
t215 = t194 and t214;
|
|
||||||
t216 = t188 and t215;
|
|
||||||
t217 = t182 and t216;
|
|
||||||
t218 = t176 and t217;
|
|
||||||
t219 = t167 nand t161;
|
|
||||||
t220 = t47 nand t42;
|
|
||||||
t221 = t100 nand t95;
|
|
||||||
t222 = t220 and t221;
|
|
||||||
t223 = t219 and t222;
|
|
||||||
t224 = t223 nand t44;
|
|
||||||
t225 = t218 and t224;
|
|
||||||
t226 = t170 nor t225;
|
|
||||||
t227 = t218 and t96;
|
|
||||||
t228 = t170 nor t227;
|
|
||||||
t229 = t226 biimp t228;
|
|
||||||
t230 = not t188;
|
|
||||||
t231 = t212 and t200;
|
|
||||||
t232 = t230 and t231;
|
|
||||||
t233 = t232 nand t194;
|
|
||||||
t234 = not t200;
|
|
||||||
t235 = t212 nand t234;
|
|
||||||
t236 = t206 and t235;
|
|
||||||
t237 = t233 and t236;
|
|
||||||
t238 = t182 and t231;
|
|
||||||
t239 = not t176;
|
|
||||||
t240 = t238 nand t239;
|
|
||||||
t241 = t237 nand t240;
|
|
||||||
t242 = t212 and t182;
|
|
||||||
t243 = t242 nand t239;
|
|
||||||
t244 = t237 nand t243;
|
|
||||||
t245 = t241 biimp t244;
|
|
||||||
|
|
||||||
tautology t229;
|
|
||||||
tautology t245;
|
|
||||||
|
|
@ -1,409 +0,0 @@
|
||||||
/* BDD Calculator data file */
|
|
||||||
|
|
||||||
initial 10000 10000;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
id0 id1 id2 id3 id4 id5 id6 id7 id8 id9
|
|
||||||
id10 id11 id12 id13 id14 id15 id16 id17 id18 id19
|
|
||||||
id20 id21 id22 id23 id24 id25 id26 id27 id28 id29
|
|
||||||
id30 id31 ic0 ic1 ic2 ic3 ic4 ic5 ic6 ic7
|
|
||||||
r ;
|
|
||||||
|
|
||||||
actions
|
|
||||||
autoreorder 0 sift;
|
|
||||||
t2 = id0;
|
|
||||||
t3 = id4;
|
|
||||||
t4 = t2 xor t3;
|
|
||||||
t5 = id8;
|
|
||||||
t6 = id12;
|
|
||||||
t7 = t5 xor t6;
|
|
||||||
t8 = t4 xor t7;
|
|
||||||
t9 = ic0;
|
|
||||||
t10 = r;
|
|
||||||
t11 = t9 and t10;
|
|
||||||
t12 = id16;
|
|
||||||
t13 = id17;
|
|
||||||
t14 = t12 xor t13;
|
|
||||||
t15 = id18;
|
|
||||||
t16 = id19;
|
|
||||||
t17 = t15 xor t16;
|
|
||||||
t18 = t14 xor t17;
|
|
||||||
t19 = id20;
|
|
||||||
t20 = id21;
|
|
||||||
t21 = t19 xor t20;
|
|
||||||
t22 = id22;
|
|
||||||
t23 = id23;
|
|
||||||
t24 = t22 xor t23;
|
|
||||||
t25 = t21 xor t24;
|
|
||||||
t26 = t18 xor t25;
|
|
||||||
t27 = t11 xor t26;
|
|
||||||
t28 = t8 xor t27;
|
|
||||||
t29 = t16 xor t23;
|
|
||||||
t30 = id27;
|
|
||||||
t31 = id31;
|
|
||||||
t32 = t30 xor t31;
|
|
||||||
t33 = t29 xor t32;
|
|
||||||
t34 = ic7;
|
|
||||||
t35 = t34 and t10;
|
|
||||||
t36 = id5;
|
|
||||||
t37 = t3 xor t36;
|
|
||||||
t38 = id6;
|
|
||||||
t39 = id7;
|
|
||||||
t40 = t38 xor t39;
|
|
||||||
t41 = t37 xor t40;
|
|
||||||
t42 = id13;
|
|
||||||
t43 = t6 xor t42;
|
|
||||||
t44 = id14;
|
|
||||||
t45 = id15;
|
|
||||||
t46 = t44 xor t45;
|
|
||||||
t47 = t43 xor t46;
|
|
||||||
t48 = t41 xor t47;
|
|
||||||
t49 = t35 xor t48;
|
|
||||||
t50 = t33 xor t49;
|
|
||||||
t51 = not t50;
|
|
||||||
t52 = t15 xor t22;
|
|
||||||
t53 = id26;
|
|
||||||
t54 = id30;
|
|
||||||
t55 = t53 xor t54;
|
|
||||||
t56 = t52 xor t55;
|
|
||||||
t57 = ic6;
|
|
||||||
t58 = t57 and t10;
|
|
||||||
t59 = id1;
|
|
||||||
t60 = t2 xor t59;
|
|
||||||
t61 = id2;
|
|
||||||
t62 = id3;
|
|
||||||
t63 = t61 xor t62;
|
|
||||||
t64 = t60 xor t63;
|
|
||||||
t65 = id9;
|
|
||||||
t66 = t5 xor t65;
|
|
||||||
t67 = id10;
|
|
||||||
t68 = id11;
|
|
||||||
t69 = t67 xor t68;
|
|
||||||
t70 = t66 xor t69;
|
|
||||||
t71 = t64 xor t70;
|
|
||||||
t72 = t58 xor t71;
|
|
||||||
t73 = t56 xor t72;
|
|
||||||
t74 = t12 xor t19;
|
|
||||||
t75 = id24;
|
|
||||||
t76 = id28;
|
|
||||||
t77 = t75 xor t76;
|
|
||||||
t78 = t74 xor t77;
|
|
||||||
t79 = ic4;
|
|
||||||
t80 = t79 and t10;
|
|
||||||
t81 = t64 xor t41;
|
|
||||||
t82 = t80 xor t81;
|
|
||||||
t83 = t78 xor t82;
|
|
||||||
t84 = t13 xor t20;
|
|
||||||
t85 = id25;
|
|
||||||
t86 = id29;
|
|
||||||
t87 = t85 xor t86;
|
|
||||||
t88 = t84 xor t87;
|
|
||||||
t89 = ic5;
|
|
||||||
t90 = t89 and t10;
|
|
||||||
t91 = t70 xor t47;
|
|
||||||
t92 = t90 xor t91;
|
|
||||||
t93 = t88 xor t92;
|
|
||||||
t94 = not t93;
|
|
||||||
t95 = t83 and t94;
|
|
||||||
t96 = t73 and t95;
|
|
||||||
t97 = t51 and t96;
|
|
||||||
t98 = t61 xor t38;
|
|
||||||
t99 = t67 xor t44;
|
|
||||||
t100 = t98 xor t99;
|
|
||||||
t101 = ic2;
|
|
||||||
t102 = t101 and t10;
|
|
||||||
t103 = t75 xor t85;
|
|
||||||
t104 = t53 xor t30;
|
|
||||||
t105 = t103 xor t104;
|
|
||||||
t106 = t18 xor t105;
|
|
||||||
t107 = t102 xor t106;
|
|
||||||
t108 = t100 xor t107;
|
|
||||||
t109 = not t108;
|
|
||||||
t110 = not t28;
|
|
||||||
t111 = t59 xor t36;
|
|
||||||
t112 = t65 xor t42;
|
|
||||||
t113 = t111 xor t112;
|
|
||||||
t114 = ic1;
|
|
||||||
t115 = t114 and t10;
|
|
||||||
t116 = t76 xor t86;
|
|
||||||
t117 = t54 xor t31;
|
|
||||||
t118 = t116 xor t117;
|
|
||||||
t119 = t105 xor t118;
|
|
||||||
t120 = t115 xor t119;
|
|
||||||
t121 = t113 xor t120;
|
|
||||||
t122 = t110 and t121;
|
|
||||||
t123 = t109 and t122;
|
|
||||||
t124 = t62 xor t39;
|
|
||||||
t125 = t68 xor t45;
|
|
||||||
t126 = t124 xor t125;
|
|
||||||
t127 = ic3;
|
|
||||||
t128 = t127 and t10;
|
|
||||||
t129 = t25 xor t118;
|
|
||||||
t130 = t128 xor t129;
|
|
||||||
t131 = t126 xor t130;
|
|
||||||
t132 = not t131;
|
|
||||||
t133 = t123 and t132;
|
|
||||||
t134 = not t121;
|
|
||||||
t135 = t110 and t134;
|
|
||||||
t136 = t109 and t135;
|
|
||||||
t137 = t136 and t131;
|
|
||||||
t138 = t108 and t135;
|
|
||||||
t139 = t138 and t132;
|
|
||||||
t140 = t137 or t139;
|
|
||||||
t141 = t133 or t140;
|
|
||||||
t142 = t28 and t134;
|
|
||||||
t143 = t109 and t142;
|
|
||||||
t144 = t143 and t132;
|
|
||||||
t145 = t141 or t144;
|
|
||||||
t146 = t97 and t145;
|
|
||||||
t147 = t28 and t146;
|
|
||||||
t148 = t2 xor t147;
|
|
||||||
t149 = t110 and t109;
|
|
||||||
t150 = t149 and t132;
|
|
||||||
t151 = t135 and t109;
|
|
||||||
t152 = t135 and t132;
|
|
||||||
t153 = t151 or t152;
|
|
||||||
t154 = t150 or t153;
|
|
||||||
t155 = t134 and t109;
|
|
||||||
t156 = t155 and t132;
|
|
||||||
t157 = t154 or t156;
|
|
||||||
t158 = t97 and t157;
|
|
||||||
t159 = t28 and t158;
|
|
||||||
t160 = t2 xor t159;
|
|
||||||
t161 = t148 biimp t160;
|
|
||||||
t162 = t121 and t146;
|
|
||||||
t163 = t59 xor t162;
|
|
||||||
t164 = t121 and t158;
|
|
||||||
t165 = t59 xor t164;
|
|
||||||
t166 = t163 biimp t165;
|
|
||||||
t202 = not t83;
|
|
||||||
t203 = t202 and t93;
|
|
||||||
t204 = t73 and t203;
|
|
||||||
t205 = t51 and t204;
|
|
||||||
t206 = t205 and t145;
|
|
||||||
t218 = t108 and t206;
|
|
||||||
t219 = t67 xor t218;
|
|
||||||
t209 = t205 and t157;
|
|
||||||
t220 = t108 and t209;
|
|
||||||
t221 = t67 xor t220;
|
|
||||||
t222 = t219 biimp t221;
|
|
||||||
t223 = t131 and t206;
|
|
||||||
t224 = t68 xor t223;
|
|
||||||
t225 = t131 and t209;
|
|
||||||
t226 = t68 xor t225;
|
|
||||||
t227 = t224 biimp t226;
|
|
||||||
t177 = not t73;
|
|
||||||
t228 = t177 and t203;
|
|
||||||
t229 = t50 and t228;
|
|
||||||
t230 = t229 and t145;
|
|
||||||
t231 = t28 and t230;
|
|
||||||
t232 = t6 xor t231;
|
|
||||||
t233 = t229 and t157;
|
|
||||||
t234 = t28 and t233;
|
|
||||||
t235 = t6 xor t234;
|
|
||||||
t236 = t232 biimp t235;
|
|
||||||
t237 = t121 and t230;
|
|
||||||
t238 = t42 xor t237;
|
|
||||||
t239 = t121 and t233;
|
|
||||||
t240 = t42 xor t239;
|
|
||||||
t241 = t238 biimp t240;
|
|
||||||
t242 = t108 and t230;
|
|
||||||
t243 = t44 xor t242;
|
|
||||||
t244 = t108 and t233;
|
|
||||||
t245 = t44 xor t244;
|
|
||||||
t246 = t243 biimp t245;
|
|
||||||
t247 = t131 and t230;
|
|
||||||
t248 = t45 xor t247;
|
|
||||||
t249 = t131 and t233;
|
|
||||||
t250 = t45 xor t249;
|
|
||||||
t251 = t248 biimp t250;
|
|
||||||
t252 = t108 and t142;
|
|
||||||
t253 = t132 and t252;
|
|
||||||
t254 = t228 and t51;
|
|
||||||
t255 = t202 and t94;
|
|
||||||
t256 = t177 and t255;
|
|
||||||
t257 = t256 and t50;
|
|
||||||
t258 = t73 and t255;
|
|
||||||
t259 = t258 and t51;
|
|
||||||
t260 = t257 or t259;
|
|
||||||
t261 = t254 or t260;
|
|
||||||
t178 = t177 and t95;
|
|
||||||
t262 = t178 and t51;
|
|
||||||
t263 = t261 or t262;
|
|
||||||
t264 = t253 and t263;
|
|
||||||
t265 = t83 and t264;
|
|
||||||
t266 = t12 xor t265;
|
|
||||||
t267 = t202 and t177;
|
|
||||||
t268 = t267 and t51;
|
|
||||||
t269 = t255 and t177;
|
|
||||||
t270 = t255 and t51;
|
|
||||||
t271 = t269 or t270;
|
|
||||||
t272 = t268 or t271;
|
|
||||||
t273 = t94 and t177;
|
|
||||||
t274 = t273 and t51;
|
|
||||||
t275 = t272 or t274;
|
|
||||||
t276 = t253 and t275;
|
|
||||||
t277 = t83 and t276;
|
|
||||||
t278 = t12 xor t277;
|
|
||||||
t279 = t266 biimp t278;
|
|
||||||
t280 = t93 and t264;
|
|
||||||
t281 = t13 xor t280;
|
|
||||||
t282 = t93 and t276;
|
|
||||||
t283 = t13 xor t282;
|
|
||||||
t284 = t281 biimp t283;
|
|
||||||
t285 = t73 and t264;
|
|
||||||
t286 = t15 xor t285;
|
|
||||||
t287 = t73 and t276;
|
|
||||||
t288 = t15 xor t287;
|
|
||||||
t289 = t286 biimp t288;
|
|
||||||
t290 = t50 and t264;
|
|
||||||
t291 = t16 xor t290;
|
|
||||||
t292 = t50 and t276;
|
|
||||||
t293 = t16 xor t292;
|
|
||||||
t294 = t291 biimp t293;
|
|
||||||
t167 = t108 and t146;
|
|
||||||
t168 = t61 xor t167;
|
|
||||||
t169 = t108 and t158;
|
|
||||||
t170 = t61 xor t169;
|
|
||||||
t171 = t168 biimp t170;
|
|
||||||
t295 = t131 and t143;
|
|
||||||
t296 = t295 and t263;
|
|
||||||
t297 = t83 and t296;
|
|
||||||
t298 = t19 xor t297;
|
|
||||||
t299 = t295 and t275;
|
|
||||||
t300 = t83 and t299;
|
|
||||||
t301 = t19 xor t300;
|
|
||||||
t302 = t298 biimp t301;
|
|
||||||
t303 = t93 and t296;
|
|
||||||
t304 = t20 xor t303;
|
|
||||||
t305 = t93 and t299;
|
|
||||||
t306 = t20 xor t305;
|
|
||||||
t307 = t304 biimp t306;
|
|
||||||
t308 = t73 and t296;
|
|
||||||
t309 = t22 xor t308;
|
|
||||||
t310 = t73 and t299;
|
|
||||||
t311 = t22 xor t310;
|
|
||||||
t312 = t309 biimp t311;
|
|
||||||
t313 = t50 and t296;
|
|
||||||
t314 = t23 xor t313;
|
|
||||||
t315 = t50 and t299;
|
|
||||||
t316 = t23 xor t315;
|
|
||||||
t317 = t314 biimp t316;
|
|
||||||
t318 = t108 and t122;
|
|
||||||
t319 = t132 and t318;
|
|
||||||
t320 = t319 and t263;
|
|
||||||
t321 = t83 and t320;
|
|
||||||
t322 = t75 xor t321;
|
|
||||||
t323 = t319 and t275;
|
|
||||||
t324 = t83 and t323;
|
|
||||||
t325 = t75 xor t324;
|
|
||||||
t326 = t322 biimp t325;
|
|
||||||
t327 = t93 and t320;
|
|
||||||
t328 = t85 xor t327;
|
|
||||||
t329 = t93 and t323;
|
|
||||||
t330 = t85 xor t329;
|
|
||||||
t331 = t328 biimp t330;
|
|
||||||
t332 = t73 and t320;
|
|
||||||
t333 = t53 xor t332;
|
|
||||||
t334 = t73 and t323;
|
|
||||||
t335 = t53 xor t334;
|
|
||||||
t336 = t333 biimp t335;
|
|
||||||
t337 = t50 and t320;
|
|
||||||
t338 = t30 xor t337;
|
|
||||||
t339 = t50 and t323;
|
|
||||||
t340 = t30 xor t339;
|
|
||||||
t341 = t338 biimp t340;
|
|
||||||
t342 = t131 and t123;
|
|
||||||
t343 = t342 and t263;
|
|
||||||
t344 = t83 and t343;
|
|
||||||
t345 = t76 xor t344;
|
|
||||||
t346 = t342 and t275;
|
|
||||||
t347 = t83 and t346;
|
|
||||||
t348 = t76 xor t347;
|
|
||||||
t349 = t345 biimp t348;
|
|
||||||
t350 = t93 and t343;
|
|
||||||
t351 = t86 xor t350;
|
|
||||||
t352 = t93 and t346;
|
|
||||||
t353 = t86 xor t352;
|
|
||||||
t354 = t351 biimp t353;
|
|
||||||
t172 = t131 and t146;
|
|
||||||
t173 = t62 xor t172;
|
|
||||||
t174 = t131 and t158;
|
|
||||||
t175 = t62 xor t174;
|
|
||||||
t176 = t173 biimp t175;
|
|
||||||
t355 = t73 and t343;
|
|
||||||
t356 = t54 xor t355;
|
|
||||||
t357 = t73 and t346;
|
|
||||||
t358 = t54 xor t357;
|
|
||||||
t359 = t356 biimp t358;
|
|
||||||
t360 = t50 and t343;
|
|
||||||
t361 = t31 xor t360;
|
|
||||||
t362 = t50 and t346;
|
|
||||||
t363 = t31 xor t362;
|
|
||||||
t364 = t361 biimp t363;
|
|
||||||
t179 = t50 and t178;
|
|
||||||
t180 = t179 and t145;
|
|
||||||
t181 = t28 and t180;
|
|
||||||
t182 = t3 xor t181;
|
|
||||||
t183 = t179 and t157;
|
|
||||||
t184 = t28 and t183;
|
|
||||||
t185 = t3 xor t184;
|
|
||||||
t186 = t182 biimp t185;
|
|
||||||
t187 = t121 and t180;
|
|
||||||
t188 = t36 xor t187;
|
|
||||||
t189 = t121 and t183;
|
|
||||||
t190 = t36 xor t189;
|
|
||||||
t191 = t188 biimp t190;
|
|
||||||
t192 = t108 and t180;
|
|
||||||
t193 = t38 xor t192;
|
|
||||||
t194 = t108 and t183;
|
|
||||||
t195 = t38 xor t194;
|
|
||||||
t196 = t193 biimp t195;
|
|
||||||
t197 = t131 and t180;
|
|
||||||
t198 = t39 xor t197;
|
|
||||||
t199 = t131 and t183;
|
|
||||||
t200 = t39 xor t199;
|
|
||||||
t201 = t198 biimp t200;
|
|
||||||
t207 = t28 and t206;
|
|
||||||
t208 = t5 xor t207;
|
|
||||||
t210 = t28 and t209;
|
|
||||||
t211 = t5 xor t210;
|
|
||||||
t212 = t208 biimp t211;
|
|
||||||
t213 = t121 and t206;
|
|
||||||
t214 = t65 xor t213;
|
|
||||||
t215 = t121 and t209;
|
|
||||||
t216 = t65 xor t215;
|
|
||||||
t217 = t214 biimp t216;
|
|
||||||
|
|
||||||
tautology t161;
|
|
||||||
tautology t166;
|
|
||||||
tautology t222;
|
|
||||||
tautology t227;
|
|
||||||
tautology t236;
|
|
||||||
tautology t241;
|
|
||||||
tautology t246;
|
|
||||||
tautology t251;
|
|
||||||
tautology t279;
|
|
||||||
tautology t284;
|
|
||||||
tautology t289;
|
|
||||||
tautology t294;
|
|
||||||
tautology t171;
|
|
||||||
tautology t302;
|
|
||||||
tautology t307;
|
|
||||||
tautology t312;
|
|
||||||
tautology t317;
|
|
||||||
tautology t326;
|
|
||||||
tautology t331;
|
|
||||||
tautology t336;
|
|
||||||
tautology t341;
|
|
||||||
tautology t349;
|
|
||||||
tautology t354;
|
|
||||||
tautology t176;
|
|
||||||
tautology t359;
|
|
||||||
tautology t364;
|
|
||||||
tautology t186;
|
|
||||||
tautology t191;
|
|
||||||
tautology t196;
|
|
||||||
tautology t201;
|
|
||||||
tautology t212;
|
|
||||||
tautology t217;
|
|
||||||
|
|
@ -1,174 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
$Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.cxx,v 1.2 2003/05/05 13:44:53 aduret Exp $
|
|
||||||
FILE: hashtbl.cc
|
|
||||||
DESCR: Compiler hash table
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C) september 1998
|
|
||||||
*************************************************************************/
|
|
||||||
#include "hashtbl.h"
|
|
||||||
|
|
||||||
/*************************************************************************
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
/*======================================================================*/
|
|
||||||
|
|
||||||
hashTable::hashTable(void)
|
|
||||||
{
|
|
||||||
table = NULL;
|
|
||||||
clear();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
hashTable::~hashTable(void)
|
|
||||||
{
|
|
||||||
delete[] table;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void hashTable::add(hashData &d)
|
|
||||||
{
|
|
||||||
if (freepos == -1)
|
|
||||||
reallocate_table();
|
|
||||||
|
|
||||||
unsigned int h = hashval(d.id);
|
|
||||||
int tmppos = table[freepos].next;
|
|
||||||
|
|
||||||
table[freepos].data = d;
|
|
||||||
table[freepos].next = table[h].first;
|
|
||||||
table[h].first = freepos;
|
|
||||||
freepos = tmppos;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
int hashTable::exists(const char *id)
|
|
||||||
{
|
|
||||||
if (size == 0)
|
|
||||||
return 0;
|
|
||||||
|
|
||||||
int p = table[hashval(id)].first;
|
|
||||||
|
|
||||||
while (p != -1)
|
|
||||||
{
|
|
||||||
if (strcmp(id, table[p].data.id) == 0)
|
|
||||||
return 1;
|
|
||||||
p = table[p].next;
|
|
||||||
}
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
int hashTable::lookup(const char *id, hashData &d) const
|
|
||||||
{
|
|
||||||
if (size == 0)
|
|
||||||
return -1;
|
|
||||||
|
|
||||||
int p = table[hashval(id)].first;
|
|
||||||
|
|
||||||
while (p != -1)
|
|
||||||
{
|
|
||||||
if (strcmp(id, table[p].data.id) == 0)
|
|
||||||
{
|
|
||||||
d = table[p].data;
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
p = table[p].next;
|
|
||||||
}
|
|
||||||
|
|
||||||
return -1;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
int hashTable::remove(const char *id)
|
|
||||||
{
|
|
||||||
if (size == 0)
|
|
||||||
return -1;
|
|
||||||
|
|
||||||
int h = hashval(id);
|
|
||||||
int next = table[h].first;
|
|
||||||
int prev = -1;
|
|
||||||
|
|
||||||
while (next != -1)
|
|
||||||
{
|
|
||||||
if (strcmp(id, table[next].data.id) == 0)
|
|
||||||
{
|
|
||||||
if (prev == -1)
|
|
||||||
table[h].first = table[next].next;
|
|
||||||
else
|
|
||||||
table[prev].next = table[next].next;
|
|
||||||
|
|
||||||
table[next].next = freepos;
|
|
||||||
freepos = next;
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
prev = next;
|
|
||||||
next = table[next].next;
|
|
||||||
}
|
|
||||||
|
|
||||||
return -1;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void hashTable::clear(void)
|
|
||||||
{
|
|
||||||
delete[] table;
|
|
||||||
freepos = -1;
|
|
||||||
size = 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void hashTable::reallocate_table(void)
|
|
||||||
{
|
|
||||||
hashElement *newtable;
|
|
||||||
int oldsize = size;
|
|
||||||
int n;
|
|
||||||
|
|
||||||
if (size > 0)
|
|
||||||
{
|
|
||||||
size *= 2;
|
|
||||||
newtable = new hashElement[size];
|
|
||||||
for (int n=0 ; n<oldsize ; n++)
|
|
||||||
newtable[n] = table[n];
|
|
||||||
delete[] table;
|
|
||||||
table = newtable;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
size = 10;
|
|
||||||
table = new hashElement[size];
|
|
||||||
}
|
|
||||||
|
|
||||||
for (n=0 ; n<oldsize ; n++)
|
|
||||||
table[n].first = -1;
|
|
||||||
|
|
||||||
for (n=oldsize ; n<size ; n++)
|
|
||||||
{
|
|
||||||
table[n].first = -1;
|
|
||||||
table[n].next = n+1;
|
|
||||||
}
|
|
||||||
table[size-1].next = -1;
|
|
||||||
freepos = oldsize;
|
|
||||||
|
|
||||||
for (n=0 ; n<oldsize ; n++)
|
|
||||||
{
|
|
||||||
unsigned int h = hashval(table[n].data.id);
|
|
||||||
table[n].next = table[h].first;
|
|
||||||
table[h].first = n;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
unsigned int hashTable::hashval(const char *s) const
|
|
||||||
{
|
|
||||||
unsigned int h = 0;
|
|
||||||
|
|
||||||
for (const char *p=s ; *p!=0 ; p++)
|
|
||||||
h = (h + *p) % size;
|
|
||||||
|
|
||||||
return h;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
/* EOF */
|
|
||||||
|
|
@ -1,56 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
$Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/hashtbl.h,v 1.2 2003/05/05 13:44:54 aduret Exp $
|
|
||||||
FILE: hashtbl.h
|
|
||||||
DESCR: Compiler hashtable
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C) september 1998
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
#ifndef _HASHTBL_H
|
|
||||||
#define _HASHTBL_H
|
|
||||||
|
|
||||||
#include <string.h>
|
|
||||||
|
|
||||||
class hashData
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
hashData(void) { id=NULL; type=0; def=NULL; }
|
|
||||||
hashData(const char *s, int t, void *d) : id(s) { type=t; def=d; }
|
|
||||||
const char *id;
|
|
||||||
int type;
|
|
||||||
void *def;
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
class hashElement
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
hashData data;
|
|
||||||
int first;
|
|
||||||
int next;
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
class hashTable
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
hashTable(void);
|
|
||||||
~hashTable(void);
|
|
||||||
void add(hashData &);
|
|
||||||
int exists(const char *);
|
|
||||||
int lookup(const char *, hashData &) const;
|
|
||||||
int remove(const char *);
|
|
||||||
void clear(void);
|
|
||||||
|
|
||||||
private:
|
|
||||||
void reallocate_table(void);
|
|
||||||
unsigned int hashval(const char *) const;
|
|
||||||
hashElement *table;
|
|
||||||
int size, freepos;
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
#endif /* _HASHTBL_H */
|
|
||||||
|
|
||||||
|
|
||||||
/* EOF */
|
|
||||||
|
|
@ -1,101 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
FILE: lexer.l
|
|
||||||
DESCR: FLEX rules for BDD calculator
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C) may 1999
|
|
||||||
*************************************************************************/
|
|
||||||
%{
|
|
||||||
#include <string.h>
|
|
||||||
#include <stdlib.h>
|
|
||||||
#include "parser_.h"
|
|
||||||
#include "parser.h"
|
|
||||||
%}
|
|
||||||
|
|
||||||
|
|
||||||
/*************************************************************************
|
|
||||||
Macros and sub-lexers
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
DIGIT [0-9]
|
|
||||||
ID [a-zA-Z_][a-zA-Z0-9_]*
|
|
||||||
LINE [^\n]
|
|
||||||
|
|
||||||
%x COMM
|
|
||||||
|
|
||||||
%%
|
|
||||||
|
|
||||||
/**************************************************************************
|
|
||||||
Tokens
|
|
||||||
**************************************************************************/
|
|
||||||
|
|
||||||
/* Keywords */
|
|
||||||
|
|
||||||
"initial" return T_initial;
|
|
||||||
"inputs" return T_inputs;
|
|
||||||
"actions" return T_actions;
|
|
||||||
"exist" return T_exist;
|
|
||||||
"forall" return T_forall;
|
|
||||||
"size" return T_size;
|
|
||||||
"dot" return T_dot;
|
|
||||||
"autoreorder" return T_autoreorder;
|
|
||||||
"reorder" return T_reorder;
|
|
||||||
"win2" return T_win2;
|
|
||||||
"win2ite" return T_win2ite;
|
|
||||||
"sift" return T_sift;
|
|
||||||
"siftite" return T_siftite;
|
|
||||||
"none" return T_none;
|
|
||||||
"cache" return T_cache;
|
|
||||||
"tautology" return T_tautology;
|
|
||||||
"true" return T_true;
|
|
||||||
"false" return T_false;
|
|
||||||
"print" return T_print;
|
|
||||||
|
|
||||||
/* Symbols and operators */
|
|
||||||
|
|
||||||
"." return T_dot;
|
|
||||||
"(" return T_lpar;
|
|
||||||
")" return T_rpar;
|
|
||||||
";" return T_semi;
|
|
||||||
"=" return T_equal;
|
|
||||||
"<>" return T_biimp;
|
|
||||||
"=>" return T_imp;
|
|
||||||
"|" return T_or;
|
|
||||||
"^" return T_xor;
|
|
||||||
"&" return T_and;
|
|
||||||
"~" return T_not;
|
|
||||||
"biimp" return T_biimp;
|
|
||||||
"imp" return T_imp;
|
|
||||||
"or" return T_or;
|
|
||||||
"xor" return T_xor;
|
|
||||||
"and" return T_and;
|
|
||||||
"not" return T_not;
|
|
||||||
"nand" return T_nand;
|
|
||||||
"nor" return T_nor;
|
|
||||||
|
|
||||||
/* Identifiers and constant values */
|
|
||||||
{ID} { strncpy(yylval.id, yytext, MAXIDLEN); return T_id; }
|
|
||||||
{DIGIT}+ { yylval.ival = atol(yytext); return T_intval; }
|
|
||||||
|
|
||||||
/* Strings */
|
|
||||||
\"[^\"]*\" { yylval.str=sdup(yytext+1);
|
|
||||||
yylval.str[strlen(yylval.str)-1]=0; return T_str; }
|
|
||||||
|
|
||||||
/* Whitespace */
|
|
||||||
[\n] { linenum++; }
|
|
||||||
[\r\t\f ] /* ignore blanks */
|
|
||||||
|
|
||||||
|
|
||||||
"//"{LINE}* /* Remove one line comments */
|
|
||||||
|
|
||||||
|
|
||||||
/**************************************************************************
|
|
||||||
Remove multi line comments
|
|
||||||
**************************************************************************/
|
|
||||||
|
|
||||||
"/*" BEGIN COMM;
|
|
||||||
<COMM>[^*\n]* /* ignore */
|
|
||||||
<COMM>"*"[^*/\n]* /* ignore */
|
|
||||||
<COMM>\n { linenum++; }
|
|
||||||
<COMM>"*/" BEGIN INITIAL;
|
|
||||||
|
|
||||||
. { yyerror("Unknown symbol"); }
|
|
||||||
|
|
@ -1,118 +0,0 @@
|
||||||
/* A Bison parser, made by GNU Bison 1.875c. */
|
|
||||||
|
|
||||||
/* Skeleton parser for Yacc-like parsing with Bison,
|
|
||||||
Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003 Free Software Foundation, Inc.
|
|
||||||
|
|
||||||
This program is free software; you can redistribute it and/or modify
|
|
||||||
it under the terms of the GNU General Public License as published by
|
|
||||||
the Free Software Foundation; either version 2, or (at your option)
|
|
||||||
any later version.
|
|
||||||
|
|
||||||
This program is distributed in the hope that it will be useful,
|
|
||||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
||||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
||||||
GNU General Public License for more details.
|
|
||||||
|
|
||||||
You should have received a copy of the GNU General Public License
|
|
||||||
along with this program; if not, write to the Free Software
|
|
||||||
Foundation, Inc., 59 Temple Place - Suite 330,
|
|
||||||
Boston, MA 02111-1307, USA. */
|
|
||||||
|
|
||||||
/* As a special exception, when this file is copied by Bison into a
|
|
||||||
Bison output file, you may use that output file without restriction.
|
|
||||||
This special exception was added by the Free Software Foundation
|
|
||||||
in version 1.24 of Bison. */
|
|
||||||
|
|
||||||
/* Tokens. */
|
|
||||||
#ifndef YYTOKENTYPE
|
|
||||||
# define YYTOKENTYPE
|
|
||||||
/* Put the tokens into the symbol table, so that GDB and other debuggers
|
|
||||||
know about them. */
|
|
||||||
enum yytokentype {
|
|
||||||
T_id = 258,
|
|
||||||
T_str = 259,
|
|
||||||
T_intval = 260,
|
|
||||||
T_true = 261,
|
|
||||||
T_false = 262,
|
|
||||||
T_initial = 263,
|
|
||||||
T_inputs = 264,
|
|
||||||
T_actions = 265,
|
|
||||||
T_size = 266,
|
|
||||||
T_dumpdot = 267,
|
|
||||||
T_autoreorder = 268,
|
|
||||||
T_reorder = 269,
|
|
||||||
T_win2 = 270,
|
|
||||||
T_win2ite = 271,
|
|
||||||
T_sift = 272,
|
|
||||||
T_siftite = 273,
|
|
||||||
T_none = 274,
|
|
||||||
T_cache = 275,
|
|
||||||
T_tautology = 276,
|
|
||||||
T_print = 277,
|
|
||||||
T_lpar = 278,
|
|
||||||
T_rpar = 279,
|
|
||||||
T_equal = 280,
|
|
||||||
T_semi = 281,
|
|
||||||
T_dot = 282,
|
|
||||||
T_forall = 283,
|
|
||||||
T_exist = 284,
|
|
||||||
T_biimp = 285,
|
|
||||||
T_imp = 286,
|
|
||||||
T_nor = 287,
|
|
||||||
T_or = 288,
|
|
||||||
T_xor = 289,
|
|
||||||
T_and = 290,
|
|
||||||
T_nand = 291,
|
|
||||||
T_not = 292
|
|
||||||
};
|
|
||||||
#endif
|
|
||||||
#define T_id 258
|
|
||||||
#define T_str 259
|
|
||||||
#define T_intval 260
|
|
||||||
#define T_true 261
|
|
||||||
#define T_false 262
|
|
||||||
#define T_initial 263
|
|
||||||
#define T_inputs 264
|
|
||||||
#define T_actions 265
|
|
||||||
#define T_size 266
|
|
||||||
#define T_dumpdot 267
|
|
||||||
#define T_autoreorder 268
|
|
||||||
#define T_reorder 269
|
|
||||||
#define T_win2 270
|
|
||||||
#define T_win2ite 271
|
|
||||||
#define T_sift 272
|
|
||||||
#define T_siftite 273
|
|
||||||
#define T_none 274
|
|
||||||
#define T_cache 275
|
|
||||||
#define T_tautology 276
|
|
||||||
#define T_print 277
|
|
||||||
#define T_lpar 278
|
|
||||||
#define T_rpar 279
|
|
||||||
#define T_equal 280
|
|
||||||
#define T_semi 281
|
|
||||||
#define T_dot 282
|
|
||||||
#define T_forall 283
|
|
||||||
#define T_exist 284
|
|
||||||
#define T_biimp 285
|
|
||||||
#define T_imp 286
|
|
||||||
#define T_nor 287
|
|
||||||
#define T_or 288
|
|
||||||
#define T_xor 289
|
|
||||||
#define T_and 290
|
|
||||||
#define T_nand 291
|
|
||||||
#define T_not 292
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
#if ! defined (YYSTYPE) && ! defined (YYSTYPE_IS_DECLARED)
|
|
||||||
typedef int YYSTYPE;
|
|
||||||
# define yystype YYSTYPE /* obsolescent; will be withdrawn */
|
|
||||||
# define YYSTYPE_IS_DECLARED 1
|
|
||||||
# define YYSTYPE_IS_TRIVIAL 1
|
|
||||||
#endif
|
|
||||||
|
|
||||||
extern YYSTYPE yylval;
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,459 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
FILE: parser.y
|
|
||||||
DESCR: BISON rules and main program for BDD calculator
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C) may 1999
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
%{
|
|
||||||
#include <string.h>
|
|
||||||
#include <stdarg.h>
|
|
||||||
#include <fstream>
|
|
||||||
#include <getopt.h>
|
|
||||||
#define IMPLEMENTSLIST /* Special for list template handling */
|
|
||||||
#include "slist.h"
|
|
||||||
#include "hashtbl.h"
|
|
||||||
#include "parser_.h"
|
|
||||||
|
|
||||||
using namespace std;
|
|
||||||
|
|
||||||
/* Definitions for storing and caching of identifiers */
|
|
||||||
#define inputTag 0
|
|
||||||
#define exprTag 1
|
|
||||||
|
|
||||||
struct nodeData
|
|
||||||
{
|
|
||||||
nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; }
|
|
||||||
nodeData(int t, char *n, bdd v) { tag=t; name=n; val=v; }
|
|
||||||
~nodeData(void) { delete[] name; }
|
|
||||||
int tag;
|
|
||||||
char *name;
|
|
||||||
bdd val;
|
|
||||||
};
|
|
||||||
|
|
||||||
typedef SList<nodeData> nodeLst;
|
|
||||||
nodeLst inputs;
|
|
||||||
hashTable names;
|
|
||||||
|
|
||||||
/* Other */
|
|
||||||
int linenum;
|
|
||||||
|
|
||||||
bddgbchandler gbcHandler = bdd_default_gbchandler;
|
|
||||||
|
|
||||||
/* Prototypes */
|
|
||||||
void actInit(token *nodes, token *cache);
|
|
||||||
void actInputs(void);
|
|
||||||
void actAddInput(token *id);
|
|
||||||
void actAssign(token *id, token *expr);
|
|
||||||
void actOpr2(token *res, token *left, token *right, int opr);
|
|
||||||
void actNot(token *res, token *right);
|
|
||||||
void actId(token *res, token *id);
|
|
||||||
void actConst(token *res, int);
|
|
||||||
void actSize(token *id);
|
|
||||||
void actDot(token *fname, token *id);
|
|
||||||
void actAutoreorder(token *times, token *method);
|
|
||||||
void actCache(void);
|
|
||||||
void actTautology(token *id);
|
|
||||||
void actExist(token *res, token *var, token *expr);
|
|
||||||
void actForall(token *res, token *var, token *expr);
|
|
||||||
void actQuantVar2(token *res, token *id, token *list);
|
|
||||||
void actQuantVar1(token *res, token *id);
|
|
||||||
void actPrint(token *id);
|
|
||||||
|
|
||||||
%}
|
|
||||||
|
|
||||||
/*************************************************************************
|
|
||||||
Token definitions
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
%token T_id T_str T_intval T_true T_false
|
|
||||||
|
|
||||||
%token T_initial T_inputs T_actions
|
|
||||||
%token T_size T_dumpdot
|
|
||||||
%token T_autoreorder T_reorder T_win2 T_win2ite T_sift T_siftite T_none
|
|
||||||
%token T_cache T_tautology T_print
|
|
||||||
|
|
||||||
%token T_lpar T_rpar
|
|
||||||
%token T_equal
|
|
||||||
%token T_semi T_dot
|
|
||||||
|
|
||||||
%right T_exist T_forall T_dot
|
|
||||||
%left T_biimp
|
|
||||||
%left T_imp
|
|
||||||
%left T_or T_nor
|
|
||||||
%left T_xor
|
|
||||||
%left T_nand T_and
|
|
||||||
%right T_not
|
|
||||||
|
|
||||||
/*************************************************************************
|
|
||||||
BISON rules
|
|
||||||
*************************************************************************/
|
|
||||||
%%
|
|
||||||
|
|
||||||
/*=[ Top ]==============================================================*/
|
|
||||||
|
|
||||||
calc:
|
|
||||||
initial inputs actions
|
|
||||||
;
|
|
||||||
|
|
||||||
/*=[ Initializers ]=====================================================*/
|
|
||||||
|
|
||||||
initial:
|
|
||||||
T_initial T_intval T_intval T_semi { actInit(&$2,&$3); }
|
|
||||||
;
|
|
||||||
|
|
||||||
inputs:
|
|
||||||
T_inputs inputSeq T_semi { actInputs(); }
|
|
||||||
;
|
|
||||||
|
|
||||||
inputSeq:
|
|
||||||
inputSeq T_id { actAddInput(&$2); }
|
|
||||||
| T_id { actAddInput(&$1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
|
|
||||||
/*=[ Actions ]==========================================================*/
|
|
||||||
|
|
||||||
actions:
|
|
||||||
T_actions actionSeq
|
|
||||||
;
|
|
||||||
|
|
||||||
actionSeq:
|
|
||||||
action T_semi actionSeq
|
|
||||||
| action T_semi
|
|
||||||
;
|
|
||||||
|
|
||||||
action:
|
|
||||||
assign
|
|
||||||
| size
|
|
||||||
| dot
|
|
||||||
| reorder
|
|
||||||
| cache
|
|
||||||
| tautology
|
|
||||||
| print
|
|
||||||
;
|
|
||||||
|
|
||||||
assign:
|
|
||||||
T_id T_equal expr { actAssign(&$1,&$3); }
|
|
||||||
;
|
|
||||||
|
|
||||||
expr:
|
|
||||||
expr T_and expr { actOpr2(&$$,&$1,&$3,bddop_and); }
|
|
||||||
| expr T_nand expr { actOpr2(&$$,&$1,&$3,bddop_nand); }
|
|
||||||
| expr T_xor expr { actOpr2(&$$,&$1,&$3,bddop_xor); }
|
|
||||||
| expr T_or expr { actOpr2(&$$,&$1,&$3,bddop_or); }
|
|
||||||
| expr T_nor expr { actOpr2(&$$,&$1,&$3,bddop_nor); }
|
|
||||||
| expr T_imp expr { actOpr2(&$$,&$1,&$3,bddop_imp); }
|
|
||||||
| expr T_biimp expr { actOpr2(&$$,&$1,&$3,bddop_biimp); }
|
|
||||||
| T_not expr { actNot(&$$,&$2); }
|
|
||||||
| T_lpar expr T_rpar { $$.bval = $2.bval; }
|
|
||||||
| T_id { actId(&$$,&$1); }
|
|
||||||
| T_true { $$.bval = new bdd(bddtrue); }
|
|
||||||
| T_false { $$.bval = new bdd(bddfalse); }
|
|
||||||
| quantifier { $$.bval = $1.bval; }
|
|
||||||
;
|
|
||||||
|
|
||||||
quantifier:
|
|
||||||
T_exist varlist T_dot expr { actExist(&$$,&$2,&$4); }
|
|
||||||
| T_forall varlist T_dot expr { actForall(&$$,&$2,&$4); }
|
|
||||||
;
|
|
||||||
|
|
||||||
varlist:
|
|
||||||
T_id varlist { actQuantVar2(&$$,&$1,&$2); }
|
|
||||||
| T_id { actQuantVar1(&$$,&$1); }
|
|
||||||
;
|
|
||||||
|
|
||||||
|
|
||||||
size:
|
|
||||||
T_size T_id { actSize(&$2); }
|
|
||||||
;
|
|
||||||
|
|
||||||
dot:
|
|
||||||
T_dumpdot T_str T_id { actDot(&$2,&$3); }
|
|
||||||
;
|
|
||||||
|
|
||||||
reorder:
|
|
||||||
T_reorder method { bdd_reorder($2.ival); }
|
|
||||||
| T_autoreorder T_intval method { actAutoreorder(&$2,&$3); }
|
|
||||||
;
|
|
||||||
|
|
||||||
method:
|
|
||||||
T_win2 { $$.ival = BDD_REORDER_WIN2; }
|
|
||||||
| T_win2ite { $$.ival = BDD_REORDER_WIN2ITE; }
|
|
||||||
| T_sift { $$.ival = BDD_REORDER_SIFT; }
|
|
||||||
| T_siftite { $$.ival = BDD_REORDER_SIFTITE; }
|
|
||||||
| T_none { $$.ival = BDD_REORDER_NONE; }
|
|
||||||
;
|
|
||||||
|
|
||||||
cache:
|
|
||||||
T_cache { actCache(); }
|
|
||||||
;
|
|
||||||
|
|
||||||
tautology:
|
|
||||||
T_tautology T_id { actTautology(&$2); }
|
|
||||||
;
|
|
||||||
|
|
||||||
print:
|
|
||||||
T_print T_id { actPrint(&$2); }
|
|
||||||
|
|
||||||
%%
|
|
||||||
/*************************************************************************
|
|
||||||
Main and more
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
void usage(void)
|
|
||||||
{
|
|
||||||
cerr << "USAGE: bddcalc [-hg] file\n";
|
|
||||||
cerr << " -h : print this message\n";
|
|
||||||
cerr << " -g : disable garbage collection info\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
int main(int ac, char **av)
|
|
||||||
{
|
|
||||||
int c;
|
|
||||||
|
|
||||||
while ((c=getopt(ac, av, "hg")) != EOF)
|
|
||||||
{
|
|
||||||
switch (c)
|
|
||||||
{
|
|
||||||
case 'h':
|
|
||||||
usage();
|
|
||||||
break;
|
|
||||||
case 'g':
|
|
||||||
gbcHandler = bdd_default_gbchandler;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (optind >= ac)
|
|
||||||
usage();
|
|
||||||
|
|
||||||
yyin = fopen(av[optind],"r");
|
|
||||||
if (!yyin)
|
|
||||||
{
|
|
||||||
cerr << "Could not open file: " << av[optind] << endl;
|
|
||||||
exit(2);
|
|
||||||
}
|
|
||||||
|
|
||||||
linenum = 1;
|
|
||||||
bdd_setcacheratio(2);
|
|
||||||
yyparse();
|
|
||||||
|
|
||||||
bdd_printstat();
|
|
||||||
bdd_done();
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void yyerror(char *fmt, ...)
|
|
||||||
{
|
|
||||||
va_list argp;
|
|
||||||
va_start(argp,fmt);
|
|
||||||
fprintf(stderr, "Parse error in (or before) line %d: ", linenum);
|
|
||||||
vfprintf(stderr, fmt, argp);
|
|
||||||
va_end(argp);
|
|
||||||
exit(3);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
/*************************************************************************
|
|
||||||
Semantic actions
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
void actInit(token *nodes, token *cache)
|
|
||||||
{
|
|
||||||
bdd_init(nodes->ival, cache->ival);
|
|
||||||
bdd_gbc_hook(gbcHandler);
|
|
||||||
bdd_reorder_verbose(0);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actInputs(void)
|
|
||||||
{
|
|
||||||
bdd_setvarnum(inputs.size());
|
|
||||||
|
|
||||||
int vnum=0;
|
|
||||||
for (nodeLst::ite i=inputs.first() ; i.more() ; i++, vnum++)
|
|
||||||
{
|
|
||||||
if (names.exists((*i).name))
|
|
||||||
yyerror("Redefinition of input %s", (*i).name);
|
|
||||||
|
|
||||||
(*i).val = bdd_ithvar(vnum);
|
|
||||||
hashData hd((*i).name, 0, &(*i));
|
|
||||||
names.add(hd);
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd_varblockall();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actAddInput(token *id)
|
|
||||||
{
|
|
||||||
inputs.append( nodeData(inputTag,sdup(id->id),bddtrue) );
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actAssign(token *id, token *expr)
|
|
||||||
{
|
|
||||||
if (names.exists(id->id))
|
|
||||||
yyerror("Redefinition of %s", id->id);
|
|
||||||
|
|
||||||
nodeData *d = new nodeData(exprTag, sdup(id->id), *expr->bval);
|
|
||||||
hashData hd(d->name, 0, d);
|
|
||||||
names.add(hd);
|
|
||||||
delete expr->bval;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actOpr2(token *res, token *left, token *right, int opr)
|
|
||||||
{
|
|
||||||
res->bval = new bdd( bdd_apply(*left->bval, *right->bval, opr) );
|
|
||||||
delete left->bval;
|
|
||||||
delete right->bval;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actNot(token *res, token *right)
|
|
||||||
{
|
|
||||||
res->bval = new bdd( bdd_not(*right->bval) );
|
|
||||||
delete right->bval;
|
|
||||||
//printf("%5d -> %f\n", fixme, bdd_satcount(*res->bval));
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actId(token *res, token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
res->bval = new bdd( ((nodeData*)hd.def)->val );
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actExist(token *res, token *var, token *expr)
|
|
||||||
{
|
|
||||||
res->bval = new bdd( bdd_exist(*expr->bval, *var->bval) );
|
|
||||||
delete var->bval;
|
|
||||||
delete expr->bval;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actForall(token *res, token *var, token *expr)
|
|
||||||
{
|
|
||||||
res->bval = new bdd( bdd_forall(*expr->bval, *var->bval) );
|
|
||||||
delete var->bval;
|
|
||||||
delete expr->bval;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actQuantVar2(token *res, token *id, token *list)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
if (hd.type == inputTag)
|
|
||||||
{
|
|
||||||
res->bval = list->bval;
|
|
||||||
*res->bval &= ((nodeData*)hd.def)->val;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("%s is not a variable", id->id);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actQuantVar1(token *res, token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
if (hd.type == inputTag)
|
|
||||||
res->bval = new bdd( ((nodeData*)hd.def)->val );
|
|
||||||
else
|
|
||||||
yyerror("%s is not a variable", id->id);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actSize(token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
cout << "Number of nodes used for " << id->id << " = "
|
|
||||||
<< bdd_nodecount(((nodeData*)hd.def)->val) << endl;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actDot(token *fname, token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
if (bdd_fnprintdot(fname->str, ((nodeData*)hd.def)->val) < 0)
|
|
||||||
cout << "Could not open file: " << fname->str << endl;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actAutoreorder(token *times, token *method)
|
|
||||||
{
|
|
||||||
if (times->ival == 0)
|
|
||||||
bdd_autoreorder(method->ival);
|
|
||||||
else
|
|
||||||
bdd_autoreorder_times(method->ival, times->ival);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actCache(void)
|
|
||||||
{
|
|
||||||
bdd_printstat();
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actTautology(token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
{
|
|
||||||
if (((nodeData*)hd.def)->val == bddtrue)
|
|
||||||
cout << "Formula " << id->id << " is a tautology!\n";
|
|
||||||
else
|
|
||||||
cout << "Formula " << id->id << " is NOT a tautology!\n";
|
|
||||||
}
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void actPrint(token *id)
|
|
||||||
{
|
|
||||||
hashData hd;
|
|
||||||
|
|
||||||
if (names.lookup(id->id,hd) == 0)
|
|
||||||
cout << id->id << " = " << bddset << ((nodeData*)hd.def)->val << endl;
|
|
||||||
else
|
|
||||||
yyerror("Unknown variable %s", id->id);
|
|
||||||
}
|
|
||||||
|
|
||||||
/* EOF */
|
|
||||||
|
|
@ -1,44 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
FILE: parser.h
|
|
||||||
DESCR: parser defs. for BDD calculator
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C) may 1999
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
#ifndef _PARSER_H
|
|
||||||
#define _PARSER_H
|
|
||||||
|
|
||||||
#include <stdio.h>
|
|
||||||
#include "bdd.h"
|
|
||||||
|
|
||||||
#define MAXIDLEN 32 /* Max. number of allowed characters in an identifier */
|
|
||||||
|
|
||||||
struct token /* BISON token data */
|
|
||||||
{
|
|
||||||
char id[MAXIDLEN+1];
|
|
||||||
char *str;
|
|
||||||
int ival;
|
|
||||||
bdd *bval;
|
|
||||||
};
|
|
||||||
|
|
||||||
#define YYSTYPE token
|
|
||||||
#define YY_SKIP_YYWRAP
|
|
||||||
#define YY_NO_UNPUT
|
|
||||||
#define yywrap() (1)
|
|
||||||
|
|
||||||
extern YYSTYPE yylval; /* Declare for flex user */
|
|
||||||
extern void yyerror(char *,...); /* Declare for flex and bison */
|
|
||||||
extern FILE *yyin;
|
|
||||||
extern int yylex(void); /* Declare for bison */
|
|
||||||
extern int yyparse(void); /* Declare for bison user */
|
|
||||||
extern int linenum; /* Declare for error handler */
|
|
||||||
|
|
||||||
/* Use this instead of strdup() to avoid malloc() */
|
|
||||||
inline char *sdup(const char *s)
|
|
||||||
{
|
|
||||||
return strcpy(new char[strlen(s)+1], s);
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif /* _PARSER_H */
|
|
||||||
|
|
||||||
/* EOF */
|
|
||||||
|
|
@ -1,99 +0,0 @@
|
||||||
A PRIMITIVE BDD CALCULATOR
|
|
||||||
--------------------------
|
|
||||||
|
|
||||||
This is a small program that parses commands for a BDD calculator. The
|
|
||||||
input file contains the definition of the basic BDD variables (inputs)
|
|
||||||
and a sequence of actions - typically assignments. The calculator can
|
|
||||||
be used for verification of combinatorial circuits (tautology check),
|
|
||||||
such as some of the ISCAS85 circuits in the "examples" directory. These
|
|
||||||
ISCAS85 have been modified by another program before they where added to
|
|
||||||
the BuDDy examples, so please do not compare the runtime results to other
|
|
||||||
test runs.
|
|
||||||
|
|
||||||
|
|
||||||
A BDD calculator file could be something like this ("example.cal"):
|
|
||||||
|
|
||||||
initial 100 100;
|
|
||||||
|
|
||||||
inputs
|
|
||||||
a b c;
|
|
||||||
|
|
||||||
actions
|
|
||||||
t1 = (a | b) & c;
|
|
||||||
t2 = (a & c) | (b & c);
|
|
||||||
t3 = t1 <> t2;
|
|
||||||
tautology t3; /* Verify that (a | b) & c == (a & c) | (b & c) */
|
|
||||||
|
|
||||||
|
|
||||||
Where the blocks are like this:
|
|
||||||
|
|
||||||
initial n c
|
|
||||||
-----------
|
|
||||||
Initialize the BDD package using 'n' bddnodes and 'c' elements in
|
|
||||||
the caches. This part is mandatory.
|
|
||||||
|
|
||||||
|
|
||||||
inputs id-seq
|
|
||||||
-------------
|
|
||||||
Define all identifiers in the sequence 'id-seq' to be primary
|
|
||||||
inputs. This also corresponds to the initial BDD variable ordering,
|
|
||||||
starting with the first identifier in the top.
|
|
||||||
|
|
||||||
|
|
||||||
outputs id-seq
|
|
||||||
--------------
|
|
||||||
Define all identifiers in the sequence 'id-seq' to be primary
|
|
||||||
outputs. The sequence is space separated.
|
|
||||||
|
|
||||||
|
|
||||||
actions act-seq
|
|
||||||
---------------
|
|
||||||
A list of all the calculations and more. This list is traversed and
|
|
||||||
interpreted in the same order as written in the file. An action can
|
|
||||||
be one of the following:
|
|
||||||
|
|
||||||
Assignments: "id = expression"
|
|
||||||
Calculate the right-hand side and assign the value to the
|
|
||||||
left-hand identifier. The expression may contain:
|
|
||||||
|
|
||||||
+ identifiers : A previously defined identifier
|
|
||||||
+ true : The constant true BDD
|
|
||||||
+ false : The constant false BDD
|
|
||||||
+ ( ... ) : Parenteses
|
|
||||||
+ E1 & E2 : Conjunction of two sub-expressions
|
|
||||||
+ E1 | E2 : Disjunction of two sub-expressions
|
|
||||||
+ E1 ^ E2 : Xor
|
|
||||||
+ E1 => E2 : Implication
|
|
||||||
+ E1 <> E2 : Biimplication
|
|
||||||
+ ~E : Negation
|
|
||||||
+ exist V.E :
|
|
||||||
+ forall V. E : Existential/Universal quantification of the
|
|
||||||
variables V in the expression E. V is a space
|
|
||||||
separated list of input names.
|
|
||||||
|
|
||||||
|
|
||||||
Tautology check: "tautology id"
|
|
||||||
Check the variable 'id' for tautology (being equal to the constant
|
|
||||||
true BDD).
|
|
||||||
|
|
||||||
Size information: "size id"
|
|
||||||
Print the number of distinct BDD nodes used to represent 'id'.
|
|
||||||
|
|
||||||
Dump as a dot file: "dot "filename" id"
|
|
||||||
Dump the BDD representing 'id' as commands to the graph drawing
|
|
||||||
program Dot. The commands are written to the file 'filename'.
|
|
||||||
|
|
||||||
Reordering: "reorder mtd"
|
|
||||||
Do a dynamic variable reordering now using the method 'mtd'. The
|
|
||||||
argument 'mtd' may be either: win2, win2ite or sift.
|
|
||||||
|
|
||||||
Automatic reordering: "autoreorder times mtd"
|
|
||||||
Enable automatic dynamic variable reordering using the method
|
|
||||||
'mtd'. The argument 'mtd' may be either: win2, win2ite, sift or
|
|
||||||
none. Use none to disable automatic reordering. The 'times'
|
|
||||||
argument supplies the number of times that reordering may be
|
|
||||||
done. Use for example 1 if you only want a "one-shot" reordering.
|
|
||||||
|
|
||||||
Cache statistics: "cache"
|
|
||||||
Print various cache statistics for the BDD kernel.
|
|
||||||
|
|
||||||
|
|
@ -1,235 +0,0 @@
|
||||||
/*************************************************************************
|
|
||||||
$Header: /Volumes/CVS/repository/spot/spot/buddy/examples/calculator/Attic/slist.h,v 1.2 2003/05/05 13:44:55 aduret Exp $
|
|
||||||
FILE: slist.h
|
|
||||||
DESCR: Single linked list
|
|
||||||
AUTH: Jorn Lind
|
|
||||||
DATE: (C)
|
|
||||||
*************************************************************************/
|
|
||||||
|
|
||||||
#ifndef _SLIST_H
|
|
||||||
#define _SLIST_H
|
|
||||||
|
|
||||||
#include <string.h>
|
|
||||||
|
|
||||||
|
|
||||||
/* === Base void list ==================================================*/
|
|
||||||
|
|
||||||
class voidSList;
|
|
||||||
|
|
||||||
class voidSList
|
|
||||||
{
|
|
||||||
protected:
|
|
||||||
class voidSListElem
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
void *data;
|
|
||||||
voidSListElem *next;
|
|
||||||
~voidSListElem(void) { delete next; }
|
|
||||||
|
|
||||||
private:
|
|
||||||
voidSListElem(void *d) { data=d; next=NULL; }
|
|
||||||
friend class voidSList;
|
|
||||||
};
|
|
||||||
|
|
||||||
public:
|
|
||||||
voidSList(void) { head=tail=NULL; len=0; }
|
|
||||||
~voidSList(void) { delete head; }
|
|
||||||
void *append(void *);
|
|
||||||
void *append(voidSListElem *p, void *d);
|
|
||||||
void *insert(void *);
|
|
||||||
int size(void) const { return len; }
|
|
||||||
int empty(void) const { return len==0; }
|
|
||||||
void reverse(void);
|
|
||||||
void eraseHead(void);
|
|
||||||
void eraseAll(void) { delete head; head=tail=NULL; len=0; }
|
|
||||||
|
|
||||||
protected:
|
|
||||||
int len;
|
|
||||||
voidSListElem *head, *tail;
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
#ifdef IMPLEMENTSLIST
|
|
||||||
|
|
||||||
void *voidSList::append(void *d)
|
|
||||||
{
|
|
||||||
voidSListElem *elem = new voidSListElem(d);
|
|
||||||
|
|
||||||
if (tail)
|
|
||||||
tail->next = elem;
|
|
||||||
else
|
|
||||||
head = elem;
|
|
||||||
|
|
||||||
tail = elem;
|
|
||||||
len++;
|
|
||||||
|
|
||||||
return elem->data;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void *voidSList::append(voidSListElem *p, void *d)
|
|
||||||
{
|
|
||||||
voidSListElem *elem = new voidSListElem(d);
|
|
||||||
|
|
||||||
if (p)
|
|
||||||
{
|
|
||||||
elem->next = p->next;
|
|
||||||
p->next = elem;
|
|
||||||
if (p == tail)
|
|
||||||
tail = p->next;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
if (tail)
|
|
||||||
tail->next = elem;
|
|
||||||
else
|
|
||||||
head = elem;
|
|
||||||
tail = elem;
|
|
||||||
}
|
|
||||||
|
|
||||||
len++;
|
|
||||||
|
|
||||||
return elem->data;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void *voidSList::insert(void *d)
|
|
||||||
{
|
|
||||||
voidSListElem *elem = new voidSListElem(d);
|
|
||||||
|
|
||||||
if (tail == NULL)
|
|
||||||
tail = elem;
|
|
||||||
|
|
||||||
elem->next = head;
|
|
||||||
head = elem;
|
|
||||||
len++;
|
|
||||||
|
|
||||||
return elem->data;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void voidSList::reverse(void)
|
|
||||||
{
|
|
||||||
voidSListElem *newTail = head;
|
|
||||||
voidSListElem *tmpHead = NULL;
|
|
||||||
|
|
||||||
if (len < 2)
|
|
||||||
return ;
|
|
||||||
|
|
||||||
while (head != NULL)
|
|
||||||
{
|
|
||||||
voidSListElem *tmpNext = head->next;
|
|
||||||
|
|
||||||
head->next = tmpHead;
|
|
||||||
tmpHead = head;
|
|
||||||
|
|
||||||
head = tmpNext;
|
|
||||||
}
|
|
||||||
|
|
||||||
tail = newTail;
|
|
||||||
head = tmpHead;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void voidSList::eraseHead(void)
|
|
||||||
{
|
|
||||||
if (head != NULL)
|
|
||||||
{
|
|
||||||
head = head->next;
|
|
||||||
if (head == NULL)
|
|
||||||
tail = NULL;
|
|
||||||
len--;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif /* IMPLEMENTSLIST */
|
|
||||||
|
|
||||||
|
|
||||||
/* === Base void list ==================================================*/
|
|
||||||
|
|
||||||
//sorting
|
|
||||||
|
|
||||||
template <class T>
|
|
||||||
class SList : private voidSList
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
class ite
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
ite(void) { next=NULL; }
|
|
||||||
ite(const ite &start) { next=start.next;}
|
|
||||||
ite(voidSListElem *start) { next=start; }
|
|
||||||
int more(void) const { return next!=NULL; }
|
|
||||||
ite &operator=(const ite &start) { next=start.next; return *this; }
|
|
||||||
ite operator++(void)
|
|
||||||
{ if (next) next=next->next; return *this; }
|
|
||||||
ite operator++(int)
|
|
||||||
{ ite tmp=*this; if (next) next=next->next; return tmp; }
|
|
||||||
T &operator*(void) const { return *((T*)next->data); }
|
|
||||||
int operator==(ite x) { return x.next==next; }
|
|
||||||
private:
|
|
||||||
voidSListElem *next;
|
|
||||||
friend class SList<T>;
|
|
||||||
};
|
|
||||||
|
|
||||||
~SList(void) { for (ite x=first() ; x.more() ; x++) delete &(*x); }
|
|
||||||
T &append(const T &d) { return *((T*)voidSList::append(new T(d))); }
|
|
||||||
T &insert(const T &d) { return *((T*)voidSList::insert(new T(d))); }
|
|
||||||
T &head(void) const { return *((T*)voidSList::head->data); }
|
|
||||||
T &tail(void) const { return *((T*)voidSList::tail->data); }
|
|
||||||
ite first(void) const { return ite(voidSList::head); }
|
|
||||||
int empty(void) const { return voidSList::empty(); }
|
|
||||||
int size(void) const { return voidSList::size(); }
|
|
||||||
void reverse(void) { voidSList::reverse(); }
|
|
||||||
void filter(int (*)(T&));
|
|
||||||
void append(SList<T> &l)
|
|
||||||
{ for (ite x=l.first() ; x.more() ; x++) append(*x); }
|
|
||||||
T &append(ite &i, const T &d)
|
|
||||||
{ return *((T*)voidSList::append(i.next, new T(d))); }
|
|
||||||
void eraseHead(void)
|
|
||||||
{ delete ((T*)voidSList::head->data); voidSList::eraseHead(); }
|
|
||||||
void eraseAll(void)
|
|
||||||
{ for (ite x=first() ; x.more() ; x++) delete &(*x); voidSList::eraseAll();}
|
|
||||||
void map(void (*f)(T&))
|
|
||||||
{ for (ite x=first() ; x.more() ; x++) f(*x); }
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
template <class T>
|
|
||||||
void SList<T>::filter(int (*f)(T&))
|
|
||||||
{
|
|
||||||
voidSListElem *prev=NULL, *next=voidSList::head;
|
|
||||||
|
|
||||||
while (next)
|
|
||||||
{
|
|
||||||
if (f(*((T*)next->data)))
|
|
||||||
{
|
|
||||||
prev = next;
|
|
||||||
next = next->next;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
voidSListElem *n = next->next;
|
|
||||||
|
|
||||||
if (prev == NULL)
|
|
||||||
voidSList::head = next->next;
|
|
||||||
else
|
|
||||||
prev->next = next->next;
|
|
||||||
if (voidSList::head == NULL)
|
|
||||||
voidSList::tail = NULL;
|
|
||||||
|
|
||||||
delete next->data;
|
|
||||||
next->next = NULL;
|
|
||||||
delete next;
|
|
||||||
|
|
||||||
next = n;
|
|
||||||
len--;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
#endif /* _SLIST_H */
|
|
||||||
|
|
||||||
|
|
||||||
/* EOF */
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
||||||
include ../Makefile.def
|
|
||||||
check_PROGRAMS = bddtest
|
|
||||||
bddtest_SOURCES = bddtest.cxx
|
|
||||||
|
|
@ -1,145 +0,0 @@
|
||||||
#include <iomanip>
|
|
||||||
#include <stdlib.h>
|
|
||||||
#include <bdd.h>
|
|
||||||
#include <iostream>
|
|
||||||
using namespace std;
|
|
||||||
|
|
||||||
static const int varnum = 5;
|
|
||||||
|
|
||||||
/**************************************************************************
|
|
||||||
Example of allsat print handler.
|
|
||||||
**************************************************************************/
|
|
||||||
|
|
||||||
void allsatHandlerPrint(char* varset, int size)
|
|
||||||
{
|
|
||||||
for (int v=0; v<size ; ++v)
|
|
||||||
{
|
|
||||||
cout << (varset[v] < 0 ? 'X' : (char)('0' + varset[v]));
|
|
||||||
}
|
|
||||||
cout << endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
/**************************************************************************
|
|
||||||
allsat handler for checking that all assignments are detected.
|
|
||||||
**************************************************************************/
|
|
||||||
|
|
||||||
static bdd allsatBDD;
|
|
||||||
static bdd allsatSumBDD;
|
|
||||||
|
|
||||||
void allsatHandler(char* varset, int size)
|
|
||||||
{
|
|
||||||
bdd x = bddtrue;
|
|
||||||
for (int v=0 ; v<size ; ++v)
|
|
||||||
if (varset[v] == 0)
|
|
||||||
x &= bdd_nithvar(v);
|
|
||||||
else if (varset[v] == 1)
|
|
||||||
x &= bdd_ithvar(v);
|
|
||||||
|
|
||||||
// Sum up all assignments
|
|
||||||
allsatSumBDD |= x;
|
|
||||||
|
|
||||||
// Remove assignment from initial set
|
|
||||||
allsatBDD -= x;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void test1_check(bdd x)
|
|
||||||
{
|
|
||||||
double anum = bdd_satcount(x);
|
|
||||||
|
|
||||||
cout << "Checking bdd with " << setw(4) << anum << " assignments: ";
|
|
||||||
|
|
||||||
allsatBDD = x;
|
|
||||||
allsatSumBDD = bddfalse;
|
|
||||||
|
|
||||||
// Calculate whole set of asignments and remove all assignments
|
|
||||||
// from original set
|
|
||||||
bdd_allsat(x, allsatHandler);
|
|
||||||
|
|
||||||
// Now the summed set should be equal to the original set
|
|
||||||
if (allsatSumBDD == x)
|
|
||||||
cout << " Sum-OK. ";
|
|
||||||
else
|
|
||||||
cout << " Sum-ERROR. ";
|
|
||||||
|
|
||||||
// The subtracted set should be empty
|
|
||||||
if (allsatBDD == bddfalse)
|
|
||||||
cout << "Sub-OK.\n";
|
|
||||||
else
|
|
||||||
cout << "Sub-ERROR.\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void test1()
|
|
||||||
{
|
|
||||||
bdd a = bdd_ithvar(0);
|
|
||||||
bdd b = bdd_ithvar(1);
|
|
||||||
bdd c = bdd_ithvar(2);
|
|
||||||
bdd d = bdd_ithvar(3);
|
|
||||||
bdd x;
|
|
||||||
|
|
||||||
x = bddtrue;
|
|
||||||
test1_check(x);
|
|
||||||
|
|
||||||
x = bddfalse;
|
|
||||||
test1_check(x);
|
|
||||||
|
|
||||||
x = a & b | !a & !b;
|
|
||||||
test1_check(x);
|
|
||||||
|
|
||||||
x = a & b | c & d;
|
|
||||||
test1_check(x);
|
|
||||||
|
|
||||||
x = a & !b | a & !d | a & b & !c;
|
|
||||||
test1_check(x);
|
|
||||||
|
|
||||||
int i;
|
|
||||||
for (i=0 ; i<varnum ; ++i)
|
|
||||||
{
|
|
||||||
test1_check(bdd_ithvar(i));
|
|
||||||
test1_check(bdd_nithvar(i));
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd set = bddtrue;
|
|
||||||
for (i=0 ; i<50 ; ++i)
|
|
||||||
{
|
|
||||||
int v = rand() % varnum;
|
|
||||||
int s = rand() % 2;
|
|
||||||
int o = rand() % 2;
|
|
||||||
|
|
||||||
if (o == 0)
|
|
||||||
{
|
|
||||||
if (s == 0)
|
|
||||||
set &= bdd_ithvar(v);
|
|
||||||
else
|
|
||||||
set &= bdd_nithvar(v);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
if (s == 0)
|
|
||||||
set |= bdd_ithvar(v);
|
|
||||||
else
|
|
||||||
set |= bdd_nithvar(v);
|
|
||||||
}
|
|
||||||
|
|
||||||
test1_check(set);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
/**************************************************************************
|
|
||||||
Main
|
|
||||||
**************************************************************************/
|
|
||||||
|
|
||||||
int main()
|
|
||||||
{
|
|
||||||
bdd_init(1000,1000);
|
|
||||||
bdd_setvarnum(varnum);
|
|
||||||
|
|
||||||
test1();
|
|
||||||
|
|
||||||
bdd_done();
|
|
||||||
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue