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