;; Object MainSolver/
;; SEMANTICDB Tags save file
(semanticdb-project-database-file "MainSolver/"
  :tables (list 
   (semanticdb-table "MainSolver.h"
    :major-mode 'c-mode
    :tags '(("MAINSOLVER_H" variable (:constant-flag t) nil [22 60]) ("Interface/AnalyzerData.h" include (:system-flag t) nil [59 94]) ("../Basics.h" include nil nil [96 118]) ("InstanceGraph/InstanceGraph.h" include nil nil [119 159]) ("FormulaCache.h" include nil nil [161 186]) ("viewStateT" type (:typedef ("unsigned char") :superclasses "unsigned char" :type "typedef") nil [339 372]) ("NIL" variable (:constant-flag t :default-value (nil)) nil [373 389]) ("IN_SUP_COMP" variable (:constant-flag t :default-value (nil)) nil [390 414]) ("SEEN" variable (:constant-flag t :default-value (nil)) nil [415 431]) ("IN_OTHER_COMP" variable (:constant-flag t :default-value (nil)) nil [432 458]) ("retStateT" type (:members (("EXIT" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [478 483]) ("RESOLVED" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [485 494]) ("PROCESS_COMPONENT" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [496 515])) :type "enum") nil [460 516]) ("retIBCPT" type (:members (("NOTHING_FOUND" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [536 550]) ("FOUND" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [552 558]) ("CONTRADICTION" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [560 574])) :type "enum") nil [519 577]) ("CMainSolver" type (:superclasses ("CInstanceGraph") :members (("decStack" variable (:type ("CDecisionStack" type (:type "class") nil nil)) (reparse-symbol classsubparts) [630 654]) ("stopWatch" variable (:type ("CStopWatch" type (:type "class") nil nil)) (reparse-symbol classsubparts) [689 712]) ("xFormulaCache" variable (:type ("CFormulaCache" type (:type "class") nil nil)) (reparse-symbol classsubparts) [722 750]) ("bcpImplQueue" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [756 787]) ("lastTimeCClDeleted" variable (:type "int") (reparse-symbol classsubparts) [810 833]) ("lastCClCleanUp" variable (:type "int") (reparse-symbol classsubparts) [837 856]) ("remPoll" variable (:type "unsigned int") (reparse-symbol classsubparts) [864 885]) ("backTrack" function (:prototype-flag t :type ("retStateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [893 915]) ("removeAllCachePollutions" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [1052 1084]) ("findVSADSDecVar" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1118 1137]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1138 1169])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1097 1170]) ("decide" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1179 1193]) ("bcp" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1201 1212]) ("handleSolution" function (:type "void") (reparse-symbol classsubparts) [1222 1671]) ("resolveConflict" function (:prototype-flag t :type ("retStateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1679 1707]) ("countSAT" function (:prototype-flag t :type ("SOLVER_StateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1719 1744]) ("performPreProcessing" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1756 1784]) ("makeCompIdFromActGraph" function (:prototype-flag t :arguments (("rComp" variable (:type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1985 2005])) :type "void") (reparse-symbol classsubparts) [1957 2006]) ("componentSearchStack" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2048 2084]) ("recordRemainingComps" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2093 2121]) ("getComp" function (:prototype-flag t :arguments (("theVar" variable (:constant-flag t :type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2142 2163]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2186 2216]) ("lookUpCls" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2225 2248]) ("lookUpVars" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2256 2280])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2129 2281]) ("printComponent" function (:prototype-flag t :arguments (("rComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2338 2364])) :type "void") (reparse-symbol classsubparts) [2318 2365]) ("assignVal" function (:typemodifiers ("inline") :arguments (("rLitId" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2403 2428]) ("ant" variable (:default-value "AntecedentT(NOT_A_CLAUSE)" :type ("AntecedentT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2429 2472])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2381 2561]) ("BCP" function (:prototype-flag t :arguments (("thePairsOfImpl" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2578 2612])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2569 2613]) ("private" label nil (reparse-symbol classsubparts) [2753 2761]) ("theQueue" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2770 2798]) ("ca_1UIPClause" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2809 2842]) ("ca_lastUIPClause" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2850 2886]) ("imaxDecLev" variable (:type "int") (reparse-symbol classsubparts) [2903 2918]) ("caIncludeCauses" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3039 3057]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3058 3076])) :type "void") (reparse-symbol classsubparts) [3018 3077]) ("caIncorporateLit" function (:prototype-flag t :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3110 3132]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3133 3151])) :type "void") (reparse-symbol classsubparts) [3088 3152]) ("caAddtoCauses" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3179 3197]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3198 3216])) :type "void") (reparse-symbol classsubparts) [3160 3217]) ("caInit" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3364 3400]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3401 3419])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3352 3420]) ("caGetCauses_lastUIP" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3453 3489])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3428 3490]) ("caGetCauses_firstUIP" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3520 3556])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3494 3557]) ("caGetPrev1UIPCCl" function (:constant-flag t :type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3799 3881]) ("caGetPrevLastUIPCCl" function (:constant-flag t :type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3885 3973]) ("getMaxDecLevFromAnalysis" function (:type "int") (reparse-symbol classsubparts) [4156 4213]) ("create1UIPCCl" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [4313 4393]) ("createLastUIPCCl" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [4401 4487]) ("implicitBCP" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5175 5194]) ("createAntClauseFor" function (:prototype-flag t :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5229 5251])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5205 5252]) ("prep_IBCP" function (:prototype-flag t :arguments (("impls" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5622 5647])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5607 5648]) ("prepFindHiddenBackBoneLits" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5754 5788]) ("prepBCP" function (:prototype-flag t :arguments (("firstLit" variable (:default-value "NOT_A_LIT)" :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [6035 6067])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [6022 6068]) ("printUnitClauses" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [6207 6231]) ("public" label nil (reparse-symbol classsubparts) [6238 6245]) ("CMainSolver" function (:prototype-flag t :constructor-flag t :type ("CMainSolver" type "class")) (reparse-symbol classsubparts) [6277 6291]) ("CMainSolver" function (:prototype-flag t :destructor-flag t :type "void") (reparse-symbol classsubparts) [6325 6340]) ("solve" function (:prototype-flag t :arguments (("lpstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [6360 6386])) :type "void") (reparse-symbol classsubparts) [6349 6387]) ("setTimeBound" function (:arguments (("i" variable (:type "long int") (reparse-symbol arg-sub-list) [6414 6425])) :type "void") (reparse-symbol classsubparts) [6396 6468])) :type "class") nil [581 6472]))
    :file "MainSolver.h"
    :pointmax 6503
    :unmatched-syntax 'nil
    )
   (semanticdb-table "MainSolver.cpp"
    :major-mode 'c++-mode
    :tags '(("MainSolver.h" include nil nil [1 24]) ("CMainSolver" function (:constructor-flag t :parent "CMainSolver" :type ("CMainSolver" type "class")) nil [70 189]) ("CMainSolver" function (:destructor-flag t :parent "CMainSolver" :type "void") nil [211 292]) ("performPreProcessing" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [296 1080]) ("solve" function (:parent "CMainSolver" :arguments (("lpstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [1106 1132])) :type "void") nil [1082 2618]) ("countSAT" function (:parent "CMainSolver" :type ("SOLVER_StateT" type (:type "class") nil nil)) nil [2621 3225]) ("findVSADSDecVar" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3263 3282]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3283 3314])) :type ("bool" type (:type "class") nil nil)) nil [3229 3927]) ("decide" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [3930 5504]) ("removeAllCachePollutions" function (:parent "CMainSolver" :type "void") nil [5506 6634]) ("backTrack" function (:parent "CMainSolver" :type ("retStateT" type (:type "class") nil nil)) nil [6636 7973]) ("bcp" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [7977 8899]) ("resolveConflict" function (:parent "CMainSolver" :type ("retStateT" type (:type "class") nil nil)) nil [8902 10619]) ("recordRemainingComps" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [10762 12132]) ("getComp" function (:parent "CMainSolver" :arguments (("theVar" variable (:constant-flag t :type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12163 12184]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12207 12237]) ("lookUpCls" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12245 12268]) ("lookUpVars" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12277 12301])) :type ("bool" type (:type "class") nil nil)) nil [12137 16045]) ("makeCompIdFromActGraph" function (:parent "CMainSolver" :arguments (("rComp" variable (:type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [16226 16246])) :type "void") nil [16185 17052]) ("printComponent" function (:parent "CMainSolver" :arguments (("rComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [17088 17114])) :type "void") nil [17055 17250]) ("BCP" function (:parent "CMainSolver" :arguments (("thePairsOfImpl" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [17326 17360])) :type ("bool" type (:type "class") nil nil)) nil [17304 20632]) ("createAntClauseFor" function (:parent "CMainSolver" :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [20672 20694])) :type ("bool" type (:type "class") nil nil)) nil [20635 21562]) ("implicitBCP" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [21564 24929]) ("caIncludeCauses" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [25192 25210]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [25211 25229])) :type "void") nil [25158 26026]) ("caAddtoCauses" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26219 26237]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26238 26256])) :type "void") nil [26187 26447]) ("caIncorporateLit" function (:parent "CMainSolver" :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26484 26506]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26507 26525])) :type "void") nil [26449 26934]) ("caInit" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26961 26997]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26998 27016])) :type ("bool" type (:type "class") nil nil)) nil [26936 27787]) ("caGetCauses_lastUIP" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [27827 27863])) :type ("bool" type (:type "class") nil nil)) nil [27789 28337]) ("caGetCauses_firstUIP" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [28379 28415])) :type ("bool" type (:type "class") nil nil)) nil [28340 29216]) ("prep_IBCP" function (:parent "CMainSolver" :arguments (("impls" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [29660 29685])) :type ("bool" type (:type "class") nil nil)) nil [29632 30046]) ("prepFindHiddenBackBoneLits" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [30048 31197]) ("prepBCP" function (:parent "CMainSolver" :arguments (("firstLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [31225 31245])) :type ("bool" type (:type "class") nil nil)) nil [31199 35099]) ("printUnitClauses" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [35289 35605]))
    :file "MainSolver.cpp"
    :pointmax 35606
    )
   (semanticdb-table "FormulaCache.h"
    :major-mode 'c-mode
    :tags 'nil
    :file "FormulaCache.h"
    )
   )
  :file "semantic.cache"
  :semantic-tag-version "2.0beta3"
  :semanticdb-version "2.0beta3"
  )