packages feed

moonlight-core-0.1.0.0: src-solver/Moonlight/Core/Fixpoint/Dense/Internal/Policy.hs

-- | The adaptive push/pull reachability policy: validated ratio thresholds and
-- the small-frontier cutoff that decide when to switch traversal direction.
module Moonlight.Core.Fixpoint.Dense.Internal.Policy
  ( ReachabilityPolicy (..),
    ReachabilityPolicyValidationError (..),
    mkReachabilityPolicy,
    defaultReachabilityPolicy,
  )
where

import Prelude

data ReachabilityPolicy = ReachabilityPolicy
  { pushToPullRatio :: !Double,
    pullToPushRatio :: !Double,
    smallFrontierLimit :: !Int
  }
  deriving stock (Eq, Show)

data ReachabilityPolicyValidationError
  = PushToPullRatioIsNaN
  | PullToPushRatioIsNaN
  | NegativePushToPullRatio !Double
  | NegativePullToPushRatio !Double
  | NegativeSmallFrontierLimit !Int
  deriving stock (Eq, Show)

mkReachabilityPolicy :: Double -> Double -> Int -> Either ReachabilityPolicyValidationError ReachabilityPolicy
mkReachabilityPolicy pushRatio pullRatio frontierLimit
  | isNaN pushRatio =
      Left PushToPullRatioIsNaN
  | isNaN pullRatio =
      Left PullToPushRatioIsNaN
  | pushRatio < 0 =
      Left (NegativePushToPullRatio pushRatio)
  | pullRatio < 0 =
      Left (NegativePullToPushRatio pullRatio)
  | frontierLimit < 0 =
      Left (NegativeSmallFrontierLimit frontierLimit)
  | otherwise =
      Right
        ReachabilityPolicy
          { pushToPullRatio = pushRatio,
            pullToPushRatio = pullRatio,
            smallFrontierLimit = frontierLimit
          }

defaultReachabilityPolicy :: ReachabilityPolicy
defaultReachabilityPolicy =
  ReachabilityPolicy
    { pushToPullRatio = 0.05,
      pullToPushRatio = 0.20,
      smallFrontierLimit = 64
    }