module ToySolver.SAT.Config
(
Config (..)
, RestartStrategy (..)
, showRestartStrategy
, parseRestartStrategy
, LearningStrategy (..)
, showLearningStrategy
, parseLearningStrategy
, BranchingStrategy (..)
, showBranchingStrategy
, parseBranchingStrategy
, PBHandlerType (..)
, showPBHandlerType
, parsePBHandlerType
, defaultRestartFirst
, defaultRestartInc
, defaultLearntSizeFirst
, defaultLearntSizeInc
, defaultCCMin
, defaultEnablePhaseSaving
, defaultEnableForwardSubsumptionRemoval
, defaultEnableBackwardSubsumptionRemoval
, defaultRandomFreq
, defaultPBSplitClausePart
) where
import Data.Char
import Data.Default.Class
data Config
= Config
{ configRestartStrategy :: !RestartStrategy
, configRestartFirst :: !Int
, configRestartInc :: !Double
, configLearningStrategy :: !LearningStrategy
, configLearntSizeFirst :: !Int
, configLearntSizeInc :: !Double
, configCCMin :: !Int
, configBranchingStrategy :: !BranchingStrategy
, configERWAStepSizeFirst :: !Double
, configERWAStepSizeDec :: !Double
, configERWAStepSizeMin :: !Double
, configEMADecay :: !Double
, configEnablePhaseSaving :: !Bool
, configEnableForwardSubsumptionRemoval :: !Bool
, configEnableBackwardSubsumptionRemoval :: !Bool
, configRandomFreq :: !Double
, configPBHandlerType :: !PBHandlerType
, configEnablePBSplitClausePart :: !Bool
, configCheckModel :: !Bool
, configVarDecay :: !Double
, configConstrDecay :: !Double
} deriving (Show, Eq, Ord)
instance Default Config where
def =
Config
{ configRestartStrategy = def
, configRestartFirst = defaultRestartFirst
, configRestartInc = defaultRestartInc
, configLearningStrategy = def
, configLearntSizeFirst = defaultLearntSizeFirst
, configLearntSizeInc = defaultLearntSizeInc
, configCCMin = defaultCCMin
, configBranchingStrategy = def
, configERWAStepSizeFirst = 0.4
, configERWAStepSizeDec = 10**(6)
, configERWAStepSizeMin = 0.06
, configEMADecay = 1 / 0.95
, configEnablePhaseSaving = defaultEnablePhaseSaving
, configEnableForwardSubsumptionRemoval = defaultEnableForwardSubsumptionRemoval
, configEnableBackwardSubsumptionRemoval = defaultEnableBackwardSubsumptionRemoval
, configRandomFreq = defaultRandomFreq
, configPBHandlerType = def
, configEnablePBSplitClausePart = defaultPBSplitClausePart
, configCheckModel = False
, configVarDecay = 1 / 0.95
, configConstrDecay = 1 / 0.999
}
data RestartStrategy = MiniSATRestarts | ArminRestarts | LubyRestarts
deriving (Show, Eq, Ord, Enum, Bounded)
instance Default RestartStrategy where
def = MiniSATRestarts
showRestartStrategy :: RestartStrategy -> String
showRestartStrategy MiniSATRestarts = "minisat"
showRestartStrategy ArminRestarts = "armin"
showRestartStrategy LubyRestarts = "luby"
parseRestartStrategy :: String -> Maybe RestartStrategy
parseRestartStrategy s =
case map toLower s of
"minisat" -> Just MiniSATRestarts
"armin" -> Just ArminRestarts
"luby" -> Just LubyRestarts
_ -> Nothing
defaultRestartFirst :: Int
defaultRestartFirst = 100
defaultRestartInc :: Double
defaultRestartInc = 1.5
data LearningStrategy
= LearningClause
| LearningHybrid
deriving (Show, Eq, Ord, Enum, Bounded)
instance Default LearningStrategy where
def = LearningClause
showLearningStrategy :: LearningStrategy -> String
showLearningStrategy LearningClause = "clause"
showLearningStrategy LearningHybrid = "hybrid"
parseLearningStrategy :: String -> Maybe LearningStrategy
parseLearningStrategy s =
case map toLower s of
"clause" -> Just LearningClause
"hybrid" -> Just LearningHybrid
_ -> Nothing
data BranchingStrategy
= BranchingVSIDS
| BranchingERWA
| BranchingLRB
deriving (Show, Eq, Ord, Enum, Bounded)
instance Default BranchingStrategy where
def = BranchingVSIDS
showBranchingStrategy :: BranchingStrategy -> String
showBranchingStrategy BranchingVSIDS = "vsids"
showBranchingStrategy BranchingERWA = "erwa"
showBranchingStrategy BranchingLRB = "lrb"
parseBranchingStrategy :: String -> Maybe BranchingStrategy
parseBranchingStrategy s =
case map toLower s of
"vsids" -> Just BranchingVSIDS
"erwa" -> Just BranchingERWA
"lrb" -> Just BranchingLRB
_ -> Nothing
defaultLearntSizeFirst :: Int
defaultLearntSizeFirst = 1
defaultLearntSizeInc :: Double
defaultLearntSizeInc = 1.1
defaultCCMin :: Int
defaultCCMin = 2
defaultRandomFreq :: Double
defaultRandomFreq = 0.005
data PBHandlerType = PBHandlerTypeCounter | PBHandlerTypePueblo
deriving (Show, Eq, Ord, Enum, Bounded)
instance Default PBHandlerType where
def = PBHandlerTypeCounter
showPBHandlerType :: PBHandlerType -> String
showPBHandlerType PBHandlerTypeCounter = "counter"
showPBHandlerType PBHandlerTypePueblo = "pueblo"
parsePBHandlerType :: String -> Maybe PBHandlerType
parsePBHandlerType s =
case map toLower s of
"counter" -> Just PBHandlerTypeCounter
"pueblo" -> Just PBHandlerTypePueblo
_ -> Nothing
defaultPBSplitClausePart :: Bool
defaultPBSplitClausePart = False
defaultEnablePhaseSaving :: Bool
defaultEnablePhaseSaving = True
defaultEnableForwardSubsumptionRemoval :: Bool
defaultEnableForwardSubsumptionRemoval = False
defaultEnableBackwardSubsumptionRemoval :: Bool
defaultEnableBackwardSubsumptionRemoval = False