diff --git a/buddy/examples/calculator/Makefile.am b/buddy/examples/calculator/Makefile.am deleted file mode 100644 index 411e56ea0..000000000 --- a/buddy/examples/calculator/Makefile.am +++ /dev/null @@ -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 diff --git a/buddy/examples/calculator/example.cal b/buddy/examples/calculator/example.cal deleted file mode 100644 index cc79b79ba..000000000 --- a/buddy/examples/calculator/example.cal +++ /dev/null @@ -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; diff --git a/buddy/examples/calculator/examples/c1355.cal b/buddy/examples/calculator/examples/c1355.cal deleted file mode 100644 index 2a665cab9..000000000 --- a/buddy/examples/calculator/examples/c1355.cal +++ /dev/null @@ -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; diff --git a/buddy/examples/calculator/examples/c1908.cal b/buddy/examples/calculator/examples/c1908.cal deleted file mode 100644 index 91f2368f0..000000000 --- a/buddy/examples/calculator/examples/c1908.cal +++ /dev/null @@ -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; diff --git a/buddy/examples/calculator/examples/c2670.cal b/buddy/examples/calculator/examples/c2670.cal deleted file mode 100644 index 0ea2dbe5c..000000000 --- a/buddy/examples/calculator/examples/c2670.cal +++ /dev/null @@ -1,1237 +0,0 @@ -/* BDD Calculator data file */ - -initial 41000 10000; - -inputs -_1 _2 _3 _4 _5 _6 _7 _8 _11 _14 -_15 _16 _19 _20 _21 _22 _23 _24 _25 _26 -_27 _28 _29 _32 _33 _34 _35 _36 _37 _40 -_43 _44 _47 _48 _49 _50 _51 _52 _53 _54 -_55 _56 _57 _60 _61 _62 _63 _64 _65 _66 -_67 _68 _69 _72 _73 _74 _75 _76 _77 _78 -_79 _80 _81 _82 _85 _86 _87 _88 _89 _90 -_91 _92 _93 _94 _95 _96 _99 _100 _101 _102 -_103 _104 _105 _106 _107 _108 _111 _112 _113 _114 -_115 _116 _117 _118 _119 _120 _123 _124 _125 _126 -_127 _128 _129 _130 _131 _132 _135 _136 _137 _138 -_139 _140 _141 _142 _452 _483 _543 _559 _567 _651 -_661 _860 _868 _1083 _1341 _1348 _1384 _1956 _1961 _1966 -_1971 _1976 _1981 _1986 _1991 _1996 _2066 _2067 _2072 _2078 -_2084 _2090 _2096 _2100 _2104 _2105 _2106 _2427 _2430 _2435 -_2438 _2443 _2446 _2451 _2454 _2474 _2678 ; - -actions -autoreorder 0 sift; - -t2 = _860; -t3 = not t2; -t4 = _56; -t5 = _543; -t6 = not t5; -t7 = t4 and t6; -t8 = _651; -t9 = t7 and t8; -t10 = _81; -t11 = t10 and t6; -t12 = not t8; -t13 = t11 and t12; -t14 = _43; -t15 = t14 and t5; -t16 = t15 and t12; -t17 = t13 or t16; -t18 = t9 or t17; -t19 = _68; -t20 = t19 and t5; -t21 = t20 and t8; -t22 = t18 or t21; -t23 = t22 and t2; -t24 = t3 or t23; -t25 = t3 or t22; -t26 = t24 biimp t25; -t27 = t6 and t8; -t28 = _87; -t29 = t28 and t6; -t30 = t29 and t12; -t31 = _49; -t32 = t31 and t5; -t33 = t32 and t12; -t34 = t30 or t33; -t35 = t27 or t34; -t36 = _74; -t37 = t36 and t5; -t38 = t37 and t8; -t39 = t35 or t38; -t40 = t29 or t33; -t41 = t27 or t40; -t42 = t36 and t8; -t43 = t41 or t42; -t44 = t39 biimp t43; -t45 = _559; -t46 = not t45; -t47 = _66; -t48 = t47 and t6; -t49 = t48 and t8; -t50 = _92; -t51 = t50 and t6; -t52 = t51 and t12; -t53 = _54; -t54 = t53 and t5; -t55 = t54 and t12; -t56 = t52 or t55; -t57 = t49 or t56; -t58 = _79; -t59 = t58 and t5; -t60 = t59 and t8; -t61 = t57 or t60; -t62 = not t61; -t63 = t46 nand t62; -t64 = t63 and t3; -t65 = t61 and t2; -t66 = t64 or t65; -t67 = t64 or t61; -t68 = t66 biimp t67; -t69 = _2100; -t70 = not t69; -t71 = _2104; -t72 = not t71; -t73 = _2105; -t74 = t72 and t73; -t75 = not t73; -t76 = t72 and t75; -t77 = t71 and t75; -t78 = t76 or t77; -t79 = t74 or t78; -t80 = t71 and t73; -t81 = t79 or t80; -t82 = t70 nand t81; -t83 = t70 and t82; -t84 = t82 and t81; -t85 = t83 or t84; -t86 = not t85; -t87 = t85 and t86; -t88 = t87 or t86; -t89 = _2096; -t90 = not t89; -t91 = _123; -t92 = t91 and t72; -t93 = t92 and t73; -t94 = _135; -t95 = t94 and t72; -t96 = t95 and t75; -t97 = _99; -t98 = t97 and t71; -t99 = t98 and t75; -t100 = t96 or t99; -t101 = t93 or t100; -t102 = _111; -t103 = t102 and t71; -t104 = t103 and t73; -t105 = t101 or t104; -t106 = t90 nand t105; -t107 = t90 and t106; -t108 = t106 and t105; -t109 = t107 or t108; -t110 = not t109; -t111 = t109 and t110; -t112 = t111 or t110; -t113 = t88 nand t112; -t114 = not t70; -t115 = not t114; -t116 = t115 nand t110; -t117 = t113 biimp t116; -t118 = _23; -t119 = _16; -t120 = not t119; -t121 = t118 and t120; -t122 = t39 and t119; -t123 = t121 or t122; -t124 = _1976; -t125 = not t124; -t126 = not t125; -t127 = t123 nand t126; -t128 = not t123; -t129 = t125 nand t128; -t130 = t127 nand t129; -t131 = not t130; -t132 = _6; -t133 = t132 and t120; -t134 = _61; -t135 = t134 and t6; -t136 = t135 and t8; -t137 = _86; -t138 = t137 and t6; -t139 = t138 and t12; -t140 = _48; -t141 = t140 and t5; -t142 = t141 and t12; -t143 = t139 or t142; -t144 = t136 or t143; -t145 = _73; -t146 = t145 and t5; -t147 = t146 and t8; -t148 = t144 or t147; -t149 = t148 and t119; -t150 = t133 or t149; -t151 = _1981; -t152 = not t151; -t153 = not t152; -t154 = t150 nand t153; -t155 = not t150; -t156 = t152 nand t155; -t157 = t154 nand t156; -t158 = not t157; -t159 = _25; -t160 = _29; -t161 = not t160; -t162 = t159 and t161; -t163 = _119; -t164 = t163 and t72; -t165 = t164 and t73; -t166 = _131; -t167 = t166 and t72; -t168 = t167 and t75; -t169 = _95; -t170 = t169 and t71; -t171 = t170 and t75; -t172 = t168 or t171; -t173 = t165 or t172; -t174 = _107; -t175 = t174 and t71; -t176 = t175 and t73; -t177 = t173 or t176; -t178 = t177 and t160; -t179 = t162 or t178; -t180 = _1991; -t181 = not t180; -t182 = not t181; -t183 = t179 nand t182; -t184 = not t179; -t185 = t181 nand t184; -t186 = t183 nand t185; -t187 = not t186; -t188 = _24; -t189 = t188 and t120; -t190 = _60; -t191 = t190 and t6; -t192 = t191 and t8; -t193 = _85; -t194 = t193 and t6; -t195 = t194 and t12; -t196 = _47; -t197 = t196 and t5; -t198 = t197 and t12; -t199 = t195 or t198; -t200 = t192 or t199; -t201 = _72; -t202 = t201 and t5; -t203 = t202 and t8; -t204 = t200 or t203; -t205 = t204 and t119; -t206 = t189 or t205; -t207 = _1986; -t208 = not t207; -t209 = not t208; -t210 = t206 nand t209; -t211 = not t206; -t212 = t208 nand t211; -t213 = t210 nand t212; -t214 = not t213; -t215 = t187 and t214; -t216 = t158 and t215; -t217 = t131 and t216; -t218 = _22; -t219 = t218 and t120; -t220 = _62; -t221 = t220 and t6; -t222 = t221 and t8; -t223 = _88; -t224 = t223 and t6; -t225 = t224 and t12; -t226 = _50; -t227 = t226 and t5; -t228 = t227 and t12; -t229 = t225 or t228; -t230 = t222 or t229; -t231 = _75; -t232 = t231 and t5; -t233 = t232 and t8; -t234 = t230 or t233; -t235 = t234 and t119; -t236 = t219 or t235; -t237 = _1971; -t238 = not t237; -t239 = not t238; -t240 = t236 nand t239; -t241 = not t236; -t242 = t238 nand t241; -t243 = t240 nand t242; -t244 = not t243; -t245 = t217 and t244; -t246 = _4; -t247 = t246 and t120; -t248 = t61 and t119; -t249 = t247 or t248; -t250 = _1348; -t251 = not t250; -t252 = not t251; -t253 = t249 nand t252; -t254 = not t249; -t255 = t251 nand t254; -t256 = t253 nand t255; -t257 = not t256; -t258 = _20; -t259 = t258 and t120; -t260 = _65; -t261 = t260 and t6; -t262 = t261 and t8; -t263 = _91; -t264 = t263 and t6; -t265 = t264 and t12; -t266 = _53; -t267 = t266 and t5; -t268 = t267 and t12; -t269 = t265 or t268; -t270 = t262 or t269; -t271 = _78; -t272 = t271 and t5; -t273 = t272 and t8; -t274 = t270 or t273; -t275 = t274 and t119; -t276 = t259 or t275; -t277 = _1956; -t278 = not t277; -t279 = not t278; -t280 = t276 nand t279; -t281 = not t276; -t282 = t278 nand t281; -t283 = t280 nand t282; -t284 = not t283; -t285 = _21; -t286 = t285 and t120; -t287 = _63; -t288 = t287 and t6; -t289 = t288 and t8; -t290 = _89; -t291 = t290 and t6; -t292 = t291 and t12; -t293 = _51; -t294 = t293 and t5; -t295 = t294 and t12; -t296 = t292 or t295; -t297 = t289 or t296; -t298 = _76; -t299 = t298 and t5; -t300 = t299 and t8; -t301 = t297 or t300; -t302 = t301 and t119; -t303 = t286 or t302; -t304 = _1966; -t305 = not t304; -t306 = not t305; -t307 = t303 nand t306; -t308 = not t303; -t309 = t305 nand t308; -t310 = t307 nand t309; -t311 = not t310; -t312 = _5; -t313 = t312 and t120; -t314 = _64; -t315 = t314 and t6; -t316 = t315 and t8; -t317 = _90; -t318 = t317 and t6; -t319 = t318 and t12; -t320 = _52; -t321 = t320 and t5; -t322 = t321 and t12; -t323 = t319 or t322; -t324 = t316 or t323; -t325 = _77; -t326 = t325 and t5; -t327 = t326 and t8; -t328 = t324 or t327; -t329 = t328 and t119; -t330 = t313 or t329; -t331 = _1961; -t332 = not t331; -t333 = not t332; -t334 = t330 nand t333; -t335 = not t330; -t336 = t332 nand t335; -t337 = t334 nand t336; -t338 = not t337; -t339 = t311 and t338; -t340 = t284 and t339; -t341 = t257 and t340; -t342 = _19; -t343 = t342 and t120; -t344 = t22 and t119; -t345 = t343 or t344; -t346 = _1341; -t347 = not t346; -t348 = not t347; -t349 = t345 nand t348; -t350 = not t345; -t351 = t347 nand t350; -t352 = t349 nand t351; -t353 = not t352; -t354 = t341 and t353; -t355 = t245 and t354; -t356 = _28; -t357 = t356 and t161; -t358 = t105 and t160; -t359 = t357 or t358; -t360 = _35; -t361 = t360 and t161; -t362 = _124; -t363 = t362 and t72; -t364 = t363 and t73; -t365 = _136; -t366 = t365 and t72; -t367 = t366 and t75; -t368 = _100; -t369 = t368 and t71; -t370 = t369 and t75; -t371 = t367 or t370; -t372 = t364 or t371; -t373 = _112; -t374 = t373 and t71; -t375 = t374 and t73; -t376 = t372 or t375; -t377 = t376 and t160; -t378 = t361 or t377; -t379 = _2090; -t380 = not t379; -t381 = not t380; -t382 = t378 nand t381; -t383 = not t378; -t384 = t380 nand t383; -t385 = t382 nand t384; -t386 = not t385; -t387 = t359 and t386; -t388 = _26; -t389 = t388 and t161; -t390 = _128; -t391 = t390 and t72; -t392 = t391 and t73; -t393 = _140; -t394 = t393 and t72; -t395 = t394 and t75; -t396 = _104; -t397 = t396 and t71; -t398 = t397 and t75; -t399 = t395 or t398; -t400 = t392 or t399; -t401 = _116; -t402 = t401 and t71; -t403 = t402 and t73; -t404 = t400 or t403; -t405 = t404 and t160; -t406 = t389 or t405; -t407 = _2067; -t408 = not t407; -t409 = not t408; -t410 = t406 nand t409; -t411 = not t406; -t412 = t408 nand t411; -t413 = t410 nand t412; -t414 = not t413; -t415 = _33; -t416 = t415 and t161; -t417 = _127; -t418 = t417 and t72; -t419 = t418 and t73; -t420 = _139; -t421 = t420 and t72; -t422 = t421 and t75; -t423 = _103; -t424 = t423 and t71; -t425 = t424 and t75; -t426 = t422 or t425; -t427 = t419 or t426; -t428 = _115; -t429 = t428 and t71; -t430 = t429 and t73; -t431 = t427 or t430; -t432 = t431 and t160; -t433 = t416 or t432; -t434 = _2072; -t435 = not t434; -t436 = not t435; -t437 = t433 nand t436; -t438 = not t433; -t439 = t435 nand t438; -t440 = t437 nand t439; -t441 = not t440; -t442 = _34; -t443 = t442 and t161; -t444 = _125; -t445 = t444 and t72; -t446 = t445 and t73; -t447 = _137; -t448 = t447 and t72; -t449 = t448 and t75; -t450 = _101; -t451 = t450 and t71; -t452 = t451 and t75; -t453 = t449 or t452; -t454 = t446 or t453; -t455 = _113; -t456 = t455 and t71; -t457 = t456 and t73; -t458 = t454 or t457; -t459 = t458 and t160; -t460 = t443 or t459; -t461 = _2084; -t462 = not t461; -t463 = not t462; -t464 = t460 nand t463; -t465 = not t460; -t466 = t462 nand t465; -t467 = t464 nand t466; -t468 = not t467; -t469 = _27; -t470 = t469 and t161; -t471 = _126; -t472 = t471 and t72; -t473 = t472 and t73; -t474 = _138; -t475 = t474 and t72; -t476 = t475 and t75; -t477 = _102; -t478 = t477 and t71; -t479 = t478 and t75; -t480 = t476 or t479; -t481 = t473 or t480; -t482 = _114; -t483 = t482 and t71; -t484 = t483 and t73; -t485 = t481 or t484; -t486 = t485 and t160; -t487 = t470 or t486; -t488 = _2078; -t489 = not t488; -t490 = not t489; -t491 = t487 nand t490; -t492 = not t487; -t493 = t489 nand t492; -t494 = t491 nand t493; -t495 = not t494; -t496 = t468 and t495; -t497 = t441 and t496; -t498 = t414 and t497; -t499 = _32; -t500 = t499 and t161; -t501 = _129; -t502 = t501 and t72; -t503 = t502 and t73; -t504 = _141; -t505 = t504 and t72; -t506 = t505 and t75; -t507 = _105; -t508 = t507 and t71; -t509 = t508 and t75; -t510 = t506 or t509; -t511 = t503 or t510; -t512 = _117; -t513 = t512 and t71; -t514 = t513 and t73; -t515 = t511 or t514; -t516 = t515 and t160; -t517 = t500 or t516; -t518 = _1996; -t519 = not t518; -t520 = not t519; -t521 = t517 nand t520; -t522 = not t517; -t523 = t519 nand t522; -t524 = t521 nand t523; -t525 = not t524; -t526 = t498 and t525; -t527 = t387 and t526; -t528 = t355 and t527; -t529 = _11; -t530 = _868; -t531 = not t530; -t532 = t529 and t531; -t533 = t529 and t530; -t534 = t532 or t533; -t535 = t528 and t534; -t536 = t43 and t119; -t537 = t121 or t536; -t538 = t537 nand t126; -t539 = not t537; -t540 = t125 nand t539; -t541 = t538 nand t540; -t542 = not t541; -t543 = t542 and t216; -t544 = t543 and t244; -t545 = t544 and t354; -t546 = t545 and t527; -t547 = t546 and t529; -t548 = t535 biimp t547; -t549 = not t535; -t550 = not t547; -t551 = t549 biimp t550; -t552 = not t376; -t553 = t458 nand t552; -t554 = not t458; -t555 = t376 nand t554; -t556 = t553 nand t555; -t557 = not t81; -t558 = t105 nand t557; -t559 = not t105; -t560 = t81 nand t559; -t561 = t558 nand t560; -t562 = not t561; -t563 = t556 nand t562; -t564 = not t556; -t565 = t561 nand t564; -t566 = t563 nand t565; -t567 = _130; -t568 = t567 and t72; -t569 = t568 and t73; -t570 = _142; -t571 = t570 and t72; -t572 = t571 and t75; -t573 = _106; -t574 = t573 and t71; -t575 = t574 and t75; -t576 = t572 or t575; -t577 = t569 or t576; -t578 = _118; -t579 = t578 and t71; -t580 = t579 and t73; -t581 = t577 or t580; -t582 = not t177; -t583 = t581 nand t582; -t584 = not t581; -t585 = t177 nand t584; -t586 = t583 nand t585; -t587 = not t404; -t588 = t515 nand t587; -t589 = not t515; -t590 = t404 nand t589; -t591 = t588 nand t590; -t592 = not t591; -t593 = t586 and t592; -t594 = not t485; -t595 = t431 nand t594; -t596 = not t431; -t597 = t485 nand t596; -t598 = t595 nand t597; -t599 = not t598; -t600 = t593 and t599; -t601 = not t586; -t602 = t592 and t601; -t603 = t602 and t598; -t604 = t600 nor t603; -t605 = t601 and t591; -t606 = t605 and t599; -t607 = t591 and t586; -t608 = t607 and t598; -t609 = t606 nor t608; -t610 = t604 nand t609; -t611 = not t610; -t612 = t566 nand t611; -t613 = not t566; -t614 = t610 nand t613; -t615 = t612 nand t614; -t616 = not t615; -t617 = _37; -t618 = not t617; -t619 = t616 and t618; -t620 = not t559; -t621 = not t620; -t622 = not t621; -t623 = t556 nand t622; -t624 = t621 nand t564; -t625 = t623 nand t624; -t626 = t625 nand t611; -t627 = not t625; -t628 = t610 nand t627; -t629 = t626 nand t628; -t630 = not t629; -t631 = t630 and t618; -t632 = t619 biimp t631; -t633 = _67; -t634 = t633 and t6; -t635 = t634 and t8; -t636 = _93; -t637 = t636 and t6; -t638 = t637 and t12; -t639 = _55; -t640 = t639 and t5; -t641 = t640 and t12; -t642 = t638 or t641; -t643 = t635 or t642; -t644 = _80; -t645 = t644 and t5; -t646 = t645 and t8; -t647 = t643 or t646; -t648 = t647 and t531; -t649 = not t234; -t650 = not t39; -t651 = not t650; -t652 = t649 nand t651; -t653 = not t649; -t654 = t650 nand t653; -t655 = t652 nand t654; -t656 = not t148; -t657 = not t204; -t658 = not t657; -t659 = t656 nand t658; -t660 = not t656; -t661 = t657 nand t660; -t662 = t659 nand t661; -t663 = not t662; -t664 = t655 nand t663; -t665 = not t655; -t666 = t662 nand t665; -t667 = t664 nand t666; -t668 = not t647; -t669 = not t22; -t670 = not t669; -t671 = t668 nand t670; -t672 = not t668; -t673 = t669 nand t672; -t674 = t671 nand t673; -t675 = not t674; -t676 = t63 and t675; -t677 = not t274; -t678 = not t677; -t679 = t62 nand t678; -t680 = not t62; -t681 = t677 nand t680; -t682 = t679 nand t681; -t683 = not t682; -t684 = t676 and t683; -t685 = not t63; -t686 = t675 and t685; -t687 = t686 and t682; -t688 = t684 nor t687; -t689 = t685 and t674; -t690 = t689 and t683; -t691 = t674 and t63; -t692 = t691 and t682; -t693 = t690 nor t692; -t694 = t688 nand t693; -t695 = not t694; -t696 = t667 nand t695; -t697 = not t667; -t698 = t694 nand t697; -t699 = t696 nand t698; -t700 = t699 and t530; -t701 = t648 or t700; -t702 = not t43; -t703 = not t702; -t704 = t649 nand t703; -t705 = t702 nand t653; -t706 = t704 nand t705; -t707 = t706 nand t663; -t708 = not t706; -t709 = t662 nand t708; -t710 = t707 nand t709; -t711 = t710 nand t695; -t712 = not t710; -t713 = t694 nand t712; -t714 = t711 nand t713; -t715 = t714 and t530; -t716 = t648 or t715; -t717 = t701 biimp t716; -t718 = t674 and t683; -t719 = not t328; -t720 = not t301; -t721 = not t720; -t722 = t719 nand t721; -t723 = not t719; -t724 = t720 nand t723; -t725 = t722 nand t724; -t726 = not t725; -t727 = t718 and t726; -t728 = t683 and t675; -t729 = t728 and t725; -t730 = t727 nor t729; -t731 = t675 and t682; -t732 = t731 and t726; -t733 = t682 and t674; -t734 = t733 and t725; -t735 = t732 nor t734; -t736 = t730 nand t735; -t737 = not t736; -t738 = t667 nand t737; -t739 = t736 nand t697; -t740 = t738 nand t739; -t741 = not t740; -t742 = t741 and t618; -t743 = t710 nand t737; -t744 = t736 nand t712; -t745 = t743 nand t744; -t746 = not t745; -t747 = t746 and t618; -t748 = t742 biimp t747; -t749 = _1384; -t750 = not t749; -t751 = t485 and t750; -t752 = t554 and t751; -t753 = _40; -t754 = t752 and t753; -t755 = not t754; -t756 = t515 and t755; -t757 = t753 and t554; -t758 = not t751; -t759 = t757 and t758; -t760 = t756 and t759; -t761 = not t760; -t762 = t519 and t755; -t763 = t762 and t759; -t764 = not t763; -t765 = t761 nand t764; -t766 = not t761; -t767 = t763 nand t766; -t768 = t765 nand t767; -t769 = t404 and t755; -t770 = t769 and t759; -t771 = not t770; -t772 = t408 and t755; -t773 = t772 and t759; -t774 = not t773; -t775 = t771 nand t774; -t776 = not t771; -t777 = t773 nand t776; -t778 = t775 nand t777; -t779 = t768 and t778; -t780 = t181 and t755; -t781 = t780 and t759; -t782 = t177 and t755; -t783 = t782 and t759; -t784 = not t783; -t785 = t781 and t784; -t786 = t779 and t785; -t787 = t773 and t771; -t788 = t763 and t761; -t789 = t778 and t788; -t790 = t787 or t789; -t791 = t786 or t790; -t792 = t204 and t755; -t793 = t792 and t759; -t794 = not t793; -t795 = t208 and t755; -t796 = t795 and t759; -t797 = t794 and t796; -t798 = not t781; -t799 = t784 nand t798; -t800 = not t784; -t801 = t781 nand t800; -t802 = t799 nand t801; -t803 = t802 and t778; -t804 = t797 and t803; -t805 = t804 and t768; -t806 = t791 or t805; -t807 = not t755; -t808 = t462 and t807; -t809 = t305 and t755; -t810 = t808 or t809; -t811 = _8; -t812 = t810 and t811; -t813 = t301 and t755; -t814 = t301 and t754; -t815 = t813 or t814; -t816 = t815 and t811; -t817 = not t816; -t818 = t812 and t817; -t819 = t234 and t755; -t820 = t234 and t754; -t821 = t819 or t820; -t822 = t821 and t811; -t823 = not t822; -t824 = t380 and t807; -t825 = t238 and t755; -t826 = t824 or t825; -t827 = t826 and t811; -t828 = not t827; -t829 = t823 nand t828; -t830 = not t823; -t831 = t827 nand t830; -t832 = t829 nand t831; -t833 = t148 and t755; -t834 = t833 and t811; -t835 = not t834; -t836 = t152 and t755; -t837 = t836 and t811; -t838 = not t837; -t839 = t835 nand t838; -t840 = not t835; -t841 = t837 nand t840; -t842 = t839 nand t841; -t843 = t832 and t842; -t844 = t818 and t843; -t845 = t39 and t755; -t846 = t845 and t811; -t847 = not t846; -t848 = t125 and t755; -t849 = t848 and t811; -t850 = not t849; -t851 = t847 nand t850; -t852 = not t847; -t853 = t849 nand t852; -t854 = t851 nand t853; -t855 = t844 and t854; -t856 = t854 and t842; -t857 = t827 and t823; -t858 = t856 and t857; -t859 = t837 and t835; -t860 = t849 and t847; -t861 = t842 and t860; -t862 = t859 or t861; -t863 = t858 or t862; -t864 = t855 or t863; -t865 = t489 and t807; -t866 = t332 and t755; -t867 = t865 or t866; -t868 = t867 and t719; -t869 = not t812; -t870 = t817 nand t869; -t871 = not t817; -t872 = t812 nand t871; -t873 = t870 nand t872; -t874 = t873 and t832; -t875 = t842 and t874; -t876 = t868 and t875; -t877 = t876 and t854; -t878 = t864 or t877; -t879 = not t867; -t880 = t719 nand t879; -t881 = t867 nand t723; -t882 = t880 nand t881; -t883 = t854 and t882; -t884 = t832 and t883; -t885 = t842 and t884; -t886 = t885 and t873; -t887 = t435 and t807; -t888 = t278 and t755; -t889 = t887 or t888; -t890 = t889 and t677; -t891 = not t889; -t892 = t677 nand t891; -t893 = t889 nand t678; -t894 = t892 nand t893; -t895 = t408 and t807; -t896 = t251 and t755; -t897 = t895 or t896; -t898 = t897 and t62; -t899 = t894 and t898; -t900 = t890 or t899; -t901 = not t897; -t902 = t62 nand t901; -t903 = t897 nand t680; -t904 = t902 nand t903; -t905 = t904 and t894; -t906 = t519 and t807; -t907 = t347 and t755; -t908 = t906 or t907; -t909 = t908 and t669; -t910 = t905 and t909; -t911 = t900 or t910; -t912 = t886 and t911; -t913 = t878 or t912; -t914 = not t913; -t915 = t806 and t914; -t916 = not t806; -t917 = not t796; -t918 = t794 nand t917; -t919 = not t794; -t920 = t796 nand t919; -t921 = t918 nand t920; -t922 = t768 and t921; -t923 = t802 and t922; -t924 = t923 and t778; -t925 = not t924; -t926 = t916 nand t925; -t927 = t926 and t913; -t928 = t915 or t927; -t929 = t756 and t757; -t930 = not t929; -t931 = not t930; -t932 = t762 and t757; -t933 = not t932; -t934 = t931 nand t933; -t935 = t769 and t757; -t936 = not t935; -t937 = not t936; -t938 = t772 and t757; -t939 = not t938; -t940 = t937 nand t939; -t941 = t934 and t940; -t942 = t780 and t757; -t943 = t782 and t757; -t944 = not t943; -t945 = t942 and t944; -t946 = t941 and t945; -t947 = t938 and t936; -t948 = t932 and t930; -t949 = t940 and t948; -t950 = t947 or t949; -t951 = t946 or t950; -t952 = t792 and t757; -t953 = not t952; -t954 = t795 and t757; -t955 = t953 and t954; -t956 = not t944; -t957 = not t942; -t958 = t956 nand t957; -t959 = t958 and t940; -t960 = t955 and t959; -t961 = t960 and t934; -t962 = t951 or t961; -t963 = not t953; -t964 = not t954; -t965 = t963 nand t964; -t966 = t934 and t965; -t967 = t958 and t966; -t968 = t967 and t940; -t969 = not t968; -t970 = not t969; -t971 = t301 and t811; -t972 = not t971; -t973 = t812 and t972; -t974 = t234 and t811; -t975 = not t974; -t976 = not t975; -t977 = t976 nand t828; -t978 = t840 nand t838; -t979 = t977 and t978; -t980 = t973 and t979; -t981 = t43 and t755; -t982 = t981 and t811; -t983 = not t982; -t984 = not t983; -t985 = t984 nand t850; -t986 = t980 and t985; -t987 = t985 and t978; -t988 = t827 and t975; -t989 = t987 and t988; -t990 = t849 and t983; -t991 = t978 and t990; -t992 = t859 or t991; -t993 = t989 or t992; -t994 = t986 or t993; -t995 = not t972; -t996 = t995 nand t869; -t997 = t996 and t977; -t998 = t978 and t997; -t999 = t868 and t998; -t1000 = t999 and t985; -t1001 = t994 or t1000; -t1002 = t723 nand t879; -t1003 = t985 and t1002; -t1004 = t977 and t1003; -t1005 = t978 and t1004; -t1006 = t1005 and t996; -t1007 = t678 nand t891; -t1008 = t1007 and t898; -t1009 = t890 or t1008; -t1010 = t680 nand t901; -t1011 = t1010 and t1007; -t1012 = t1011 and t909; -t1013 = t1009 or t1012; -t1014 = t1006 and t1013; -t1015 = t1001 or t1014; -t1016 = t970 and t1015; -t1017 = t962 or t1016; -t1018 = t928 biimp t1017; -t1019 = not t619; -t1020 = not t742; -t1021 = t1019 and t1020; -t1022 = t89 nand t70; -t1023 = t69 nand t90; -t1024 = t1022 nand t1023; -t1025 = _2678; -t1026 = t1025 nand t408; -t1027 = not t1025; -t1028 = t407 nand t1027; -t1029 = t1026 nand t1028; -t1030 = t434 nand t489; -t1031 = t488 nand t435; -t1032 = t1030 nand t1031; -t1033 = not t1032; -t1034 = t1029 and t1033; -t1035 = t461 nand t380; -t1036 = t379 nand t462; -t1037 = t1035 nand t1036; -t1038 = not t1037; -t1039 = t1034 and t1038; -t1040 = not t1029; -t1041 = t1033 and t1040; -t1042 = t1041 and t1037; -t1043 = t1039 nor t1042; -t1044 = t1040 and t1032; -t1045 = t1044 and t1038; -t1046 = t1032 and t1029; -t1047 = t1046 and t1037; -t1048 = t1045 nor t1047; -t1049 = t1043 nand t1048; -t1050 = not t1049; -t1051 = t1024 nand t1050; -t1052 = not t1024; -t1053 = t1049 nand t1052; -t1054 = t1051 nand t1053; -t1055 = t1021 and t1054; -t1056 = t151 nand t208; -t1057 = t207 nand t152; -t1058 = t1056 nand t1057; -t1059 = t180 nand t519; -t1060 = t518 nand t181; -t1061 = t1059 nand t1060; -t1062 = not t1061; -t1063 = t1058 nand t1062; -t1064 = not t1058; -t1065 = t1061 nand t1064; -t1066 = t1063 nand t1065; -t1067 = _2474; -t1068 = t1067 nand t278; -t1069 = not t1067; -t1070 = t277 nand t1069; -t1071 = t1068 nand t1070; -t1072 = t331 nand t305; -t1073 = t304 nand t332; -t1074 = t1072 nand t1073; -t1075 = not t1074; -t1076 = t1071 and t1075; -t1077 = t237 nand t125; -t1078 = t124 nand t238; -t1079 = t1077 nand t1078; -t1080 = not t1079; -t1081 = t1076 and t1080; -t1082 = not t1071; -t1083 = t1075 and t1082; -t1084 = t1083 and t1079; -t1085 = t1081 nor t1084; -t1086 = t1082 and t1074; -t1087 = t1086 and t1080; -t1088 = t1074 and t1071; -t1089 = t1088 and t1079; -t1090 = t1087 nor t1089; -t1091 = t1085 nand t1090; -t1092 = not t1091; -t1093 = t1066 nand t1092; -t1094 = not t1066; -t1095 = t1091 nand t1094; -t1096 = t1093 nand t1095; -t1097 = _2454; -t1098 = _2451; -t1099 = not t1098; -t1100 = t1097 nand t1099; -t1101 = not t1097; -t1102 = t1098 nand t1101; -t1103 = t1100 nand t1102; -t1104 = t346 nand t251; -t1105 = t250 nand t347; -t1106 = t1104 nand t1105; -t1107 = not t1106; -t1108 = t1103 nand t1107; -t1109 = not t1103; -t1110 = t1106 nand t1109; -t1111 = t1108 nand t1110; -t1112 = _2430; -t1113 = _2427; -t1114 = not t1113; -t1115 = t1112 nand t1114; -t1116 = not t1112; -t1117 = t1113 nand t1116; -t1118 = t1115 nand t1117; -t1119 = _2438; -t1120 = _2435; -t1121 = not t1120; -t1122 = t1119 nand t1121; -t1123 = not t1119; -t1124 = t1120 nand t1123; -t1125 = t1122 nand t1124; -t1126 = not t1125; -t1127 = t1118 and t1126; -t1128 = _2446; -t1129 = _2443; -t1130 = not t1129; -t1131 = t1128 nand t1130; -t1132 = not t1128; -t1133 = t1129 nand t1132; -t1134 = t1131 nand t1133; -t1135 = not t1134; -t1136 = t1127 and t1135; -t1137 = not t1118; -t1138 = t1126 and t1137; -t1139 = t1138 and t1134; -t1140 = t1136 nor t1139; -t1141 = t1137 and t1125; -t1142 = t1141 and t1135; -t1143 = t1125 and t1118; -t1144 = t1143 and t1134; -t1145 = t1142 nor t1144; -t1146 = t1140 nand t1145; -t1147 = not t1146; -t1148 = t1111 nand t1147; -t1149 = not t1111; -t1150 = t1146 nand t1149; -t1151 = t1148 nand t1150; -t1152 = not t1151; -t1153 = _14; -t1154 = t1152 and t1153; -t1155 = not t1154; -t1156 = t1096 and t1155; -t1157 = not t928; -t1158 = t928 and t1157; -t1159 = t1157 and t928; -t1160 = t1158 or t1159; -t1161 = not t1160; -t1162 = t1160 and t1161; -t1163 = t1162 or t1161; -t1164 = t1156 and t1163; -t1165 = t1055 and t1164; -t1166 = _2106; -t1167 = _96; -t1168 = _132; -t1169 = _82; -t1170 = t1168 and t1169; -t1171 = t1167 and t1170; -t1172 = _44; -t1173 = t1171 and t1172; -t1174 = not t1173; -t1175 = t1166 and t1174; -t1176 = not t1175; -t1177 = _567; -t1178 = _108; -t1179 = _120; -t1180 = _57; -t1181 = t1179 and t1180; -t1182 = t1178 and t1181; -t1183 = _69; -t1184 = t1182 and t1183; -t1185 = not t1184; -t1186 = t1177 and t1185; -t1187 = not t1186; -t1188 = t1176 and t1187; -t1189 = t1165 and t1188; -t1190 = not t631; -t1191 = not t747; -t1192 = t1190 and t1191; -t1193 = t1192 and t1054; -t1194 = t1193 and t1156; -t1195 = t1194 and t1188; -t1196 = t1189 biimp t1195; -t1197 = not t1189; -t1198 = not t1195; -t1199 = t1197 biimp t1198; - -tautology t26; -tautology t44; -tautology t68; -tautology t117; -tautology t548; -tautology t551; -tautology t632; -tautology t717; -tautology t717; -tautology t748; -tautology t1018; -tautology t1196; -tautology t1199; diff --git a/buddy/examples/calculator/examples/c3540.cal b/buddy/examples/calculator/examples/c3540.cal deleted file mode 100644 index 09ffb757e..000000000 --- a/buddy/examples/calculator/examples/c3540.cal +++ /dev/null @@ -1,2007 +0,0 @@ -/* BDD Calculator data file */ - -initial 13000 10000; - -inputs -_1 _13 _20 _33 _41 _45 _50 _58 _68 _77 -_87 _97 _107 _116 _124 _125 _128 _132 _137 _143 -_150 _159 _169 _179 _190 _200 _213 _222 _223 _226 -_232 _238 _244 _250 _257 _264 _270 _274 _283 _294 -_303 _311 _317 _322 _326 _329 _330 _343 _1698 _2897 -; - -actions -autoreorder 0 sift; - -t695 = _330; -t9 = _1; -t10 = _13; -t11 = t9 and t10; -t154 = _33; -t180 = _41; -t181 = t154 and t180; -t182 = not t181; -t183 = t11 and t182; -t184 = not t183; -t47 = _270; -t322 = t184 and t47; -t186 = not t9; -t187 = _45; -t188 = t186 and t187; -t189 = not t180; -t190 = t188 and t189; -t191 = not t190; -t323 = t322 and t191; -t193 = _274; -t194 = t184 and t193; -t195 = t194 and t190; -t324 = t323 or t195; -t325 = _303; -t155 = not t154; -t198 = not t155; -t326 = t325 and t198; -t17 = _257; -t200 = _1698; -t201 = t200 or t154; -t202 = not t201; -t327 = t17 and t202; -t328 = t326 or t327; -t18 = _264; -t205 = t155 and t201; -t329 = t18 and t205; -t330 = t328 or t329; -t331 = t183 and t330; -t332 = t324 or t331; -t185 = t184 and t18; -t192 = t185 and t191; -t196 = t192 or t195; -t197 = _294; -t199 = t197 and t198; -t16 = _250; -t203 = t16 and t202; -t204 = t199 or t203; -t206 = t17 and t205; -t207 = t204 or t206; -t208 = t183 and t207; -t209 = t196 or t208; -t241 = t184 and t16; -t242 = not t188; -t243 = t241 and t242; -t244 = t194 and t188; -t245 = t243 or t244; -t48 = _116; -t246 = t48 and t198; -t27 = _238; -t247 = t27 and t202; -t248 = t246 or t247; -t35 = _244; -t249 = t35 and t205; -t250 = t248 or t249; -t251 = t183 and t250; -t252 = t245 or t251; -t283 = t184 and t17; -t284 = t283 and t191; -t285 = t284 or t195; -t286 = _283; -t287 = t286 and t198; -t288 = t35 and t202; -t289 = t287 or t288; -t290 = t16 and t205; -t291 = t289 or t290; -t292 = t183 and t291; -t293 = t285 or t292; -t744 = t252 and t293; -t745 = t209 and t744; -t746 = t332 and t745; -t211 = _179; -t747 = not t211; -t748 = t746 and t747; -t335 = not t332; -t213 = not t209; -t255 = not t252; -t296 = not t293; -t749 = t255 and t296; -t750 = t213 and t749; -t751 = t335 and t750; -t752 = t751 and t211; -t753 = t748 or t752; -t696 = t186 and t10; -t12 = _20; -t151 = not t12; -t697 = t696 and t151; -t698 = _213; -t699 = t697 and t698; -t700 = _343; -t716 = t699 nand t700; -t754 = not t716; -t755 = t753 and t754; -t150 = _169; -t39 = _107; -t103 = not t39; -t152 = not t151; -t153 = t103 and t152; -t156 = t155 or t12; -t157 = not t156; -t158 = t48 and t157; -t159 = t153 or t158; -t41 = _87; -t160 = t151 and t156; -t161 = t41 and t160; -t162 = t159 or t161; -t163 = t9 nand t10; -t164 = t9 and t12; -t165 = t164 nand t154; -t166 = t163 and t165; -t167 = not t166; -t168 = t162 and t167; -t169 = t10 and t12; -t170 = not t169; -t171 = t9 or t170; -t172 = t39 nor t171; -t173 = t168 or t172; -t174 = t155 or t9; -t175 = t39 and t174; -t176 = t166 and t171; -t177 = t175 and t176; -t178 = t173 or t177; -t179 = t150 and t178; -t210 = t179 and t209; -t212 = t211 and t178; -t214 = t212 and t213; -t215 = t210 nor t214; -t216 = _190; -t217 = t173 nor t177; -t218 = t216 and t217; -t219 = t218 and t213; -t220 = _200; -t221 = t220 and t217; -t222 = t221 and t209; -t223 = t219 or t222; -t224 = not t217; -t225 = t223 or t224; -t226 = t215 and t225; -t110 = not t41; -t43 = _97; -t109 = not t43; -t227 = t110 and t109; -t228 = t227 nand t103; -t229 = t228 and t152; -t230 = t43 and t157; -t231 = t229 or t230; -t5 = _68; -t232 = t5 and t160; -t233 = t231 or t232; -t234 = t233 and t167; -t235 = t41 nor t171; -t236 = t234 or t235; -t237 = t41 and t174; -t238 = t237 and t176; -t239 = t236 or t238; -t240 = t150 and t239; -t253 = t240 and t252; -t254 = t211 and t239; -t256 = t254 and t255; -t257 = t253 nor t256; -t258 = t236 nor t238; -t259 = t216 and t258; -t260 = t259 and t255; -t261 = t220 and t258; -t262 = t261 and t252; -t263 = t260 or t262; -t264 = not t258; -t265 = t263 or t264; -t266 = t257 and t265; -t267 = t39 nand t109; -t268 = t43 nand t103; -t269 = t267 nand t268; -t270 = not t269; -t271 = t270 and t152; -t272 = t39 and t157; -t273 = t271 or t272; -t36 = _77; -t274 = t36 and t160; -t275 = t273 or t274; -t276 = t275 and t167; -t277 = t43 nor t171; -t278 = t276 or t277; -t279 = t43 and t174; -t280 = t279 and t176; -t281 = t278 or t280; -t282 = t150 and t281; -t294 = t282 and t293; -t295 = t211 and t281; -t297 = t295 and t296; -t298 = t294 nor t297; -t299 = t278 nor t280; -t300 = t216 and t299; -t301 = t300 and t296; -t302 = t220 and t299; -t303 = t302 and t293; -t304 = t301 or t303; -t305 = not t299; -t306 = t304 or t305; -t307 = t298 and t306; -t308 = t266 and t307; -t309 = t226 and t308; -t310 = t48 and t152; -t311 = t286 and t157; -t312 = t310 or t311; -t313 = t43 and t160; -t314 = t312 or t313; -t315 = t314 and t167; -t316 = t48 nor t171; -t317 = t315 or t316; -t318 = t48 and t174; -t319 = t318 and t176; -t320 = t317 or t319; -t321 = t150 and t320; -t333 = t321 and t332; -t334 = t211 and t320; -t336 = t334 and t335; -t337 = t333 nor t336; -t338 = t317 nor t319; -t339 = t216 and t338; -t340 = t339 and t335; -t341 = t220 and t338; -t342 = t341 and t332; -t343 = t340 or t342; -t344 = not t338; -t345 = t343 or t344; -t346 = t337 and t345; -t347 = t309 and t346; -t756 = t347 and t716; -t757 = t755 or t756; -t758 = t695 and t757; -t701 = t699 and t700; -t473 = t36 and t152; -t474 = t41 and t157; -t475 = t473 or t474; -t3 = _58; -t476 = t3 and t160; -t477 = t475 or t476; -t478 = t477 and t167; -t479 = t36 nor t171; -t480 = t478 or t479; -t356 = t151 or t9; -t481 = t36 and t356; -t482 = t481 and t176; -t483 = t480 or t482; -t938 = t701 and t483; -t484 = t150 and t483; -t485 = t184 and t35; -t362 = t180 or t187; -t363 = t186 and t362; -t364 = not t363; -t486 = t485 and t364; -t366 = t194 and t363; -t487 = t486 or t366; -t488 = t39 and t198; -t31 = _232; -t489 = t31 and t202; -t490 = t488 or t489; -t491 = t27 and t205; -t492 = t490 or t491; -t493 = t183 and t492; -t494 = t487 or t493; -t495 = t484 and t494; -t496 = t211 and t483; -t497 = not t494; -t498 = t496 and t497; -t499 = t495 nor t498; -t500 = t480 nor t482; -t501 = t216 and t500; -t502 = t501 and t497; -t503 = t220 and t500; -t504 = t503 and t494; -t505 = t502 or t504; -t506 = not t500; -t507 = t505 or t506; -t508 = t499 and t507; -t939 = not t508; -t940 = t938 nand t939; -t941 = not t938; -t942 = t508 nand t941; -t943 = t940 nand t942; -t634 = t210 or t214; -t635 = t308 nand t634; -t636 = t253 or t256; -t637 = not t636; -t638 = t294 or t297; -t639 = t266 nand t638; -t640 = t637 and t639; -t641 = t635 and t640; -t642 = t333 or t336; -t643 = t642 and t307; -t644 = t226 and t643; -t645 = t644 nand t266; -t646 = t641 nand t645; -t759 = t646 and t716; -t760 = not t759; -t944 = t943 nand t760; -t945 = not t943; -t946 = t759 nand t945; -t947 = t944 nand t946; -t948 = not t947; -t949 = t758 nand t948; -t950 = not t758; -t951 = t947 nand t950; -t952 = t949 nand t951; -t798 = t10 and t151; -t799 = t798 nand t187; -t800 = t9 and t799; -t801 = not t800; -t953 = t952 and t801; -t21 = not t10; -t22 = t9 and t21; -t740 = t12 and t22; -t741 = t740 nand t189; -t742 = not t741; -t954 = t952 and t742; -t955 = t953 or t954; -t956 = _143; -t805 = t151 or t216; -t806 = not t220; -t807 = t12 and t211; -t808 = t806 and t807; -t809 = t805 nand t808; -t810 = not t809; -t957 = t956 and t810; -t394 = _150; -t812 = t151 nor t216; -t813 = t220 and t807; -t814 = t812 nand t813; -t815 = not t814; -t958 = t394 and t815; -t437 = _159; -t817 = t812 nand t808; -t818 = not t817; -t959 = t437 and t818; -t2 = _50; -t820 = t12 and t220; -t821 = not t807; -t822 = t820 and t821; -t823 = t805 nand t822; -t824 = not t823; -t960 = t2 and t824; -t826 = t12 nand t220; -t827 = t826 and t821; -t828 = t805 nand t827; -t829 = not t828; -t961 = t3 and t829; -t962 = _132; -t831 = t812 nand t827; -t832 = not t831; -t963 = t962 and t832; -t834 = t812 nand t822; -t835 = not t834; -t964 = t5 and t835; -t965 = t963 or t964; -t966 = t961 or t965; -t967 = t960 or t966; -t968 = t959 or t967; -t969 = t958 or t968; -t970 = t957 or t969; -t971 = _137; -t843 = t805 nand t813; -t844 = not t843; -t972 = t971 and t844; -t973 = t970 nor t972; -t974 = t973 and t155; -t975 = t197 and t810; -t976 = t286 and t815; -t977 = t48 and t818; -t978 = t39 and t824; -t830 = t43 and t829; -t852 = _311; -t979 = t852 and t832; -t980 = t41 and t835; -t981 = t979 or t980; -t982 = t830 or t981; -t983 = t978 or t982; -t984 = t977 or t983; -t985 = t976 or t984; -t986 = t975 or t985; -t987 = t325 and t844; -t988 = t986 nor t987; -t989 = t988 and t154; -t990 = t974 or t989; -t870 = t151 or t150; -t871 = t11 nand t870; -t872 = not t871; -t991 = t990 and t872; -t992 = t21 nand t155; -t993 = not t992; -t994 = t945 and t993; -t995 = t991 or t994; -t121 = not t36; -t996 = t871 and t992; -t997 = t121 and t996; -t998 = t995 nor t997; -t900 = t800 and t741; -t999 = t998 and t900; -t1000 = t955 or t999; -t1001 = t955 nor t999; -t1002 = not t1001; -t1003 = t1000 and t1002; -t511 = t193 and t190; -t548 = t323 or t511; -t549 = t548 or t331; -t512 = t192 or t511; -t513 = t512 or t208; -t523 = t193 and t188; -t524 = t243 or t523; -t525 = t524 or t251; -t535 = t284 or t511; -t536 = t535 or t292; -t773 = t525 and t536; -t774 = t513 and t773; -t775 = t549 and t774; -t776 = t775 and t747; -t551 = not t549; -t515 = not t513; -t527 = not t525; -t538 = not t536; -t777 = t527 and t538; -t778 = t515 and t777; -t779 = t551 and t778; -t780 = t779 and t211; -t781 = t776 or t780; -t782 = t781 and t754; -t514 = t179 and t513; -t516 = t212 and t515; -t517 = t514 nor t516; -t518 = t216 and t515; -t519 = t220 and t513; -t520 = t518 or t519; -t521 = t520 or t224; -t522 = t517 and t521; -t526 = t240 and t525; -t528 = t254 and t527; -t529 = t526 nor t528; -t530 = t216 and t527; -t531 = t220 and t525; -t532 = t530 or t531; -t533 = t532 or t264; -t534 = t529 and t533; -t537 = t282 and t536; -t539 = t295 and t538; -t540 = t537 nor t539; -t541 = t216 and t538; -t542 = t220 and t536; -t543 = t541 or t542; -t544 = t543 or t305; -t545 = t540 and t544; -t546 = t534 and t545; -t547 = t522 and t546; -t550 = t321 and t549; -t552 = t334 and t551; -t553 = t550 nor t552; -t554 = t216 and t551; -t555 = t220 and t549; -t556 = t554 or t555; -t557 = t556 or t344; -t558 = t553 and t557; -t559 = t547 and t558; -t783 = t559 and t716; -t784 = t782 or t783; -t785 = t695 and t784; -t614 = t481 and t166; -t615 = t480 or t614; -t1004 = t701 and t615; -t616 = t150 and t615; -t563 = t193 and t363; -t617 = t486 or t563; -t618 = t617 or t493; -t619 = t616 and t618; -t620 = t211 and t615; -t621 = not t618; -t622 = t620 and t621; -t623 = t619 nor t622; -t624 = t216 and t621; -t625 = t220 and t618; -t626 = t624 or t625; -t627 = t480 nor t614; -t628 = not t627; -t629 = t626 or t628; -t630 = t623 and t629; -t1005 = not t630; -t1006 = t1004 nand t1005; -t1007 = not t1004; -t1008 = t630 nand t1007; -t1009 = t1006 nand t1008; -t664 = t514 or t516; -t665 = t546 nand t664; -t666 = t526 or t528; -t667 = not t666; -t668 = t537 or t539; -t669 = t534 nand t668; -t670 = t667 and t669; -t671 = t665 and t670; -t672 = t550 or t552; -t673 = t672 and t545; -t674 = t522 and t673; -t675 = t674 nand t534; -t676 = t671 nand t675; -t786 = t676 and t716; -t1010 = not t786; -t1011 = t1009 nand t1010; -t1012 = not t1009; -t1013 = t786 nand t1012; -t1014 = t1011 nand t1013; -t1015 = not t1014; -t1016 = t785 nand t1015; -t1017 = not t785; -t1018 = t1014 nand t1017; -t1019 = t1016 nand t1018; -t1020 = t1019 and t801; -t1021 = t1019 and t742; -t1022 = t1020 or t1021; -t913 = t10 nand t870; -t914 = not t913; -t1023 = t990 and t914; -t1024 = not t1005; -t1025 = not t1024; -t1026 = t1025 and t993; -t1027 = t1023 or t1026; -t1028 = t913 and t992; -t1029 = t121 and t1028; -t1030 = t1027 nor t1029; -t1031 = t1030 and t900; -t1032 = t1022 nor t1031; -t1033 = not t1032; -t1034 = t1003 biimp t1033; -t4 = not t3; -t430 = t5 nand t4; -t6 = not t5; -t431 = t3 nand t6; -t432 = t430 nand t431; -t1035 = t432 and t36; -t127 = not t2; -t1036 = not t127; -t1037 = t1035 and t1036; -t1038 = t5 and t127; -t1039 = t1037 or t1038; -t1040 = t9 nand t21; -t1041 = not t1040; -t1042 = t1039 and t1041; -t1043 = t48 and t269; -t13 = t11 nand t12; -t14 = not t13; -t1044 = t1043 and t14; -t1045 = t1042 or t1044; -t348 = t6 and t152; -t349 = t36 and t157; -t350 = t348 or t349; -t351 = t2 and t160; -t352 = t350 or t351; -t353 = t352 and t167; -t354 = t5 nor t171; -t355 = t353 or t354; -t357 = t5 and t356; -t358 = t357 and t176; -t359 = t355 or t358; -t1046 = t701 and t359; -t360 = t150 and t359; -t361 = t184 and t27; -t365 = t361 and t364; -t367 = t365 or t366; -t368 = t43 and t198; -t29 = _226; -t369 = t29 and t202; -t370 = t368 or t369; -t371 = t31 and t205; -t372 = t370 or t371; -t373 = t183 and t372; -t374 = t367 or t373; -t375 = t360 and t374; -t376 = t211 and t359; -t377 = not t374; -t378 = t376 and t377; -t379 = t375 nor t378; -t380 = t355 nor t358; -t381 = t216 and t380; -t382 = t381 and t377; -t383 = t220 and t380; -t384 = t383 and t374; -t385 = t382 or t384; -t386 = not t380; -t387 = t385 or t386; -t388 = t379 and t387; -t1047 = not t388; -t1048 = t1046 nand t1047; -t1049 = not t1046; -t1050 = t388 nand t1049; -t1051 = t1048 nand t1050; -t433 = not t432; -t434 = t433 and t152; -t435 = t5 and t157; -t436 = t434 or t435; -t438 = t437 and t160; -t439 = t436 or t438; -t440 = t439 and t167; -t441 = t3 nor t171; -t442 = t440 or t441; -t443 = t3 and t356; -t444 = t443 and t176; -t445 = t442 or t444; -t1052 = t699 and t445; -t446 = t150 and t445; -t447 = t184 and t31; -t448 = t447 and t364; -t449 = t448 or t366; -t450 = t41 and t198; -t411 = _223; -t451 = t411 and t202; -t452 = t450 or t451; -t453 = t29 and t205; -t454 = t452 or t453; -t455 = t183 and t454; -t456 = t449 or t455; -t457 = t446 and t456; -t458 = t211 and t445; -t459 = not t456; -t460 = t458 and t459; -t461 = t457 nor t460; -t462 = t442 nor t444; -t463 = t216 and t462; -t464 = t463 and t459; -t465 = t220 and t462; -t466 = t465 and t456; -t467 = t464 or t466; -t468 = not t462; -t469 = t467 or t468; -t470 = t461 and t469; -t1053 = not t470; -t1054 = t1052 nand t1053; -t1055 = not t1052; -t1056 = t470 nand t1055; -t1057 = t1054 nand t1056; -t1058 = t757 and t1057; -t1059 = t1051 and t1058; -t1060 = t1059 and t943; -t389 = t127 and t4; -t390 = t389 nand t6; -t391 = t390 and t152; -t392 = t3 and t157; -t393 = t391 or t392; -t395 = t394 and t160; -t396 = t393 or t395; -t397 = t396 and t167; -t398 = t2 nor t171; -t399 = t397 or t398; -t400 = t2 and t356; -t401 = t400 and t176; -t402 = t399 or t401; -t403 = t150 and t402; -t404 = t184 and t29; -t405 = t404 and t364; -t406 = t405 or t366; -t407 = t36 and t198; -t408 = _222; -t409 = t408 and t202; -t410 = t407 or t409; -t412 = t411 and t205; -t413 = t410 or t412; -t414 = t183 and t413; -t415 = t406 or t414; -t416 = t403 and t415; -t417 = t211 and t402; -t418 = not t415; -t419 = t417 and t418; -t420 = t416 nor t419; -t421 = t399 nor t401; -t422 = t216 and t421; -t423 = t422 and t418; -t424 = t220 and t421; -t425 = t424 and t415; -t426 = t423 or t425; -t427 = not t421; -t428 = t426 or t427; -t429 = t420 and t428; -t471 = t429 and t470; -t472 = t388 and t471; -t509 = t472 and t508; -t1061 = t757 and t509; -t1062 = not t1061; -t1063 = t1060 nand t1062; -t1064 = not t1060; -t1065 = t1061 nand t1064; -t1066 = t1063 nand t1065; -t1067 = t695 and t1066; -t648 = t375 or t378; -t649 = t471 nand t648; -t650 = t416 or t419; -t651 = not t650; -t652 = t457 or t460; -t653 = t429 nand t652; -t654 = t651 and t653; -t655 = t649 and t654; -t656 = t495 or t498; -t657 = t656 and t470; -t658 = t388 and t657; -t659 = t658 nand t429; -t660 = t655 nand t659; -t1068 = t759 and t509; -t1069 = t660 or t1068; -t1070 = t1057 and t1051; -t1071 = t656 and t716; -t1072 = t1070 nand t1071; -t1073 = t697 nand t698; -t1074 = t652 and t1073; -t1075 = not t1074; -t1076 = t648 and t716; -t1077 = t1057 nand t1076; -t1078 = t1075 and t1077; -t1079 = t1072 and t1078; -t1080 = t943 and t1070; -t1081 = t1080 nand t759; -t1082 = t1079 nand t1081; -t1083 = not t1082; -t1084 = t1069 nand t1083; -t1085 = not t1069; -t1086 = t1082 nand t1085; -t1087 = t1084 nand t1086; -t1088 = not t1087; -t1089 = t1067 nand t1088; -t1090 = not t1067; -t1091 = t1087 nand t1090; -t1092 = t1089 nand t1091; -t1093 = t1040 and t13; -t1094 = t1092 and t1093; -t1095 = t1045 or t1094; -t1096 = t1045 nor t1094; -t1097 = not t1096; -t1098 = t1095 and t1097; -t560 = t357 and t166; -t561 = t355 or t560; -t1099 = t701 and t561; -t562 = t150 and t561; -t564 = t365 or t563; -t565 = t564 or t373; -t566 = t562 and t565; -t567 = t211 and t561; -t568 = not t565; -t569 = t567 and t568; -t570 = t566 nor t569; -t571 = t216 and t568; -t572 = t220 and t565; -t573 = t571 or t572; -t574 = t355 nor t560; -t575 = not t574; -t576 = t573 or t575; -t577 = t570 and t576; -t1100 = not t577; -t1101 = t1099 nand t1100; -t1102 = not t1099; -t1103 = t577 nand t1102; -t1104 = t1101 nand t1103; -t595 = t443 and t166; -t596 = t442 or t595; -t1105 = t699 and t596; -t597 = t150 and t596; -t598 = t448 or t563; -t599 = t598 or t455; -t600 = t597 and t599; -t601 = t211 and t596; -t602 = not t599; -t603 = t601 and t602; -t604 = t600 nor t603; -t605 = t216 and t602; -t606 = t220 and t599; -t607 = t605 or t606; -t608 = t442 nor t595; -t609 = not t608; -t610 = t607 or t609; -t611 = t604 and t610; -t1106 = not t611; -t1107 = t1105 nand t1106; -t1108 = not t1105; -t1109 = t611 nand t1108; -t1110 = t1107 nand t1109; -t1111 = t784 and t1110; -t1112 = t1104 and t1111; -t1113 = t1112 and t1009; -t578 = t400 and t166; -t579 = t399 or t578; -t580 = t150 and t579; -t581 = t405 or t563; -t582 = t581 or t414; -t583 = t580 and t582; -t584 = t211 and t579; -t585 = not t582; -t586 = t584 and t585; -t587 = t583 nor t586; -t588 = t216 and t585; -t589 = t220 and t582; -t590 = t588 or t589; -t591 = t399 nor t578; -t592 = not t591; -t593 = t590 or t592; -t594 = t587 and t593; -t612 = t594 and t611; -t613 = t577 and t612; -t631 = t613 and t630; -t1114 = t784 and t631; -t1115 = not t1114; -t1116 = t1113 nand t1115; -t1117 = not t1113; -t1118 = t1114 nand t1117; -t1119 = t1116 nand t1118; -t1120 = t695 and t1119; -t678 = t566 or t569; -t679 = t612 nand t678; -t680 = t583 or t586; -t681 = not t680; -t682 = t600 or t603; -t683 = t594 nand t682; -t684 = t681 and t683; -t685 = t679 and t684; -t686 = t619 or t622; -t687 = t686 and t611; -t688 = t577 and t687; -t689 = t688 nand t594; -t690 = t685 nand t689; -t1121 = t786 and t631; -t1122 = t690 or t1121; -t1123 = t1110 and t1104; -t1124 = t686 and t716; -t1125 = t1123 nand t1124; -t1126 = t682 and t1073; -t1127 = not t1126; -t1128 = t678 and t716; -t1129 = t1110 nand t1128; -t1130 = t1127 and t1129; -t1131 = t1125 and t1130; -t1132 = t1009 and t1123; -t1133 = t1132 nand t786; -t1134 = t1131 nand t1133; -t1135 = not t1134; -t1136 = t1122 nand t1135; -t1137 = not t1122; -t1138 = t1134 nand t1137; -t1139 = t1136 nand t1138; -t1140 = not t1139; -t1141 = t1120 nand t1140; -t1142 = not t1120; -t1143 = t1139 nand t1142; -t1144 = t1141 nand t1143; -t1145 = t1144 and t1093; -t1146 = t1045 nor t1145; -t1147 = not t1146; -t1148 = t1098 biimp t1147; -t702 = t701 and t320; -t703 = not t346; -t704 = t702 nand t703; -t705 = not t702; -t706 = t346 nand t705; -t707 = t704 nand t706; -t708 = t701 and t178; -t709 = not t226; -t710 = t708 nand t709; -t711 = not t708; -t712 = t226 nand t711; -t713 = t710 nand t712; -t714 = t707 and t713; -t1149 = t701 and t281; -t1150 = not t307; -t1151 = t1149 nand t1150; -t1152 = not t1149; -t1153 = t307 nand t1152; -t1154 = t1151 nand t1153; -t1155 = t714 and t1154; -t1156 = t695 and t1155; -t1157 = t701 and t239; -t1158 = not t266; -t1159 = t1157 nand t1158; -t1160 = not t1157; -t1161 = t266 nand t1160; -t1162 = t1159 nand t1161; -t1163 = t638 and t716; -t1164 = not t1163; -t717 = t634 and t716; -t1165 = t1154 nand t717; -t1166 = t1164 and t1165; -t1167 = t1154 and t713; -t718 = t642 and t716; -t1168 = t1167 nand t718; -t1169 = t1166 nand t1168; -t1170 = not t1169; -t1171 = t1162 nand t1170; -t1172 = not t1162; -t1173 = t1169 nand t1172; -t1174 = t1171 nand t1173; -t1175 = not t1174; -t1176 = t1156 nand t1175; -t1177 = not t1156; -t1178 = t1174 nand t1177; -t1179 = t1176 nand t1178; -t1180 = t1179 and t801; -t1181 = not t1179; -t761 = t758 and t760; -t1182 = t761 nor t759; -t1183 = t1181 nor t1182; -t1184 = t695 and t707; -t1185 = not t718; -t1186 = t713 nand t1185; -t1187 = not t713; -t1188 = t718 nand t1187; -t1189 = t1186 nand t1188; -t1190 = not t1189; -t1191 = t1184 nand t1190; -t1192 = not t1184; -t1193 = t1189 nand t1192; -t1194 = t1191 nand t1193; -t715 = t695 and t714; -t719 = t713 and t718; -t720 = t717 or t719; -t721 = not t720; -t1195 = t1154 nand t721; -t1196 = not t1154; -t1197 = t720 nand t1196; -t1198 = t1195 nand t1197; -t1199 = not t1198; -t1200 = t715 nand t1199; -t1201 = not t715; -t1202 = t1198 nand t1201; -t1203 = t1200 nand t1202; -t1204 = t1194 and t1203; -t1205 = t1179 and t1204; -t1206 = t1205 and t1182; -t1207 = t1183 or t1206; -t1208 = t1207 and t742; -t1209 = t1180 or t1208; -t1210 = t394 and t810; -t1211 = t437 and t815; -t1212 = t2 and t818; -t1213 = t3 and t824; -t1214 = t5 and t829; -t1215 = t971 and t832; -t1216 = t36 and t835; -t1217 = t1215 or t1216; -t1218 = t1214 or t1217; -t1219 = t1213 or t1218; -t1220 = t1212 or t1219; -t1221 = t1211 or t1220; -t1222 = t1210 or t1221; -t1223 = t956 and t844; -t1224 = t1222 nor t1223; -t1225 = t1224 and t155; -t1226 = t325 and t810; -t1227 = t197 and t815; -t1228 = t286 and t818; -t1229 = t48 and t824; -t1230 = t39 and t829; -t850 = _317; -t1231 = t850 and t832; -t1232 = t43 and t835; -t1233 = t1231 or t1232; -t1234 = t1230 or t1233; -t1235 = t1229 or t1234; -t1236 = t1228 or t1235; -t1237 = t1227 or t1236; -t1238 = t1226 or t1237; -t1239 = t852 and t844; -t1240 = t1238 nor t1239; -t1241 = t1240 and t154; -t1242 = t1225 or t1241; -t1243 = t1242 and t872; -t874 = t21 and t151; -t875 = t874 nand t155; -t876 = not t875; -t1244 = t1172 and t876; -t1245 = t1243 or t1244; -t60 = not t18; -t61 = t47 nand t60; -t62 = not t47; -t63 = t18 nand t62; -t64 = t61 nand t63; -t65 = not t16; -t66 = t17 nand t65; -t67 = not t17; -t68 = t16 nand t67; -t69 = t66 nand t68; -t70 = not t69; -t71 = t64 nand t70; -t72 = not t64; -t73 = t69 nand t72; -t74 = t71 nand t73; -t884 = t22 and t12; -t885 = t884 nand t154; -t886 = not t885; -t1246 = t74 and t886; -t890 = t884 nand t155; -t891 = not t890; -t1247 = t1246 or t891; -t894 = t885 and t890; -t1248 = t110 and t894; -t1249 = t1247 or t1248; -t897 = t871 and t875; -t1250 = t1249 and t897; -t1251 = t1245 nor t1250; -t1252 = t1251 and t900; -t1253 = t1209 or t1252; -t1254 = t1209 nor t1252; -t1255 = not t1254; -t1256 = t1253 and t1255; -t724 = not t558; -t725 = t702 nand t724; -t726 = t558 nand t705; -t727 = t725 nand t726; -t728 = not t522; -t729 = t708 nand t728; -t730 = t522 nand t711; -t731 = t729 nand t730; -t732 = t727 and t731; -t1257 = not t545; -t1258 = t1149 nand t1257; -t1259 = t545 nand t1152; -t1260 = t1258 nand t1259; -t1261 = t732 and t1260; -t1262 = t695 and t1261; -t1263 = not t534; -t1264 = t1157 nand t1263; -t1265 = t534 nand t1160; -t1266 = t1264 nand t1265; -t1267 = t668 and t716; -t1268 = not t1267; -t734 = t664 and t716; -t1269 = t1260 nand t734; -t1270 = t1268 and t1269; -t1271 = t1260 and t731; -t735 = t672 and t716; -t1272 = t1271 nand t735; -t1273 = t1270 nand t1272; -t1274 = not t1273; -t1275 = t1266 nand t1274; -t1276 = not t1266; -t1277 = t1273 nand t1276; -t1278 = t1275 nand t1277; -t1279 = not t1278; -t1280 = t1262 nand t1279; -t1281 = not t1262; -t1282 = t1278 nand t1281; -t1283 = t1280 nand t1282; -t1284 = t1283 and t801; -t1285 = not t1283; -t1286 = t785 nor t786; -t1287 = t1285 nor t1286; -t1288 = t695 and t727; -t1289 = not t735; -t1290 = t731 nand t1289; -t1291 = not t731; -t1292 = t735 nand t1291; -t1293 = t1290 nand t1292; -t1294 = not t1293; -t1295 = t1288 nand t1294; -t1296 = not t1288; -t1297 = t1293 nand t1296; -t1298 = t1295 nand t1297; -t733 = t695 and t732; -t736 = t731 and t735; -t737 = t734 or t736; -t1299 = not t737; -t1300 = t1260 nand t1299; -t1301 = not t1260; -t1302 = t737 nand t1301; -t1303 = t1300 nand t1302; -t1304 = not t1303; -t1305 = t733 nand t1304; -t1306 = not t733; -t1307 = t1303 nand t1306; -t1308 = t1305 nand t1307; -t1309 = t1298 and t1308; -t1310 = t1309 and t1283; -t1311 = t1287 or t1310; -t1312 = t1311 and t742; -t1313 = t1284 or t1312; -t1314 = t1242 and t914; -t1315 = not t1263; -t1316 = not t1315; -t1317 = t1316 and t876; -t1318 = t1314 or t1317; -t920 = t21 and t12; -t921 = t920 nand t154; -t922 = not t921; -t1319 = t74 and t922; -t924 = t920 nand t155; -t925 = not t924; -t1320 = t1319 or t925; -t1321 = t110 and t921; -t1322 = t1320 or t1321; -t931 = t913 and t875; -t1323 = t1322 and t931; -t1324 = t1318 nor t1323; -t1325 = t1324 and t900; -t1326 = t1313 nor t1325; -t1327 = not t1326; -t1328 = t1256 biimp t1327; -t1329 = t1194 and t801; -t1330 = not t1194; -t1331 = not t1330; -t1332 = t1182 nand t1331; -t1333 = not t1182; -t1334 = t1330 nand t1333; -t1335 = t1332 nand t1334; -t1336 = not t1335; -t1337 = t1336 and t742; -t1338 = t1329 or t1337; -t1339 = t2 and t810; -t1340 = t3 and t815; -t1341 = t5 and t818; -t1342 = t36 and t824; -t1343 = t41 and t829; -t1344 = t394 and t832; -t1345 = t1344 or t1232; -t1346 = t1343 or t1345; -t1347 = t1342 or t1346; -t1348 = t1341 or t1347; -t1349 = t1340 or t1348; -t1350 = t1339 or t1349; -t1351 = t437 and t844; -t1352 = t1350 nor t1351; -t1353 = t1352 and t155; -t1354 = t850 and t810; -t1355 = t852 and t815; -t1356 = t325 and t818; -t1357 = t197 and t824; -t1358 = t286 and t829; -t865 = _326; -t1359 = t865 and t832; -t1360 = t48 and t835; -t1361 = t1359 or t1360; -t1362 = t1358 or t1361; -t1363 = t1357 or t1362; -t1364 = t1356 or t1363; -t1365 = t1355 or t1364; -t1366 = t1354 or t1365; -t848 = _322; -t1367 = t848 and t844; -t1368 = t1366 nor t1367; -t1369 = t1368 and t154; -t1370 = t1353 or t1369; -t1371 = t1370 and t872; -t1372 = t1187 and t876; -t1373 = t1371 or t1372; -t75 = not t27; -t76 = t35 nand t75; -t77 = not t35; -t78 = t27 nand t77; -t79 = t76 nand t78; -t80 = not t29; -t81 = t31 nand t80; -t82 = not t31; -t83 = t29 nand t82; -t84 = t81 nand t83; -t85 = not t84; -t86 = t79 nand t85; -t87 = not t79; -t88 = t84 nand t87; -t89 = t86 nand t88; -t90 = not t89; -t879 = not t187; -t880 = not t879; -t1374 = t90 and t880; -t102 = not t48; -t765 = t227 and t103; -t766 = t102 and t765; -t1375 = t5 nand t36; -t1376 = t766 and t1375; -t1377 = t127 and t1376; -t1378 = t1377 and t3; -t1379 = t1378 and t879; -t1380 = t1374 nor t1379; -t1381 = t1380 and t886; -t1382 = t102 nand t765; -t1383 = t1382 and t891; -t1384 = t1381 or t1383; -t1385 = t103 and t894; -t1386 = t1384 or t1385; -t1387 = t1386 and t897; -t1388 = t1373 nor t1387; -t1389 = t1388 and t900; -t1390 = t1338 or t1389; -t1391 = t1338 nor t1389; -t1392 = not t1391; -t1393 = t1390 and t1392; -t1394 = t1298 and t801; -t1395 = not t1298; -t1396 = not t1395; -t1397 = t1286 nand t1396; -t1398 = not t1286; -t1399 = t1395 nand t1398; -t1400 = t1397 nand t1399; -t1401 = not t1400; -t1402 = t1401 and t742; -t1403 = t1394 or t1402; -t1404 = t1370 and t914; -t1405 = not t728; -t1406 = not t1405; -t1407 = t1406 and t876; -t1408 = t1404 or t1407; -t1409 = t1380 and t922; -t1410 = t1382 and t925; -t1411 = t1409 or t1410; -t928 = t921 and t924; -t1412 = t103 and t928; -t1413 = t1411 or t1412; -t1414 = t1413 and t931; -t1415 = t1408 nor t1414; -t1416 = t1415 and t900; -t1417 = t1403 nor t1416; -t1418 = not t1417; -t1419 = t1393 biimp t1418; -t1420 = t1203 and t801; -t1421 = t1194 and t1182; -t1422 = not t1203; -t1423 = t1421 nand t1422; -t1424 = not t1421; -t1425 = t1203 nand t1424; -t1426 = t1423 nand t1425; -t1427 = t1426 and t742; -t1428 = t1420 or t1427; -t1429 = t437 and t810; -t1430 = t2 and t815; -t1431 = t3 and t818; -t1432 = t5 and t824; -t1433 = t36 and t829; -t1434 = t956 and t832; -t1435 = t1434 or t980; -t1436 = t1433 or t1435; -t1437 = t1432 or t1436; -t1438 = t1431 or t1437; -t1439 = t1430 or t1438; -t1440 = t1429 or t1439; -t1441 = t394 and t844; -t1442 = t1440 nor t1441; -t1443 = t1442 and t155; -t1444 = t852 and t810; -t1445 = t325 and t815; -t1446 = t197 and t818; -t1447 = t286 and t824; -t1448 = t48 and t829; -t1449 = t848 and t832; -t836 = t39 and t835; -t1450 = t1449 or t836; -t1451 = t1448 or t1450; -t1452 = t1447 or t1451; -t1453 = t1446 or t1452; -t1454 = t1445 or t1453; -t1455 = t1444 or t1454; -t1456 = t850 and t844; -t1457 = t1455 nor t1456; -t1458 = t1457 and t154; -t1459 = t1443 or t1458; -t1460 = t1459 and t872; -t1461 = t1196 and t876; -t1462 = t1460 or t1461; -t104 = not t103; -t105 = t102 nand t104; -t106 = not t102; -t107 = t103 nand t106; -t108 = t105 nand t107; -t111 = not t110; -t112 = t109 nand t111; -t113 = not t109; -t114 = t110 nand t113; -t115 = t112 nand t114; -t116 = not t115; -t117 = t108 nand t116; -t118 = not t108; -t119 = t115 nand t118; -t120 = t117 nand t119; -t1463 = t120 and t886; -t1464 = t1463 or t891; -t1465 = t109 and t894; -t1466 = t1464 or t1465; -t1467 = t1466 and t897; -t1468 = t1462 nor t1467; -t1469 = t1468 and t900; -t1470 = t1428 or t1469; -t1471 = t1428 nor t1469; -t1472 = not t1471; -t1473 = t1470 and t1472; -t1474 = t1308 and t801; -t1475 = t1298 and t1286; -t1476 = not t1308; -t1477 = t1475 nand t1476; -t1478 = not t1475; -t1479 = t1308 nand t1478; -t1480 = t1477 nand t1479; -t1481 = t1480 and t742; -t1482 = t1474 or t1481; -t1483 = t1459 and t914; -t1484 = not t1257; -t1485 = not t1484; -t1486 = t1485 and t876; -t1487 = t1483 or t1486; -t1488 = t120 and t922; -t1489 = t1488 or t925; -t1490 = t109 and t921; -t1491 = t1489 or t1490; -t1492 = t1491 and t931; -t1493 = t1487 nor t1492; -t1494 = t1493 and t900; -t1495 = t1482 nor t1494; -t1496 = not t1495; -t1497 = t1473 biimp t1496; -t1498 = t757 and t943; -t1499 = t1498 and t1051; -t1500 = t695 and t1499; -t1501 = not t1076; -t1502 = t1051 nand t1071; -t1503 = t1501 and t1502; -t1504 = t1051 and t943; -t1505 = t1504 nand t759; -t1506 = t1503 nand t1505; -t1507 = not t1506; -t1508 = t1057 nand t1507; -t1509 = not t1057; -t1510 = t1506 nand t1509; -t1511 = t1508 nand t1510; -t1512 = not t1511; -t1513 = t1500 nand t1512; -t1514 = not t1500; -t1515 = t1511 nand t1514; -t1516 = t1513 nand t1515; -t1517 = t1516 and t801; -t1518 = t695 and t1498; -t1519 = t759 and t943; -t1520 = t1071 or t1519; -t1521 = not t1520; -t1522 = t1051 nand t1521; -t1523 = not t1051; -t1524 = t1520 nand t1523; -t1525 = t1522 nand t1524; -t1526 = not t1525; -t1527 = t1518 nand t1526; -t1528 = not t1518; -t1529 = t1525 nand t1528; -t1530 = t1527 nand t1529; -t1531 = t695 and t1061; -t1532 = t1531 and t1085; -t1533 = t1532 nor t1069; -t1534 = t1530 and t1533; -t1535 = not t1516; -t1536 = t1534 nand t1535; -t1537 = not t1534; -t1538 = t1516 nand t1537; -t1539 = t1536 nand t1538; -t1540 = t1539 and t742; -t1541 = t1517 or t1540; -t1542 = t962 and t810; -t1543 = t971 and t815; -t1544 = t956 and t818; -t1545 = t394 and t824; -t1546 = t437 and t829; -t1547 = _125; -t1548 = t1547 and t832; -t1549 = t2 and t835; -t1550 = t1548 or t1549; -t1551 = t1546 or t1550; -t1552 = t1545 or t1551; -t1553 = t1544 or t1552; -t1554 = t1543 or t1553; -t1555 = t1542 or t1554; -t1556 = _128; -t1557 = t1556 and t844; -t1558 = t1555 nor t1557; -t1559 = t1558 and t155; -t1560 = t48 and t810; -t1561 = t39 and t815; -t1562 = t43 and t818; -t825 = t41 and t824; -t1563 = t197 and t832; -t1564 = t1563 or t964; -t1565 = t1433 or t1564; -t1566 = t825 or t1565; -t1567 = t1562 or t1566; -t1568 = t1561 or t1567; -t1569 = t1560 or t1568; -t1570 = t286 and t844; -t1571 = t1569 nor t1570; -t1572 = t1571 and t154; -t1573 = t1559 or t1572; -t1574 = t1573 and t872; -t1575 = t1509 and t993; -t1576 = t1574 or t1575; -t1577 = t4 and t996; -t1578 = t1576 nor t1577; -t1579 = t1578 and t900; -t1580 = t1541 or t1579; -t1581 = t784 and t1009; -t1582 = t1581 and t1104; -t1583 = t695 and t1582; -t1584 = not t1128; -t1585 = t1104 nand t1124; -t1586 = t1584 and t1585; -t1587 = t1104 and t1009; -t1588 = t1587 nand t786; -t1589 = t1586 nand t1588; -t1590 = not t1589; -t1591 = t1110 nand t1590; -t1592 = not t1110; -t1593 = t1589 nand t1592; -t1594 = t1591 nand t1593; -t1595 = not t1594; -t1596 = t1583 nand t1595; -t1597 = not t1583; -t1598 = t1594 nand t1597; -t1599 = t1596 nand t1598; -t1600 = t1599 and t801; -t1601 = t695 and t1581; -t1602 = t786 and t1009; -t1603 = t1124 or t1602; -t1604 = not t1603; -t1605 = t1104 nand t1604; -t1606 = not t1104; -t1607 = t1603 nand t1606; -t1608 = t1605 nand t1607; -t1609 = not t1608; -t1610 = t1601 nand t1609; -t1611 = not t1601; -t1612 = t1608 nand t1611; -t1613 = t1610 nand t1612; -t1614 = t695 and t1114; -t1615 = t1614 nor t1122; -t1616 = t1613 and t1615; -t1617 = not t1599; -t1618 = t1616 nand t1617; -t1619 = not t1616; -t1620 = t1599 nand t1619; -t1621 = t1618 nand t1620; -t1622 = t1621 and t742; -t1623 = t1600 or t1622; -t1624 = t1573 and t914; -t1625 = not t1106; -t1626 = not t1625; -t1627 = t1626 and t993; -t1628 = t1624 or t1627; -t1629 = t4 and t1028; -t1630 = t1628 nor t1629; -t1631 = t1630 and t900; -t1632 = t1623 or t1631; -t1633 = t1580 biimp t1632; -t1634 = t695 and t1060; -t1635 = t699 and t402; -t1636 = not t429; -t1637 = t1635 nand t1636; -t1638 = not t1635; -t1639 = t429 nand t1638; -t1640 = t1637 nand t1639; -t1641 = t1640 nand t1083; -t1642 = not t1640; -t1643 = t1082 nand t1642; -t1644 = t1641 nand t1643; -t1645 = not t1644; -t1646 = t1634 nand t1645; -t1647 = not t1634; -t1648 = t1644 nand t1647; -t1649 = t1646 nand t1648; -t1650 = t1649 and t801; -t1651 = not t1649; -t1652 = t1651 nor t1533; -t1653 = t1530 and t1516; -t1654 = t1649 and t1653; -t1655 = t1654 and t1533; -t1656 = t1652 or t1655; -t1657 = t1656 and t742; -t1658 = t1650 or t1657; -t1659 = t1556 and t810; -t1660 = t962 and t815; -t1661 = t971 and t818; -t1662 = t956 and t824; -t1663 = t394 and t829; -t1664 = _124; -t1665 = t1664 and t832; -t1666 = t437 and t835; -t1667 = t1665 or t1666; -t1668 = t1663 or t1667; -t1669 = t1662 or t1668; -t1670 = t1661 or t1669; -t1671 = t1660 or t1670; -t1672 = t1659 or t1671; -t1673 = t1547 and t844; -t1674 = t1672 nor t1673; -t1675 = t155 nand t189; -t1676 = not t1675; -t1677 = t1674 and t1676; -t1678 = t39 and t810; -t1679 = t43 and t815; -t1680 = t41 and t818; -t1681 = t286 and t832; -t1682 = t3 and t835; -t1683 = t1681 or t1682; -t1684 = t1214 or t1683; -t1685 = t1342 or t1684; -t1686 = t1680 or t1685; -t1687 = t1679 or t1686; -t1688 = t1678 or t1687; -t1689 = t48 and t844; -t1690 = t1688 nor t1689; -t1691 = t154 nand t189; -t1692 = not t1691; -t1693 = t1690 and t1692; -t1694 = t1677 or t1693; -t1695 = t1675 and t1691; -t1696 = t127 and t1695; -t1697 = t1694 or t1696; -t1698 = t1697 and t872; -t1699 = t1642 and t993; -t1700 = t1698 or t1699; -t1701 = t127 and t996; -t1702 = t1700 nor t1701; -t1703 = t1702 and t900; -t1704 = t1658 or t1703; -t1705 = t695 and t1113; -t1706 = t699 and t579; -t1707 = not t594; -t1708 = t1706 nand t1707; -t1709 = not t1706; -t1710 = t594 nand t1709; -t1711 = t1708 nand t1710; -t1712 = t1711 nand t1135; -t1713 = not t1711; -t1714 = t1134 nand t1713; -t1715 = t1712 nand t1714; -t1716 = not t1715; -t1717 = t1705 nand t1716; -t1718 = not t1705; -t1719 = t1715 nand t1718; -t1720 = t1717 nand t1719; -t1721 = t1720 and t801; -t1722 = not t1720; -t1723 = t1722 nor t1615; -t1724 = t1613 and t1599; -t1725 = t1724 and t1720; -t1726 = t1723 or t1725; -t1727 = t1726 and t742; -t1728 = t1721 or t1727; -t1729 = t1697 and t914; -t1730 = not t1707; -t1731 = not t1730; -t1732 = t1731 and t993; -t1733 = t1729 or t1732; -t1734 = t127 and t1028; -t1735 = t1733 nor t1734; -t1736 = t1735 and t900; -t1737 = t1728 or t1736; -t1738 = t1704 biimp t1737; -t1739 = t1530 and t801; -t1740 = not t1530; -t1741 = not t1740; -t1742 = t1533 nand t1741; -t1743 = not t1533; -t1744 = t1740 nand t1743; -t1745 = t1742 nand t1744; -t1746 = not t1745; -t1747 = t1746 and t742; -t1748 = t1739 or t1747; -t1749 = t971 and t810; -t1750 = t956 and t815; -t1751 = t394 and t818; -t1752 = t437 and t824; -t1753 = t2 and t829; -t1754 = t1556 and t832; -t1755 = t1754 or t1682; -t1756 = t1753 or t1755; -t1757 = t1752 or t1756; -t1758 = t1751 or t1757; -t1759 = t1750 or t1758; -t1760 = t1749 or t1759; -t1761 = t962 and t844; -t1762 = t1760 nor t1761; -t1763 = t1762 and t155; -t1764 = t286 and t810; -t1765 = t48 and t815; -t1766 = t39 and t818; -t1767 = t43 and t824; -t1768 = t325 and t832; -t1769 = t1768 or t1216; -t1770 = t1343 or t1769; -t1771 = t1767 or t1770; -t1772 = t1766 or t1771; -t1773 = t1765 or t1772; -t1774 = t1764 or t1773; -t1775 = t197 and t844; -t1776 = t1774 nor t1775; -t1777 = t1776 and t154; -t1778 = t1763 or t1777; -t1779 = t1778 and t872; -t1780 = t1523 and t993; -t1781 = t1779 or t1780; -t1782 = t6 and t996; -t1783 = t1781 nor t1782; -t1784 = t1783 and t900; -t1785 = t1748 or t1784; -t1786 = t1748 nor t1784; -t1787 = not t1786; -t1788 = t1785 and t1787; -t1789 = t1613 and t801; -t1790 = not t1613; -t1791 = not t1790; -t1792 = t1615 nand t1791; -t1793 = not t1615; -t1794 = t1790 nand t1793; -t1795 = t1792 nand t1794; -t1796 = not t1795; -t1797 = t1796 and t742; -t1798 = t1789 or t1797; -t1799 = t1778 and t914; -t1800 = not t1100; -t1801 = not t1800; -t1802 = t1801 and t993; -t1803 = t1799 or t1802; -t1804 = t6 and t1028; -t1805 = t1803 nor t1804; -t1806 = t1805 and t900; -t1807 = t1798 nor t1806; -t1808 = not t1807; -t1809 = t1788 biimp t1808; -t793 = not t695; -t794 = t707 nand t793; -t795 = not t707; -t796 = t695 nand t795; -t797 = t794 nand t796; -t802 = t797 and t801; -t803 = t797 and t742; -t804 = t802 or t803; -t811 = t3 and t810; -t816 = t5 and t815; -t819 = t36 and t818; -t833 = t437 and t832; -t837 = t833 or t836; -t838 = t830 or t837; -t839 = t825 or t838; -t840 = t819 or t839; -t841 = t816 or t840; -t842 = t811 or t841; -t845 = t2 and t844; -t846 = t842 nor t845; -t847 = t846 and t155; -t849 = t848 and t810; -t851 = t850 and t815; -t853 = t852 and t818; -t854 = t325 and t824; -t855 = t197 and t829; -t856 = _329; -t857 = t856 and t832; -t858 = t286 and t835; -t859 = t857 or t858; -t860 = t855 or t859; -t861 = t854 or t860; -t862 = t853 or t861; -t863 = t851 or t862; -t864 = t849 or t863; -t866 = t865 and t844; -t867 = t864 nor t866; -t868 = t867 and t154; -t869 = t847 or t868; -t873 = t869 and t872; -t877 = t795 and t876; -t878 = t873 or t877; -t122 = not t6; -t123 = t121 nand t122; -t124 = not t121; -t125 = t6 nand t124; -t126 = t123 nand t125; -t128 = t4 nand t127; -t129 = not t4; -t130 = t2 nand t129; -t131 = t128 nand t130; -t132 = not t131; -t133 = t126 nand t132; -t134 = not t126; -t135 = t131 nand t134; -t136 = t133 nand t135; -t881 = t136 and t880; -t7 = t4 nand t6; -t8 = t2 and t7; -t882 = t8 and t879; -t883 = t881 nor t882; -t887 = t883 and t886; -t888 = t109 nand t103; -t889 = t41 nand t888; -t892 = t889 and t891; -t893 = t887 or t892; -t895 = t102 and t894; -t896 = t893 or t895; -t898 = t896 and t897; -t899 = t878 nor t898; -t901 = t899 and t900; -t903 = t804 nor t901; -t1810 = t903 and t1391; -t1811 = t1471 and t1810; -t1812 = t1811 and t1254; -t1813 = t1541 nor t1579; -t1814 = t1001 and t1786; -t1815 = t1813 and t1814; -t1816 = t1658 nor t1703; -t1817 = t1815 and t1816; -t1818 = t1812 and t1817; -t1819 = not t1818; -t906 = t727 nand t793; -t907 = not t727; -t908 = t695 nand t907; -t909 = t906 nand t908; -t910 = t909 and t801; -t911 = t909 and t742; -t912 = t910 or t911; -t915 = t869 and t914; -t916 = not t724; -t917 = not t916; -t918 = t917 and t876; -t919 = t915 or t918; -t923 = t883 and t922; -t926 = t889 and t925; -t927 = t923 or t926; -t929 = t102 and t928; -t930 = t927 or t929; -t932 = t930 and t931; -t933 = t919 nor t932; -t934 = t933 and t900; -t935 = t912 nor t934; -t1820 = t935 and t1417; -t1821 = t1495 and t1820; -t1822 = t1821 and t1326; -t1823 = t1623 nor t1631; -t1824 = t1032 and t1807; -t1825 = t1823 and t1824; -t1826 = t1728 nor t1736; -t1827 = t1825 and t1826; -t1828 = t1822 and t1827; -t1829 = not t1828; -t1830 = t1819 biimp t1829; -t1831 = t1813 and t1816; -t1832 = not t698; -t1833 = t1832 nor t700; -t1834 = t1831 and t1833; -t1835 = t1834 nor t1818; -t1836 = t698 and t1835; -t1837 = not t1836; -t1838 = t1823 and t1826; -t1839 = t1838 and t1833; -t1840 = t1839 nor t1828; -t1841 = t698 and t1840; -t1842 = not t1841; -t1843 = t1837 biimp t1842; -t15 = t8 and t14; -t19 = t17 or t18; -t20 = t16 and t19; -t23 = t22 nand t12; -t24 = not t23; -t25 = t20 and t24; -t26 = t15 or t25; -t28 = t27 nand t5; -t30 = t29 nand t2; -t32 = t31 nand t3; -t33 = t30 and t32; -t34 = t28 and t33; -t37 = t35 nand t36; -t38 = t34 and t37; -t40 = t18 nand t39; -t42 = t16 nand t41; -t44 = t17 nand t43; -t45 = t42 and t44; -t46 = t40 and t45; -t49 = t47 nand t48; -t50 = t46 and t49; -t51 = t38 nand t50; -t52 = t13 and t23; -t53 = t51 and t52; -t54 = t26 or t53; -t55 = t26 nor t53; -t56 = not t55; -t57 = t54 nand t56; -t58 = not t56; -t59 = t57 biimp t58; -t1844 = not t1470; -t1845 = t1253 nand t1844; -t1846 = not t1253; -t1847 = t1470 nand t1846; -t1848 = t1845 nand t1847; -t902 = t804 or t901; -t1849 = not t902; -t1850 = t1390 nand t1849; -t1851 = not t1390; -t1852 = t902 nand t1851; -t1853 = t1850 nand t1852; -t1854 = not t1853; -t1855 = t1848 nand t1854; -t1856 = not t1848; -t1857 = t1853 nand t1856; -t1858 = t1855 nand t1857; -t1859 = not t1858; -t1860 = not t1000; -t1861 = t1785 nand t1860; -t1862 = not t1785; -t1863 = t1000 nand t1862; -t1864 = t1861 nand t1863; -t1865 = not t1864; -t1866 = t1832 or t700; -t1867 = t1580 and t1866; -t1868 = t1866 and t1704; -t1869 = not t1868; -t1870 = t1867 nand t1869; -t1871 = not t1867; -t1872 = t1868 nand t1871; -t1873 = t1870 nand t1872; -t1874 = t1865 and t1873; -t1875 = _2897; -t1876 = t1833 nand t1875; -t1877 = t1874 and t1876; -t1878 = t1864 and t1873; -t1879 = t1833 and t1875; -t1880 = t1878 and t1879; -t1881 = not t1873; -t1882 = t1864 and t1881; -t1883 = t1882 and t1876; -t1884 = t1880 or t1883; -t1885 = t1877 or t1884; -t1886 = t1865 and t1881; -t1887 = t1886 and t1879; -t1888 = t1885 or t1887; -t1889 = not t1888; -t1890 = t1859 nand t1889; -t1891 = not t1859; -t1892 = t1888 nand t1891; -t1893 = t1890 nand t1892; -t1894 = t1798 or t1806; -t1895 = t1022 or t1031; -t1896 = not t1895; -t1897 = t1894 nand t1896; -t1898 = not t1894; -t1899 = t1895 nand t1898; -t1900 = t1897 nand t1899; -t1901 = t1632 and t1866; -t1902 = t1866 and t1737; -t1903 = not t1902; -t1904 = t1901 nand t1903; -t1905 = not t1901; -t1906 = t1902 nand t1905; -t1907 = t1904 nand t1906; -t1908 = not t1907; -t1909 = t1900 and t1908; -t1910 = t1909 and t1876; -t1911 = not t1900; -t1912 = t1911 and t1907; -t1913 = t1910 or t1912; -t1914 = t1911 and t1879; -t1915 = t1913 or t1914; -t1916 = not t1915; -t1917 = not t1916; -t1918 = t1313 or t1325; -t1919 = t1482 or t1494; -t1920 = not t1919; -t1921 = t1918 nand t1920; -t1922 = not t1918; -t1923 = t1919 nand t1922; -t1924 = t1921 nand t1923; -t1925 = t1403 or t1416; -t1926 = t912 or t934; -t1927 = not t1926; -t1928 = t1925 nand t1927; -t1929 = not t1925; -t1930 = t1926 nand t1929; -t1931 = t1928 nand t1930; -t1932 = not t1931; -t1933 = t1924 nand t1932; -t1934 = not t1924; -t1935 = t1931 nand t1934; -t1936 = t1933 nand t1935; -t1937 = not t1936; -t1938 = not t1937; -t1939 = not t1938; -t1940 = t1917 nand t1939; -t1941 = t1938 nand t1916; -t1942 = t1940 and t1941; -t1943 = t1893 biimp t1942; -t1944 = not t1580; -t1945 = t1704 nand t1944; -t1946 = not t1704; -t1947 = t1580 nand t1946; -t1948 = t1945 nand t1947; -t1949 = t1948 nand t1865; -t1950 = not t1948; -t1951 = t1864 nand t1950; -t1952 = t1949 nand t1951; -t1953 = t1952 nand t1859; -t1954 = not t1952; -t1955 = t1858 nand t1954; -t1956 = t1953 nand t1955; -t1957 = not t1956; -t1958 = not t1632; -t1959 = t1737 nand t1958; -t1960 = not t1737; -t1961 = t1632 nand t1960; -t1962 = t1959 nand t1961; -t1963 = t1962 nand t1911; -t1964 = not t1962; -t1965 = t1900 nand t1964; -t1966 = t1963 nand t1965; -t1967 = not t1966; -t1968 = not t1967; -t1969 = t1938 nand t1968; -t1970 = t1967 nand t1937; -t1971 = t1969 nand t1970; -t1972 = t1957 biimp t1971; -t91 = t74 nand t90; -t92 = not t74; -t93 = t89 nand t92; -t94 = t91 nand t93; -t95 = not t94; -t96 = not t90; -t97 = not t92; -t98 = t96 nand t97; -t99 = t92 nand t90; -t100 = t98 nand t99; -t101 = t95 biimp t100; -t137 = not t136; -t138 = t120 nand t137; -t139 = not t120; -t140 = t136 nand t139; -t141 = t138 nand t140; -t142 = not t141; -t143 = not t142; -t144 = not t140; -t145 = not t144; -t146 = not t138; -t147 = not t146; -t148 = t145 nand t147; -t149 = t143 biimp t148; -t510 = t347 and t509; -t632 = t559 and t631; -t633 = t510 biimp t632; -t647 = t509 nand t646; -t661 = not t660; -t662 = t647 and t661; -t663 = not t662; -t677 = t631 nand t676; -t691 = not t690; -t692 = t677 and t691; -t693 = not t692; -t694 = t663 biimp t693; -t722 = t715 and t721; -t723 = t722 or t720; -t738 = t733 or t737; -t739 = t723 biimp t738; -t743 = t8 and t742; -t762 = t761 or t759; -t763 = t762 and t186; -t764 = t743 or t763; -t767 = t741 and t9; -t768 = t766 and t767; -t769 = t764 or t768; -t770 = t764 nor t768; -t771 = not t770; -t772 = t769 and t771; -t787 = t785 or t786; -t788 = t787 and t186; -t789 = t743 or t788; -t790 = t789 nor t768; -t791 = not t790; -t792 = t772 biimp t791; -t904 = not t903; -t905 = t902 and t904; -t936 = not t935; -t937 = t905 biimp t936; - -tautology t1034; -tautology t1148; -tautology t1328; -tautology t1419; -tautology t1497; -tautology t1633; -tautology t1738; -tautology t1809; -tautology t1830; -tautology t1843; -tautology t59; -tautology t1943; -tautology t1972; -tautology t101; -tautology t149; -tautology t633; -tautology t694; -tautology t739; -tautology t792; -tautology t937; diff --git a/buddy/examples/calculator/examples/c432.cal b/buddy/examples/calculator/examples/c432.cal deleted file mode 100644 index 60db3370e..000000000 --- a/buddy/examples/calculator/examples/c432.cal +++ /dev/null @@ -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; diff --git a/buddy/examples/calculator/examples/c499.cal b/buddy/examples/calculator/examples/c499.cal deleted file mode 100644 index 7982182d3..000000000 --- a/buddy/examples/calculator/examples/c499.cal +++ /dev/null @@ -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; diff --git a/buddy/examples/calculator/hashtbl.cxx b/buddy/examples/calculator/hashtbl.cxx deleted file mode 100644 index 7a7965499..000000000 --- a/buddy/examples/calculator/hashtbl.cxx +++ /dev/null @@ -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 - -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 */ diff --git a/buddy/examples/calculator/lexer.lxx b/buddy/examples/calculator/lexer.lxx deleted file mode 100644 index 0049dd6c8..000000000 --- a/buddy/examples/calculator/lexer.lxx +++ /dev/null @@ -1,101 +0,0 @@ -/************************************************************************* - FILE: lexer.l - DESCR: FLEX rules for BDD calculator - AUTH: Jorn Lind - DATE: (C) may 1999 -*************************************************************************/ -%{ -#include -#include -#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; -[^*\n]* /* ignore */ -"*"[^*/\n]* /* ignore */ -\n { linenum++; } -"*/" BEGIN INITIAL; - -. { yyerror("Unknown symbol"); } diff --git a/buddy/examples/calculator/parser.h b/buddy/examples/calculator/parser.h deleted file mode 100644 index 25e3eb302..000000000 --- a/buddy/examples/calculator/parser.h +++ /dev/null @@ -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; - - - diff --git a/buddy/examples/calculator/parser.yxx b/buddy/examples/calculator/parser.yxx deleted file mode 100644 index 3f814c761..000000000 --- a/buddy/examples/calculator/parser.yxx +++ /dev/null @@ -1,459 +0,0 @@ -/************************************************************************* - FILE: parser.y - DESCR: BISON rules and main program for BDD calculator - AUTH: Jorn Lind - DATE: (C) may 1999 -*************************************************************************/ - -%{ -#include -#include -#include -#include -#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 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 */ diff --git a/buddy/examples/calculator/parser_.h b/buddy/examples/calculator/parser_.h deleted file mode 100644 index 7b59b0067..000000000 --- a/buddy/examples/calculator/parser_.h +++ /dev/null @@ -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 -#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 */ diff --git a/buddy/examples/calculator/readme b/buddy/examples/calculator/readme deleted file mode 100644 index b281b90d3..000000000 --- a/buddy/examples/calculator/readme +++ /dev/null @@ -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. - diff --git a/buddy/examples/calculator/slist.h b/buddy/examples/calculator/slist.h deleted file mode 100644 index 37b3199c0..000000000 --- a/buddy/examples/calculator/slist.h +++ /dev/null @@ -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 - - -/* === 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 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; - }; - - ~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 &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 -void SList::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 */ diff --git a/buddy/examples/internal/Makefile.am b/buddy/examples/internal/Makefile.am deleted file mode 100644 index eb8820a5d..000000000 --- a/buddy/examples/internal/Makefile.am +++ /dev/null @@ -1,3 +0,0 @@ -include ../Makefile.def -check_PROGRAMS = bddtest -bddtest_SOURCES = bddtest.cxx diff --git a/buddy/examples/internal/bddtest.cxx b/buddy/examples/internal/bddtest.cxx deleted file mode 100644 index 1400cb214..000000000 --- a/buddy/examples/internal/bddtest.cxx +++ /dev/null @@ -1,145 +0,0 @@ -#include -#include -#include -#include -using namespace std; - -static const int varnum = 5; - -/************************************************************************** - Example of allsat print handler. -**************************************************************************/ - -void allsatHandlerPrint(char* varset, int size) -{ - for (int v=0; v