funsat-0.5: 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 checkDepthFirst Funsat.Resolution Clause Funsat.Types ClauseId Funsat.Resolution clauses Funsat.Types CNF 1 (Data Constructor) Funsat.Types 2 (Type/Class) Funsat.Types combine Text.Tabular configRestart Funsat.Solver configRestartBump Funsat.Solver configUseRestarts Funsat.Solver configUseVSIDS Funsat.Solver contains Funsat.Types defaultConfig Funsat.Solver DPLLConfig Funsat.Solver EmptySource Funsat.Resolution evalSSTErrMonad Funsat.Monad freezeAss Funsat.Types GenCNF Funsat.Types getUnit Funsat.Types IAssignment Funsat.Types initResolutionTrace Funsat.Resolution inLit Funsat.Types isFalseUnder Funsat.Types isTrueUnder Funsat.Types isUndefUnder Funsat.Types isUnitUnder Funsat.Types L Funsat.Types liftST Funsat.Monad, Control.Monad.MonadST 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 readSTRef Control.Monad.MonadST ResolutionError Funsat.Resolution ResolutionTrace 1 (Data Constructor) Funsat.Resolution 2 (Type/Class) Funsat.Resolution ResolveError Funsat.Resolution 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 verify Funsat.Solver VerifyError Funsat.Solver with Funsat.Types without Funsat.Types WrapString Funsat.Solver writeSTRef Control.Monad.MonadST