module Satyros.DPLL.Decision where import Control.Lens (use) import qualified Data.Set as Set import qualified Satyros.CNF as CNF import Satyros.DPLL.Effect (DPLL, decisionComplete, decisionResult) import Satyros.DPLL.Storage (unassignedVariables) import Satyros.DPLL.StorageUtil (assignDecisionVariable) import System.Random.Stateful (StateGenM (StateGenM), randomM, randomRM) decision :: (Functor f) => DPLL s f () decision :: DPLL s f () decision = do Set Variable xs <- Getting (Set Variable) (Storage s) (Set Variable) -> DPLL s f (Set Variable) forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a use Getting (Set Variable) (Storage s) (Set Variable) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables if Set Variable -> Bool forall a. Set a -> Bool Set.null Set Variable xs then DPLL s f () forall (f :: * -> *) s. Functor f => DPLL s f () decisionComplete else do Int i <- (Int, Int) -> StateGenM (Storage s) -> DPLL s f Int forall g r (m :: * -> *) a. (RandomGenM g r m, Random a) => (a, a) -> g -> m a randomRM (Int 0, Set Variable -> Int forall a. Set a -> Int Set.size Set Variable xs Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) StateGenM (Storage s) forall g. StateGenM g StateGenM Positivity s <- StateGenM (Storage s) -> DPLL s f Positivity forall g r (m :: * -> *) a. (RandomGenM g r m, Random a) => g -> m a randomM StateGenM (Storage s) forall g. StateGenM g StateGenM Literal -> DPLL s f () forall (f :: * -> *) s. Functor f => Literal -> DPLL s f () decisionResult (Literal -> DPLL s f ()) -> (Variable -> Literal) -> Variable -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Positivity -> Variable -> Literal CNF.Literal Positivity s (Variable -> DPLL s f ()) -> Variable -> DPLL s f () forall a b. (a -> b) -> a -> b $ Set Variable -> [Variable] forall a. Set a -> [a] Set.toList Set Variable xs [Variable] -> Int -> Variable forall a. [a] -> Int -> a !! Int i decisionResultHandler :: (Functor f) => CNF.Literal -> DPLL s f () decisionResultHandler :: Literal -> DPLL s f () decisionResultHandler = Literal -> DPLL s f () forall (f :: * -> *) s. Functor f => Literal -> DPLL s f () assignDecisionVariable