TAGS 49.9 KB
Newer Older
Masahiko Sakai's avatar
Masahiko Sakai committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302

Debug.C,187
vec<cchar*>* debug_names 24,1320
void dump(28,1455
void dump(34,1662
void dump(46,1958
void dump(54,2117
void dump(65,2363
void dump(77,2614
void dump(95,3162
void dump(110,3471

Hardware_adders.C,78
int estimatedAdderCost(24,1322
void rippleAdder(48,1831
void addPb(77,2840

Hardware_clausify.C,930
struct Clausifier23,1321
    Solver&      s;Clausifier::s25,1341
    vec<Lit>     tmp_clause;Clausifier::tmp_clause26,1361
    vec<Formula> tmp_marked;Clausifier::tmp_marked27,1390
    Clausifier(Clausifier::Clausifier29,1420
    static /*WARNING*/ CMap<int>      occ;Clausifier::occ31,1459
    static /*WARNING*/ CMap<Var>      vmap;Clausifier::vmap32,1502
    static /*WARNING*/ CMap<Clausifier::CMap33,1546
    static /*WARNING*/ CMap<Lit,true> vmapp;Clausifier::vmapp33,1546
    FMap<bool>   seen;Clausifier::seen34,1591
    inline void clause(Clausifier::clause36,1615
    inline void clause(Clausifier::clause38,1749
    inline void clause(Clausifier::clause40,1910
void Clausifier::usage(56,2439
void Clausifier::collect(75,2867
void Clausifier::_collect(84,3094
Lit Clausifier::polarityClausify(98,3429
Lit Clausifier::basicClausify(253,8745
void clausify(348,11530
void clausify(364,11905

Hardware_sorters.C,245
macro Formula operator && operator &&24,1403
macro Formula operator || operator ||36,1747
static inline void cmp2(42,1927
static void riffle(55,2180
static void unriffle(64,2381
static void oddEvenMerge(73,2596
void oddEvenSort(97,3377

Main.C,1348
bool     opt_satlive 41,1842
bool     opt_ansi 42,1873
char*    opt_cnf 43,1904
int      opt_verbosity 44,1935
bool     opt_try 45,1963
SolverT  opt_solver 47,2124
ConvertT opt_convert 48,2165
ConvertT opt_convert_goal 49,2204
bool     opt_convert_weak 50,2243
bool     opt_avoid_interval_constraint 51,2278
GpwT     opt_convert_gpw 54,2401
bool     opt_convert_bdd_monotonic 55,2443
int      opt_convert_bdd_decomposition 57,2544
bool     opt_convert_bdd_interval 58,2620
bool     opt_convert_bdd_increasing_order 59,2663
double   opt_bdd_thres 60,2714
double   opt_sort_thres 61,2746
double   opt_goal_bias 62,2779
Int      opt_goal 63,2811
Command  opt_command 64,2849
bool     opt_branch_pbvars 65,2892
int      opt_polarity_sug 66,2928
bool     opt_old_format 67,2960
bool     opt_extract_ucore 68,2996
int      opt_ucore_mode 69,3032
bool     opt_model_check 71,3065
char*    opt_input 73,3102
char*    opt_result 74,3130
cchar* doc 78,3260
bool oneof(140,6808
void parseOptions(161,7258
void reportf(266,12652
PbSolver*   pb_solver 297,13395
bool model_check(301,13541
void outputResult(328,14319
static void SIGINT_handler(368,15479
static void SIGTERM_handler(375,15716
void printStats(383,15945
PbSolver::solve_Command convert(394,16609
int main(408,17036
#define N 458,19049
void test(460,19063

MiniSat.C,1024
namespace MiniSat 25,1337
#define L_IND 31,1514
#define L_ind 32,1538
#define L_LIT 33,1591
#define L_lit(34,1616
inline void check(MiniSat::check37,1746
void removeWatch(MiniSat::removeWatch44,1909
bool Solver::newClause(59,2421
void Solver::remove(142,5159
bool Solver::simplify(170,6017
Var Solver::newVar(189,6540
bool Solver::assume(208,7034
void Solver::cancelUntil(216,7267
void Solver::record(230,7795
#define ANALYZE_LIT(245,8149
void Solver::analyze(273,9534
#define REMOVABLE_LIT(362,12266
bool Solver::removable(376,13467
bool Solver::enqueue(414,14748
Clause* Solver::propagate(441,15620
struct reduceDB_lt 517,18360
struct reduceDB_lt { bool operator () reduceDB_lt::operator ()517,18360
void Solver::reduceDB(518,18503
void Solver::simplifyDB(548,19524
lbool Solver::search(590,20976
double Solver::progressEstimate(687,24197
void Solver::varRescaleActivity(700,24489
void Solver::claRescaleActivity(710,24674
bool Solver::solve(727,25315
void Solver::exportClauses(772,27076

OptimalBase.C,155
int primes[primes25,1428
#define ExpensiveBigConstants32,2449
#define AllDigitsImportant33,2479
void optimizeBase(37,2509
void optimizeBase(128,5640

PbParser.C,1649
class FileBuffer 28,1470
    File    in;FileBuffer::in29,1489
    int     next;FileBuffer::next30,1505
    int     line;FileBuffer::line32,1531
    FileBuffer(FileBuffer::FileBuffer33,1549
   ~FileBuffer(FileBuffer::~FileBuffer37,1759
    int  operator * FileBuffer::operator *38,1779
    void operator ++ FileBuffer::operator ++39,1820
class StringBuffer 43,1901
    cchar*  ptr;StringBuffer::ptr44,1922
    cchar*  last;StringBuffer::last45,1939
    int     line;StringBuffer::line47,1965
    StringBuffer(StringBuffer::StringBuffer48,1983
    StringBuffer(StringBuffer::StringBuffer49,2076
   ~StringBuffer(StringBuffer::~StringBuffer50,2161
    int  operator * StringBuffer::operator *51,2183
    void operator ++ StringBuffer::operator ++52,2246
static void skipWhitespace(90,3659
static void skipLine(95,3797
static void skipComments(102,3953
static bool skipEndOfLine(106,4136
static bool skipText(113,4346
static Int parseInt(120,4515
static char* parseIdent(142,5238
void parseExpr(156,5817
void parseSize(184,6747
void parseGoal(207,7194
int parseInequality(228,7815
bool parseConstrs(252,8352
static bool parse_PB(297,9707
void parse_PB_file(318,10428
#define Solver 329,10793
struct DummySolver 331,10821
    Map<DummySolver::Map332,10842
    Map<cchar*, int> name2index;DummySolver::name2index332,10842
    vec<cchar*>      index2name;DummySolver::index2name333,10875
    int getVar(DummySolver::getVar335,10909
    void alloc(DummySolver::alloc342,11141
    void addGoal(DummySolver::addGoal344,11241
    bool addConstr(DummySolver::addConstr346,11343
void test(352,11609

PbSolver.C,673
int n_defequivs=26,1379
int n_goalasps=27,1398
int PbSolver::getVar(33,1552
void PbSolver::allocConstrs(51,2054
void PbSolver::addGoal(58,2184
bool PbSolver::addConstr(68,2510
#define Copy 83,3054
#define CopyInv 84,3230
static Int gcd(217,7316
bool PbSolver::normalizePb(235,8190
void PbSolver::storePb(366,12571
bool PbSolver::propagate(383,13331
void PbSolver::propagate(474,15938
void PbSolver::setupOccurs(522,17675
static bool lhsEq(549,18572
static bool lhsEqc(555,18850
void PbSolver::findIntervals(562,19071
bool PbSolver::rewriteAlmostClauses(609,20520
Int evalGoal(704,23310
void PbSolver::exportVar(730,24062
void PbSolver::solve(740,24311

PbSolver_convert.C,35
bool PbSolver::convertPbs(31,1843

PbSolver_convertAdd.C,94
static inline void bitAdder(27,1449
static Formula lte(37,1730
void linearAddition(60,2470

PbSolver_convertBdd.C,99
#define lit2fml(28,1483
  buildBDD_i(33,1586
  buildBDD(141,6296
Formula convertToBdd(239,9602

PbSolver_convertSort.C,361
#define pf(26,1441
void nothing(28,1480
#define lit2fml(34,1606
void buildSorter(38,1658
void buildSorter(48,1937
class Exception_TooBig 57,2161
void buildConstraint(60,2196
void convert(136,4738
Formula lexComp(150,5094
Formula lexComp(171,5910
Formula buildConstraint(177,6068
Formula buildConstraintGpw(218,7297
Formula buildConstraint(251,8210

SatELite.C,4594
namespace SatELite 30,1605
bool opt_confl_1sub SatELite::opt_confl_1sub35,1845
bool opt_confl_ksub SatELite::opt_confl_ksub36,1875
bool opt_var_elim SatELite::opt_var_elim37,1906
bool opt_0sub SatELite::opt_0sub38,1936
bool opt_1sub SatELite::opt_1sub39,1966
bool opt_2sub SatELite::opt_2sub40,1996
bool opt_repeated_sub SatELite::opt_repeated_sub41,2027
bool opt_def_elim SatELite::opt_def_elim42,2058
bool opt_unit_def SatELite::opt_unit_def43,2088
bool opt_hyper1_res SatELite::opt_hyper1_res44,2118
bool opt_pure_literal SatELite::opt_pure_literal45,2148
bool opt_asym_branch SatELite::opt_asym_branch46,2179
bool opt_keep_all SatELite::opt_keep_all47,2210
bool opt_no_random SatELite::opt_no_random48,2241
bool opt_pre_sat SatELite::opt_pre_sat49,2272
bool opt_ext_sat SatELite::opt_ext_sat50,2303
bool opt_niver SatELite::opt_niver51,2334
cchar* input_file SatELite::input_file52,2365
cchar* output_file SatELite::output_file53,2394
cchar* varmap_file SatELite::varmap_file54,2423
cchar* elimed_file SatELite::elimed_file55,2452
cchar* model_file SatELite::model_file56,2481
extern int verbosity;SatELite::verbosity57,2510
#define BCNF_CHUNK_LIMIT 70,3047
class BcnfWriter SatELite::BcnfWriter77,3200
    FILE*   out;SatELite::BcnfWriter::out78,3219
    int     n_vars;SatELite::BcnfWriter::n_vars79,3236
    int     n_clauses;SatELite::BcnfWriter::n_clauses80,3256
    int     chunk_sz;SatELite::BcnfWriter::chunk_sz81,3279
    int*    chunk;SatELite::BcnfWriter::chunk82,3301
    int     stated_n_vars;SatELite::BcnfWriter::stated_n_vars85,3329
    int     stated_n_clauses;SatELite::BcnfWriter::stated_n_clauses86,3385
    int  nVars SatELite::BcnfWriter::nVars92,3515
    int  nClauses(SatELite::BcnfWriter::nClauses93,3558
BcnfWriter::BcnfWriter(97,3609
BcnfWriter::~BcnfWriter(111,4335
void BcnfWriter::addClause(129,4744
static vec<FILE*>  tmp_fps;153,5773
static vec<cchar*> tmp_files;154,5801
FILE* createTmpFile(158,5878
void deleteTmpFile(178,6463
void deleteTmpFiles(199,7145
FINALIZER(209,7318
struct Size24 230,8008
struct Size24 { char dummy[Size24::dummy230,8008
struct Size28 231,8043
struct Size28 { char dummy[Size28::dummy231,8043
VecAlloc<Size24> mem24;232,8078
VecAlloc<Size28> mem28;233,8102
template <> macro void* ymalloc<ymalloc236,8177
macro void yfree(244,8399
#define ymalloc 255,8710
#define yfree 256,8734
int Solver::allocClauseId(264,9001
void Solver::freeClauseId(286,9473
Clause Solver::allocClause(298,9692
Clause Solver::addClause(321,10491
void Solver::deallocClause(431,13911
void Solver::unlinkClause(443,14183
bool Solver::propagateClause(499,15719
void Solver::calcReason(530,16569
void Solver::strengthenClause(542,16964
void Solver::setOccurMode(560,17454
void Solver::setupWatches(585,18340
Var Solver::newVar(609,19182
bool Solver::assume(637,19961
inline void Solver::undoOne(646,20206
void Solver::cancel(660,20570
void Solver::cancelUntil(672,20931
void Solver::record(678,21113
Solver::~Solver(690,21401
void Solver::analyze(716,23422
bool Solver::enqueue(916,30807
void Solver::propagateToplevel(957,32445
Clause Solver::propagate(1002,34390
Clause Solver::propagate(1039,35327
Clause Solver::propagate(1098,37012
bool satisfied(1165,39508
struct reduceDB_lt 1173,39773
struct reduceDB_lt { bool operator () reduceDB_lt::operator ()1173,39773
void Solver::reduceDB(1174,39875
void Solver::compressDB(1201,40632
void Solver::simplifyDB(1235,42109
lbool Solver::search(1286,44826
void Solver::extendModel(1371,48206
double Solver::progressEstimate(1468,51237
void Solver::varRescaleActivity(1482,51625
void Solver::claRescaleActivity(1492,51810
bool Solver::solve(1510,52898
#define Report(1565,55698
#define Report2(1567,55821
macro bool has(1570,55913
bool subset(1579,56110
bool subset(1593,56502
macro bool subset(1603,56673
bool selfSubset(1608,56799
macro bool selfSubset(1627,57312
void Solver::findSubsumed(1638,57574
bool Solver::isSubsumed(1662,58230
void Solver::subsume0(1687,58844
void Solver::subsume1(1702,59119
void Solver::subsume1(1754,60417
void Solver::simplifyBySubsumption(1784,61044
void Solver::orderVarsForElim(2047,72133
bool merge(2068,72716
bool merge(2091,73605
Lit Solver::findUnitDef(2115,74271
bool Solver::findDef(2147,75277
int Solver::substitute(2205,77030
void Solver::asymmetricBranching(2287,79436
bool Solver::maybeEliminate(2416,83997
    #define MigrateToPsNs 2434,84520
    #define DeallocPsNs 2435,84732
void Solver::clauseReduction(2621,92037

Debug.h,49
#define Debug_h21,1295
macro void dump(41,1840

Hardware.h,27
#define Hardware_h21,1298

Main.h,1248
#define Main_h21,1294
enum SolverT 28,1430
enum SolverT  { st_MiniSat,28,1430
enum SolverT  { st_MiniSat, st_SatELite,28,1430
enum SolverT  { st_MiniSat, st_SatELite, st_GlueMiniSat,28,1430
enum SolverT  { st_MiniSat, st_SatELite, st_GlueMiniSat, st_MiniSat22,28,1430
enum SolverT  { st_MiniSat, st_SatELite, st_GlueMiniSat, st_MiniSat22, st_Glucose10 28,1430
enum ConvertT 29,1517
enum ConvertT { ct_Sorters,29,1517
enum ConvertT { ct_Sorters, ct_Adders,29,1517
enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs,29,1517
enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs, ct_Mixed,29,1517
enum ConvertT { ct_Sorters, ct_Adders, ct_BDDs, ct_Mixed, ct_Undef 29,1517
enum Command 30,1587
enum Command  { cmd_Minimize,30,1587
enum Command  { cmd_Minimize, cmd_FirstSolution,30,1587
enum Command  { cmd_Minimize, cmd_FirstSolution, cmd_AllSolutions 30,1587
enum GpwT 31,1656
enum GpwT     { gt_none,31,1656
enum GpwT     { gt_none, gt_positive,31,1656
enum GpwT     { gt_none, gt_positive, gt_negative,31,1656
enum GpwT     { gt_none, gt_positive, gt_negative, gt_low,31,1656
enum GpwT     { gt_none, gt_positive, gt_negative, gt_low, gt_high,31,1656
enum GpwT     { gt_none, gt_positive, gt_negative, gt_low, gt_high, gt_both 31,1656

MiniSat.h,4368
#define MiniSat_h27,1596
class Clause 38,1840
    uint    size_learnt;39,1855
    Lit     data[data40,1880
    Clause(43,1963
    int     size 48,2163
    bool    learnt 49,2234
    Lit     operator 50,2304
    Lit&    operator 51,2370
    float&  activity 52,2436
class LitClauseUnion 60,2664
    void* data;LitClauseUnion::data61,2687
    LitClauseUnion(LitClauseUnion::LitClauseUnion62,2703
    bool        isLit LitClauseUnion::isLit67,2849
    bool        isNull LitClauseUnion::isNull68,2934
    Lit         getLit LitClauseUnion::getLit69,3010
    Clause*     getClause LitClauseUnion::getClause70,3103
    bool        operator==(LitClauseUnion::operator==71,3180
    bool        operator!=(LitClauseUnion::operator!=72,3258
inline LitClauseUnion makeLit 74,3339
inline LitClauseUnion makeClause 75,3449
struct SolverStats 82,3693
    int64   clauses,SolverStats::clauses83,3740
    int64   clauses, clauses_literals,SolverStats::clauses_literals83,3740
    int64   clauses, clauses_literals, learnts,SolverStats::learnts83,3740
    int64   clauses, clauses_literals, learnts, learnts_literals,SolverStats::learnts_literals83,3740
    int64   clauses, clauses_literals, learnts, learnts_literals, max_literals,SolverStats::max_literals83,3740
    int64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;SolverStats::tot_literals83,3740
    SolverStats(SolverStats::SolverStats84,3834
struct SearchParams 88,3965
    double  var_decay,SearchParams::var_decay89,3987
    double  var_decay, clause_decay,SearchParams::clause_decay89,3987
    double  var_decay, clause_decay, random_var_freq;SearchParams::random_var_freq89,3987
    SearchParams(SearchParams::SearchParams90,4090
class Solver 94,4210
    vec<Clause*>        clauses;Solver::clauses96,4236
    vec<Clause*>        learnts;Solver::learnts97,4308
    double              cla_inc;Solver::cla_inc98,4375
    double              cla_decay;Solver::cla_decay99,4451
    vec<double>         activity;Solver::activity101,4553
    vec<char>           polarity;Solver::polarity102,4651
    double              var_inc;Solver::var_inc103,4799
    double              var_decay;Solver::var_decay104,4877
    VarOrder            order;Solver::order105,5026
                        watches;Solver::watches108,5144
    bool                ok;Solver::ok111,5292
    vec<int>            assigns;Solver::assigns112,5429
    vec<Lit>            trail;Solver::trail113,5550
    vec<char>           polarity_sug;Solver::polarity_sug114,5619
    vec<int>            trail_lim;Solver::trail_lim116,5769
    vec<Lit>            trail_copy;Solver::trail_copy117,5872
    vec<LitClauseUnion> reason;Solver::reason118,5933
    vec<int>            level;Solver::level119,6065
    int                 root_level;Solver::root_level120,6173
    int                 last_simplify;Solver::last_simplify121,6248
    int                 qhead;Solver::qhead122,6347
    vec<char>           analyze_seen;Solver::analyze_seen126,6484
    vec<Lit>            toclear;Solver::toclear127,6522
    vec<Lit>            stack;Solver::stack128,6555
    Clause*             tmp_binary;Solver::tmp_binary129,6586
    void    varBumpActivity(Solver::varBumpActivity151,7343
    void    varDecayActivity(Solver::varDecayActivity155,7588
    void    claDecayActivity(Solver::claDecayActivity157,7707
    void    claBumpActivity Solver::claBumpActivity163,7921
    bool    locked Solver::locked165,8086
    int     decisionLevel(Solver::decisionLevel168,8276
    Solver(Solver::Solver171,8352
   ~Solver(Solver::~Solver187,9002
    lbool   value(Solver::value193,9211
    lbool   value(Solver::value194,9274
    int     nAssigns(Solver::nAssigns196,9381
    int     nClauses(Solver::nClauses197,9433
    int     nLearnts(Solver::nLearnts198,9487
    SolverStats stats;Solver::stats202,9596
    int     nVars Solver::nVars207,9704
    bool    addUnit(Solver::addUnit208,9758
    bool    addClause(Solver::addClause209,9825
    bool    okay(Solver::okay215,10051
    bool    solve(Solver::solve218,10163
    double      progress_estimate;Solver::progress_estimate220,10225
    vec<lbool>  model;Solver::model221,10283
    int         verbosity;Solver::verbosity222,10385

OptimalBase.h,30
#define OptimalBase_h21,1301

PbParser.h,27
#define PbParser_h21,1298

PbSolver.h,2357
#define PbSolver_h21,1298
class Linear 32,1563
    int     orig_size;Linear::orig_size33,1578
    int     size;Linear::size35,1644
    Int     lo,Linear::lo36,1692
    Int     lo, hi;Linear::hi36,1692
    Lit     dlt;Linear::dlt38,1851
    char    data[Linear::data40,1942
    Linear(Linear::Linear43,2068
    Lit operator [] Linear::operator []49,2410
    Int operator () Linear::operator ()50,2486
    Lit& operator [] Linear::operator []51,2586
    Int& operator () Linear::operator ()52,2657
class PbSolver 63,3021
    Solver              sat_solver;PbSolver::sat_solver65,3049
    bool&               ok;PbSolver::ok66,3115
    StackAlloc<char*>   mem;PbSolver::mem70,3448
    vec<Linear*>        constrs;PbSolver::constrs73,3639
    Linear*             goal;PbSolver::goal74,3711
    vec<int>            n_occurs;PbSolver::n_occurs76,3889
    vec<vec<int> >      occur;PbSolver::occur77,3967
    int                 propQ_head;PbSolver::propQ_head79,4085
    bool    addUnit PbSolver::addUnit86,4274
    PbSolver(PbSolver::PbSolver96,4823
    lbool   value(PbSolver::value113,5534
    lbool   value(PbSolver::value114,5608
    int     nVars(PbSolver::nVars115,5736
    int     nConstrs(PbSolver::nConstrs116,5798
    BasicSolverStats& stats;PbSolver::stats119,5882
    int     declared_n_vars;PbSolver::declared_n_vars121,5912
    int     declared_n_constrs;PbSolver::declared_n_constrs122,6021
    int     pb_n_vars;PbSolver::pb_n_vars123,6132
    int     pb_n_constrs;PbSolver::pb_n_constrs124,6227
    Map<PbSolver::Map126,6325
    Map<cchar*, int>    name2index;PbSolver::name2index126,6325
    vec<cchar*>         index2name;PbSolver::index2name127,6361
    vec<bool>           best_model;PbSolver::best_model128,6397
    Int                 best_goalvalue;PbSolver::best_goalvalue129,6480
    vec<int>            ucore_var_id;PbSolver::ucore_var_id130,6601
    bool    okay(PbSolver::okay141,6986
    enum solve_Command PbSolver::solve_Command143,7025
    enum solve_Command { sc_Minimize,PbSolver::solve_Command::sc_Minimize143,7025
    enum solve_Command { sc_Minimize, sc_FirstSolution,PbSolver::solve_Command::sc_FirstSolution143,7025
    enum solve_Command { sc_Minimize, sc_FirstSolution, sc_AllSolutions PbSolver::solve_Command::sc_AllSolutions143,7025

SatELite.h,8386
#define SatELite_h27,1566
class Queue 60,2463
    vec<T>  elems;61,2477
    int     first;62,2496
    Queue(64,2523
    void insert(65,2554
    T    dequeue(66,2596
    void clear(67,2646
    int  size(68,2699
    bool has(69,2755
#define BUMP_MORE82,3369
struct Clause_t 91,3517
    int     id_;Clause_t::id_92,3535
            uint64  abst_;Clause_t::abst_95,3611
            uint    size_learnt;Clause_t::size_learnt96,3638
            char    _vec[Clause_t::_vec99,3699
    Lit     data[Clause_t::data102,3761
    vec<Lit>&   Vec(Clause_t::Vec104,3783
    bool       dynamic Clause_t::dynamic108,3880
    int        size Clause_t::size109,3947
    Lit&       operator [] Clause_t::operator []110,4047
    const Lit& operator [] Clause_t::operator []111,4143
    Lit&       operator () Clause_t::operator ()112,4239
    const Lit& operator () Clause_t::operator ()113,4328
    void       push Clause_t::push114,4417
    void       clear Clause_t::clear115,4500
    vec<Lit>&  asVec Clause_t::asVec116,4583
    Clause_t(Clause_t::Clause_t119,4687
   ~Clause_t(Clause_t::~Clause_t120,4745
class Clause 124,4811
    Clause_t* ptr_;Clause::ptr_125,4826
    Clause(Clause::Clause127,4854
    Clause(Clause::Clause128,4894
    Clause(Clause::Clause129,4932
    Clause_t* ptr(Clause::ptr130,4970
    bool    operator == Clause::operator ==132,5018
    bool    null(Clause::null133,5095
    void    zero(Clause::zero134,5166
    bool       dynamic Clause::dynamic136,5230
    int        size Clause::size137,5304
    Lit&       operator [] Clause::operator []138,5375
    const Lit& operator [] Clause::operator []139,5448
    Lit&       operator () Clause::operator ()140,5521
    const Lit& operator () Clause::operator ()141,5594
    void       push Clause::push144,5684
    void       clear Clause::clear145,5756
    vec<Lit>&  asVec Clause::asVec146,5828
    int        id Clause::id149,5921
    uint64     abst Clause::abst150,6009
    bool       learnt Clause::learnt151,6099
    float&     activity Clause::activity152,6199
const Clause Clause_NULL 155,6337
macro bool operator < operator <157,6375
macro uint hash(158,6464
class CSet 166,6637
    vec<int>    where;CSet::where167,6650
    vec<Clause> which;CSet::which168,6715
    vec<int>    free;CSet::free169,6807
    Clause  operator [] CSet::operator []172,6884
    int     size CSet::size173,6951
    int     nElems CSet::nElems174,7018
    bool    add(CSet::add176,7100
    bool    exclude(CSet::exclude192,7503
    void    clear(CSet::clear202,7781
macro void remove(218,8122
template <class T> macro void maybeRemove(226,8307
macro int find(229,8419
macro int find(235,8567
struct SolverStats 245,8918
    int64   reduceDBs;SolverStats::reduceDBs246,8965
    SolverStats(SolverStats::SolverStats247,8988
struct SearchParams 251,9033
    double  var_decay,SearchParams::var_decay252,9055
    double  var_decay, clause_decay,SearchParams::clause_decay252,9055
    double  var_decay, clause_decay, random_var_freq;SearchParams::random_var_freq252,9055
    bool    simplify;SearchParams::simplify253,9158
    SearchParams(SearchParams::SearchParams254,9180
enum OccurMode 257,9326
enum OccurMode { occ_Off,OccurMode::occ_Off257,9326
enum OccurMode { occ_Off, occ_Permanent,OccurMode::occ_Permanent257,9326
enum OccurMode { occ_Off, occ_Permanent, occ_All OccurMode::occ_All257,9326
struct Solver 260,9380
    bool                ok;Solver::ok264,9410
    vec<Clause>         constrs;Solver::constrs265,9547
    vec<int>            constrs_free;Solver::constrs_free266,9614
    vec<Clause>         learnts;Solver::learnts267,9688
    vec<int>            learnts_free;Solver::learnts_free268,9754
    double              cla_inc;Solver::cla_inc269,9827
    double              cla_decay;Solver::cla_decay270,9903
    int                 n_literals;Solver::n_literals271,10004
    FILE*               elim_out;Solver::elim_out272,10116
    char*               elim_out_file;Solver::elim_out_file273,10220
    vec<vec<Clause>*>   iter_vecs;Solver::iter_vecs274,10278
    vec<CSet*>          iter_sets;Solver::iter_sets275,10425
    vec<double>         activity;Solver::activity277,10505
    vec<char>           polarity_sug;Solver::polarity_sug278,10603
    double              var_inc;Solver::var_inc279,10744
    double              var_decay;Solver::var_decay280,10822
    vec<double>         lt_activity;Solver::lt_activity282,10992
    VarOrder2           order;Solver::order283,11055
    VarOrder            order;Solver::order285,11150
    vec<vec<Clause> >   watches;Solver::watches288,11247
    bool                watches_setup;Solver::watches_setup289,11393
    vec<vec<Clause> >   occur;Solver::occur290,11490
    OccurMode           occur_mode;Solver::occur_mode291,11596
    vec<int>            n_occurs;Solver::n_occurs292,11680
    Queue<Lit>          propQ;Solver::propQ293,11804
    vec<int>            assigns;Solver::assigns295,11867
    vec<Lit>            units;Solver::units296,11962
    vec<Lit>            trail;Solver::trail297,12079
    vec<int>            trail_lim;Solver::trail_lim298,12148
    vec<Clause>         reason;Solver::reason299,12251
    vec<int>            level;Solver::level300,12383
    int                 root_level;Solver::root_level301,12491
    int                 last_simplify;Solver::last_simplify302,12566
    vec<char>           touched;Solver::touched304,12666
    vec<Var>            touched_list;Solver::touched_list305,12815
    CSet                cl_touched;Solver::cl_touched306,12900
    CSet                cl_added;Solver::cl_added307,12965
    bool                fwd_subsump;Solver::fwd_subsump308,13025
    vec<char>           var_elimed;Solver::var_elimed310,13100
    vec<char>           frozen;Solver::frozen311,13202
    int64               last_inspects;Solver::last_inspects313,13303
    vec<char>           seen_tmp;Solver::seen_tmp317,13514
    vec<char>           touched_tmp;Solver::touched_tmp318,13582
    vec<Lit>            unit_tmp;Solver::unit_tmp319,13706
    vec<Lit>            io_tmp;Solver::io_tmp320,13771
    void    createTmpFiles(Solver::createTmpFiles346,14906
    void    deleteTmpFiles(Solver::deleteTmpFiles352,15158
    void    registerIteration Solver::registerIteration353,15258
    void    unregisterIteration(Solver::unregisterIteration354,15344
    void    registerIteration Solver::registerIteration355,15433
    void    unregisterIteration(Solver::unregisterIteration356,15519
    void    varBumpActivity(Solver::varBumpActivity362,15713
    void    varDecayActivity(Solver::varDecayActivity369,16032
    void    claBumpActivity(Solver::claBumpActivity372,16152
    void    claDecayActivity(Solver::claDecayActivity373,16256
    bool    locked Solver::locked383,16568
    int     decisionLevel(Solver::decisionLevel384,16639
    void    watch Solver::watch386,16701
    void    unwatch Solver::unwatch387,16775
    Solver(Solver::Solver395,16964
    lbool   value(Solver::value425,18103
    lbool   value(Solver::value426,18160
    int     nAssigns Solver::nAssigns428,18261
    int     nLiterals(Solver::nLiterals429,18314
    int     nClauses Solver::nClauses430,18365
    int     nLearnts Solver::nLearnts431,18442
    SolverStats stats;Solver::stats435,18574
    int     nVars Solver::nVars440,18682
    void    addUnit(Solver::addUnit441,18736
    void    removeClause(Solver::removeClause445,18955
    void    freeze(Solver::freeze447,19070
    void    thaw Solver::thaw448,19115
    bool    okay(Solver::okay452,19184
    bool    solve(Solver::solve455,19312
    double      progress_estimate;Solver::progress_estimate457,19378
    vec<lbool>  model;Solver::model458,19436
    int         verbosity;Solver::verbosity459,19538
    void touch(Solver::touch463,19669
    void touch(Solver::touch464,19750
    bool updateOccur(Solver::updateOccur465,19791
#define L_IND 494,20861
#define L_ind 495,20885
#define L_LIT 496,20938
#define L_lit(497,20963
  inline void check(501,21107
  #define check 503,21162
macro void dump(507,21194
macro void dump(513,21428
macro void dump(520,21700
macro void dump(526,21943

Solver.h,1551
#define Solver_h21,1296
class Solver 30,1497
    MiniSat ::Solver*    minisat;Solver::minisat31,1512
    SatELite::Solver*    satelite;Solver::satelite32,1546
    GlueMiniSat::Solver* glueminisat;Solver::glueminisat33,1581
    BasicSolverStats     basicStats;Solver::basicStats35,1620
    bool                 dummyOK;Solver::dummyOK36,1657
    GlueMiniSat::Lit lit2lit(Solver::lit2lit38,1692
    void vec2vec(Solver::vec2vec41,1800
    lbool lbool2lbool(Solver::lbool2lbool45,1966
    bool& ok_ref(Solver::ok_ref56,2251
    BasicSolverStats& stats_ref Solver::stats_ref66,2913
    int assigns(Solver::assigns74,3181
    int trail_size(Solver::trail_size81,3470
    Lit trail(Solver::trail88,3736
    void setVerbosity(Solver::setVerbosity95,4087
    Var newVar(Solver::newVar120,5913
    bool addClause(Solver::addClause128,6256
    bool addUnit(Solver::addUnit139,6653
    void freeze(Solver::freeze146,6927
    void suggestPolarity(Solver::suggestPolarity152,7053
    bool solve(Solver::solve157,7266
    bool solve(Solver::solve173,7931
    lbool model(Solver::model177,8116
    bool varElimed(Solver::varElimed184,8366
    int ucore_vars(Solver::ucore_vars190,8505
    int ucore_varsSize(Solver::ucore_varsSize198,8696
    int ucore_clauses(Solver::ucore_clauses206,8887
    int ucore_clausesSize(Solver::ucore_clausesSize214,9087
    bool okay(Solver::okay222,9287
    int nVars(Solver::nVars229,9508
    void exportCnf(Solver::exportCnf232,9645
    Solver(Solver::Solver253,10705

SolverTypes.h,997
#define SolverTypes_h28,1558
typedef int Var;40,1865
#define var_Undef 41,1882
class Lit 44,1907
    int     x;Lit::x45,1919
    Lit(Lit::Lit47,1942
    explicit Lit(Lit::Lit48,2013
inline Lit operator ~ operator ~59,2332
inline bool sign 60,2398
inline int  var 61,2443
inline int  index(62,2489
inline Lit  toLit(63,2627
inline bool operator == operator ==64,2682
inline bool operator < operator <65,2754
macro uint64 abstLit(70,3005
#define L_LIT 74,3178
#define L_lit(75,3203
struct BasicSolverStats 79,3345
    int64   starts,BasicSolverStats::starts80,3371
    int64   starts, decisions,BasicSolverStats::decisions80,3371
    int64   starts, decisions, propagations,BasicSolverStats::propagations80,3371
    int64   starts, decisions, propagations, inspects,BasicSolverStats::inspects80,3371
    int64   starts, decisions, propagations, inspects, conflicts;BasicSolverStats::conflicts80,3371
    BasicSolverStats(BasicSolverStats::BasicSolverStats81,3437

VarOrder.h,630
#define VarOrder_h28,1622
struct VarOrder_lt 36,1788
    const vec<double>&  activity;37,1809
    bool operator 38,1843
    VarOrder_lt(39,1917
class VarOrder 42,1982
    const vec<int>&     assigns;VarOrder::assigns43,1999
    const vec<double>&  activity;VarOrder::activity44,2087
    Heap<VarOrder_lt>   heap;VarOrder::heap45,2173
    double              random_seed;VarOrder::random_seed46,2203
    vec<char>           dvars;VarOrder::dvars49,2293
    VarOrder(VarOrder::VarOrder51,2325
void VarOrder::newVar(62,2848
void VarOrder::update(71,3015
void VarOrder::undo(78,3100
Var VarOrder::select(85,3194

ADTs/FEnv.C,264
namespace FEnv 22,1298
    vec<NodeData>       nodes;FEnv::nodes23,1315
    Map<FEnv::Map24,1346
    Map<NodeData, int>  uniqueness_table;FEnv::uniqueness_table24,1346
    vec<int>            stack;FEnv::stack26,1389
bool eval(34,1533
bool eval(73,2802

ADTs/File.C,175
void File::open(23,1299
void File::open(35,1598
void File::close(67,2514
void File::seek(78,2686
int64 File::tell(92,3053
void putUInt(105,3328
uint64 getUInt(138,4334

ADTs/Global.C,103
char* vnsprintf(26,1356
char* nsprintf(48,1870
macro bool hasChar(59,2137
void splitString(63,2257

ADTs/FEnv.h,4539
#define FEnv_h21,1294
#define ENV 26,1412
#define FML 27,1429
#define UNDEF_INDEX 28,1449
enum Op 32,1511
enum Op { op_And,32,1511
enum Op { op_And, op_Equiv 32,1511
class FML 37,1696
    unsigned  data;FML::data38,1708
    FML(FML::FML40,1736
    FML(FML::FML41,1770
    operator unsigned(FML::operator unsigned43,1936
namespace ENV 48,2092
    struct NodeData ENV::NodeData49,2108
        unsigned data0;ENV::NodeData::data050,2130
        unsigned data1;ENV::NodeData::data151,2154
        unsigned data2;ENV::NodeData::data252,2178
        NodeData(ENV::NodeData::NodeData54,2203
        unsigned hash(ENV::NodeData::hash56,2365
        bool operator == ENV::NodeData::operator ==57,2459
    extern vec<NodeData>       nodes;ENV::nodes60,2603
    extern Map<ENV::Map61,2641
    extern Map<NodeData, int>  uniqueness_table;ENV::uniqueness_table61,2641
macro bool operator == operator ==66,2794
macro bool operator != operator !=67,2871
macro bool operator < operator <68,2948
template<> struct Hash<Hash69,3025
template<> struct Hash<FML> { unsigned operator () Hash::operator ()69,3025
macro FML   neg 71,3118
macro FML   unsign(72,3188
macro FML   id 73,3259
macro bool  sign 75,3350
macro bool  compo 76,3411
macro int   index 77,3472
macro int   sindex(78,3533
macro FML FormulaC(80,3595
macro FML FormulaA(81,3680
namespace ENV 82,3765
    macro FML Comp_new(ENV::Comp_new83,3781
    macro FML Atom_new(ENV::Atom_new84,3870
#define tag_Atom 90,4080
#define tag_Bin 92,4109
#define tag_ITE 93,4128
#define tag_FA 94,4147
#define tag_ITEn 95,4166
#define tag_ITEp 96,4220
macro int ctag(98,4266
macro int ctag(99,4342
macro int tag 100,4418
macro bool Atom_p(102,4487
macro bool Bin_p 103,4534
macro bool ITE_p 104,4589
macro bool FA_p 105,4644
macro bool ITEn_p 106,4698
macro bool ITEp_p 107,4755
macro Op   op 110,4913
macro FML  left 111,4990
macro FML  right 112,5075
macro FML  cond 113,5160
macro FML  tt 114,5245
macro FML  ff 115,5330
macro bool isCarry(116,5415
macro FML  FA_x 117,5494
macro FML  FA_y 118,5579
macro FML  FA_c 119,5664
macro ENV::NodeData Bin_newData(123,5851
macro ENV::NodeData ITE_newData(132,6142
macro ENV::NodeData ITEn_newData(141,6431
macro ENV::NodeData ITEp_newData(150,6722
macro ENV::NodeData FA_newData(160,7014
namespace ENV 170,7385
    macro FML new_helper(ENV::new_helper171,7401
    macro FML newS_helper(ENV::newS_helper176,7575
macro FML Bin_new 185,7874
macro FML Bin_newS(188,8115
macro FML ITE_new 190,8231
macro FML ITE_newS(193,8464
macro FML ITEn_new 195,8575
macro FML ITEn_newS(198,8811
macro FML ITEp_new 200,8924
macro FML ITEp_newS(203,9160
macro FML FA_new 205,9273
macro FML FA_newS(208,9547
#define atom_Undef 212,9788
#define atom_True 213,9812
const FML _undef_ 215,9837
const FML _error_ 216,9891
const FML _1_ 217,9945
const FML _0_ 218,9999
macro bool Exeception_p(221,10086
macro bool Exeception_p(222,10156
macro bool Const_p 223,10226
macro bool Const_p 224,10295
macro bool Var_p 225,10364
macro bool Var_p 226,10425
macro Formula var(230,10525
namespace ENV 235,10685
    template <class T, bool sgn ENV::sgn236,10701
        typedef FML Key;ENV::Key238,10782
        typedef T   Datum;ENV::Datum239,10807
namespace ENV 245,11052
    template <class T, bool sgn ENV::sgn246,11068
        typedef FML Key;ENV::Key250,11178
        typedef T   Datum;ENV::Datum251,11203
    template <class T, bool sgn ENV::sgn258,11590
        typedef FML Key;ENV::Key263,11721
        typedef T   Datum;ENV::Datum264,11746
#define AMap 270,11952
#define CMap 271,11979
#define FMap 272,12006
macro Formula operator ~ operator ~276,12135
macro Formula operator & operator &279,12196
macro Formula operator | operator |291,12540
macro Formula operator ^ operator ^294,12616
macro Formula operator &= operator &=307,12975
macro Formula operator |= operator |=308,13047
macro Formula operator ^= operator ^=309,13119
macro Formula FAs(312,13193
macro Formula FAc(332,13740
macro Formula ITE(356,14334
macro Formula ITEp(380,15066
macro Formula ITEn(381,15149
namespace FEnv 388,15385
    extern vec<int> stack;FEnv::stack389,15402
    macro void clear(FEnv::clear390,15429
    macro void push(FEnv::push391,15497
    macro void pop(FEnv::pop392,15550
    macro void keep(FEnv::keep396,15697
    macro int  topSize(FEnv::topSize397,15737
#undef ENV404,15952
#undef FML405,15963
#undef UNDEF_INDEX406,15974

ADTs/File.h,1163
#define File_h21,1294
#define lseek64 27,1372
#define open64 28,1451
#define File_BufSize 35,1654
enum FileMode 37,1763
enum FileMode { READ,37,1763
enum FileMode { READ, WRITE 37,1763
class File 42,1863
    int         fd;File::fd43,1876
    FileMode    mode;File::mode44,1935
    uchar*      buf;File::buf45,1986
    int         size;File::size46,2039
    int         pos;File::pos47,2129
    bool        own_fd;File::own_fd48,2187
    #define DEFAULTS 51,2296
    File(File::File52,2379
    File(File::File54,2409
    File(File::File57,2510
    #undef DEFAULTS59,2586
   ~File(File::~File61,2607
    bool null(File::null68,2906
    int releaseDescriptor(File::releaseDescriptor71,3000
    FileMode getMode(File::getMode77,3228
    void setMode(File::setMode80,3281
    int getCharQ(File::getCharQ91,3561
    int putCharQ(File::putCharQ102,3968
    int getChar(File::getChar111,4286
    int putChar(File::putChar115,4382
    bool eof(File::eof119,4484
    void flush(File::flush128,4742
macro uint64 encode64(144,5134
macro int64  decode64(145,5250
macro void   putInt 146,5364
macro uint64 getInt 147,5441

ADTs/Global.h,4895
#define Global_h27,1579
typedef INT64              int64;45,1909
typedef UINT64             uint64;46,1943
typedef INT_PTR            intp;47,1978
typedef UINT_PTR           uintp;48,2011
#define I64_fmt 49,2045
typedef long long          int64;51,2074
typedef unsigned long long uint64;52,2108
typedef __PTRDIFF_TYPE__   intp;53,2143
typedef unsigned __PTRDIFF_TYPE__ uintp;54,2176
#define I64_fmt 55,2217
typedef signed char    schar;58,2247
typedef unsigned char  uchar;59,2277
typedef unsigned int   uint;60,2307
typedef unsigned long  ulong;61,2336
typedef const char     cchar;62,2366
typedef short          int16;63,2396
typedef unsigned short uint16;64,2426
typedef int            int32;65,2457
typedef unsigned       uint32;66,2487
#define LP64 70,2536
#define macro 73,2653
template<class T> macro T min(75,2682
template<class T> macro T max(76,2750
template <> struct STATIC_ASSERTION_FAILURE<STATIC_ASSERTION_FAILURE79,2868
#define TEMPLATE_FAIL 80,2921
#define PANIC(82,2978
#define Ping 83,3059
#define INITIALIZER(85,3155
#define FINALIZER(86,3324
#define elemsof(88,3494
macro void swp(91,3558
#define ___noreturn 97,3697
#define ___unused 98,3751
#define ___const 99,3803
#define ___format(100,3854
#define ___malloc 102,3993
#define ___malloc104,4051
#define ___noreturn107,4082
#define ___unused108,4102
#define ___const109,4120
#define ___format(110,4137
#define ___malloc111,4169
template<class T> macro T* xmalloc(123,4566
template<class T> macro T* xrealloc(128,4718
template<class T> macro void xfree(133,4892
macro char* Xstrdup(137,5012
#define xstrdup(142,5165
macro char* xstrndup(145,5249
macro double drand(157,5656
macro int irand(164,5884
macro double cpuTime(174,6112
macro double cpuTime(179,6242
struct Pair 191,6561
    Fst     fst;Pair::fst195,6629
    Snd     snd;Pair::snd196,6646
    Pair(Pair::Pair198,6664
    Pair(Pair::Pair199,6683
    Pair(Pair::Pair202,6790
    void split(Pair::split204,6866
inline bool operator == operator ==208,6979
inline bool operator < operator <212,7140
inline Pair<Fst, Snd> Pair_new(217,7327
struct Interval 223,7448
  Data  fst,Interval::fst225,7467
  Data  fst, snd;Interval::snd225,7467
  Interval(Interval::Interval227,7486
  Interval(Interval::Interval228,7507
  Interval(Interval::Interval231,7596
  void split(Interval::split233,7664
inline bool operator == operator ==240,7853
inline bool operator < operator <244,8008
inline Interval<Data> Interval_new(248,8137
class vec 293,9435
    T*  data;vec::data294,9447
    int sz;vec::sz295,9461
    int cap;vec::cap296,9473
    typedef int Key;vec::Key303,9585
    typedef T   Datum;vec::Datum304,9606
    vec(vec::vec307,9651
    vec(vec::vec308,9722
    vec(vec::vec309,9807
    vec(vec::vec310,9897
   ~vec(vec::~vec311,10041
    T*       release vec::release314,10164
    operator T* vec::operator T*315,10264
    operator const vec::operator const316,10351
    int      size vec::size319,10432
    void     shrink vec::shrink320,10486
    void     shrink_ vec::shrink_321,10605
    void     pop vec::pop322,10684
    void     clear_ vec::clear_326,10870
    void     capacity vec::capacity327,10921
    void     push vec::push330,10995
    void     push vec::push331,11096
    void     push_ vec::push_333,11288
    const T& last vec::last334,11350
    T&       last vec::last335,11412
    const T& operator [] vec::operator []339,11515
    T&       operator [] vec::operator []340,11615
    const T& operator [] vec::operator []342,11723
    T&       operator [] vec::operator []343,11791
    vec<T>&  operator = vec::operator =347,11911
             vec vec::vec348,11984
    void copyTo(vec::copyTo351,12086
    void moveTo(vec::moveTo352,12213
void vec<T>::grow(grow356,12365
void vec<T>::growTo(growTo363,12603
void vec<T>::growTo(growTo370,12788
void vec<T>::clear(clear377,12956
macro void xfreeAll(389,13345
class lbool 398,13574
    int     value;lbool::value399,13588
    explicit lbool(lbool::lbool400,13607
    lbool(lbool::lbool403,13657
    lbool(lbool::lbool404,13690
    int toInt(lbool::toInt405,13732
    bool  operator == lbool::operator ==407,13777
    bool  operator != lbool::operator !=408,13859
    lbool operator ~ lbool::operator ~409,13941
inline int   toInt 415,14125
inline lbool toLbool(416,14177
inline char  name 417,14228
const lbool l_True 419,14407
const lbool l_False 420,14442
const lbool l_Undef 421,14477
const lbool l_Error 422,14512
#define __SGI_STL_INTERNAL_RELOPS430,14814
template <class T> macro bool operator != operator !=431,14848
template <class T> macro bool operator > operator >432,14937
template <class T> macro bool operator <= operator <=433,15026
template <class T> macro bool operator >= operator >=434,15115

ADTs/Hash_standard.h,1666
#define Hash_standard_h21,1303
static int prime_twins[prime_twins28,1449
template <class K> struct Hash 35,1808
template <class K> struct Hash  { uint operator () Hash::operator ()35,1808
template <class K> struct Equal 36,1922
template <class K> struct Equal { bool operator () Equal::operator ()36,1922
template <class K> struct Hash_params 38,2039
    static uint hash Hash_params::hash39,2079
    static bool equal(Hash_params::equal40,2152
#define DefineHash(51,2485
#define DefineEqual(52,2596
template <class S, class T> struct Hash <Pair<S,T> > { uint operator () operator ()57,2732
template <class S, class T> struct Equal<Pair<S,T> > { bool operator () operator ()58,2912
template <class S> struct Hash 62,3133
template <class S> struct Hash <Interval<S> > { uint operator () Hash::operator ()62,3133
template <class S> struct Equal<Equal63,3271
template <class S> struct Equal<Interval<S> > { bool operator () Equal::operator ()63,3271
template <class K> struct Hash<Hash69,3448
template <class K> struct Hash<const K*> { uint operator () Hash::operator ()69,3448
template <class K> struct Hash<Hash70,3616
template <class K> struct Hash<K*>       { uint operator () Hash::operator ()70,3616
template <class K> struct Hash<Hash72,3790
template <class K> struct Hash<const K*> { uint operator () Hash::operator ()72,3790
template <class K> struct Hash<Hash73,3914
template <class K> struct Hash<K*>       { uint operator () Hash::operator ()73,3914
DefineHash (const char*, uint v = 0; for (int i = 0; key[i] != '\0'; i++) v 78,4061
DefineHash (char*, uint v = 0; for (int i = 0; key[i] != '\0'; i++) v 80,4263

ADTs/Heap.h,813
#define __HEAP__21,1296
static inline int left 23,1314
static inline int right(24,1364
static inline int parent(25,1418
class Heap 28,1487
    C        comp;Heap::comp30,1509
    vec<int> heap;Heap::heap31,1528
    vec<int> indices;Heap::indices32,1567
    inline void percolateUp(Heap::percolateUp34,1615
    inline void percolateDown(Heap::percolateDown46,1931
    bool ok(Heap::ok60,2373
    Heap(Heap::Heap63,2448
    void setBounds Heap::setBounds65,2492
    bool inHeap Heap::inHeap66,2569
    void increase Heap::increase67,2642
    bool empty Heap::empty68,2735
    void insert(Heap::insert70,2795
    int  getmin(Heap::getmin77,2939
    int  peekmin(Heap::peekmin88,3203
    bool heapProperty(Heap::heapProperty90,3247
    bool heapProperty(Heap::heapProperty91,3303

ADTs/Int.h,2798
#define Int_h21,1293
struct Exception_IntOverflow 28,1431
    char* where;29,1462
    Exception_IntOverflow(30,1479
#define Int_Max__ 41,1815
#define Int_Min__ 42,1857
#define Int_Undef__ 43,1890
#define A1 47,2031
#define A2 48,2071
class Int 53,2327
    int64   data;Int::data54,2339
    Int(Int::Int56,2365
    Int(Int::Int57,2398
    Int(Int::Int58,2428
    uint hash(Int::hash62,2563
    bool operator == Int::operator ==64,2632
    bool operator != Int::operator !=65,2704
    bool operator < Int::operator <66,2776
    bool operator > Int::operator >67,2848
    bool operator <= Int::operator <=68,2920
    bool operator >= Int::operator >=69,2992
    Int  operator & Int::operator &71,3065
    Int& operator >>= Int::operator >>=72,3141
    Int  operator - Int::operator -74,3204
    Int& operator ++ Int::operator ++75,3268
    Int& operator -= Int::operator -=76,3335
    Int& operator += Int::operator +=77,3414
    Int& operator *= Int::operator *=78,3493
    Int& operator /= Int::operator /=79,3572
    Int  operator + Int::operator +80,3651
    Int  operator - Int::operator -81,3727
    Int  operator * Int::operator *82,3803
    Int  operator / Int::operator /83,3879
    Int  operator % Int::operator %84,3955
#define Int_MAX 91,4317
#define Int_MIN 92,4348
#undef A194,4380
#undef A295,4390
#define A1 108,4795
#define A2 109,4824
#define Int_MIN 113,4979
#define Int_MAX 114,5011
class Int 117,5044
    mpz_t*  data;Int::data118,5056
    bool small(Int::small120,5281
    Int(Int::Int125,5408
    Int(Int::Int127,5484
    Int(Int::Int132,5593
    Int(Int::Int137,5717
   ~Int(Int::~Int145,5933
    Int& operator = Int::operator =152,6050
    bool operator == Int::operator ==173,6729
    bool operator < Int::operator <180,6960
    bool operator != Int::operator !=197,7532
    bool operator >= Int::operator >=198,7608
    bool operator > Int::operator >199,7683
    bool operator <= Int::operator <=200,7755
    Int  operator + Int::operator +204,7900
    Int  operator - Int::operator -205,8016
    Int  operator * Int::operator *206,8132
    Int  operator / Int::operator /207,8248
    Int  operator % Int::operator %208,8364
    Int& operator += Int::operator +=210,8481
    Int& operator -= Int::operator -=211,8581
    Int& operator *= Int::operator *=212,8681
    Int& operator /= Int::operator /=213,8781
    Int& operator %= Int::operator %=214,8881
    Int& operator ++ Int::operator ++215,8981
    Int& operator -- Int::operator --216,9033
    Int operator - Int::operator -218,9086
    Int add(Int::add226,9336
    Int  operator & Int::operator &238,9587
    Int& operator >>= Int::operator >>=239,9700
    uint hash(Int::hash258,10325

ADTs/Map.h,186
#define Map_h27,1464
    typedef K Key;115,3972
    typedef D Datum;116,3991
    Map<K,D,Par>& operator = operator =129,4483
    #define SEARCH(157,5684
    #undef SEARCH247,8624

ADTs/Sort.h,748
#define Sort_h29,1639
struct LessThan_default 38,1798
    bool operator () LessThan_default::operator ()39,1824
struct LessThan_reverse 43,1896
    bool operator () LessThan_reverse::operator ()44,1922
void selectionSort(52,2114
template <class T> static inline void selectionSort(66,2466
void sort(71,2634
template <class T, class LessThan> void sort(95,3218
template <class T> static inline void sort(97,3358
void sortUnique(102,3508
template <class T> static inline void sortUnique(121,3843
template <class T, class LessThan> void sort(129,4088
template <class T> void sort(131,4192
template <class T> void sortr(133,4272
template <class T, class LessThan> void sortUnique(137,4355
template <class T> void sortUnique(143,4577

ADTs/StackAlloc.h,274
#define StackAlloc_h21,1300
struct Allocator 27,1442
template<class T, int cap=37,1672
template<class T, int cap,61,2403
T* StackAlloc<T,cap,lim>::alloc_helper(alloc_helper62,2439
template<class T, int cap,79,3013
void StackAlloc<T,cap,lim>::freeAll(freeAll80,3049

ADTs/VecAlloc.h,65
#define VecAlloc_h2,19
template <class T, int chunk_size 8,161

ADTs/VecMaps.h,1469
#define VecMaps_h21,1297
class BitMap 28,1493
    vec<unsigned>   v;BitMap::v29,1508
    bool            bool_null;BitMap::bool_null30,1531
    unsigned word(BitMap::word32,1563
    unsigned mask(BitMap::mask33,1644
    typedef int  Key;BitMap::Key35,1740
    typedef bool Datum;BitMap::Datum36,1762
    BitMap(BitMap::BitMap38,1787
    BitMap(BitMap::BitMap39,1845
    BitMap(BitMap::BitMap40,1903
    bool at(BitMap::at42,2025
    void set(BitMap::set46,2208
    void clear(BitMap::clear53,2486
class VecMap 58,2546
    vec<T>  v;VecMap::v59,2561
    T       T_null;VecMap::T_null60,2576
    typedef int Key;VecMap::Key63,2605
    typedef T   Datum;VecMap::Datum64,2626
    VecMap(VecMap::VecMap66,2650
    VecMap(VecMap::VecMap67,2721
    VecMap(VecMap::VecMap68,2792
    T at(VecMap::at70,2864
    void set(VecMap::set74,3030
    void clear(VecMap::clear78,3192
struct VecMap<VecMap82,3244
    VecMap(VecMap::VecMap83,3275
    VecMap(VecMap::VecMap84,3340
    VecMap(VecMap::VecMap85,3405
class DeckMap 90,3494
    VecMap<T>   pos,DeckMap::pos91,3510
    VecMap<T>   pos, neg;DeckMap::neg91,3510
    typedef int Key;DeckMap::Key94,3545
    typedef T   Datum;DeckMap::Datum95,3566
    DeckMap(DeckMap::DeckMap97,3590
    DeckMap(DeckMap::DeckMap98,3671
    DeckMap(DeckMap::DeckMap99,3752
    T at(DeckMap::at101,3834
    void set(DeckMap::set104,3939
    void clear(DeckMap::clear107,4057