-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Solver.CDCL.Config
-- Copyright   :  (c) Masahiro Sakai 2017
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Solver.CDCL.Config
  ( -- * Solver configulation
    Config (..)
  , RestartStrategy (..)
  , showRestartStrategy
  , parseRestartStrategy
  , LearningStrategy (..)
  , showLearningStrategy
  , parseLearningStrategy
  , BranchingStrategy (..)
  , showBranchingStrategy
  , parseBranchingStrategy
  , PBHandlerType (..)
  , showPBHandlerType
  , parsePBHandlerType
  ) where

import Data.Char
import Data.Default.Class

data Config
  = Config
  { Config -> RestartStrategy
configRestartStrategy :: !RestartStrategy
  , Config -> Int
configRestartFirst :: !Int
    -- ^ The initial restart limit. (default 100)
    -- Zero and negative values are used to disable restart.
  , Config -> Double
configRestartInc :: !Double
    -- ^ The factor with which the restart limit is multiplied in each restart. (default 1.5)
    -- This must be @>1@.
  , Config -> LearningStrategy
configLearningStrategy :: !LearningStrategy
  , Config -> Int
configLearntSizeFirst :: !Int
    -- ^ The initial limit for learnt constraints.
    -- Negative value means computing default value from problem instance.
  , Config -> Double
configLearntSizeInc :: !Double
    -- ^ The limit for learnt constraints is multiplied with this factor periodically. (default 1.1)
    -- This must be @>1@.
  , Config -> Int
configCCMin :: !Int
    -- ^ Controls conflict constraint minimization (0=none, 1=local, 2=recursive)
  , Config -> BranchingStrategy
configBranchingStrategy :: !BranchingStrategy
  , Config -> Double
configERWAStepSizeFirst :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is initialized with this value. (default 0.4)
  , Config -> Double
configERWAStepSizeDec :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is decreased by this value after each conflict. (default 0.06)
  , Config -> Double
configERWAStepSizeMin :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is decreased until it reach the value. (default 0.06)
  , Config -> Double
configEMADecay :: !Double
    -- ^ inverse of the variable EMA decay factor used by LRB branching heuristic. (default 1 / 0.95)
  , Config -> Bool
configEnablePhaseSaving :: !Bool
  , Config -> Bool
configEnableForwardSubsumptionRemoval :: !Bool
  , Config -> Bool
configEnableBackwardSubsumptionRemoval :: !Bool
  , Config -> Double
configRandomFreq :: !Double
    -- ^ The frequency with which the decision heuristic tries to choose a random variable
  , Config -> PBHandlerType
configPBHandlerType :: !PBHandlerType
  , Config -> Bool
configEnablePBSplitClausePart :: !Bool
    -- ^ Split PB-constraints into a PB part and a clause part.
    --
    -- Example from minisat+ paper:
    --
    -- * 4 x1 + 4 x2 + 4 x3 + 4 x4 + 2y1 + y2 + y3 ≥ 4
    --
    -- would be split into
    --
    -- * x1 + x2 + x3 + x4 + ¬z ≥ 1 (clause part)
    --
    -- * 2 y1 + y2 + y3 + 4 z ≥ 4 (PB part)
    --
    -- where z is a newly introduced variable, not present in any other constraint.
    --
    -- Reference:
    --
    -- * N . Eéen and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.
    --
  , Config -> Bool
configCheckModel :: !Bool
  , Config -> Double
configVarDecay :: !Double
    -- ^ Inverse of the variable activity decay factor. (default 1 / 0.95)
  , Config -> Double
configConstrDecay :: !Double
    -- ^ Inverse of the constraint activity decay factor. (1 / 0.999)
  } deriving (Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show, Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq, Eq Config
Eq Config
-> (Config -> Config -> Ordering)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Bool)
-> (Config -> Config -> Config)
-> (Config -> Config -> Config)
-> Ord Config
Config -> Config -> Bool
Config -> Config -> Ordering
Config -> Config -> Config
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Config -> Config -> Config
$cmin :: Config -> Config -> Config
max :: Config -> Config -> Config
$cmax :: Config -> Config -> Config
>= :: Config -> Config -> Bool
$c>= :: Config -> Config -> Bool
> :: Config -> Config -> Bool
$c> :: Config -> Config -> Bool
<= :: Config -> Config -> Bool
$c<= :: Config -> Config -> Bool
< :: Config -> Config -> Bool
$c< :: Config -> Config -> Bool
compare :: Config -> Config -> Ordering
$ccompare :: Config -> Config -> Ordering
$cp1Ord :: Eq Config
Ord)

instance Default Config where
  def :: Config
def =
    Config :: RestartStrategy
-> Int
-> Double
-> LearningStrategy
-> Int
-> Double
-> Int
-> BranchingStrategy
-> Double
-> Double
-> Double
-> Double
-> Bool
-> Bool
-> Bool
-> Double
-> PBHandlerType
-> Bool
-> Bool
-> Double
-> Double
-> Config
Config
    { configRestartStrategy :: RestartStrategy
configRestartStrategy = RestartStrategy
forall a. Default a => a
def
    , configRestartFirst :: Int
configRestartFirst = Int
100
    , configRestartInc :: Double
configRestartInc = Double
1.5
    , configLearningStrategy :: LearningStrategy
configLearningStrategy = LearningStrategy
forall a. Default a => a
def
    , configLearntSizeFirst :: Int
configLearntSizeFirst = -Int
1
    , configLearntSizeInc :: Double
configLearntSizeInc = Double
1.1
    , configCCMin :: Int
configCCMin = Int
2
    , configBranchingStrategy :: BranchingStrategy
configBranchingStrategy = BranchingStrategy
forall a. Default a => a
def
    , configERWAStepSizeFirst :: Double
configERWAStepSizeFirst = Double
0.4
    , configERWAStepSizeDec :: Double
configERWAStepSizeDec = Double
10Double -> Double -> Double
forall a. Floating a => a -> a -> a
**(-Double
6)
    , configERWAStepSizeMin :: Double
configERWAStepSizeMin = Double
0.06
    , configEMADecay :: Double
configEMADecay = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
0.95
    , configEnablePhaseSaving :: Bool
configEnablePhaseSaving = Bool
True
    , configEnableForwardSubsumptionRemoval :: Bool
configEnableForwardSubsumptionRemoval = Bool
False
    , configEnableBackwardSubsumptionRemoval :: Bool
configEnableBackwardSubsumptionRemoval = Bool
False
    , configRandomFreq :: Double
configRandomFreq = Double
0.005
    , configPBHandlerType :: PBHandlerType
configPBHandlerType = PBHandlerType
forall a. Default a => a
def
    , configEnablePBSplitClausePart :: Bool
configEnablePBSplitClausePart = Bool
False
    , configCheckModel :: Bool
configCheckModel = Bool
False
    , configVarDecay :: Double
configVarDecay = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
0.95
    , configConstrDecay :: Double
configConstrDecay = Double
1 Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
0.999
    }

-- | Restart strategy.
--
-- The default value can be obtained by 'def'.
data RestartStrategy = MiniSATRestarts | ArminRestarts | LubyRestarts
  deriving (Int -> RestartStrategy -> ShowS
[RestartStrategy] -> ShowS
RestartStrategy -> String
(Int -> RestartStrategy -> ShowS)
-> (RestartStrategy -> String)
-> ([RestartStrategy] -> ShowS)
-> Show RestartStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RestartStrategy] -> ShowS
$cshowList :: [RestartStrategy] -> ShowS
show :: RestartStrategy -> String
$cshow :: RestartStrategy -> String
showsPrec :: Int -> RestartStrategy -> ShowS
$cshowsPrec :: Int -> RestartStrategy -> ShowS
Show, RestartStrategy -> RestartStrategy -> Bool
(RestartStrategy -> RestartStrategy -> Bool)
-> (RestartStrategy -> RestartStrategy -> Bool)
-> Eq RestartStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RestartStrategy -> RestartStrategy -> Bool
$c/= :: RestartStrategy -> RestartStrategy -> Bool
== :: RestartStrategy -> RestartStrategy -> Bool
$c== :: RestartStrategy -> RestartStrategy -> Bool
Eq, Eq RestartStrategy
Eq RestartStrategy
-> (RestartStrategy -> RestartStrategy -> Ordering)
-> (RestartStrategy -> RestartStrategy -> Bool)
-> (RestartStrategy -> RestartStrategy -> Bool)
-> (RestartStrategy -> RestartStrategy -> Bool)
-> (RestartStrategy -> RestartStrategy -> Bool)
-> (RestartStrategy -> RestartStrategy -> RestartStrategy)
-> (RestartStrategy -> RestartStrategy -> RestartStrategy)
-> Ord RestartStrategy
RestartStrategy -> RestartStrategy -> Bool
RestartStrategy -> RestartStrategy -> Ordering
RestartStrategy -> RestartStrategy -> RestartStrategy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RestartStrategy -> RestartStrategy -> RestartStrategy
$cmin :: RestartStrategy -> RestartStrategy -> RestartStrategy
max :: RestartStrategy -> RestartStrategy -> RestartStrategy
$cmax :: RestartStrategy -> RestartStrategy -> RestartStrategy
>= :: RestartStrategy -> RestartStrategy -> Bool
$c>= :: RestartStrategy -> RestartStrategy -> Bool
> :: RestartStrategy -> RestartStrategy -> Bool
$c> :: RestartStrategy -> RestartStrategy -> Bool
<= :: RestartStrategy -> RestartStrategy -> Bool
$c<= :: RestartStrategy -> RestartStrategy -> Bool
< :: RestartStrategy -> RestartStrategy -> Bool
$c< :: RestartStrategy -> RestartStrategy -> Bool
compare :: RestartStrategy -> RestartStrategy -> Ordering
$ccompare :: RestartStrategy -> RestartStrategy -> Ordering
$cp1Ord :: Eq RestartStrategy
Ord, Int -> RestartStrategy
RestartStrategy -> Int
RestartStrategy -> [RestartStrategy]
RestartStrategy -> RestartStrategy
RestartStrategy -> RestartStrategy -> [RestartStrategy]
RestartStrategy
-> RestartStrategy -> RestartStrategy -> [RestartStrategy]
(RestartStrategy -> RestartStrategy)
-> (RestartStrategy -> RestartStrategy)
-> (Int -> RestartStrategy)
-> (RestartStrategy -> Int)
-> (RestartStrategy -> [RestartStrategy])
-> (RestartStrategy -> RestartStrategy -> [RestartStrategy])
-> (RestartStrategy -> RestartStrategy -> [RestartStrategy])
-> (RestartStrategy
    -> RestartStrategy -> RestartStrategy -> [RestartStrategy])
-> Enum RestartStrategy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: RestartStrategy
-> RestartStrategy -> RestartStrategy -> [RestartStrategy]
$cenumFromThenTo :: RestartStrategy
-> RestartStrategy -> RestartStrategy -> [RestartStrategy]
enumFromTo :: RestartStrategy -> RestartStrategy -> [RestartStrategy]
$cenumFromTo :: RestartStrategy -> RestartStrategy -> [RestartStrategy]
enumFromThen :: RestartStrategy -> RestartStrategy -> [RestartStrategy]
$cenumFromThen :: RestartStrategy -> RestartStrategy -> [RestartStrategy]
enumFrom :: RestartStrategy -> [RestartStrategy]
$cenumFrom :: RestartStrategy -> [RestartStrategy]
fromEnum :: RestartStrategy -> Int
$cfromEnum :: RestartStrategy -> Int
toEnum :: Int -> RestartStrategy
$ctoEnum :: Int -> RestartStrategy
pred :: RestartStrategy -> RestartStrategy
$cpred :: RestartStrategy -> RestartStrategy
succ :: RestartStrategy -> RestartStrategy
$csucc :: RestartStrategy -> RestartStrategy
Enum, RestartStrategy
RestartStrategy -> RestartStrategy -> Bounded RestartStrategy
forall a. a -> a -> Bounded a
maxBound :: RestartStrategy
$cmaxBound :: RestartStrategy
minBound :: RestartStrategy
$cminBound :: RestartStrategy
Bounded)

instance Default RestartStrategy where
  def :: RestartStrategy
def = RestartStrategy
MiniSATRestarts

showRestartStrategy :: RestartStrategy -> String
showRestartStrategy :: RestartStrategy -> String
showRestartStrategy RestartStrategy
MiniSATRestarts = String
"minisat"
showRestartStrategy RestartStrategy
ArminRestarts = String
"armin"
showRestartStrategy RestartStrategy
LubyRestarts = String
"luby"

parseRestartStrategy :: String -> Maybe RestartStrategy
parseRestartStrategy :: String -> Maybe RestartStrategy
parseRestartStrategy String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"minisat" -> RestartStrategy -> Maybe RestartStrategy
forall a. a -> Maybe a
Just RestartStrategy
MiniSATRestarts
    String
"armin" -> RestartStrategy -> Maybe RestartStrategy
forall a. a -> Maybe a
Just RestartStrategy
ArminRestarts
    String
"luby" -> RestartStrategy -> Maybe RestartStrategy
forall a. a -> Maybe a
Just RestartStrategy
LubyRestarts
    String
_ -> Maybe RestartStrategy
forall a. Maybe a
Nothing

-- | Learning strategy.
--
-- The default value can be obtained by 'def'.
data LearningStrategy
  = LearningClause
  | LearningHybrid
  deriving (Int -> LearningStrategy -> ShowS
[LearningStrategy] -> ShowS
LearningStrategy -> String
(Int -> LearningStrategy -> ShowS)
-> (LearningStrategy -> String)
-> ([LearningStrategy] -> ShowS)
-> Show LearningStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LearningStrategy] -> ShowS
$cshowList :: [LearningStrategy] -> ShowS
show :: LearningStrategy -> String
$cshow :: LearningStrategy -> String
showsPrec :: Int -> LearningStrategy -> ShowS
$cshowsPrec :: Int -> LearningStrategy -> ShowS
Show, LearningStrategy -> LearningStrategy -> Bool
(LearningStrategy -> LearningStrategy -> Bool)
-> (LearningStrategy -> LearningStrategy -> Bool)
-> Eq LearningStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LearningStrategy -> LearningStrategy -> Bool
$c/= :: LearningStrategy -> LearningStrategy -> Bool
== :: LearningStrategy -> LearningStrategy -> Bool
$c== :: LearningStrategy -> LearningStrategy -> Bool
Eq, Eq LearningStrategy
Eq LearningStrategy
-> (LearningStrategy -> LearningStrategy -> Ordering)
-> (LearningStrategy -> LearningStrategy -> Bool)
-> (LearningStrategy -> LearningStrategy -> Bool)
-> (LearningStrategy -> LearningStrategy -> Bool)
-> (LearningStrategy -> LearningStrategy -> Bool)
-> (LearningStrategy -> LearningStrategy -> LearningStrategy)
-> (LearningStrategy -> LearningStrategy -> LearningStrategy)
-> Ord LearningStrategy
LearningStrategy -> LearningStrategy -> Bool
LearningStrategy -> LearningStrategy -> Ordering
LearningStrategy -> LearningStrategy -> LearningStrategy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LearningStrategy -> LearningStrategy -> LearningStrategy
$cmin :: LearningStrategy -> LearningStrategy -> LearningStrategy
max :: LearningStrategy -> LearningStrategy -> LearningStrategy
$cmax :: LearningStrategy -> LearningStrategy -> LearningStrategy
>= :: LearningStrategy -> LearningStrategy -> Bool
$c>= :: LearningStrategy -> LearningStrategy -> Bool
> :: LearningStrategy -> LearningStrategy -> Bool
$c> :: LearningStrategy -> LearningStrategy -> Bool
<= :: LearningStrategy -> LearningStrategy -> Bool
$c<= :: LearningStrategy -> LearningStrategy -> Bool
< :: LearningStrategy -> LearningStrategy -> Bool
$c< :: LearningStrategy -> LearningStrategy -> Bool
compare :: LearningStrategy -> LearningStrategy -> Ordering
$ccompare :: LearningStrategy -> LearningStrategy -> Ordering
$cp1Ord :: Eq LearningStrategy
Ord, Int -> LearningStrategy
LearningStrategy -> Int
LearningStrategy -> [LearningStrategy]
LearningStrategy -> LearningStrategy
LearningStrategy -> LearningStrategy -> [LearningStrategy]
LearningStrategy
-> LearningStrategy -> LearningStrategy -> [LearningStrategy]
(LearningStrategy -> LearningStrategy)
-> (LearningStrategy -> LearningStrategy)
-> (Int -> LearningStrategy)
-> (LearningStrategy -> Int)
-> (LearningStrategy -> [LearningStrategy])
-> (LearningStrategy -> LearningStrategy -> [LearningStrategy])
-> (LearningStrategy -> LearningStrategy -> [LearningStrategy])
-> (LearningStrategy
    -> LearningStrategy -> LearningStrategy -> [LearningStrategy])
-> Enum LearningStrategy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: LearningStrategy
-> LearningStrategy -> LearningStrategy -> [LearningStrategy]
$cenumFromThenTo :: LearningStrategy
-> LearningStrategy -> LearningStrategy -> [LearningStrategy]
enumFromTo :: LearningStrategy -> LearningStrategy -> [LearningStrategy]
$cenumFromTo :: LearningStrategy -> LearningStrategy -> [LearningStrategy]
enumFromThen :: LearningStrategy -> LearningStrategy -> [LearningStrategy]
$cenumFromThen :: LearningStrategy -> LearningStrategy -> [LearningStrategy]
enumFrom :: LearningStrategy -> [LearningStrategy]
$cenumFrom :: LearningStrategy -> [LearningStrategy]
fromEnum :: LearningStrategy -> Int
$cfromEnum :: LearningStrategy -> Int
toEnum :: Int -> LearningStrategy
$ctoEnum :: Int -> LearningStrategy
pred :: LearningStrategy -> LearningStrategy
$cpred :: LearningStrategy -> LearningStrategy
succ :: LearningStrategy -> LearningStrategy
$csucc :: LearningStrategy -> LearningStrategy
Enum, LearningStrategy
LearningStrategy -> LearningStrategy -> Bounded LearningStrategy
forall a. a -> a -> Bounded a
maxBound :: LearningStrategy
$cmaxBound :: LearningStrategy
minBound :: LearningStrategy
$cminBound :: LearningStrategy
Bounded)

instance Default LearningStrategy where
  def :: LearningStrategy
def = LearningStrategy
LearningClause

showLearningStrategy :: LearningStrategy -> String
showLearningStrategy :: LearningStrategy -> String
showLearningStrategy LearningStrategy
LearningClause = String
"clause"
showLearningStrategy LearningStrategy
LearningHybrid = String
"hybrid"

parseLearningStrategy :: String -> Maybe LearningStrategy
parseLearningStrategy :: String -> Maybe LearningStrategy
parseLearningStrategy String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"clause" -> LearningStrategy -> Maybe LearningStrategy
forall a. a -> Maybe a
Just LearningStrategy
LearningClause
    String
"hybrid" -> LearningStrategy -> Maybe LearningStrategy
forall a. a -> Maybe a
Just LearningStrategy
LearningHybrid
    String
_ -> Maybe LearningStrategy
forall a. Maybe a
Nothing

-- | Branching strategy.
--
-- The default value can be obtained by 'def'.
--
-- 'BranchingERWA' and 'BranchingLRB' is based on [Liang et al 2016].
--
-- * J. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning rate based branching heuristic for SAT solvers,"
--   in Proceedings of Theory and Applications of Satisfiability Testing (SAT 2016), pp. 123-140.
--   <http://link.springer.com/chapter/10.1007/978-3-319-40970-2_9>
--   <https://cs.uwaterloo.ca/~ppoupart/publications/sat/learning-rate-branching-heuristic-SAT.pdf>
data BranchingStrategy
  = BranchingVSIDS
    -- ^ VSIDS (Variable State Independent Decaying Sum) branching heuristic
  | BranchingERWA
    -- ^ ERWA (Exponential Recency Weighted Average) branching heuristic
  | BranchingLRB
    -- ^ LRB (Learning Rate Branching) heuristic
  deriving (Int -> BranchingStrategy -> ShowS
[BranchingStrategy] -> ShowS
BranchingStrategy -> String
(Int -> BranchingStrategy -> ShowS)
-> (BranchingStrategy -> String)
-> ([BranchingStrategy] -> ShowS)
-> Show BranchingStrategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BranchingStrategy] -> ShowS
$cshowList :: [BranchingStrategy] -> ShowS
show :: BranchingStrategy -> String
$cshow :: BranchingStrategy -> String
showsPrec :: Int -> BranchingStrategy -> ShowS
$cshowsPrec :: Int -> BranchingStrategy -> ShowS
Show, BranchingStrategy -> BranchingStrategy -> Bool
(BranchingStrategy -> BranchingStrategy -> Bool)
-> (BranchingStrategy -> BranchingStrategy -> Bool)
-> Eq BranchingStrategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BranchingStrategy -> BranchingStrategy -> Bool
$c/= :: BranchingStrategy -> BranchingStrategy -> Bool
== :: BranchingStrategy -> BranchingStrategy -> Bool
$c== :: BranchingStrategy -> BranchingStrategy -> Bool
Eq, Eq BranchingStrategy
Eq BranchingStrategy
-> (BranchingStrategy -> BranchingStrategy -> Ordering)
-> (BranchingStrategy -> BranchingStrategy -> Bool)
-> (BranchingStrategy -> BranchingStrategy -> Bool)
-> (BranchingStrategy -> BranchingStrategy -> Bool)
-> (BranchingStrategy -> BranchingStrategy -> Bool)
-> (BranchingStrategy -> BranchingStrategy -> BranchingStrategy)
-> (BranchingStrategy -> BranchingStrategy -> BranchingStrategy)
-> Ord BranchingStrategy
BranchingStrategy -> BranchingStrategy -> Bool
BranchingStrategy -> BranchingStrategy -> Ordering
BranchingStrategy -> BranchingStrategy -> BranchingStrategy
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy
$cmin :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy
max :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy
$cmax :: BranchingStrategy -> BranchingStrategy -> BranchingStrategy
>= :: BranchingStrategy -> BranchingStrategy -> Bool
$c>= :: BranchingStrategy -> BranchingStrategy -> Bool
> :: BranchingStrategy -> BranchingStrategy -> Bool
$c> :: BranchingStrategy -> BranchingStrategy -> Bool
<= :: BranchingStrategy -> BranchingStrategy -> Bool
$c<= :: BranchingStrategy -> BranchingStrategy -> Bool
< :: BranchingStrategy -> BranchingStrategy -> Bool
$c< :: BranchingStrategy -> BranchingStrategy -> Bool
compare :: BranchingStrategy -> BranchingStrategy -> Ordering
$ccompare :: BranchingStrategy -> BranchingStrategy -> Ordering
$cp1Ord :: Eq BranchingStrategy
Ord, Int -> BranchingStrategy
BranchingStrategy -> Int
BranchingStrategy -> [BranchingStrategy]
BranchingStrategy -> BranchingStrategy
BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
BranchingStrategy
-> BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
(BranchingStrategy -> BranchingStrategy)
-> (BranchingStrategy -> BranchingStrategy)
-> (Int -> BranchingStrategy)
-> (BranchingStrategy -> Int)
-> (BranchingStrategy -> [BranchingStrategy])
-> (BranchingStrategy -> BranchingStrategy -> [BranchingStrategy])
-> (BranchingStrategy -> BranchingStrategy -> [BranchingStrategy])
-> (BranchingStrategy
    -> BranchingStrategy -> BranchingStrategy -> [BranchingStrategy])
-> Enum BranchingStrategy
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: BranchingStrategy
-> BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
$cenumFromThenTo :: BranchingStrategy
-> BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
enumFromTo :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
$cenumFromTo :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
enumFromThen :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
$cenumFromThen :: BranchingStrategy -> BranchingStrategy -> [BranchingStrategy]
enumFrom :: BranchingStrategy -> [BranchingStrategy]
$cenumFrom :: BranchingStrategy -> [BranchingStrategy]
fromEnum :: BranchingStrategy -> Int
$cfromEnum :: BranchingStrategy -> Int
toEnum :: Int -> BranchingStrategy
$ctoEnum :: Int -> BranchingStrategy
pred :: BranchingStrategy -> BranchingStrategy
$cpred :: BranchingStrategy -> BranchingStrategy
succ :: BranchingStrategy -> BranchingStrategy
$csucc :: BranchingStrategy -> BranchingStrategy
Enum, BranchingStrategy
BranchingStrategy -> BranchingStrategy -> Bounded BranchingStrategy
forall a. a -> a -> Bounded a
maxBound :: BranchingStrategy
$cmaxBound :: BranchingStrategy
minBound :: BranchingStrategy
$cminBound :: BranchingStrategy
Bounded)

instance Default BranchingStrategy where
  def :: BranchingStrategy
def = BranchingStrategy
BranchingVSIDS

showBranchingStrategy :: BranchingStrategy -> String
showBranchingStrategy :: BranchingStrategy -> String
showBranchingStrategy BranchingStrategy
BranchingVSIDS = String
"vsids"
showBranchingStrategy BranchingStrategy
BranchingERWA  = String
"erwa"
showBranchingStrategy BranchingStrategy
BranchingLRB   = String
"lrb"

parseBranchingStrategy :: String -> Maybe BranchingStrategy
parseBranchingStrategy :: String -> Maybe BranchingStrategy
parseBranchingStrategy String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"vsids" -> BranchingStrategy -> Maybe BranchingStrategy
forall a. a -> Maybe a
Just BranchingStrategy
BranchingVSIDS
    String
"erwa"  -> BranchingStrategy -> Maybe BranchingStrategy
forall a. a -> Maybe a
Just BranchingStrategy
BranchingERWA
    String
"lrb"   -> BranchingStrategy -> Maybe BranchingStrategy
forall a. a -> Maybe a
Just BranchingStrategy
BranchingLRB
    String
_ -> Maybe BranchingStrategy
forall a. Maybe a
Nothing

-- | Pseudo boolean constraint handler implimentation.
--
-- The default value can be obtained by 'def'.
data PBHandlerType = PBHandlerTypeCounter | PBHandlerTypePueblo
  deriving (Int -> PBHandlerType -> ShowS
[PBHandlerType] -> ShowS
PBHandlerType -> String
(Int -> PBHandlerType -> ShowS)
-> (PBHandlerType -> String)
-> ([PBHandlerType] -> ShowS)
-> Show PBHandlerType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PBHandlerType] -> ShowS
$cshowList :: [PBHandlerType] -> ShowS
show :: PBHandlerType -> String
$cshow :: PBHandlerType -> String
showsPrec :: Int -> PBHandlerType -> ShowS
$cshowsPrec :: Int -> PBHandlerType -> ShowS
Show, PBHandlerType -> PBHandlerType -> Bool
(PBHandlerType -> PBHandlerType -> Bool)
-> (PBHandlerType -> PBHandlerType -> Bool) -> Eq PBHandlerType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PBHandlerType -> PBHandlerType -> Bool
$c/= :: PBHandlerType -> PBHandlerType -> Bool
== :: PBHandlerType -> PBHandlerType -> Bool
$c== :: PBHandlerType -> PBHandlerType -> Bool
Eq, Eq PBHandlerType
Eq PBHandlerType
-> (PBHandlerType -> PBHandlerType -> Ordering)
-> (PBHandlerType -> PBHandlerType -> Bool)
-> (PBHandlerType -> PBHandlerType -> Bool)
-> (PBHandlerType -> PBHandlerType -> Bool)
-> (PBHandlerType -> PBHandlerType -> Bool)
-> (PBHandlerType -> PBHandlerType -> PBHandlerType)
-> (PBHandlerType -> PBHandlerType -> PBHandlerType)
-> Ord PBHandlerType
PBHandlerType -> PBHandlerType -> Bool
PBHandlerType -> PBHandlerType -> Ordering
PBHandlerType -> PBHandlerType -> PBHandlerType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PBHandlerType -> PBHandlerType -> PBHandlerType
$cmin :: PBHandlerType -> PBHandlerType -> PBHandlerType
max :: PBHandlerType -> PBHandlerType -> PBHandlerType
$cmax :: PBHandlerType -> PBHandlerType -> PBHandlerType
>= :: PBHandlerType -> PBHandlerType -> Bool
$c>= :: PBHandlerType -> PBHandlerType -> Bool
> :: PBHandlerType -> PBHandlerType -> Bool
$c> :: PBHandlerType -> PBHandlerType -> Bool
<= :: PBHandlerType -> PBHandlerType -> Bool
$c<= :: PBHandlerType -> PBHandlerType -> Bool
< :: PBHandlerType -> PBHandlerType -> Bool
$c< :: PBHandlerType -> PBHandlerType -> Bool
compare :: PBHandlerType -> PBHandlerType -> Ordering
$ccompare :: PBHandlerType -> PBHandlerType -> Ordering
$cp1Ord :: Eq PBHandlerType
Ord, Int -> PBHandlerType
PBHandlerType -> Int
PBHandlerType -> [PBHandlerType]
PBHandlerType -> PBHandlerType
PBHandlerType -> PBHandlerType -> [PBHandlerType]
PBHandlerType -> PBHandlerType -> PBHandlerType -> [PBHandlerType]
(PBHandlerType -> PBHandlerType)
-> (PBHandlerType -> PBHandlerType)
-> (Int -> PBHandlerType)
-> (PBHandlerType -> Int)
-> (PBHandlerType -> [PBHandlerType])
-> (PBHandlerType -> PBHandlerType -> [PBHandlerType])
-> (PBHandlerType -> PBHandlerType -> [PBHandlerType])
-> (PBHandlerType
    -> PBHandlerType -> PBHandlerType -> [PBHandlerType])
-> Enum PBHandlerType
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: PBHandlerType -> PBHandlerType -> PBHandlerType -> [PBHandlerType]
$cenumFromThenTo :: PBHandlerType -> PBHandlerType -> PBHandlerType -> [PBHandlerType]
enumFromTo :: PBHandlerType -> PBHandlerType -> [PBHandlerType]
$cenumFromTo :: PBHandlerType -> PBHandlerType -> [PBHandlerType]
enumFromThen :: PBHandlerType -> PBHandlerType -> [PBHandlerType]
$cenumFromThen :: PBHandlerType -> PBHandlerType -> [PBHandlerType]
enumFrom :: PBHandlerType -> [PBHandlerType]
$cenumFrom :: PBHandlerType -> [PBHandlerType]
fromEnum :: PBHandlerType -> Int
$cfromEnum :: PBHandlerType -> Int
toEnum :: Int -> PBHandlerType
$ctoEnum :: Int -> PBHandlerType
pred :: PBHandlerType -> PBHandlerType
$cpred :: PBHandlerType -> PBHandlerType
succ :: PBHandlerType -> PBHandlerType
$csucc :: PBHandlerType -> PBHandlerType
Enum, PBHandlerType
PBHandlerType -> PBHandlerType -> Bounded PBHandlerType
forall a. a -> a -> Bounded a
maxBound :: PBHandlerType
$cmaxBound :: PBHandlerType
minBound :: PBHandlerType
$cminBound :: PBHandlerType
Bounded)

instance Default PBHandlerType where
  def :: PBHandlerType
def = PBHandlerType
PBHandlerTypeCounter

showPBHandlerType :: PBHandlerType -> String
showPBHandlerType :: PBHandlerType -> String
showPBHandlerType PBHandlerType
PBHandlerTypeCounter = String
"counter"
showPBHandlerType PBHandlerType
PBHandlerTypePueblo = String
"pueblo"

parsePBHandlerType :: String -> Maybe PBHandlerType
parsePBHandlerType :: String -> Maybe PBHandlerType
parsePBHandlerType String
s =
  case (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
s of
    String
"counter" -> PBHandlerType -> Maybe PBHandlerType
forall a. a -> Maybe a
Just PBHandlerType
PBHandlerTypeCounter
    String
"pueblo" -> PBHandlerType -> Maybe PBHandlerType
forall a. a -> Maybe a
Just PBHandlerType
PBHandlerTypePueblo
    String
_ -> Maybe PBHandlerType
forall a. Maybe a
Nothing