1#FIG 3.2 2Landscape 3Center 4Inches 5Letter 6100.00 7Single 8-2 91200 2 105 1 1 1 0 7 50 0 -1 4.000 0 0 1 0 8315.625 4800.000 8175 4725 8475 4800 8175 4875 11 2 1 1.00 60.00 120.00 125 1 1 1 0 7 50 0 -1 4.000 0 0 1 0 8315.625 5250.000 8175 5175 8475 5250 8175 5325 13 2 1 1.00 60.00 120.00 146 3150 4500 4650 5550 152 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 16 3150 4500 4650 4500 4650 5550 3150 5550 3150 4500 174 0 0 50 0 0 16 0.0000 4 210 915 3442 5085 addFact()\001 18-6 196 2250 3075 3675 3975 206 2325 3300 3525 3825 214 0 0 50 0 0 16 0.0000 4 165 1140 2362 3487 Union-Find\001 224 0 0 50 0 0 16 0.0000 4 165 885 2362 3772 Database\001 23-6 242 4 0 1 0 7 50 0 -1 0.000 0 0 7 0 0 5 25 3637 3975 3637 3075 2287 3075 2287 3975 3637 3975 26-6 276 3150 6150 4575 6450 282 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 29 3150 6450 4575 6450 4575 6150 3150 6150 3150 6450 304 0 0 50 0 0 12 0.0000 4 180 795 3465 6345 fact queue\001 31-6 326 2175 2325 3975 2700 332 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 34 2175 2325 3975 2325 3975 2700 2175 2700 2175 2325 354 0 0 50 0 0 12 0.0000 4 180 825 2662 2557 Notify List\001 36-6 376 3825 2925 5250 4125 386 4200 3300 4875 3825 394 0 0 50 0 0 16 0.0000 4 165 465 4237 3487 SAT\001 404 0 0 50 0 0 16 0.0000 4 165 600 4237 3772 solver\001 41-6 422 3 0 1 0 7 50 0 -1 0.000 0 0 0 0 0 7 43 5212 3525 4874 2940 4200 2940 3862 3525 4200 4110 4874 4110 44 5212 3525 45-6 466 9225 3825 10425 4425 474 0 0 50 0 0 20 0.0000 4 195 990 9262 4087 Decision\001 484 0 0 50 0 0 20 0.0000 4 195 1155 9262 4417 Procedure\001 49-6 502 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 51 2 1 2.00 60.00 120.00 52 4650 4650 6375 4650 6375 3750 8175 3750 532 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 5 54 2 1 2.00 60.00 120.00 55 9000 5700 9000 7275 5250 7275 5250 6300 4575 6300 562 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 57 2 1 1.00 60.00 120.00 58 3150 6300 2925 6300 2925 5925 3900 5925 3900 5550 592 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 60 2 1 1.00 60.00 120.00 61 3300 4500 3300 3975 622 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 63 2 1 1.00 60.00 120.00 64 4500 4500 4500 4125 652 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 66 2 1 1.00 60.00 120.00 67 3000 3075 3000 2700 682 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 5 69 2 1 2.00 60.00 120.00 70 9600 5700 9600 7575 2550 7575 2550 5325 3150 5325 712 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 72 2 1 1.00 60.00 120.00 73 10275 5700 10275 7950 2100 7950 2100 4950 3075 4950 742 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 75 2 1 1.00 60.00 120.00 76 4650 4800 6600 4800 6600 4275 8175 4275 772 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 78 2 1 1.00 60.00 120.00 79 4650 5025 6825 5025 6825 4725 8175 4725 802 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 81 2 1 1.00 60.00 120.00 82 3150 2325 3150 450 10425 450 10425 2625 832 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 84 2 1 1.00 60.00 120.00 85 4800 2925 4800 1500 8700 1500 8700 2625 862 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 87 2 1 1.00 60.00 120.00 88 4650 5250 8175 5250 892 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 90 2 1 1.00 60.00 120.00 91 4650 5475 8175 5475 922 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 3 93 2 1 1.00 60.00 120.00 94 8175 5475 10950 5475 10950 5700 952 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 96 2 1 1.00 60.00 120.00 97 10950 5700 10950 8250 1725 8250 1725 2550 2175 2550 982 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 99 2 1 2.00 60.00 120.00 100 4575 2925 4575 1125 9300 1125 9300 2625 1012 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 102 2 1 2.00 60.00 120.00 103 4350 2925 4350 825 9750 825 9750 2625 1042 2 1 3 0 6 60 0 36 8.000 0 0 -1 0 0 5 105 1350 1725 6150 1725 6150 6900 1350 6900 1350 1725 1062 2 1 3 0 6 60 0 36 8.000 0 0 -1 0 0 5 107 8175 2625 11550 2625 11550 5700 8175 5700 8175 2625 1082 1 0 1 0 7 50 0 -1 0.000 0 0 -1 1 0 2 109 2 1 1.00 60.00 120.00 110 75 4725 3150 4725 1112 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 6 112 2 1 1.00 60.00 120.00 113 8400 5700 8400 6075 5250 6075 5250 5925 4350 5925 4350 5550 1142 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 115 2 1 1.00 60.00 120.00 116 4650 4575 6000 4575 6000 3375 8175 3375 1172 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 8 118 2 1 1.00 60.00 120.00 119 8625 5700 8625 6450 5625 6450 5625 6225 5100 6225 5100 6075 120 4125 6075 4125 5550 1212 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 122 2 1 1.00 60.00 120.00 123 8175 3375 8625 3375 9150 4575 8625 5700 1242 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 125 2 1 1.00 60.00 120.00 126 8175 3750 8400 3750 8775 4650 8400 5700 1274 0 0 50 0 0 20 0.0000 4 195 555 1575 2250 Core\001 1284 0 0 50 0 0 14 0.0000 4 195 1350 6525 3675 computeType()\001 1294 0 0 50 0 0 14 0.0000 4 195 1275 7575 7200 enqueueFact()\001 1304 0 0 50 0 0 14 0.0000 4 195 1455 7575 7500 setInconsistent()\001 1314 0 0 50 0 0 14 0.0000 4 195 1590 7575 7875 enqueueEquality()\001 1324 0 0 50 0 0 14 0.0000 4 195 1560 6675 4200 addSharedTerm()\001 1334 0 0 50 0 0 14 0.0000 4 195 780 7050 4650 rewrite()\001 1344 0 0 50 0 0 14 0.0000 4 195 600 7200 5100 solve()\001 1354 0 0 50 0 0 14 0.0000 4 195 1680 7125 1425 notifyInconsistent()\001 1364 0 0 50 0 0 14 0.0000 4 195 1065 8775 675 assertFact()\001 1374 0 0 50 0 0 14 0.0000 4 195 960 8025 1050 checkSat()\001 1384 0 0 50 0 0 14 0.0000 4 195 735 9525 375 update()\001 1394 0 0 50 0 0 14 0.0000 4 195 615 7200 5625 setup()\001 1404 0 0 50 0 0 14 0.0000 4 195 1785 7575 8175 Expr::addToNotify()\001 1414 0 0 50 0 0 14 0.0000 4 195 840 150 4650 user input\001 1424 0 0 50 0 0 12 0.0000 4 180 1140 6525 3300 computeTCC()\001 1434 0 0 50 0 0 12 0.0000 4 180 735 7200 6375 getTCC()\001 1444 0 0 50 0 0 12 0.0000 4 180 2055 6225 6000 getType() / getBaseType()\001 145