-- | (This is a part of MIOS.) -- Basic data types used throughout mios. {-# LANGUAGE BangPatterns , PatternSynonyms #-} {-# LANGUAGE Safe #-} module SAT.Mios.Types ( -- * Interface to caller SolverResult , Certificate (..) , SolverException (..) , CNFDescription (..) -- * Solver Configuration , MiosConfiguration (..) , defaultConfiguration -- * internal structure , module SAT.Mios.Vec -- * Variable , Var , bottomVar , int2var -- * Internal encoded Literal , Lit , lit2int , int2lit , bottomLit , positiveLit , lit2var , var2lit , negateLit -- * Assignment on the lifted Bool domain , LiftedBool , lit2lbool , Int (LiftedF, LiftedT, LBottom, Conflict) -- a heap , VarOrder (..) -- * statistics , StatIndex (..) , DumpMode (..) {- -- * dump statistics , DumpTag (..) , DumpedValue , MiosStats (..) , QuadLearntC (..) , MiosDump (..) -} ) where import Data.Bits import SAT.Mios.Vec -- | terminate and find an SAT/UNSAT answer data Certificate = SAT [Int] | UNSAT [Int] -- FIXME: replace with DRAT deriving (Eq, Ord, Read, Show) -- | abnormal termination flags data SolverException = StateUNSAT -- 0 | StateSAT -- 1 | OutOfMemory -- 2 | TimeOut -- 3 | InternalInconsistent -- 4 | UndescribedError -- 5 deriving (Bounded, Enum, Eq, Ord, Show) -- | the 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 error type SolverResult = Either SolverException Certificate -- | represents "Var". type Var = Int -- | Special constant in 'Var' (p.7) bottomVar :: Var bottomVar = 0 -- | converts a usual Int as literal to an internal 'Var' presentation. -- -- >>> int2var 1 -- 1 -- the first literal is the first variable -- >>> int2var 2 -- 2 -- literal @2@ is variable 2 -- >>> int2var (-2) -- 2 -- literal @-2@ is corresponding to variable 2 -- {-# INLINE int2var #-} int2var :: Int -> Int int2var = abs -- | The literal data has an 'index' method which converts the literal to -- a "small" integer suitable for array indexing. The 'var' method returns -- the underlying variable of the literal, and the 'sign' method if the literal -- is signed (False for /x/ and True for /-x/). type Lit = Int -- | Special constant in 'Lit' (p.7) bottomLit :: Lit bottomLit = 0 {- -- | converts "Var" into 'Lit' newLit :: Var -> Lit newLit = error "newLit undefined" -} -- | returns @True@ if the literal is positive {-# INLINE positiveLit #-} positiveLit :: Lit -> Bool positiveLit = even -- | negates literal -- -- >>> negateLit 2 -- 3 -- >>> negateLit 3 -- 2 -- >>> negateLit 4 -- 5 -- >>> negateLit 5 -- 4 {-# INLINE negateLit #-} negateLit :: Lit -> Lit negateLit l = complementBit l 0 -- if even l then l + 1 else l - 1 ---------------------------------------- ----------------- Var ---------------------------------------- -- | converts 'Lit' into 'Var'. -- -- >>> lit2var 2 -- 1 -- >>> lit2var 3 -- 1 -- >>> lit2var 4 -- 2 -- >>> lit2var 5 -- 2 {-# INLINE lit2var #-} lit2var :: Lit -> Var lit2var !n = shiftR n 1 -- | converts a 'Var' to the corresponing literal. -- -- >>> var2lit 1 True -- 2 -- >>> var2lit 1 False -- 3 -- >>> var2lit 2 True -- 4 -- >>> var2lit 2 False -- 5 {-# INLINE var2lit #-} var2lit :: Var -> Bool -> Lit var2lit !v True = shiftL v 1 var2lit !v _ = shiftL v 1 + 1 ---------------------------------------- ----------------- Int ---------------------------------------- -- | converts 'Int' into 'Lit' as @lit2int . int2lit == id@. -- -- >>> int2lit 1 -- 2 -- >>> int2lit (-1) -- 3 -- >>> int2lit 2 -- 4 -- >>> int2lit (-2) -- 5 -- {-# INLINE int2lit #-} int2lit :: Int -> Lit int2lit n | 0 < n = 2 * n | otherwise = -2 * n + 1 -- | converts `Lit' into 'Int' as @int2lit . lit2int == id@. -- -- >>> lit2int 2 -- 1 -- >>> lit2int 3 -- -1 -- >>> lit2int 4 -- 2 -- >>> lit2int 5 -- -2 {-# INLINE lit2int #-} lit2int :: Lit -> Int lit2int l = case divMod l 2 of (i, 0) -> i (i, _) -> - i -- | Lifted Boolean domain (p.7) that extends 'Bool' with "⊥" means /undefined/ -- design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2. type LiftedBool = Int -- | /FALSE/ on the Lifted Bool domain pattern LiftedF :: Int pattern LiftedF = -1 -- | /TRUE/ on the Lifted Bool domain pattern LiftedT :: Int pattern LiftedT = 1 -- | /UNDEFINED/ on the Lifted Bool domain pattern LBottom :: Int pattern LBottom = 0 -- | /CONFLICT/ on the Lifted Bool domain pattern Conflict :: Int pattern Conflict = 2 -- | returns the value of a literal as a 'LiftedBool' {-# INLINE lit2lbool #-} lit2lbool :: Lit -> LiftedBool lit2lbool l = if positiveLit l then LiftedT else LiftedF {- -- | converts 'Bool' into 'LBool' {-# INLINE lbool #-} lbool :: Bool -> LiftedBool lbool True = LTrue lbool False = LFalse -} -- | Assisting 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. class VarOrder o where {- -- | constructor newVarOrder :: (VecFamily v1 Bool, VecFamily v2 Double) => v1 -> v2 -> IO o newVarOrder _ _ = error "newVarOrder undefined" -- | Called when a new variable is created. newVar :: o -> IO Var newVar = error "newVar undefined" -} -- | should be called when a variable has increased in activity. update :: o -> Var -> IO () update _ = error "update undefined" {- -- | should be called when all variables have been assigned. updateAll :: o -> IO () updateAll = error "updateAll undefined" -} -- | should be called when a variable becomes unbound (may be selected again). undo :: o -> Var -> IO () undo _ _ = error "undo undefined" -- | returns a new, unassigned var as the next decision. select :: o -> IO Var select = error "select undefined" -- | Misc information on a CNF data CNFDescription = CNFDescription { _numberOfVariables :: !Int -- ^ the number of variables , _numberOfClauses :: !Int -- ^ the number of clauses , _pathname :: Maybe FilePath -- ^ given filename } deriving (Eq, Ord, Read, Show) -- | Solver's parameters; random decision rate was dropped. data MiosConfiguration = MiosConfiguration { variableDecayRate :: !Double -- ^ decay rate for variable activity , clauseDecayRate :: !Double -- ^ decay rate for clause activity , dumpStat :: !Int -- ^ dump stats data during solving } deriving (Eq, Ord, Read, Show) -- | dafault configuration -- -- * Minisat-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)@. -- defaultConfiguration :: MiosConfiguration defaultConfiguration = MiosConfiguration 0.95 0.999 0 -------------------------------------------------------------------------------- Statistics -- | stat index data StatIndex = NumOfBackjump -- ^ the number of backjump | NumOfRestart -- ^ the number of restart | NumOfBlockRestart -- ^ the number of blacking start | NumOfGeometricRestart -- ^ the number of classic restart | NumOfPropagation -- ^ the number of propagation | NumOfReduction -- ^ the number of reduction | NumOfClause -- ^ the number of 'alive' given clauses | NumOfLearnt -- ^ the number of 'alive' learnt clauses | NumOfVariable -- ^ the number of 'alive' variables | NumOfAssigned -- ^ the number of assigned variables | EndOfStatIndex -- ^ Don't use this dummy. deriving (Bounded, Enum, Eq, Ord, Read, Show) -- | formats of state dump data DumpMode = NoDump | DumpCSVHeader | DumpCSV | DumpJSON deriving (Bounded, Enum, Eq, Ord, Read, Show) data DumpTag = TerminateS | PropagationS | ConflictS | LearntS | BackjumpS | RestartS | LearningRateS | ExtraS deriving (Bounded, Enum, Eq, Ord, Read, Show) type DumpedValue = (DumpTag, Either Double Int) newtype MiosStats = MiosStats [DumpedValue] deriving (Eq, Ord, Read, Show) data MiosDump = MiosDump { _dumpedConf :: (String, MiosConfiguration) , _dupmedCNFDesc :: CNFDescription , _dumpedStat :: MiosStats } deriving (Eq, Ord, Read, Show)