funsat-0.5.1: A modern DPLL-style SAT solver Contents Index

Search:

AntecedentImplication Funsat.Resolution AntecedentMissing Funsat.Resolution AntecedentNotUnit Funsat.Resolution assign Funsat.Types CannotResolve Funsat.Resolution Cfg Funsat.Solver CGNA Funsat.Types CGNodeAnnot Funsat.Types checkDepthFirst Funsat.Resolution Clause Funsat.Types ClauseId Funsat.Types clauses Funsat.Types CNF 1 (Type/Class) Funsat.Types 2 (Data Constructor) Funsat.Types combine Text.Tabular configRestart Funsat.Solver configRestartBump Funsat.Solver configUseRestarts Funsat.Solver configUseVSIDS Funsat.Solver conflictSide Funsat.Types contains Funsat.Types Cut 1 (Type/Class) Funsat.Types 2 (Data Constructor) Funsat.Types cutGraph Funsat.Types cutUIP Funsat.Types defaultConfig Funsat.Solver DPLLConfig Funsat.Solver EmptySource Funsat.Resolution evalSSTErrMonad Funsat.Monad freezeAss Funsat.Types FrozenLevelArray Funsat.Types FrozenVarOrder 1 (Type/Class) Funsat.Types 2 (Data Constructor) Funsat.Types IAssignment Funsat.Types initResolutionTrace Funsat.Resolution inLit Funsat.Types L Funsat.Types Level Funsat.Types LevelArray Funsat.Types liftST Control.Monad.MonadST, Funsat.Monad Lit Funsat.Types litAssignment Funsat.Types litSign Funsat.Types MAssignment Funsat.Types mkTable Text.Tabular Model Funsat.Types modifySTRef Control.Monad.MonadST MonadST Control.Monad.MonadST newSTRef Control.Monad.MonadST numClauses Funsat.Types numVars Funsat.Types OrphanSource Funsat.Resolution PartialResolutionTrace 1 (Type/Class) Funsat.Types 2 (Data Constructor) Funsat.Types readSTRef Control.Monad.MonadST ReasonMap Funsat.Types reasonSide Funsat.Types ResolutionError Funsat.Resolution ResolutionTrace 1 (Type/Class) Funsat.Resolution 2 (Data Constructor) Funsat.Resolution ResolveError Funsat.Resolution resSourceMap Funsat.Types resTrace Funsat.Types resTraceIdCount Funsat.Types resTraceOriginalSingles Funsat.Types runSSTErrMonad Funsat.Monad Sat Funsat.Solver SatError Funsat.Solver Setlike Funsat.Types ShowWrapped Funsat.Solver Solution Funsat.Solver solve Funsat.Solver solve1 Funsat.Solver SSTErrMonad Funsat.Monad Stats 1 (Type/Class) Funsat.Solver 2 (Data Constructor) Funsat.Solver statsAvgLearntLen Funsat.Solver statsNumConfl Funsat.Solver statsNumConflTotal Funsat.Solver statsNumDecisions Funsat.Solver statsNumImpl Funsat.Solver statsNumLearnt Funsat.Solver statSummary Funsat.Solver statTable Funsat.Solver statusUnder Funsat.Types Table 1 (Type/Class) Text.Tabular 2 (Data Constructor) Text.Tabular thawAss Funsat.Types traceAntecedents Funsat.Resolution traceFinalAssignment Funsat.Resolution traceFinalClauseId Funsat.Resolution traceOriginalClauses Funsat.Resolution traceSources Funsat.Resolution unassign Funsat.Types unLit Funsat.Types unsafeFreezeAss Funsat.Types unsafeThawAss Funsat.Types Unsat Funsat.Solver UnsatError Funsat.Solver UnsatisfiableCore Funsat.Resolution unTable Text.Tabular unVar Funsat.Types unwrapString Funsat.Solver V Funsat.Types Var Funsat.Types var Funsat.Types VarOrder 1 (Type/Class) Funsat.Types 2 (Data Constructor) Funsat.Types varOrderArr Funsat.Types verify Funsat.Solver VerifyError Funsat.Solver WatchArray Funsat.Types WatchedPair Funsat.Types with Funsat.Types without Funsat.Types WrapString Funsat.Solver writeSTRef Control.Monad.MonadST