!{8eQ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                  ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9:;<=>?@ABCDEFGHIJKLMNOPSafejk{QRSTUVWXSafe%;=jk)miosCNF expressionmios<class of objects that can be interpeted as a bool expressionmios?the start index for the generated variables by Tseitin encodingmios'returns the number of variables in the mios%returns the number of clauses in the Ymios return a clause: list only if it contains some real clause (not a literal)Zmiosreturns the number of valiable used as the output of this expression. and returns itself it the expression is a literal. Otherwise the number is a integer larger than  . Therefore &1 + max tseitinBase the-returned-value) is the next literal variable for future.miosdisjunction constructorasList $ "3" -|- "4"[[3,4,-5],[-3,5],[-4,5]]asList (("3" -|- "4") -|- "-1")/[[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]] miosconjunction constructorasList $ "3" -&- "-2"[[-3,2,4],[3,-4],[-2,-4]]asList $ "3" -|- ("1" -&- "2")0[[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]] mios negate a formasList $ neg ("1" -|- "2")&[[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]] miosequal on BoolForm miosnegation on BoolForm miosimplication as a short cutasList ("1" ->- "2")&[[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]miosmerge [BoolForm] by '(-|-)'mios an alias of miosmerge [BoolForm] by '(-&-)'mios an alias of mios converts a BoolForm to "[[Int]]"mios,converts a *satisfied* BoolForm to "[[Int]]"mios"make latex string from CNF, using asLatex $ "3" -|- "4"C"\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"mios"make latex string from CNF, using   Safejk/[miosparse a non-signed integer\miosparse a (signed) integer]mios+return integer list that terminates at zero^mios#top level interface for parsing CNFmios;read a minisat output: ((numbefOfVariables, 0), [Literal])fromFile "result"((3, 0), [1, -2, 3])miosreturn clauses as [[Int]] from file$clauseListFromMinisatOutput "result"[1,-2,3]Safejk:_ _miosparse a non-signed integer`miosparse a (signed) integeramios0Parse something like: p FORMAT VARIABLES CLAUSESbmios=Parse something like: c This in an example of a comment line.cmiosParse the preamble partdmios+return integer list that terminates at zeroemios%Parse something like: 1 -2 0 4 0 -3 0fmios#top level interface for parsing CNFgmios(driver:: String -> Either ParseError Int miosNread a CNF file and return: ((numbefOfVariables, numberOfClauses), [Literal])fromFile "acnf",((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]!miosreturn clauses as [[Int]] from fileclauseListFromFile "a.cnf"#[[1, 2], [-2, 3], [-1, 2, -3], [3]] ! !Safejk@"miosWrite the DIMACS to file f, using ##mios1Convert [Clause] to String, where Clause is [Int]toDIMACSString [] "p cnf 0 0\n""toDIMACSString [[-1, 2], [-3, -4]]"p cnf 4 2\n-1 2 0\n-3 -4 0\n"/toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]],"p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"$mios converts [[Int]] to a String%mios converts [[Int]] to a LaTeX expression"#$%"#$%SafejkA&miosString from BoolFrom'miosString from BoolFrom  !"#&' !"#&' Trustworthy ;<=>?AFTjkV(miosStack of Int, an alias of Vec Int)miosInterface on stacks*miosreturns a new stack.+mios(pushs an value to the tail of the stack.,miospops the last element.-miospeeks the last element..miosshrinks the stack./miosMutable Double0mios Mutable Int Note: Int' is identical to (1mios Mutable Bool2mios5Interface for single (one-length vector) mutable data3mios"allocates and returns an new data.4miosgets the value.5miossets the value.6mioscalls an update function on it.hmios0A thin abstract layer for mutable unboxed Vector7miosAnother abstraction layer on Vector0 which reserves zero element for internal use. Note+: If you want to use the 0-th element, use  UVector Int.8miosThe interface on vectors.9mios returns the n -th value.:mios sets the n -th value.;mioserases all elements in it.<mios returns the nF-th value (index starts from zero in any case). | swaps two elements.=mioscalls the update function.>miosreturns a new vector.?miossets all elements.@miosextends the size of stack by n8; note: values in new elements aren't initialized maybe.Amiosconverts to a list.Dmios%returns the number of allocated slotsEmiosreturns a new ( from [Int].Fmios5sort the content of a stack, in small-to-large order.()*+,-./01263457CB8;A9:<=>?@DEF8;A9:<=>?@7CB263451/0)*+,-.(EDFSafeejk5Nmiosformats of state dumpSmios stat indexTmiosthe number of backjumpUmiosthe number of restartVmiosthe number of blacking startWmiosthe number of classic restartXmiosthe number of propagationYmiosthe number of reductionZmiosthe number of alive given clauses[miosthe number of alive learnt clauses\miosthe number of alive variables]mios the number of assigned variables^miosDon't use this dummy._mios6Solver's parameters; random decision rate was dropped.amios decay rate for variable activitybmiosdecay rate for clause activitycmiosdump stats data during solvingdmiosthe coefficients for restartsemiosrestart expansion factorfmiosstatic Steps between restartsgmiosMisc information on a CNFimiosthe number of variablesjmiosthe number of clauseskmiosgiven filenamelmiosExponential Moving Average, EMAmmiosAssisting ADT for the dynamic variable ordering of the solver. The constructor takes references to the assignment vector and the activity vector of the solver. The method select@ will return the unassigned variable with the highest activity.nmios;should be called when a variable has increased in activity.omiosIshould be called when a variable becomes unbound (may be selected again).pmios3returns a new, unassigned var as the next decision.qmios)Lifted Boolean domain (p.7) that extends i with """ means  undefinedb design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.rmiosThe literal data has an indexZ method which converts the literal to a "small" integer suitable for array indexing. The varB method returns the underlying variable of the literal, and the sign- method if the literal is signed (False for x and True for -x).smios represents Var.tmiosthe type that Mios returns This captures the following three cases: * solved with a satisfiable assigment, * proved that it's an unsatisfiable problem, and * aborted due to Mios specification or an internal errorumiosabnormal termination flags|mios&terminate and find an SAT/UNSAT answermiosCONFLICT on the Lifted Bool domainmios UNDEFINED on the Lifted Bool domainmiosTRUE on the Lifted Bool domainmiosFALSE on the Lifted Bool domainmiosSpecial constant in s (p.7)mios/converts a usual Int as literal to an internal s presentation. int2var 1-1 -- the first literal is the first variable int2var 22 -- literal @2@ is variable 2 int2var (-2)02 -- literal @-2@ is corresponding to variable 2miosSpecial constant in r (p.7)miosreturns True if the literal is positivemiosnegates literal negateLit 23 negateLit 32 negateLit 45 negateLit 54mios converts r into s. lit2var 21 lit2var 31 lit2var 42 lit2var 52mios converts a s to the corresponing literal.var2lit 1 True2var2lit 1 False3var2lit 2 True4var2lit 2 False5mios converts  into r as lit2int . int2lit == id. int2lit 12 int2lit (-1)3 int2lit 24 int2lit (-2)5mios converts r into  as int2lit . lit2int == id. lit2int 21 lit2int 3-1 lit2int 42 lit2int 5-2mios$returns the value of a literal as a qmios>returns a new EMA from a flag (slow or fast) and a window sizemiosreturns an EMA valuemiosupdates an EMAmiosdafault configurationMinisat-1.14 uses (0.95, 0.999, 0.2 = 20 / 1000).Minisat-2.20 uses (0.95, 0.999, 0).Gulcose-4.0 uses (0.8 , 0.999, 0).Mios-1.2 uses (0.95, 0.999, 0).c()*+,-./01263457CB8;A9:<=>?@DEFNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Ht|}~uvwxyz{ghijk_`abcdefsrqmnoplSTUVWXYZ[\]^NOPQRSafejkUmiosconfiguration swithcesmiosdefault option settingsmiosdefinition of mios optionmiosgenerates help messagemiosbuilds MiosProgramOption$ from string given as command optionmiosbuilds MiosProgramOption from a Stringmios converts MiosProgramOption into SIHConfiguration!_`abcdef!_`abcdef  Trustworthy "#%;=>?DjkfmiosMutable  Vectormios Fig. 7.(p.11): normal, null (and binary) clause. This matches both of Clause and GClause in MiniSat.miosliterals and rankmiosanother metrics of this clausemiosXactivity of this clause , protected :: !Bool' -- ^ protected from reducemioscopies vec and return a new P. Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.mios/returns the rank, a goodness, of a given clausemiossets the rank of a given clausemiosreturns a new .mios is a  StackfamilyLon literals since literals in it will be discared if satisifed at level = 0.mios is a 2! on the number of literals in it.mios is a 8 of r.miosThe equality on  is defined with reallyUnsafePtrEquality.mios is a vector of .  Trustworthy "#%;=>?jk miosImmutable Vector of miosClause + Blocking LiteralmiosClause + Blocking LiteralmiosResizable vector of .mios!sets the expire flag to a clause.mios/returns the associated Int vector, which holds blocking literals.mios O(1) insertermiosn is the number of s, m. is default size of each watcher list. | For n2 vars, we need [0 .. 2 + 2 * n - 1] slots, namely  2 * (n + 1)'-length vector FIXME: sometimes n > 1Mmiosreturns the watcher List for Literal l.jmios/returns the associated Int vector, which holds blocking literals.mios is a mios is a ) on clauses.mios is a 2 on the number of clauses in it.mios is a collection of mios is a mios is a ) on clauses.mios is a 2 on the number of clauses in it.mios is an r-indexed collection of .  Trustworthy%jkmiosan immutable Vector of ClauseSimpleManagerkmios@biclause should be stored into index:0, so the real limit is 64.miosreturns a new lmiosreturns ' for caluses which have suitable sizes.miosnIf a nice candidate as a learnt is stored, return it. Otherwise allocate a new clause in heap then return it.mios9Note: only not-too-large and learnt clauses are recycled. Safe "#%NV^jk=mmiosA heap tree built from two 7]. This implementation is identical wtih that in Minisat-1.14. Note: the zero-th element of heapL is used for holding the number of elements. Note: VarHeap itself is not a VarOrder*, because it requires a pointer to solver.mios Fig. 2.(p.9) Internal State of the solvermiosList of problem constraints.miosList of learnt clauses.mioslist of constraint wathing p, literal-indexedmios,The current assignments indexed on variablesmios)The last assignments indexed on variablesmios*List of assignments in chronological ordermios3Separator indices for different decision levels in .mios4 is divided at qHead; assignment part and queue partmios8For each variable, the constraint that implied its valuemios5For each variable, the decision level it was assignedmios4For each variable, the number of depending decisions mios(Set of literals in the case of conflicts mios3Heuristic measurement of the activity of a variable mios*Keeps track of the dynamic variable order. miossearch paramerters miosnumber of variablesmios.Clause activity increment amount to bump with.mios0Variable activity increment amount to bump with.mios-Separates incremental and search assumptions.miosused in miosused in miosused in mios internal flagmiosused in miosused in miosused in mioslast decision level used in miosclause recyclermiosused in  and  to create a learnt clausemiosstatistics information holdermiosused in lbd computationmiosused in lbd computationmiosNumber of Assignments FastmiosNumber of Assignments Slow mios%Backjumped and Restart Dicision Level!miosConflicting Level"mios(Literal Block) Distance Fast#mios(Literal Block) Distance Slow$mios"next restart in number of conflict%miosincremented by blocking&miosaverage phase of restart'mios?returns an everything-is-initialized solver from the arguments.(mios)returns the number of current assigments.)mios,returns the number of constraints (clauses).*mios%returns the number of learnt clauses.+mios#returns the current decision level.,miosreturns the assignment (:: q =  [-1, 0, -1]) from s.-miosreturns the assignment (:: q =  [-1, 0, -1]) from r..miosFig. 7. (p.11) returns True- if the clause is locked (used as a reason). Learnt clauses only/miosreturns the value of S.0miossets to S.1mios(increments a stat data corresponding to S.2mios!returns the statistics as a list.3miosassigns a value to the n -th variable4mios Fig. 9 (p.14) Puts a new fact on the propagation queue, as well as immediately updating the variable's value in the assignment vector. If a conflict arises, FalseB is returned and the propagation queue is cleared. The parameter from3 contains a reference to the constraint from which p was propagated (defaults to Nothing if omitted).5miosFig. 12 (p.17) returns False if immediate conflict.Pre-condition: propagation queue is empty6miosE#M22: Revert to the states at given level (keeping all assignment at  but not beyond).nmios,returns the value on the root (renamed from getmin).7mios>Interfate to select a decision var based on variable activity.GSTUVWXYZ[\]^      !"#$%&'()*+,-./0123456G      !"#$%&'()*+,-.3456STUVWXYZ[\]^/012 Safe"#%jk`8mios7validates the assignment even if the implementation of / is wrong; we re-implement some functions here.omioschecks uniqueness of learnts88Safe"#%^jkZ9miosFig. 14 (p.19) Bumping of clause activity:miosFig. 14 (p.19)pmiosFig. 14 (p.19)qmios$value for rescaling clause activity.;miosFig. 14 (p.19)<miosFig. 14 (p.19)rmiosFig. 14 (p.19)smiosFig. 8. (p.12)^ create a new clause and adds it to watcher lists. Constructor function for clauses. Returns False' if top-level conflict is determined.  outClausec may be set to Null if the new clause is already satisfied under the current top-level assignment.Post-condition: psD is cleared. For learnt clauses, all literals will be false except lits[0] (this by design of the analyze method). For the propagation to work, the second watch must be put on the literal which will first be unbound by backtracking. (Note that none of the learnt-clause specific things needs to done for a user defined contraint type.) Left False if the clause is in a confilct Left True if the clause is satisfied Right clause' if the clause is enqueued successfully=miosreturns False~ if a conflict has occured. This function is called only before the solving phase to register the given clauses (not learnt).>mios2returns a POSIVITE value of Literal Block Distancetmios6returns a vector index of NDD for the nth bit of a varumios3returns a bit index of NDD for the nth bit of a varvmios updates a var's ndl, which is assigned by a  clause?miosupdates all assigned vars' ndl@miosreturns the NDLAmios62, 74, #91BmiosJprint statatistic data to stdio. This should be called after each restart. 9:;<=>?@AB ;<9:=>?@ABSafe "#%V^jkEwmios#114:  RemoveWatchxmiosFig. 8. (p.12)` creates a new LEARNT clause and adds it to watcher lists. This is a strippped-down version of  newClause in Solver.ymios Simplify.f At the top-level, a constraint may be given the opportunity to simplify its representation (returns Falsef) or state that the constraint is satisfied under the current assignment and can be removed (returns True). A constraint must not be simplifiable to produce unit information or to be conflicting; in that case the propagation has not been correctly defined.OMIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.zmiosM114: Fig. 10. (p.15)-analyze : (confl : Clause*) (out_learnt : vec Lit"&) (out_btlevel :: int&) -> [void]A__Description:_- Analzye confilct and produce a reason clause.Pre-conditions: *  out_learntW is assumed to be cleared. * Corrent decision level must be greater than root level.Post-conditions:8 * 'out_learnt[0]' is the asserting literal at level  out_btlevel. * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the rest of literals. There may be others from the same level though.analyze is invoked from search{mios#M114 Check if p can be removed, abstract_levelsf is used to abort early if the algorithm is visiting literals at levels that cannot be removed later.Implementation memo: an'toClear is initialized by ps in analyze (a copy of learnt-). This is used only in this function and analyze.|miosE#114 analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void] Description:] Specialized analysis proceduce to express the final conflict in terms of assumptions.  root_levelk is allowed to point beyond end of trace (useful if called after conflict while making assumptions). If  skip_first is TRUE, the first literal of conflE is ignored (needed if conflict arose before search even started).}mios&M114: propagate : [void] -> [Clause+] Description:u Porpagates all enqueued facts. If a conflict arises, the conflicting clause is returned. otherwise CRef_undef.Post-conditions:C * the propagation queue is empty, even if there was a conflict.memo:  propagate is invoked by search,simpleDB and D~mios#M22 reduceDB: () -> [void] Description: Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked clauses are clauses that are reason to some assignment. Binary clauses are never removed.mios;applies a (good to bad) quick semi-sort to the vector in a  and returns the number of privileged clauses. This function uses the same criteria as reduceDB_lt in glucose 4.0: 1. binary clause 2. smaller LBD 3. larger activity defined as MiniSatThey are encoded into an Int64! as the following (11+51 layout):11 bits for rank (LBD):  51 bits for converted activity: Cmios#M22simplify : [void] -> [bool] Description: Simplify the clause database according to the current top-level assigment. Currently, the only thing done here is the removal of satisfied clauses, but more things can be put here.mios#M22Hsearch : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] Description:Z Search for a model the specified number of conflicts. NOTE: Use negative value for  nof_conflicts indicate infinity.Output: *  if a partial assigment that is consistent with respect to the clause set is found. If all variables are decision variables, that means that the clause set is satisfiable. * : if the clause set is unsatisfiable or some error occured.DmiosFig. 16. (p.20) Main solve method.Pre-condition: If assumptions are used, C must be called right before using this method. If not, a top-level conflict (resulting in a non-usable internal state) cannot be distinguished from a conflict under assumptions.miosThough 4 is defined in , most functions in M114 use  unsafeEnqueue.miosPre-condition: propagation queue is empty.'3=BCD'3=BCDSafe%]jkdlEmios version nameFmios*returns a MiosProgramOption for the targetGmios'returns a new solver injected a problemHmios;returns the data on a given CNF file. Only solver knows it.Imiospexecutes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.miosprint messages on solver's result Note: the last field of benchmark CSV is: * 0 if UNSAT * 1 if satisfiable (by finding an assignment) * other bigger values are used for aborted cases. TODO: this function shuld return  IO String in someday.Jmios9NOT MAINTAINED NOW new top-level interface that returns:%conflicting literal set :: Left [Int]%satisfiable assignment :: Right [Int]KmiosEThe easiest interface for Haskell programs. This returns the result  ::[[Int]] for a given (CNFDescription, [[Int]]). The first argument target can be build by %Just target <- cnfFromFile targetfiles. The second part of the first argument is a list of vector, which 0th element is the number of its real elements.Lmiosvsolves the problem (2rd arg) under the configuration (1st arg). and returns an assignment as list of literals :: Int.Mmios~validates a given assignment for the problem (2nd arg). This is another entry point for standalone programs; see app/mios.hs.Nmioshreturns True if a given assignment (2nd arg) satisfies the problem (1st arg). if you want to check the answer which a slover returned, run solver 8 answer , where 8 / :: Traversable t => Solver -> t Lit -> IO Bool.OmiosFIXME: swtich to DRAT'dumps an assigment to file. 2nd arg isTrue* if the assigment is satisfiable assigmentFalse if notJdo y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model smiosparses the header of a CNF filemios>parses ByteString then injects the clauses in it into a solverPmiospexecutes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.7_`abcdefghijkt|}~8EFGHIJKLMNOPEghijkt|}~FGHIMJKLP8NO !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUV)WXYZ[\]^_`abcdefghijklmnopqrsttuvwxyz{{|}~                                           ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G HIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnklopqmrstuv w x y z { |}~s!mios-1.6.2-CFjboSyf5RBJJJjb65kAA1SAT.Mios.TypesSAT.Mios.Util.BoolExp"SAT.Mios.Util.DIMACS.MinisatReaderSAT.Mios.Util.DIMACS.ReaderSAT.Mios.Util.DIMACS.WriterSAT.Mios.Util.DIMACS SAT.Mios.VecSAT.Mios.OptionParserSAT.Mios.ClauseSAT.Mios.ClauseManagerSAT.Mios.ClausePoolSAT.Mios.SolverSAT.Mios.ValidatorSAT.Mios.Criteria SAT.Mios.MainSAT.Mios Paths_miossearchanalyzeghc-prim GHC.TypesIntBoolFormCnf BoolComponenttoBF tseitinBasenumberOfVariablesnumberOfClauses-|--&-neg-=--!-->- disjunctionOf-|||- conjunctionOf-&&&-asList_asListasLatex_asLatex $fOrdBoolForm$fBoolComponentBool$fBoolComponentBoolForm$fBoolComponent[]$fBoolComponentL$fBoolComponentInt $fEqBoolForm$fShowBoolFormfromMinisatOutputclauseListFromMinisatOutputfromFileclauseListFromFiletoFiletoDIMACSStringtoString toLatexStringasDIMACSStringasDIMACSString_Stack StackFamilynewStackpushTopopFromlastOfshrinkByDouble'Int'Bool' SingleStoragenew'get'set'modify'Vec VecFamilygetNthsetNthreset swapBetween modifyNthnewVecsetAllgrowByByteArrayDouble ByteArrayInt realLengthnewStackFromList sortStack$fVecFamilyMVectorInt$fVecFamilyVecInt$fVecFamilyVecDouble$fSingleStorageVecDouble$fSingleStorageVecInt$fSingleStorageMVectorBool$fStackFamilyVecIntDumpModeNoDump DumpCSVHeaderDumpCSVDumpJSON StatIndex NumOfBackjump NumOfRestartNumOfBlockRestartNumOfGeometricRestartNumOfPropagationNumOfReduction NumOfClause NumOfLearnt NumOfVariable NumOfAssignedEndOfStatIndexMiosConfigurationvariableDecayRateclauseDecayRatedumpSolverStatMode emaCoeffsrestartExpansion restartStepCNFDescription_numberOfVariables_numberOfClauses _pathnameEMAVarOrderupdateVOundoVOselectVO LiftedBoolLitVar SolverResultSolverException StateUNSATStateSAT OutOfMemoryTimeOutInternalInconsistentUndescribedError CertificateSATUNSATConflictLBottomLiftedTLiftedF bottomVarint2var bottomLit positiveLit negateLitlit2varvar2litint2litlit2int lit2lboolnewEMAgetEMA updateEMAdefaultConfiguration$fEqCertificate$fOrdCertificate$fReadCertificate$fShowCertificate$fBoundedSolverException$fEnumSolverException$fEqSolverException$fOrdSolverException$fShowSolverException$fEqCNFDescription$fOrdCNFDescription$fReadCNFDescription$fShowCNFDescription$fEqMiosConfiguration$fOrdMiosConfiguration$fReadMiosConfiguration$fShowMiosConfiguration$fBoundedStatIndex$fEnumStatIndex $fEqStatIndex$fOrdStatIndex$fReadStatIndex$fShowStatIndex$fBoundedDumpMode$fEnumDumpMode $fEqDumpMode $fOrdDumpMode$fReadDumpMode$fShowDumpMode$fBoundedDumpTag $fEnumDumpTag $fEqDumpTag $fOrdDumpTag $fReadDumpTag $fShowDumpTag $fEqMiosStats$fOrdMiosStats$fReadMiosStats$fShowMiosStats $fEqMiosDump $fOrdMiosDump$fReadMiosDump$fShowMiosDumpMiosProgramOption _targetFile_targets _outputFile_confVariableDecayRate_confClauseDecayRate _confRestartE _confRestartS_confCheckAnswer _confVerbose_confBenchmark _confBenchSeq _confNoAnswer _confDumpStat_validateAssignment _displayHelp_displayVersionmiosDefaultOption miosOptions miosUsagemiosParseOptionsmiosParseOptionsFromArgs toMiosConf ClauseVectorClause NullClauselitsrankactivitynewClauseFromStackgetRanksetRanknewClauseVector$fStackFamilyClauseInt$fSingleStorageClauseInt$fVecFamilyClauseInt $fShowClause $fEqClause$fVecFamilyMVectorClause WatcherListClauseExtManagerClauseSimpleManager ClauseManager newManagergetClauseVector markClause getKeyVectorpushClauseWithKeynewWatcherList getNthWatcher"$fClauseManagerClauseSimpleManager&$fStackFamilyClauseSimpleManagerClause%$fSingleStorageClauseSimpleManagerInt!$fVecFamilyClauseExtManagerClause$fClauseManagerClauseExtManager#$fStackFamilyClauseExtManagerClause"$fSingleStorageClauseExtManagerInt$fVecFamilyVectorClause ClausePool newClausePoolmakeClauseFromStack putBackToPoolSolverclauseslearntswatchesassignsphasestrailtrailLimqHeadreasonlevelndd conflicts activitiesorderconfignVarsclaIncvarInc rootLevel learntSAdj learntSCnt maxLearntsokan'seen an'toClearan'stack an'lastDLclsPool litsLearntstatslbd'seenlbd'keyemaAFastemaASlowemaBDLvlemaCDLvlemaDFastemaDSlow nextRestart restartExp emaRstBias newSolvernAssignsnClausesnLearnts decisionLevelvalueVarvalueLitlockedgetStatsetStat incrementStatgetStats setAssignenqueueassume cancelUntil$fVarOrderSolvervalidatevarBumpActivityvarDecayActivityclaBumpActivityclaDecayActivity addClauselbdOf updateNDDnddOfcheckRestartCondition dumpStats simplifyDBsolve versionId buildOption buildSolverbuildDescription executeSolver runSolversolveSATsolveSATWithConfigurationexecuteValidatorvalidateAssignmentdumpAssigmentAsCNFshowAnswerFromStringversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName clausesOf tseitinNumberpintintseqNumsparseMinisatOutput problemLine commentLines preambleCNF parseClausesparseCNFdriverUVectorBool setKeyVector storeLimit getManagerVarHeap getHeapRootcheckUniquenessvarRescaleActivityclaActivityThresholdclaRescaleActivity clauseNew varBit2vIndex varBit2bIndex updateNddOf removeWatchnewLearntClausesimplifyanalyzeRemovable analyzeFinal propagatereduceDB sortClauses rankWidth activityWidthTrueFalse unsafeEnqueue unsafeAssume reportResultinjectClausesFromCNF