module ToySolver.SAT.Config
(
Config (..)
, RestartStrategy (..)
, showRestartStrategy
, parseRestartStrategy
, LearningStrategy (..)
, showLearningStrategy
, parseLearningStrategy
, BranchingStrategy (..)
, showBranchingStrategy
, parseBranchingStrategy
, PBHandlerType (..)
, showPBHandlerType
, parsePBHandlerType
) 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 = 100
, configRestartInc = 1.5
, configLearningStrategy = def
, configLearntSizeFirst = -1
, configLearntSizeInc = 1.1
, configCCMin = 2
, configBranchingStrategy = def
, configERWAStepSizeFirst = 0.4
, configERWAStepSizeDec = 10**(-6)
, configERWAStepSizeMin = 0.06
, configEMADecay = 1 / 0.95
, configEnablePhaseSaving = True
, configEnableForwardSubsumptionRemoval = False
, configEnableBackwardSubsumptionRemoval = False
, configRandomFreq = 0.005
, configPBHandlerType = def
, configEnablePBSplitClausePart = False
, 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
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
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