Safe Haskell	Safe
Language	Haskell2010

SAT.Mios.Types

Contents

Interface to caller
Solver Configuration
internal structure
Variable
Internal encoded Literal
Assignment on the lifted Bool domain
statistics

Description

(This is a part of MIOS.) Basic data types used throughout mios.

Synopsis

type SolverResult = Either SolverException Certificate
data Certificate
- = SAT [Int]
- | UNSAT [Int]
data SolverException
- = StateUNSAT
- | StateSAT
- | OutOfMemory
- | TimeOut
- | InternalInconsistent
- | UndescribedError
data CNFDescription = CNFDescription {
- _numberOfVariables :: !Int
- _numberOfClauses :: !Int
- _pathname :: !FilePath
}
data MiosConfiguration = MiosConfiguration {
- variableDecayRate :: !Double
- clauseDecayRate :: !Double
- dumpSolverStatMode :: !Int
- emaCoeffs :: !(Int, Int)
- restartExpansion :: !Double
- restartStep :: !Double
}
defaultConfiguration :: MiosConfiguration
module SAT.Mios.Vec
type Var = Int
bottomVar :: Var
int2var :: Int -> Int
type Lit = Int
lit2int :: Lit -> Int
int2lit :: Int -> Lit
bottomLit :: Lit
positiveLit :: Lit -> Bool
lit2var :: Lit -> Var
var2lit :: Var -> Bool -> Lit
negateLit :: Lit -> Lit
type LiftedBool = Int
lit2lbool :: Lit -> LiftedBool
data Int where
- pattern LiftedF :: Int
- pattern LiftedT :: Int
- pattern LBottom :: Int
- pattern Conflict :: Int
class VarOrder o where
type EMA = (Double', Maybe Double', Double)
newEMA :: Bool -> Int -> IO EMA
getEMA :: EMA -> IO Double
updateEMA :: EMA -> Double -> IO Double
data StatIndex
- = NumOfBackjump
- | NumOfRestart
- | NumOfBlockRestart
- | NumOfGeometricRestart
- | NumOfPropagation
- | NumOfReduction
- | NumOfClause
- | NumOfLearnt
- | NumOfVariable
- | NumOfAssigned
- | EndOfStatIndex
data DumpMode
- = NoDump
- | DumpCSVHeader
- | DumpCSV
- | DumpJSON

Interface to caller

type SolverResult = Either SolverException Certificate Source #

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

data Certificate Source #

terminate and find an SAT/UNSAT answer

Constructors

SAT [Int]
UNSAT [Int]

Instances

Eq Certificate Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: Certificate -> Certificate -> Bool # (/=) :: Certificate -> Certificate -> Bool #
Ord Certificate Source #
Instance details Defined in SAT.Mios.Types Methods compare :: Certificate -> Certificate -> Ordering # (<) :: Certificate -> Certificate -> Bool # (<=) :: Certificate -> Certificate -> Bool # (>) :: Certificate -> Certificate -> Bool # (>=) :: Certificate -> Certificate -> Bool # max :: Certificate -> Certificate -> Certificate # min :: Certificate -> Certificate -> Certificate #
Read Certificate Source #
Instance details Defined in SAT.Mios.Types Methods readsPrec :: Int -> ReadS Certificate # readList :: ReadS [Certificate] # readPrec :: ReadPrec Certificate # readListPrec :: ReadPrec [Certificate] #
Show Certificate Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> Certificate -> ShowS # show :: Certificate -> String # showList :: [Certificate] -> ShowS #

data SolverException Source #

abnormal termination flags

Constructors

StateUNSAT
StateSAT
OutOfMemory
TimeOut
InternalInconsistent
UndescribedError

Instances

Bounded SolverException Source #
Instance details Defined in SAT.Mios.Types Methods minBound :: SolverException # maxBound :: SolverException #
Enum SolverException Source #
Instance details Defined in SAT.Mios.Types Methods succ :: SolverException -> SolverException # pred :: SolverException -> SolverException # toEnum :: Int -> SolverException # fromEnum :: SolverException -> Int # enumFrom :: SolverException -> [SolverException] # enumFromThen :: SolverException -> SolverException -> [SolverException] # enumFromTo :: SolverException -> SolverException -> [SolverException] # enumFromThenTo :: SolverException -> SolverException -> SolverException -> [SolverException] #
Eq SolverException Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: SolverException -> SolverException -> Bool # (/=) :: SolverException -> SolverException -> Bool #
Ord SolverException Source #
Instance details Defined in SAT.Mios.Types Methods compare :: SolverException -> SolverException -> Ordering # (<) :: SolverException -> SolverException -> Bool # (<=) :: SolverException -> SolverException -> Bool # (>) :: SolverException -> SolverException -> Bool # (>=) :: SolverException -> SolverException -> Bool # max :: SolverException -> SolverException -> SolverException # min :: SolverException -> SolverException -> SolverException #
Show SolverException Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> SolverException -> ShowS # show :: SolverException -> String # showList :: [SolverException] -> ShowS #

data CNFDescription Source #

Misc information on a CNF

Constructors

CNFDescription
Fields _numberOfVariables :: !Int the number of variables _numberOfClauses :: !Int the number of clauses _pathname :: !FilePath given filename

Instances

Eq CNFDescription Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: CNFDescription -> CNFDescription -> Bool # (/=) :: CNFDescription -> CNFDescription -> Bool #
Ord CNFDescription Source #
Instance details Defined in SAT.Mios.Types Methods compare :: CNFDescription -> CNFDescription -> Ordering # (<) :: CNFDescription -> CNFDescription -> Bool # (<=) :: CNFDescription -> CNFDescription -> Bool # (>) :: CNFDescription -> CNFDescription -> Bool # (>=) :: CNFDescription -> CNFDescription -> Bool # max :: CNFDescription -> CNFDescription -> CNFDescription # min :: CNFDescription -> CNFDescription -> CNFDescription #
Read CNFDescription Source #
Instance details Defined in SAT.Mios.Types Methods readsPrec :: Int -> ReadS CNFDescription # readList :: ReadS [CNFDescription] # readPrec :: ReadPrec CNFDescription # readListPrec :: ReadPrec [CNFDescription] #
Show CNFDescription Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> CNFDescription -> ShowS # show :: CNFDescription -> String # showList :: [CNFDescription] -> ShowS #

Solver Configuration

data MiosConfiguration Source #

Solver's parameters; random decision rate was dropped.

Constructors

MiosConfiguration
Fields variableDecayRate :: !Double decay rate for variable activity clauseDecayRate :: !Double decay rate for clause activity dumpSolverStatMode :: !Int dump stats data during solving emaCoeffs :: !(Int, Int) the coefficients for restarts restartExpansion :: !Double restart expansion factor restartStep :: !Double static Steps between restarts

Instances

Eq MiosConfiguration Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: MiosConfiguration -> MiosConfiguration -> Bool # (/=) :: MiosConfiguration -> MiosConfiguration -> Bool #
Ord MiosConfiguration Source #
Instance details Defined in SAT.Mios.Types Methods compare :: MiosConfiguration -> MiosConfiguration -> Ordering # (<) :: MiosConfiguration -> MiosConfiguration -> Bool # (<=) :: MiosConfiguration -> MiosConfiguration -> Bool # (>) :: MiosConfiguration -> MiosConfiguration -> Bool # (>=) :: MiosConfiguration -> MiosConfiguration -> Bool # max :: MiosConfiguration -> MiosConfiguration -> MiosConfiguration # min :: MiosConfiguration -> MiosConfiguration -> MiosConfiguration #
Read MiosConfiguration Source #
Instance details Defined in SAT.Mios.Types Methods readsPrec :: Int -> ReadS MiosConfiguration # readList :: ReadS [MiosConfiguration] # readPrec :: ReadPrec MiosConfiguration # readListPrec :: ReadPrec [MiosConfiguration] #
Show MiosConfiguration Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> MiosConfiguration -> ShowS # show :: MiosConfiguration -> String # showList :: [MiosConfiguration] -> ShowS #

defaultConfiguration :: MiosConfiguration Source #

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).

internal structure

module SAT.Mios.Vec

Variable

type Var = Int Source #

represents Var.

bottomVar :: Var Source #

Special constant in Var (p.7)

int2var :: Int -> Int Source #

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

Internal encoded Literal

type Lit = Int Source #

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).

lit2int :: Lit -> Int Source #

converts Lit into Int as int2lit . lit2int == id.

>>> lit2int 2
1
>>> lit2int 3
-1
>>> lit2int 4
2
>>> lit2int 5
-2

int2lit :: Int -> Lit Source #

converts Int into Lit as lit2int . int2lit == id.

>>> int2lit 1
2
>>> int2lit (-1)
3
>>> int2lit 2
4
>>> int2lit (-2)
5

bottomLit :: Lit Source #

Special constant in Lit (p.7)

positiveLit :: Lit -> Bool Source #

returns True if the literal is positive

lit2var :: Lit -> Var Source #

converts Lit into Var.

>>> lit2var 2
1
>>> lit2var 3
1
>>> lit2var 4
2
>>> lit2var 5
2

var2lit :: Var -> Bool -> Lit Source #

converts a Var to the corresponing literal.

>>> var2lit 1 True
2
>>> var2lit 1 False
3
>>> var2lit 2 True
4
>>> var2lit 2 False
5

negateLit :: Lit -> Lit Source #

negates literal

>>> negateLit 2
3
>>> negateLit 3
2
>>> negateLit 4
5
>>> negateLit 5
4

Assignment on the lifted Bool domain

type LiftedBool = Int Source #

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.

lit2lbool :: Lit -> LiftedBool Source #

returns the value of a literal as a LiftedBool

data Int where #

A fixed-precision integer type with at least the range [-2^29 .. 2^29-1]. The exact range for a given implementation can be determined by using minBound and maxBound from the Bounded class.

Bundled Patterns

pattern LiftedF :: Int	FALSE on the Lifted Bool domain
pattern LiftedT :: Int	TRUE on the Lifted Bool domain
pattern LBottom :: Int	UNDEFINED on the Lifted Bool domain
pattern Conflict :: Int	CONFLICT on the Lifted Bool domain

Instances

Bounded Int	Since: base-2.1
Instance details Defined in GHC.Enum Methods minBound :: Int # maxBound :: Int #
Enum Int	Since: base-2.1
Instance details Defined in GHC.Enum Methods succ :: Int -> Int # pred :: Int -> Int # toEnum :: Int -> Int # fromEnum :: Int -> Int # enumFrom :: Int -> [Int] # enumFromThen :: Int -> Int -> [Int] # enumFromTo :: Int -> Int -> [Int] # enumFromThenTo :: Int -> Int -> Int -> [Int] #
Eq Int
Instance details Defined in GHC.Classes Methods (==) :: Int -> Int -> Bool # (/=) :: Int -> Int -> Bool #
Integral Int	Since: base-2.0.1
Instance details Defined in GHC.Real Methods quot :: Int -> Int -> Int # rem :: Int -> Int -> Int # div :: Int -> Int -> Int # mod :: Int -> Int -> Int # quotRem :: Int -> Int -> (Int, Int) # divMod :: Int -> Int -> (Int, Int) # toInteger :: Int -> Integer #
Num Int	Since: base-2.1
Instance details Defined in GHC.Num Methods (+) :: Int -> Int -> Int # (-) :: Int -> Int -> Int # (*) :: Int -> Int -> Int # negate :: Int -> Int # abs :: Int -> Int # signum :: Int -> Int # fromInteger :: Integer -> Int #
Ord Int
Instance details Defined in GHC.Classes Methods compare :: Int -> Int -> Ordering # (<) :: Int -> Int -> Bool # (<=) :: Int -> Int -> Bool # (>) :: Int -> Int -> Bool # (>=) :: Int -> Int -> Bool # max :: Int -> Int -> Int # min :: Int -> Int -> Int #
Read Int	Since: base-2.1
Instance details Defined in GHC.Read Methods readsPrec :: Int -> ReadS Int # readList :: ReadS [Int] # readPrec :: ReadPrec Int # readListPrec :: ReadPrec [Int] #
Real Int	Since: base-2.0.1
Instance details Defined in GHC.Real Methods toRational :: Int -> Rational #
Show Int	Since: base-2.1
Instance details Defined in GHC.Show Methods showsPrec :: Int -> Int -> ShowS # show :: Int -> String # showList :: [Int] -> ShowS #
Ix Int	Since: base-2.1
Instance details Defined in GHC.Arr Methods range :: (Int, Int) -> [Int] # index :: (Int, Int) -> Int -> Int # unsafeIndex :: (Int, Int) -> Int -> Int inRange :: (Int, Int) -> Int -> Bool # rangeSize :: (Int, Int) -> Int # unsafeRangeSize :: (Int, Int) -> Int
Bits Int	Since: base-2.1
Instance details Defined in Data.Bits Methods (.&.) :: Int -> Int -> Int # (.\|.) :: Int -> Int -> Int # xor :: Int -> Int -> Int # complement :: Int -> Int # shift :: Int -> Int -> Int # rotate :: Int -> Int -> Int # zeroBits :: Int # bit :: Int -> Int # setBit :: Int -> Int -> Int # clearBit :: Int -> Int -> Int # complementBit :: Int -> Int -> Int # testBit :: Int -> Int -> Bool # bitSizeMaybe :: Int -> Maybe Int # bitSize :: Int -> Int # isSigned :: Int -> Bool # shiftL :: Int -> Int -> Int # unsafeShiftL :: Int -> Int -> Int # shiftR :: Int -> Int -> Int # unsafeShiftR :: Int -> Int -> Int # rotateL :: Int -> Int -> Int # rotateR :: Int -> Int -> Int # popCount :: Int -> Int #
FiniteBits Int	Since: base-4.6.0.0
Instance details Defined in Data.Bits Methods finiteBitSize :: Int -> Int # countLeadingZeros :: Int -> Int # countTrailingZeros :: Int -> Int #
Prim Int
Instance details Defined in Data.Primitive.Types Methods sizeOf# :: Int -> Int# # alignment# :: Int -> Int# # indexByteArray# :: ByteArray# -> Int# -> Int # readByteArray# :: MutableByteArray# s -> Int# -> State# s -> (#State# s, Int#) # writeByteArray# :: MutableByteArray# s -> Int# -> Int -> State# s -> State# s # setByteArray# :: MutableByteArray# s -> Int# -> Int# -> Int -> State# s -> State# s # indexOffAddr# :: Addr# -> Int# -> Int # readOffAddr# :: Addr# -> Int# -> State# s -> (#State# s, Int#) # writeOffAddr# :: Addr# -> Int# -> Int -> State# s -> State# s # setOffAddr# :: Addr# -> Int# -> Int# -> Int -> State# s -> State# s #
Unbox Int
Instance details Defined in Data.Vector.Unboxed.Base
BoolComponent Int Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: Int -> BoolForm Source #
Vector Vector Int
Instance details Defined in Data.Vector.Unboxed.Base Methods basicUnsafeFreeze :: PrimMonad m => Mutable Vector (PrimState m) Int -> m (Vector Int) # basicUnsafeThaw :: PrimMonad m => Vector Int -> m (Mutable Vector (PrimState m) Int) # basicLength :: Vector Int -> Int # basicUnsafeSlice :: Int -> Int -> Vector Int -> Vector Int # basicUnsafeIndexM :: Monad m => Vector Int -> Int -> m Int # basicUnsafeCopy :: PrimMonad m => Mutable Vector (PrimState m) Int -> Vector Int -> m () # elemseq :: Vector Int -> Int -> b -> b #
MVector MVector Int
Instance details Defined in Data.Vector.Unboxed.Base Methods basicLength :: MVector s Int -> Int # basicUnsafeSlice :: Int -> Int -> MVector s Int -> MVector s Int # basicOverlaps :: MVector s Int -> MVector s Int -> Bool # basicUnsafeNew :: PrimMonad m => Int -> m (MVector (PrimState m) Int) # basicInitialize :: PrimMonad m => MVector (PrimState m) Int -> m () # basicUnsafeReplicate :: PrimMonad m => Int -> Int -> m (MVector (PrimState m) Int) # basicUnsafeRead :: PrimMonad m => MVector (PrimState m) Int -> Int -> m Int # basicUnsafeWrite :: PrimMonad m => MVector (PrimState m) Int -> Int -> Int -> m () # basicClear :: PrimMonad m => MVector (PrimState m) Int -> m () # basicSet :: PrimMonad m => MVector (PrimState m) Int -> Int -> m () # basicUnsafeCopy :: PrimMonad m => MVector (PrimState m) Int -> MVector (PrimState m) Int -> m () # basicUnsafeMove :: PrimMonad m => MVector (PrimState m) Int -> MVector (PrimState m) Int -> m () # basicUnsafeGrow :: PrimMonad m => MVector (PrimState m) Int -> Int -> m (MVector (PrimState m) Int) #
StackFamily Clause Lit Source #	`Clause` is a `Stackfamily`on literals since literals in it will be discared if satisifed at level = 0.
Instance details Defined in SAT.Mios.Clause Methods newStack :: Int -> IO Clause Source # pushTo :: Clause -> Lit -> IO () Source # popFrom :: Clause -> IO () Source # lastOf :: Clause -> IO Lit Source # shrinkBy :: Clause -> Int -> IO () Source #
SingleStorage Clause Int Source #	`Clause` is a `SingleStorage` on the number of literals in it.
Instance details Defined in SAT.Mios.Clause Methods new' :: Int -> IO Clause Source # get' :: Clause -> IO Int Source # set' :: Clause -> Int -> IO () Source # modify' :: Clause -> (Int -> Int) -> IO () Source #
SingleStorage ClauseExtManager Int Source #	`ClauseExtManager` is a `SingleStorage` on the number of clauses in it.
Instance details Defined in SAT.Mios.ClauseManager Methods new' :: Int -> IO ClauseExtManager Source # get' :: ClauseExtManager -> IO Int Source # set' :: ClauseExtManager -> Int -> IO () Source # modify' :: ClauseExtManager -> (Int -> Int) -> IO () Source #
SingleStorage ClauseSimpleManager Int Source #	`ClauseSimpleManager` is a `SingleStorage` on the number of clauses in it.
Instance details Defined in SAT.Mios.ClauseManager Methods new' :: Int -> IO ClauseSimpleManager Source # get' :: ClauseSimpleManager -> IO Int Source # set' :: ClauseSimpleManager -> Int -> IO () Source # modify' :: ClauseSimpleManager -> (Int -> Int) -> IO () Source #
VecFamily Clause Lit Source #	`Clause` is a `VecFamily` of `Lit`.
Instance details Defined in SAT.Mios.Clause Methods getNth :: Clause -> Int -> IO Lit Source # setNth :: Clause -> Int -> Lit -> IO () Source # reset :: Clause -> IO () Source # swapBetween :: Clause -> Int -> Int -> IO () Source # modifyNth :: Clause -> (Lit -> Lit) -> Int -> IO () Source # newVec :: Int -> Lit -> IO Clause Source # setAll :: Clause -> Lit -> IO () Source # growBy :: Clause -> Int -> IO Clause Source # asList :: Clause -> IO [Lit] Source #
Generic1 (URec Int :: k -> *)
Instance details Defined in GHC.Generics Associated Types type Rep1 (URec Int) :: k -> * # Methods from1 :: URec Int a -> Rep1 (URec Int) a # to1 :: Rep1 (URec Int) a -> URec Int a #
Functor (URec Int :: * -> *)
Instance details Defined in GHC.Generics Methods fmap :: (a -> b) -> URec Int a -> URec Int b # (<$) :: a -> URec Int b -> URec Int a #
Foldable (URec Int :: * -> *)
Instance details Defined in Data.Foldable Methods fold :: Monoid m => URec Int m -> m # foldMap :: Monoid m => (a -> m) -> URec Int a -> m # foldr :: (a -> b -> b) -> b -> URec Int a -> b # foldr' :: (a -> b -> b) -> b -> URec Int a -> b # foldl :: (b -> a -> b) -> b -> URec Int a -> b # foldl' :: (b -> a -> b) -> b -> URec Int a -> b # foldr1 :: (a -> a -> a) -> URec Int a -> a # foldl1 :: (a -> a -> a) -> URec Int a -> a # toList :: URec Int a -> [a] # null :: URec Int a -> Bool # length :: URec Int a -> Int # elem :: Eq a => a -> URec Int a -> Bool # maximum :: Ord a => URec Int a -> a # minimum :: Ord a => URec Int a -> a # sum :: Num a => URec Int a -> a # product :: Num a => URec Int a -> a #
Traversable (URec Int :: * -> *)
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> URec Int a -> f (URec Int b) # sequenceA :: Applicative f => URec Int (f a) -> f (URec Int a) # mapM :: Monad m => (a -> m b) -> URec Int a -> m (URec Int b) # sequence :: Monad m => URec Int (m a) -> m (URec Int a) #
Eq (URec Int p)
Instance details Defined in GHC.Generics Methods (==) :: URec Int p -> URec Int p -> Bool # (/=) :: URec Int p -> URec Int p -> Bool #
Ord (URec Int p)
Instance details Defined in GHC.Generics Methods compare :: URec Int p -> URec Int p -> Ordering # (<) :: URec Int p -> URec Int p -> Bool # (<=) :: URec Int p -> URec Int p -> Bool # (>) :: URec Int p -> URec Int p -> Bool # (>=) :: URec Int p -> URec Int p -> Bool # max :: URec Int p -> URec Int p -> URec Int p # min :: URec Int p -> URec Int p -> URec Int p #
Show (URec Int p)
Instance details Defined in GHC.Generics Methods showsPrec :: Int -> URec Int p -> ShowS # show :: URec Int p -> String # showList :: [URec Int p] -> ShowS #
Generic (URec Int p)
Instance details Defined in GHC.Generics Associated Types type Rep (URec Int p) :: * -> * # Methods from :: URec Int p -> Rep (URec Int p) x # to :: Rep (URec Int p) x -> URec Int p #
data Vector Int
Instance details Defined in Data.Vector.Unboxed.Base data Vector Int = V_Int (Vector Int)
data Vec Int Source #
Instance details Defined in SAT.Mios.Vec data Vec Int = ByteArrayInt (MutableByteArray RealWorld)
data URec Int (p :: k)	Used for marking occurrences of `Int#` Since: base-4.9.0.0
Instance details Defined in GHC.Generics data URec Int (p :: k) = UInt { uInt# :: Int# }
data MVector s Int
Instance details Defined in Data.Vector.Unboxed.Base data MVector s Int = MV_Int (MVector s Int)
type Rep1 (URec Int :: k -> *)
Instance details Defined in GHC.Generics type Rep1 (URec Int :: k -> ) = D1 (MetaData "URec" "GHC.Generics" "base" False) (C1 (MetaCons "UInt" PrefixI True) (S1 (MetaSel (Just "uInt#") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (UInt :: k -> )))
type Rep (URec Int p)
Instance details Defined in GHC.Generics type Rep (URec Int p) = D1 (MetaData "URec" "GHC.Generics" "base" False) (C1 (MetaCons "UInt" PrefixI True) (S1 (MetaSel (Just "uInt#") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (UInt :: * -> *)))

class VarOrder o where Source #

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.

Methods

updateVO :: o -> Var -> IO () Source #

should be called when a variable has increased in activity.

undoVO :: o -> Var -> IO () Source #

should be called when a variable becomes unbound (may be selected again).

selectVO :: o -> IO Var Source #

returns a new, unassigned var as the next decision.

Instances

VarOrder Solver Source #	Interfate to select a decision var based on variable activity.
Instance details Defined in SAT.Mios.Solver Methods updateVO :: Solver -> Var -> IO () Source # undoVO :: Solver -> Var -> IO () Source # selectVO :: Solver -> IO Var Source #

type EMA = (Double', Maybe Double', Double) Source #

Exponential Moving Average, EMA

newEMA :: Bool -> Int -> IO EMA Source #

returns a new EMA from a flag (slow or fast) and a window size

getEMA :: EMA -> IO Double Source #

returns an EMA value

updateEMA :: EMA -> Double -> IO Double Source #

updates an EMA

statistics

data StatIndex Source #

stat index

Constructors

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.

Instances

Bounded StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods minBound :: StatIndex # maxBound :: StatIndex #
Enum StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods succ :: StatIndex -> StatIndex # pred :: StatIndex -> StatIndex # toEnum :: Int -> StatIndex # fromEnum :: StatIndex -> Int # enumFrom :: StatIndex -> [StatIndex] # enumFromThen :: StatIndex -> StatIndex -> [StatIndex] # enumFromTo :: StatIndex -> StatIndex -> [StatIndex] # enumFromThenTo :: StatIndex -> StatIndex -> StatIndex -> [StatIndex] #
Eq StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: StatIndex -> StatIndex -> Bool # (/=) :: StatIndex -> StatIndex -> Bool #
Ord StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods compare :: StatIndex -> StatIndex -> Ordering # (<) :: StatIndex -> StatIndex -> Bool # (<=) :: StatIndex -> StatIndex -> Bool # (>) :: StatIndex -> StatIndex -> Bool # (>=) :: StatIndex -> StatIndex -> Bool # max :: StatIndex -> StatIndex -> StatIndex # min :: StatIndex -> StatIndex -> StatIndex #
Read StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods readsPrec :: Int -> ReadS StatIndex # readList :: ReadS [StatIndex] # readPrec :: ReadPrec StatIndex # readListPrec :: ReadPrec [StatIndex] #
Show StatIndex Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> StatIndex -> ShowS # show :: StatIndex -> String # showList :: [StatIndex] -> ShowS #

data DumpMode Source #

formats of state dump

Constructors

NoDump
DumpCSVHeader
DumpCSV
DumpJSON

Instances

Bounded DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods minBound :: DumpMode # maxBound :: DumpMode #
Enum DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods succ :: DumpMode -> DumpMode # pred :: DumpMode -> DumpMode # toEnum :: Int -> DumpMode # fromEnum :: DumpMode -> Int # enumFrom :: DumpMode -> [DumpMode] # enumFromThen :: DumpMode -> DumpMode -> [DumpMode] # enumFromTo :: DumpMode -> DumpMode -> [DumpMode] # enumFromThenTo :: DumpMode -> DumpMode -> DumpMode -> [DumpMode] #
Eq DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods (==) :: DumpMode -> DumpMode -> Bool # (/=) :: DumpMode -> DumpMode -> Bool #
Ord DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods compare :: DumpMode -> DumpMode -> Ordering # (<) :: DumpMode -> DumpMode -> Bool # (<=) :: DumpMode -> DumpMode -> Bool # (>) :: DumpMode -> DumpMode -> Bool # (>=) :: DumpMode -> DumpMode -> Bool # max :: DumpMode -> DumpMode -> DumpMode # min :: DumpMode -> DumpMode -> DumpMode #
Read DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods readsPrec :: Int -> ReadS DumpMode # readList :: ReadS [DumpMode] # readPrec :: ReadPrec DumpMode # readListPrec :: ReadPrec [DumpMode] #
Show DumpMode Source #
Instance details Defined in SAT.Mios.Types Methods showsPrec :: Int -> DumpMode -> ShowS # show :: DumpMode -> String # showList :: [DumpMode] -> ShowS #