From 805b6fb70b6a8051fe016cf2b49683c1aaa28690 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Jun 2004 14:19:59 +0000 Subject: [PATCH] Initial revision --- buddy/examples/bddcalc/example.cal | 10 + buddy/examples/bddcalc/examples/c1355.cal | 818 +++++++++ buddy/examples/bddcalc/examples/c1908.cal | 531 ++++++ buddy/examples/bddcalc/examples/c2670.cal | 1237 +++++++++++++ buddy/examples/bddcalc/examples/c3540.cal | 2007 +++++++++++++++++++++ buddy/examples/bddcalc/examples/c432.cal | 260 +++ buddy/examples/bddcalc/examples/c499.cal | 409 +++++ buddy/examples/bddcalc/examples/readme | 3 + buddy/examples/bddcalc/hashtbl.cxx | 174 ++ buddy/examples/bddcalc/hashtbl.h | 56 + buddy/examples/bddcalc/lexer.l | 101 ++ buddy/examples/bddcalc/makefile | 45 + buddy/examples/bddcalc/parser.h | 44 + buddy/examples/bddcalc/parser.hxx | 118 ++ buddy/examples/bddcalc/parser.y | 463 +++++ buddy/examples/bddcalc/readme | 99 + buddy/examples/bddcalc/slist.h | 235 +++ buddy/examples/bddcalc/tokens.h | 39 + buddy/examples/bddtest/bddtest.cxx | 145 ++ buddy/examples/bddtest/makefile | 38 + buddy/examples/cmilner/cmilner.c | 292 +++ buddy/examples/fdd/fdd.cxx | 78 + 22 files changed, 7202 insertions(+) create mode 100644 buddy/examples/bddcalc/example.cal create mode 100644 buddy/examples/bddcalc/examples/c1355.cal create mode 100644 buddy/examples/bddcalc/examples/c1908.cal create mode 100644 buddy/examples/bddcalc/examples/c2670.cal create mode 100644 buddy/examples/bddcalc/examples/c3540.cal create mode 100644 buddy/examples/bddcalc/examples/c432.cal create mode 100644 buddy/examples/bddcalc/examples/c499.cal create mode 100644 buddy/examples/bddcalc/examples/readme create mode 100644 buddy/examples/bddcalc/hashtbl.cxx create mode 100644 buddy/examples/bddcalc/hashtbl.h create mode 100644 buddy/examples/bddcalc/lexer.l create mode 100644 buddy/examples/bddcalc/makefile create mode 100644 buddy/examples/bddcalc/parser.h create mode 100644 buddy/examples/bddcalc/parser.hxx create mode 100644 buddy/examples/bddcalc/parser.y create mode 100644 buddy/examples/bddcalc/readme create mode 100644 buddy/examples/bddcalc/slist.h create mode 100644 buddy/examples/bddcalc/tokens.h create mode 100644 buddy/examples/bddtest/bddtest.cxx create mode 100644 buddy/examples/bddtest/makefile create mode 100644 buddy/examples/cmilner/cmilner.c create mode 100644 buddy/examples/fdd/fdd.cxx diff --git a/buddy/examples/bddcalc/example.cal b/buddy/examples/bddcalc/example.cal new file mode 100644 index 000000000..cc79b79ba --- /dev/null +++ b/buddy/examples/bddcalc/example.cal @@ -0,0 +1,10 @@ +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/bddcalc/examples/c1355.cal b/buddy/examples/bddcalc/examples/c1355.cal new file mode 100644 index 000000000..2a665cab9 --- /dev/null +++ b/buddy/examples/bddcalc/examples/c1355.cal @@ -0,0 +1,818 @@ +/* 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/bddcalc/examples/c1908.cal b/buddy/examples/bddcalc/examples/c1908.cal new file mode 100644 index 000000000..91f2368f0 --- /dev/null +++ b/buddy/examples/bddcalc/examples/c1908.cal @@ -0,0 +1,531 @@ +/* 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/bddcalc/examples/c2670.cal b/buddy/examples/bddcalc/examples/c2670.cal new file mode 100644 index 000000000..0ea2dbe5c --- /dev/null +++ b/buddy/examples/bddcalc/examples/c2670.cal @@ -0,0 +1,1237 @@ +/* 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/bddcalc/examples/c3540.cal b/buddy/examples/bddcalc/examples/c3540.cal new file mode 100644 index 000000000..09ffb757e --- /dev/null +++ b/buddy/examples/bddcalc/examples/c3540.cal @@ -0,0 +1,2007 @@ +/* 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/bddcalc/examples/c432.cal b/buddy/examples/bddcalc/examples/c432.cal new file mode 100644 index 000000000..60db3370e --- /dev/null +++ b/buddy/examples/bddcalc/examples/c432.cal @@ -0,0 +1,260 @@ +/* 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/bddcalc/examples/c499.cal b/buddy/examples/bddcalc/examples/c499.cal new file mode 100644 index 000000000..7982182d3 --- /dev/null +++ b/buddy/examples/bddcalc/examples/c499.cal @@ -0,0 +1,409 @@ +/* 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/bddcalc/examples/readme b/buddy/examples/bddcalc/examples/readme new file mode 100644 index 000000000..50a49a022 --- /dev/null +++ b/buddy/examples/bddcalc/examples/readme @@ -0,0 +1,3 @@ + The files here are from the ISCAS85 benchmark set. They have been + adjustet such that the comparison of two combinatorial circuits + are joined into one file. diff --git a/buddy/examples/bddcalc/hashtbl.cxx b/buddy/examples/bddcalc/hashtbl.cxx new file mode 100644 index 000000000..a6ccbe58c --- /dev/null +++ b/buddy/examples/bddcalc/hashtbl.cxx @@ -0,0 +1,174 @@ +/************************************************************************* + $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/bddcalc/hashtbl.cxx,v 1.1 2004/06/28 14:19:59 adl 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/bddcalc/lexer.l b/buddy/examples/bddcalc/lexer.l new file mode 100644 index 000000000..7818adb25 --- /dev/null +++ b/buddy/examples/bddcalc/lexer.l @@ -0,0 +1,101 @@ +/************************************************************************* + FILE: lexer.l + DESCR: FLEX rules for BDD calculator + AUTH: Jorn Lind + DATE: (C) may 1999 +*************************************************************************/ +%{ +#include +#include +#include "parser.h" +#include "tokens.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/bddcalc/makefile b/buddy/examples/bddcalc/makefile new file mode 100644 index 000000000..783dd7002 --- /dev/null +++ b/buddy/examples/bddcalc/makefile @@ -0,0 +1,45 @@ +# --------------------------- +# Makefile for BDD calculator +# --------------------------- + +all: bddcalc + +# --- Compiler flags +CFLAGS = -O3 -pedantic -Wall -ansi -L../../src -I../../src + +# --- C++ compiler +CPP = g++ + +# --- C compiler +CC = gcc + +# --- You may need to change these according to your flex and bison versions +parser.cxx: parser.h parser.y + yacc -d -o parser.cxx parser.y + mv parser.cxx.h tokens.h + +lexer.cxx: tokens.h parser.h lexer.l + flex -olexer.cxx lexer.l + + +# --- Do not touch --- + +.SUFFIXES: .cxx .c + +.cxx.o: + $(CPP) $(CFLAGS) -c $< + +.c.o: + $(CC) $(CFLAGS) -c $< + +bddcalc: parser.o lexer.o hashtbl.o bddlib + $(CPP) $(CFLAGS) parser.o lexer.o hashtbl.o -o bddcalc -lbdd -lm + +bddlib: + cd ../../src ; make + +clean: + rm -f *~ examples/*~ + rm -f *.o + rm -f bddcalc parser.cxx lexer.cxx + diff --git a/buddy/examples/bddcalc/parser.h b/buddy/examples/bddcalc/parser.h new file mode 100644 index 000000000..7b59b0067 --- /dev/null +++ b/buddy/examples/bddcalc/parser.h @@ -0,0 +1,44 @@ +/************************************************************************* + 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/bddcalc/parser.hxx b/buddy/examples/bddcalc/parser.hxx new file mode 100644 index 000000000..c96c7dca9 --- /dev/null +++ b/buddy/examples/bddcalc/parser.hxx @@ -0,0 +1,118 @@ +/* A Bison parser, made by GNU Bison 1.875. */ + +/* Skeleton parser for Yacc-like parsing with Bison, + Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002 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/bddcalc/parser.y b/buddy/examples/bddcalc/parser.y new file mode 100644 index 000000000..9b57db30d --- /dev/null +++ b/buddy/examples/bddcalc/parser.y @@ -0,0 +1,463 @@ +/************************************************************************* + 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" + + /* 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) +{ + using namespace std ; + 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) +{ + using namespace std ; + 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) +{ + using namespace std ; + 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) +{ + using namespace std ; + 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) +{ + using namespace std ; + 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) +{ + using namespace std ; + 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/bddcalc/readme b/buddy/examples/bddcalc/readme new file mode 100644 index 000000000..b281b90d3 --- /dev/null +++ b/buddy/examples/bddcalc/readme @@ -0,0 +1,99 @@ +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/bddcalc/slist.h b/buddy/examples/bddcalc/slist.h new file mode 100644 index 000000000..b3c0dac6d --- /dev/null +++ b/buddy/examples/bddcalc/slist.h @@ -0,0 +1,235 @@ +/************************************************************************* + $Header: /Volumes/CVS/repository/spot/spot/buddy/examples/bddcalc/slist.h,v 1.1 2004/06/28 14:19:59 adl 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/bddcalc/tokens.h b/buddy/examples/bddcalc/tokens.h new file mode 100644 index 000000000..6a41e8d5b --- /dev/null +++ b/buddy/examples/bddcalc/tokens.h @@ -0,0 +1,39 @@ +#ifndef YYERRCODE +#define YYERRCODE 256 +#endif + +#define T_id 257 +#define T_str 258 +#define T_intval 259 +#define T_true 260 +#define T_false 261 +#define T_initial 262 +#define T_inputs 263 +#define T_actions 264 +#define T_size 265 +#define T_dumpdot 266 +#define T_autoreorder 267 +#define T_reorder 268 +#define T_win2 269 +#define T_win2ite 270 +#define T_sift 271 +#define T_siftite 272 +#define T_none 273 +#define T_cache 274 +#define T_tautology 275 +#define T_print 276 +#define T_lpar 277 +#define T_rpar 278 +#define T_equal 279 +#define T_semi 280 +#define T_dot 281 +#define T_exist 282 +#define T_forall 283 +#define T_biimp 284 +#define T_imp 285 +#define T_or 286 +#define T_nor 287 +#define T_xor 288 +#define T_nand 289 +#define T_and 290 +#define T_not 291 diff --git a/buddy/examples/bddtest/bddtest.cxx b/buddy/examples/bddtest/bddtest.cxx new file mode 100644 index 000000000..4056cc0db --- /dev/null +++ b/buddy/examples/bddtest/bddtest.cxx @@ -0,0 +1,145 @@ +#include +#include +#include + +static const int varnum = 5; + +/************************************************************************** + Example of allsat print handler. +**************************************************************************/ + +void allsatHandlerPrint(char* varset, int size) +{ + using namespace std ; + for (int v=0; v +#include +#include +#include "bdd.h" + +int N; /* Number of cyclers */ +int *normvar; /* Current state variables */ +int *primvar; /* Next state variables */ + +bdd normvarset; +bddPair *pairs; + +bdd A(bdd* x, bdd* y, int z) +{ + bdd res = bddtrue, tmp1, tmp2; + int i; + + for(i=0 ; i 1 -> 2 -> 3 -> 4 -> 5 -> -> 7 -> 0 + */ + +#include "fdd.h" + +/* Use the transition relation "transRel" to iterate through the statespace + */ +void findStateSpace(bdd transRel) +{ + using namespace std ; + /* Create a new pair for renaming the next-state variables to + * current-state variables */ + bddPair *p = bdd_newpair(); + fdd_setpair(p,1,0); + + /* Get a BDD that represents all the current-state variables */ + bdd currentStateVar = fdd_ithset(0); + + /* Start with the initial state */ + bdd reachedStates = fdd_ithvar(0,0); + + bdd tmp = bddfalse; + + /* Repeat until no new states are found */ + do + { + tmp = reachedStates; + + /* Calculate: Newset = (exists V_cur. transRel & Reached)[cur/next] */ + bdd newset; + newset = reachedStates & transRel; + newset = bdd_exist(newset, currentStateVar); + newset = bdd_replace(newset, p); + + cout << "Front: " << (newset - reachedStates) << endl; + + /* Add the new states to the found states */ + reachedStates = reachedStates | newset; + } + while (tmp != reachedStates); +} + + +int main() { + using namespace std ; + /* Initialize BuDDy and declare two interleaved FDD variable blocks + * with the domain [0..7] */ + int domain[2] = {8,8}; + + bdd_init(100,100); + fdd_extdomain(domain, 2); + + /* Initialize the transition relation with no transitions */ + bdd T = bddfalse; + + /* Add all the transitions (from state 'i' to state 'i+1') */ + for (int i=0 ; i<8 ; i++) + { + /* Set the current state to be state 'i' */ + bdd current = fdd_ithvar(0,i); + + /* Set the next state to be state 'i+1' */ + bdd next = fdd_ithvar(1, (i+1) % 8); + + /* Add the transition */ + T = T | (current & next); + } + + cout << fddset << "Transition relation: " << T << endl << endl; + + /* Calculate the reachable statespace */ + findStateSpace(T); +}