module ToySolver.SAT.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
  { configRestartStrategy :: !RestartStrategy
  , configRestartFirst :: !Int
    -- ^ The initial restart limit. (default 100)
    -- Zero and negative values are used to disable restart.
  , configRestartInc :: !Double
    -- ^ The factor with which the restart limit is multiplied in each restart. (default 1.5)
    -- This must be @>1@.
  , configLearningStrategy :: !LearningStrategy
  , configLearntSizeFirst :: !Int
    -- ^ The initial limit for learnt constraints.
    -- Negative value means computing default value from problem instance.
  , configLearntSizeInc :: !Double
    -- ^ The limit for learnt constraints is multiplied with this factor periodically. (default 1.1)
    -- This must be @>1@.                     
  , configCCMin :: !Int
    -- ^ Controls conflict constraint minimization (0=none, 1=local, 2=recursive)
  , configBranchingStrategy :: !BranchingStrategy
  , configERWAStepSizeFirst :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is initialized with this value. (default 0.4)
  , configERWAStepSizeDec :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is decreased by this value after each conflict. (default 0.06)
  , configERWAStepSizeMin :: !Double
    -- ^ step-size α in ERWA and LRB branching heuristic is decreased until it reach the value. (default 0.06)
  , configEMADecay :: !Double
    -- ^ inverse of the variable EMA decay factor used by LRB branching heuristic. (default 1 / 0.95)
  , configEnablePhaseSaving :: !Bool
  , configEnableForwardSubsumptionRemoval :: !Bool
  , configEnableBackwardSubsumptionRemoval :: !Bool
  , configRandomFreq :: !Double
    -- ^ The frequency with which the decision heuristic tries to choose a random variable
  , configPBHandlerType :: !PBHandlerType
  , 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.
    --                               
  , configCheckModel :: !Bool
  , configVarDecay :: !Double
    -- ^ Inverse of the variable activity decay factor. (default 1 / 0.95)
  , configConstrDecay :: !Double
    -- ^ Inverse of the constraint activity decay factor. (1 / 0.999)
  } 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
    }

-- | Restart strategy.
--
-- The default value can be obtained by 'def'.
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

-- | Learning strategy.
--
-- The default value can be obtained by 'def'.
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

-- | 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 (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

-- | Pseudo boolean constraint handler implimentation.
--
-- The default value can be obtained by 'def'.
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