-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A modern DPLL-style SAT solver -- -- Funsat is a native Haskell SAT solver that uses modern techniques for -- solving SAT instances. Current features include two-watched literals, -- conflict-directed learning, non-chronological backtracking, a -- VSIDS-like dynamic variable ordering, and restarts. Our goal is to -- facilitate convenient embedding of a reasonably fast SAT solver as a -- constraint solving backend in other applications. Currently along this -- theme we provide unsatisfiable core generation (see -- Funsat.Resolution) and a logical circuit interface (see -- Funsat.Circuit). New in 0.6: circuits and BSD3 license. @package funsat @version 0.6.0 -- | Tabular output. -- -- Converts any matrix of showable data types into a tabular form for -- which the layout is automatically done properly. Currently there is no -- maximum row width, just a dynamically-calculated column width. -- -- If the input matrix is mal-formed, the largest well-formed submatrix -- is chosen. That is, elements along too-long dimensions are chopped -- off. module Text.Tabular newtype Table a Table :: [Row a] -> Table a mkTable :: (Show a) => [[a]] -> Table a combine :: (Show a) => Table a -> Table a -> Table a unTable :: Table a -> [[a]] instance (Show a) => Show (Table a) -- | Idea from -- http://haskell.org/pipermail/libraries/2003-September/001411.html module Control.Monad.MonadST -- | A type class for monads that are able to perform ST actions. class (Monad m) => MonadST s m | m -> s liftST :: (MonadST s m) => ST s a -> m a readSTRef :: (MonadST s m) => STRef s a -> m a writeSTRef :: (MonadST s m) => STRef s a -> a -> m () newSTRef :: (MonadST s m) => a -> m (STRef s a) modifySTRef :: (MonadST s m) => STRef s a -> (a -> a) -> m () instance MonadST s (ST s) -- | The main SAT solver monad. Embeds ST. See type -- SSTErrMonad, which stands for ''State ST Error Monad''. module Funsat.Monad liftST :: (MonadST s m) => ST s a -> m a -- | runSSTErrMonad m s executes a SSTErrMonad action with -- initial state s until an error occurs or a result is -- returned. runSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> (st -> ST s (Either e a, st)) evalSSTErrMonad :: (Error e) => SSTErrMonad e st s a -> st -> ST s (Either e a) -- | SSTErrMonad e st s a: the error type e, state type -- st, ST thread s and result type a. -- -- This is a monad embedding ST and supporting error handling -- and state threading. It uses CPS to avoid checking Left and -- Right for every >>=; instead only checks on -- catchError. Idea adapted from -- http://haskell.org/haskellwiki/Performance/Monads. data SSTErrMonad e st s a instance (Error e) => MonadPlus (SSTErrMonad e st s) instance (Error e) => MonadError e (SSTErrMonad e st s) instance MonadState st (SSTErrMonad e st s) instance Monad (SSTErrMonad e st s) instance MonadST s (SSTErrMonad e st s) -- | Data types used when dealing with SAT problems in funsat. module Funsat.Types newtype Var V :: Int -> Var unVar :: Var -> Int newtype Lit L :: Int -> Lit unLit :: Lit -> Int -- | Transform the number inside the literal. inLit :: (Int -> Int) -> Lit -> Lit -- | The polarity of the literal. Negative literals are false; positive -- literals are true. The 0-literal is an error. litSign :: Lit -> Bool -- | The variable for the given literal. var :: Lit -> Var -- | The positive literal for the given variable. lit :: Var -> Lit type Clause = [Lit] data CNF CNF :: Int -> Int -> Set Clause -> CNF numVars :: CNF -> Int numClauses :: CNF -> Int clauses :: CNF -> Set Clause -- | The solution to a SAT problem. In each case we return an assignment, -- which is obviously right in the Sat case; in the Unsat -- case, the reason is to assist in the generation of an unsatisfiable -- core. data Solution Sat :: IAssignment -> Solution Unsat :: IAssignment -> Solution finalAssignment :: Solution -> IAssignment -- | Represents a container of type t storing elements of type -- a that support membership, insertion, and deletion. -- -- There are various data structures used in funsat which are essentially -- used as ''set-like'' objects. I've distilled their interface into -- three methods. These methods are used extensively in the -- implementation of the solver. class (Ord a) => Setlike t a without :: (Setlike t a) => t -> a -> t with :: (Setlike t a) => t -> a -> t contains :: (Setlike t a) => t -> a -> Bool -- | An ''immutable assignment''. Stores the current assignment according -- to the following convention. A literal L i is in the -- assignment if in location (abs i) in the array, i is -- present. Literal L i is absent if in location (abs -- i) there is 0. It is an error if the location (abs i) is -- any value other than 0 or i or negate i. -- -- Note that the Model instance for Lit and -- IAssignment takes constant time to execute because of this -- representation for assignments. Also updating an assignment with -- newly-assigned literals takes constant time, and can be done -- destructively, but safely. type IAssignment = UArray Var Int showAssignment :: IAssignment -> String -- | Mutable array corresponding to the IAssignment representation. type MAssignment s = STUArray s Var Int -- | Same as freeze, but at the right type so GHC doesn't yell at -- me. freezeAss :: MAssignment s -> ST s IAssignment -- | See freezeAss. unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment thawAss :: IAssignment -> ST s (MAssignment s) unsafeThawAss :: IAssignment -> ST s (MAssignment s) -- | Destructively update the assignment with the given literal. assign :: MAssignment s -> Lit -> ST s (MAssignment s) -- | Destructively undo the assignment to the given literal. unassign :: MAssignment s -> Lit -> ST s (MAssignment s) -- | The assignment as a list of signed literals. litAssignment :: IAssignment -> [Lit] -- | The union of the reason side and the conflict side are all the nodes -- in the cutGraph (excepting, perhaps, the nodes on the reason -- side at decision level 0, which should never be present in a learned -- clause). data Cut f gr a b Cut :: f Node -> f Node -> Node -> gr a b -> Cut f gr a b -- | The reason side contains at least the decision variables. reasonSide :: Cut f gr a b -> f Node -- | The conflict side contains the conflicting literal. conflictSide :: Cut f gr a b -> f Node cutUIP :: Cut f gr a b -> Node cutGraph :: Cut f gr a b -> gr a b -- | Annotate each variable in the conflict graph with literal (indicating -- its assignment) and decision level. The only reason we make a new -- datatype for this is for its Show instance. data CGNodeAnnot CGNA :: Lit -> Int -> CGNodeAnnot -- | An instance of this class is able to answer the question, Is a -- truth-functional object x true under the model m? Or -- is m a model for x? There are three possible answers -- for this question: True (''the object is true under -- m''), False (''the object is false under -- m''), and undefined, meaning its status is uncertain or -- unknown (as is the case with a partial assignment). -- -- The only method in this class is so named so it reads well when used -- infix. Also see: isTrueUnder, isFalseUnder, -- isUndefUnder. class Model a m statusUnder :: (Model a m) => a -> m -> Either () Bool type Level = Int -- | A level array maintains a record of the decision level of each -- variable in the solver. If level is such an array, then -- level[i] == j means the decision level for var number -- i is j. j must be non-negative when the -- level is defined, and noLevel otherwise. -- -- Whenever an assignment of variable v is made at decision -- level i, level[unVar v] is set to i. type LevelArray s = STUArray s Var Level -- | Immutable version. type FrozenLevelArray = UArray Var Level -- | The VSIDS-like dynamic variable ordering. newtype VarOrder s VarOrder :: STUArray s Var Double -> VarOrder s varOrderArr :: VarOrder s -> STUArray s Var Double newtype FrozenVarOrder FrozenVarOrder :: (UArray Var Double) -> FrozenVarOrder -- | Each pair of watched literals is paired with its clause and id. type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId) type WatchArray s = STArray s Lit [WatchedPair s] data PartialResolutionTrace PartialResolutionTrace :: !Int -> ![Int] -> ![(Clause, ClauseId)] -> Map ClauseId [ClauseId] -> PartialResolutionTrace resTraceIdCount :: PartialResolutionTrace -> !Int resTrace :: PartialResolutionTrace -> ![Int] resTraceOriginalSingles :: PartialResolutionTrace -> ![(Clause, ClauseId)] resSourceMap :: PartialResolutionTrace -> Map ClauseId [ClauseId] type ReasonMap = Map Var (Clause, ClauseId) type ClauseId = Int instance Show PartialResolutionTrace instance Show FrozenVarOrder instance Show (VarOrder s) instance Eq Solution instance Show CNF instance Read CNF instance Eq CNF instance Eq Lit instance Ord Lit instance Enum Lit instance Ix Lit instance Eq Var instance Ord Var instance Enum Var instance Ix Var instance Show (STArray s a b) instance Show (STUArray s Var Double) instance Show (STUArray s Var Int) instance Show (STRef s a) instance Model Clause IAssignment instance Model Var IAssignment instance Model Lit IAssignment instance Show CGNodeAnnot instance (Show (f Node), Show (gr a b)) => Show (Cut f gr a b) instance Hash Var instance Hash Lit instance (Ord a, Hash a) => Setlike (BitSet a) a instance (Ord k, Ord a) => Setlike (Map k a) (k, a) instance Setlike IAssignment Lit instance (Ord a) => Setlike [a] a instance (Ord a) => Setlike (Set a) a instance Show Solution instance Read Lit instance Show Lit instance Num Lit instance Num Var instance Show Var -- | A circuit is a standard one of among many ways of representing a -- propositional logic formula. This module provides a flexible circuit -- type class and various representations that admit efficient conversion -- to funsat CNF. -- -- The implementation for this module was adapted from -- http://okmij.org/ftp/Haskell/DSLSharing.hs. module Funsat.Circuit -- | A class representing a grammar for logical circuits. Default -- implemenations are indicated. class Circuit repr true :: (Circuit repr, Ord var, Show var) => repr var false :: (Circuit repr, Ord var, Show var) => repr var input :: (Circuit repr, Ord var, Show var) => var -> repr var not :: (Circuit repr, Ord var, Show var) => repr var -> repr var and :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var or :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var ite :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var -> repr var onlyif :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var iff :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var xor :: (Circuit repr, Ord var, Show var) => repr var -> repr var -> repr var -- | Instances of CastCircuit admit converting one circuit -- representation to another. class CastCircuit c castCircuit :: (CastCircuit c, Circuit cOut, Ord var, Show var) => c var -> cOut var -- | A Circuit constructed using common-subexpression elimination. -- This is a compact representation that facilitates converting to CNF. -- See runShared. newtype Shared v Shared :: State (CMaps v) CCode -> Shared v unShared :: Shared v -> State (CMaps v) CCode -- | A shared circuit that has already been constructed. data FrozenShared v FrozenShared :: !CCode -> !CMaps v -> FrozenShared v -- | Reify a sharing circuit. runShared :: Shared v -> FrozenShared v -- | 0 is false, 1 is true. Any positive value labels a logical circuit -- node. type CircuitHash = Int falseHash :: CircuitHash trueHash :: CircuitHash -- | A CCode represents a circuit element for Shared -- circuits. A CCode is a flattened tree node which has been -- assigned a unique number in the corresponding map inside CMaps, -- which indicates children, if any. -- -- For example, CAnd i has the two children of the tuple -- lookup i (andMap cmaps) assuming cmaps :: CMaps v. data CCode CTrue :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CFalse :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CVar :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CAnd :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash COr :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CNot :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CXor :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash COnlyif :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CIff :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash CIte :: !CircuitHash -> CCode circuitHash :: CCode -> !CircuitHash -- | Maps used to implement the common-subexpression sharing implementation -- of the Circuit class. See Shared. data CMaps v CMaps :: [CircuitHash] -> Bimap CircuitHash v -> Bimap CircuitHash (CCode, CCode) -> Bimap CircuitHash (CCode, CCode) -> Bimap CircuitHash CCode -> Bimap CircuitHash (CCode, CCode) -> Bimap CircuitHash (CCode, CCode) -> Bimap CircuitHash (CCode, CCode) -> Bimap CircuitHash (CCode, CCode, CCode) -> CMaps v -- | Source of unique IDs used in Shared circuit generation. Should -- not include 0 or 1. hashCount :: CMaps v -> [CircuitHash] -- | Mapping of generated integer IDs to variables. varMap :: CMaps v -> Bimap CircuitHash v andMap :: CMaps v -> Bimap CircuitHash (CCode, CCode) orMap :: CMaps v -> Bimap CircuitHash (CCode, CCode) notMap :: CMaps v -> Bimap CircuitHash CCode xorMap :: CMaps v -> Bimap CircuitHash (CCode, CCode) onlyifMap :: CMaps v -> Bimap CircuitHash (CCode, CCode) iffMap :: CMaps v -> Bimap CircuitHash (CCode, CCode) iteMap :: CMaps v -> Bimap CircuitHash (CCode, CCode, CCode) -- | A CMaps with an initial hashCount of 2. emptyCMaps :: CMaps v -- | Explicit tree representation, which is a generic description of a -- circuit. This representation enables a conversion operation to any -- other type of circuit. Trees evaluate from variable values at the -- leaves to the root. data Tree v TTrue :: Tree v TFalse :: Tree v TLeaf :: v -> Tree v TNot :: (Tree v) -> Tree v TAnd :: (Tree v) -> (Tree v) -> Tree v TOr :: (Tree v) -> (Tree v) -> Tree v TXor :: (Tree v) -> (Tree v) -> Tree v TIff :: (Tree v) -> (Tree v) -> Tree v TOnlyIf :: (Tree v) -> (Tree v) -> Tree v TIte :: (Tree v) -> (Tree v) -> (Tree v) -> Tree v foldTree :: (t -> v -> t) -> t -> Tree v -> t -- | Performs obvious constant propagations. simplifyTree :: Tree v -> Tree v -- | A circuit type that constructs a Graph representation. This is -- useful for visualising circuits, for example using the -- graphviz package. data Graph v runGraph :: (DynGraph gr) => Graph v -> gr (NodeType v) EdgeType -- | Given a frozen shared circuit, construct a DynGraph that -- exactly represents it. Useful for debugging constraints generated as -- Shared circuits. shareGraph :: (DynGraph gr, Eq v, Show v) => FrozenShared v -> gr (FrozenShared v) (FrozenShared v) -- | Node type labels for graphs. data NodeType v NInput :: v -> NodeType v NTrue :: NodeType v NFalse :: NodeType v NAnd :: NodeType v NOr :: NodeType v NNot :: NodeType v NXor :: NodeType v NIff :: NodeType v NOnlyIf :: NodeType v NIte :: NodeType v data EdgeType -- | the edge is the condition for an ite element ETest :: EdgeType -- | the edge is the then branch for an ite element EThen :: EdgeType -- | the edge is the else branch for an ite element EElse :: EdgeType -- | no special annotation EVoid :: EdgeType type BEnv v = Map v Bool -- | A circuit evaluator, that is, a circuit represented as a function from -- variable values to booleans. newtype Eval v Eval :: (BEnv v -> Bool) -> Eval v unEval :: Eval v -> BEnv v -> Bool -- | Evaluate a circuit given inputs. runEval :: BEnv v -> Eval v -> Bool -- | A circuit problem packages up the CNF corresponding to a given -- FrozenShared circuit, and the mapping between the variables in -- the CNF and the circuit elements of the circuit. data CircuitProblem v CircuitProblem :: CNF -> FrozenShared v -> Bimap Var CCode -> CircuitProblem v problemCnf :: CircuitProblem v -> CNF problemCircuit :: CircuitProblem v -> FrozenShared v problemCodeMap :: CircuitProblem v -> Bimap Var CCode -- | Produces a CNF formula that is satisfiable if and only if the input -- circuit is satisfiable. Note that it does not produce an equivalent -- CNF formula. It is not equivalent in general because the -- transformation introduces variables into the CNF which were not -- present as circuit inputs. (Variables in the CNF correspond to circuit -- elements.) Returns equisatisfiable CNF along with the frozen input -- circuit, and the mapping between the variables of the CNF and the -- circuit elements. -- -- The implementation uses the Tseitin transformation, to guarantee that -- the output CNF formula is linear in the size of the circuit. Contrast -- this with the naive DeMorgan-laws transformation which produces an -- exponential-size CNF formula. toCNF :: (Ord v, Show v) => FrozenShared v -> CircuitProblem v -- | Projects a funsat Solution back into the original circuit -- space, returning a boolean environment containing an assignment of all -- circuit inputs to true and false. projectCircuitSolution :: (Ord v) => Solution -> CircuitProblem v -> BEnv v instance Eq EdgeType instance Ord EdgeType instance Show EdgeType instance Read EdgeType instance (Eq v) => Eq (NodeType v) instance (Ord v) => Ord (NodeType v) instance (Show v) => Show (NodeType v) instance (Read v) => Read (NodeType v) instance (Show v) => Show (Tree v) instance (Eq v) => Eq (Tree v) instance (Ord v) => Ord (Tree v) instance (Eq v) => Eq (CMaps v) instance (Show v) => Show (CMaps v) instance Eq CCode instance Ord CCode instance Show CCode instance Read CCode instance (Eq v) => Eq (FrozenShared v) instance (Show v) => Show (FrozenShared v) instance Circuit Graph instance Circuit Eval instance CastCircuit Tree instance Circuit Tree instance Circuit Shared instance CastCircuit FrozenShared instance CastCircuit Shared -- | Generates and checks a resolution proof of Unsat from a -- resolution trace of a SAT solver (Funsat.Solver.solve will -- generate this trace). As a side effect of this process an -- unsatisfiable core is generated from the resolution trace. This -- core is a (hopefully small) subset of the input clauses which is still -- unsatisfiable. Intuitively, it a concise reason why the problem is -- unsatisfiable. -- -- The resolution trace checker is based on the implementation from the -- paper ''Validating SAT Solvers Using an Independent Resolution-Based -- Checker: Practical Implementations and Other Applications'' by Lintao -- Zhang and Sharad Malik. Unsatisfiable cores are discussed in the paper -- ''Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean -- Formula'' by Zhang and Malik. module Funsat.Resolution -- | Check the given resolution trace of a (putatively) unsatisfiable -- formula. If the result is ResolutionError, the proof trace has -- failed to establish the unsatisfiability of the formula. Otherwise, an -- unsatisfiable core of clauses is returned. -- -- This function simply calls checkDepthFirst. genUnsatCore :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore -- | The depth-first method. checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore -- | A resolution trace records how the SAT solver proved the original CNF -- formula unsatisfiable. data ResolutionTrace ResolutionTrace :: ClauseId -> IAssignment -> Map ClauseId [ClauseId] -> Map ClauseId Clause -> Map Var ClauseId -> ResolutionTrace -- | The id of the last, conflicting clause in the solving process. traceFinalClauseId :: ResolutionTrace -> ClauseId -- | Final assignment. -- -- Precondition: All variables assigned at decision level zero. traceFinalAssignment :: ResolutionTrace -> IAssignment -- | Invariant: Each id has at least one source (otherwise that id -- should not even have a mapping). -- -- Invariant: Should be ordered topologically backward (?) from -- each conflict clause. (IOW, record each clause id as its encountered -- when generating the conflict clause.) traceSources :: ResolutionTrace -> Map ClauseId [ClauseId] -- | Original clauses of the CNF input formula. traceOriginalClauses :: ResolutionTrace -> Map ClauseId Clause traceAntecedents :: ResolutionTrace -> Map Var ClauseId initResolutionTrace :: ClauseId -> IAssignment -> ResolutionTrace -- | A type indicating an error in the checking process. Assuming this -- checker's code is correct, such an error indicates a bug in the SAT -- solver. data ResolutionError -- | Indicates that the clauses do not properly resolve on the variable. ResolveError :: Var -> Clause -> Clause -> ResolutionError -- | Indicates that the clauses do not have complementary variables or have -- too many. The complementary variables (if any) are in the list. CannotResolve :: [Var] -> Clause -> Clause -> ResolutionError -- | Indicates that the constructed antecedent clause not unit under -- traceFinalAssignment. AntecedentNotUnit :: Clause -> ResolutionError -- | Indicates that in the clause-lit pair, the unit literal of clause is -- the literal, but it ought to be the variable. AntecedentImplication :: (Clause, Lit) -> Var -> ResolutionError -- | Indicates that the variable has no antecedent mapping, in which case -- it should never have been assigned/encountered in the first place. AntecedentMissing :: Var -> ResolutionError -- | Indicates that the clause id has an entry in traceSources but -- no resolution sources. EmptySource :: ClauseId -> ResolutionError -- | Indicates that the clause id is referenced but has no entry in -- traceSources. OrphanSource :: ClauseId -> ResolutionError -- | Unsatisfiable cores are not unique. type UnsatisfiableCore = [Clause] instance Show ResolutionError instance Show ResolutionTrace instance Error ResolutionError -- | Funsat aims to be a reasonably efficient modern SAT solver that is -- easy to integrate as a backend to other projects. SAT is NP-complete, -- and thus has reductions from many other interesting problems. We hope -- this implementation is efficient enough to make it useful to solve -- medium-size, real-world problem mapped from another space. We also aim -- to test the solver rigorously to encourage confidence in its output. -- -- One particular nicetie facilitating integration of Funsat into other -- projects is the efficient calculation of an unsatisfiable core -- for unsatisfiable problems (see the Funsat.Resolution module). -- In the case a problem is unsatisfiable, as a by-product of checking -- the proof of unsatisfiability, Funsat will generate a minimal set of -- input clauses that are also unsatisfiable. -- -- -- -- -- -- module Funsat.Solver -- | Run the DPLL-based SAT solver on the given CNF instance. Returns a -- solution, along with internal solver statistics and possibly a -- resolution trace. The trace is for checking a proof of Unsat, -- and thus is only present when the result is Unsat. solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace) -- | Solve with the default configuration defaultConfig. solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace) -- | The solution to a SAT problem. In each case we return an assignment, -- which is obviously right in the Sat case; in the Unsat -- case, the reason is to assist in the generation of an unsatisfiable -- core. data Solution Sat :: IAssignment -> Solution Unsat :: IAssignment -> Solution -- | Verify the solution. In case of Sat, checks that the assignment -- is well-formed and satisfies the CNF problem. In case of Unsat, -- runs a resolution-based checker on a trace of the SAT solver. verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyError data VerifyError -- | Indicates a unsatisfactory assignment that was claimed satisfactory. -- Each clause is tagged with its status using -- Model.statusUnder. SatError :: [(Clause, Either () Bool)] -> VerifyError -- | Indicates an error in the resultion checking process. UnsatError :: ResolutionError -> VerifyError -- | Configuration parameters for the solver. data DPLLConfig Cfg :: !Int64 -> !Double -> !Bool -> !Bool -> DPLLConfig -- | Number of conflicts before a restart. configRestart :: DPLLConfig -> !Int64 -- | configRestart is altered after each restart by multiplying it -- by this value. configRestartBump :: DPLLConfig -> !Double -- | If true, use dynamic variable ordering. configUseVSIDS :: DPLLConfig -> !Bool configUseRestarts :: DPLLConfig -> !Bool -- | A default configuration based on the formula to solve. -- -- defaultConfig :: CNF -> DPLLConfig data Stats Stats :: Int64 -> Int64 -> Int64 -> Double -> Int64 -> Int64 -> Stats -- | Number of conflicts since last restart. statsNumConfl :: Stats -> Int64 -- | Number of conflicts since beginning of solving. statsNumConflTotal :: Stats -> Int64 -- | Number of learned clauses currently in DB (fluctuates because DB is -- compacted every restart). statsNumLearnt :: Stats -> Int64 -- | Avg. number of literals per learnt clause. statsAvgLearntLen :: Stats -> Double -- | Total number of decisions since beginning of solving. statsNumDecisions :: Stats -> Int64 -- | Total number of unit implications since beginning of solving. statsNumImpl :: Stats -> Int64 -- | The show instance uses the wrapped string. newtype ShowWrapped WrapString :: String -> ShowWrapped unwrapString :: ShowWrapped -> String -- | Convert statistics to a nice-to-display tabular form. statTable :: Stats -> Table ShowWrapped -- | Converts statistics into a tabular, human-readable summary. statSummary :: Stats -> String instance Show VerifyError instance Show (FunsatState s) instance Show DPLLConfig instance Show Stats instance Show ShowWrapped instance Error () instance Error (Lit, Clause, ClauseId)