#FIG 3.2 Landscape Center Inches Letter 100.00 Single -2 1200 2 5 1 1 1 0 7 50 0 -1 4.000 0 0 1 0 8315.625 4800.000 8175 4725 8475 4800 8175 4875 2 1 1.00 60.00 120.00 5 1 1 1 0 7 50 0 -1 4.000 0 0 1 0 8315.625 5250.000 8175 5175 8475 5250 8175 5325 2 1 1.00 60.00 120.00 6 3150 4500 4650 5550 2 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 3150 4500 4650 4500 4650 5550 3150 5550 3150 4500 4 0 0 50 0 0 16 0.0000 4 210 915 3442 5085 addFact()\001 -6 6 2250 3075 3675 3975 6 2325 3300 3525 3825 4 0 0 50 0 0 16 0.0000 4 165 1140 2362 3487 Union-Find\001 4 0 0 50 0 0 16 0.0000 4 165 885 2362 3772 Database\001 -6 2 4 0 1 0 7 50 0 -1 0.000 0 0 7 0 0 5 3637 3975 3637 3075 2287 3075 2287 3975 3637 3975 -6 6 3150 6150 4575 6450 2 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 3150 6450 4575 6450 4575 6150 3150 6150 3150 6450 4 0 0 50 0 0 12 0.0000 4 180 795 3465 6345 fact queue\001 -6 6 2175 2325 3975 2700 2 2 0 1 0 7 50 0 -1 0.000 0 0 -1 0 0 5 2175 2325 3975 2325 3975 2700 2175 2700 2175 2325 4 0 0 50 0 0 12 0.0000 4 180 825 2662 2557 Notify List\001 -6 6 3825 2925 5250 4125 6 4200 3300 4875 3825 4 0 0 50 0 0 16 0.0000 4 165 465 4237 3487 SAT\001 4 0 0 50 0 0 16 0.0000 4 165 600 4237 3772 solver\001 -6 2 3 0 1 0 7 50 0 -1 0.000 0 0 0 0 0 7 5212 3525 4874 2940 4200 2940 3862 3525 4200 4110 4874 4110 5212 3525 -6 6 9225 3825 10425 4425 4 0 0 50 0 0 20 0.0000 4 195 990 9262 4087 Decision\001 4 0 0 50 0 0 20 0.0000 4 195 1155 9262 4417 Procedure\001 -6 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 2 1 2.00 60.00 120.00 4650 4650 6375 4650 6375 3750 8175 3750 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 5 2 1 2.00 60.00 120.00 9000 5700 9000 7275 5250 7275 5250 6300 4575 6300 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 2 1 1.00 60.00 120.00 3150 6300 2925 6300 2925 5925 3900 5925 3900 5550 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 3300 4500 3300 3975 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 4500 4500 4500 4125 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 3000 3075 3000 2700 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 5 2 1 2.00 60.00 120.00 9600 5700 9600 7575 2550 7575 2550 5325 3150 5325 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 2 1 1.00 60.00 120.00 10275 5700 10275 7950 2100 7950 2100 4950 3075 4950 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 4650 4800 6600 4800 6600 4275 8175 4275 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 4650 5025 6825 5025 6825 4725 8175 4725 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 3150 2325 3150 450 10425 450 10425 2625 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 4800 2925 4800 1500 8700 1500 8700 2625 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 4650 5250 8175 5250 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 4650 5475 8175 5475 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 3 2 1 1.00 60.00 120.00 8175 5475 10950 5475 10950 5700 2 1 0 1 0 7 50 0 -1 4.000 0 0 -1 1 0 5 2 1 1.00 60.00 120.00 10950 5700 10950 8250 1725 8250 1725 2550 2175 2550 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 2 1 2.00 60.00 120.00 4575 2925 4575 1125 9300 1125 9300 2625 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 4 2 1 2.00 60.00 120.00 4350 2925 4350 825 9750 825 9750 2625 2 2 1 3 0 6 60 0 36 8.000 0 0 -1 0 0 5 1350 1725 6150 1725 6150 6900 1350 6900 1350 1725 2 2 1 3 0 6 60 0 36 8.000 0 0 -1 0 0 5 8175 2625 11550 2625 11550 5700 8175 5700 8175 2625 2 1 0 1 0 7 50 0 -1 0.000 0 0 -1 1 0 2 2 1 1.00 60.00 120.00 75 4725 3150 4725 2 1 0 3 0 7 50 0 -1 0.000 0 0 -1 1 0 6 2 1 1.00 60.00 120.00 8400 5700 8400 6075 5250 6075 5250 5925 4350 5925 4350 5550 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 4650 4575 6000 4575 6000 3375 8175 3375 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 8 2 1 1.00 60.00 120.00 8625 5700 8625 6450 5625 6450 5625 6225 5100 6225 5100 6075 4125 6075 4125 5550 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 8175 3375 8625 3375 9150 4575 8625 5700 2 1 1 1 0 7 50 0 -1 4.000 0 0 -1 1 0 4 2 1 1.00 60.00 120.00 8175 3750 8400 3750 8775 4650 8400 5700 4 0 0 50 0 0 20 0.0000 4 195 555 1575 2250 Core\001 4 0 0 50 0 0 14 0.0000 4 195 1350 6525 3675 computeType()\001 4 0 0 50 0 0 14 0.0000 4 195 1275 7575 7200 enqueueFact()\001 4 0 0 50 0 0 14 0.0000 4 195 1455 7575 7500 setInconsistent()\001 4 0 0 50 0 0 14 0.0000 4 195 1590 7575 7875 enqueueEquality()\001 4 0 0 50 0 0 14 0.0000 4 195 1560 6675 4200 addSharedTerm()\001 4 0 0 50 0 0 14 0.0000 4 195 780 7050 4650 rewrite()\001 4 0 0 50 0 0 14 0.0000 4 195 600 7200 5100 solve()\001 4 0 0 50 0 0 14 0.0000 4 195 1680 7125 1425 notifyInconsistent()\001 4 0 0 50 0 0 14 0.0000 4 195 1065 8775 675 assertFact()\001 4 0 0 50 0 0 14 0.0000 4 195 960 8025 1050 checkSat()\001 4 0 0 50 0 0 14 0.0000 4 195 735 9525 375 update()\001 4 0 0 50 0 0 14 0.0000 4 195 615 7200 5625 setup()\001 4 0 0 50 0 0 14 0.0000 4 195 1785 7575 8175 Expr::addToNotify()\001 4 0 0 50 0 0 14 0.0000 4 195 840 150 4650 user input\001 4 0 0 50 0 0 12 0.0000 4 180 1140 6525 3300 computeTCC()\001 4 0 0 50 0 0 12 0.0000 4 180 735 7200 6375 getTCC()\001 4 0 0 50 0 0 12 0.0000 4 180 2055 6225 6000 getType() / getBaseType()\001