module Satyros.DPLL.Assignment where

import           Control.Lens (At (at), Index, IxValue, Ixed, Traversal',
                               Wrapped (Unwrapped, _Wrapped'), _1, _2, _Just,
                               from, iso, ix, (?~))
import           Data.Bool    (bool)
import           Data.Map     (Map)
import qualified Data.Map     as Map
import           Data.Set     (Set)
import           GHC.Generics (Generic)
import qualified Satyros.CNF  as CNF

newtype Assignment = Assignment { Assignment -> Map Variable (Bool, Maybe Clause)
getAssignment :: Map CNF.Variable (Bool, Maybe CNF.Clause) }
  deriving stock ((forall x. Assignment -> Rep Assignment x)
-> (forall x. Rep Assignment x -> Assignment) -> Generic Assignment
forall x. Rep Assignment x -> Assignment
forall x. Assignment -> Rep Assignment x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Assignment x -> Assignment
$cfrom :: forall x. Assignment -> Rep Assignment x
Generic)
  deriving newtype (Int -> Assignment -> ShowS
[Assignment] -> ShowS
Assignment -> String
(Int -> Assignment -> ShowS)
-> (Assignment -> String)
-> ([Assignment] -> ShowS)
-> Show Assignment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Assignment] -> ShowS
$cshowList :: [Assignment] -> ShowS
show :: Assignment -> String
$cshow :: Assignment -> String
showsPrec :: Int -> Assignment -> ShowS
$cshowsPrec :: Int -> Assignment -> ShowS
Show)

instance Wrapped Assignment where
  type Unwrapped Assignment = Map CNF.Variable (Bool, Maybe CNF.Clause)
  _Wrapped' :: p (Unwrapped Assignment) (f (Unwrapped Assignment))
-> p Assignment (f Assignment)
_Wrapped' = (Assignment -> Map Variable (Bool, Maybe Clause))
-> (Map Variable (Bool, Maybe Clause) -> Assignment)
-> Iso
     Assignment
     Assignment
     (Map Variable (Bool, Maybe Clause))
     (Map Variable (Bool, Maybe Clause))
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso Assignment -> Map Variable (Bool, Maybe Clause)
getAssignment Map Variable (Bool, Maybe Clause) -> Assignment
Assignment

type instance Index Assignment = CNF.Variable
type instance IxValue Assignment = (Bool, Maybe CNF.Clause)

instance Ixed Assignment
instance At Assignment where
  at :: Index Assignment -> Lens' Assignment (Maybe (IxValue Assignment))
at Index Assignment
i = (Map Variable (Bool, Maybe Clause)
 -> f (Map Variable (Bool, Maybe Clause)))
-> Assignment -> f Assignment
forall s. Wrapped s => Iso' s (Unwrapped s)
_Wrapped' ((Map Variable (Bool, Maybe Clause)
  -> f (Map Variable (Bool, Maybe Clause)))
 -> Assignment -> f Assignment)
-> ((Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause)))
    -> Map Variable (Bool, Maybe Clause)
    -> f (Map Variable (Bool, Maybe Clause)))
-> (Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause)))
-> Assignment
-> f Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map Variable (Bool, Maybe Clause))
-> Lens'
     (Map Variable (Bool, Maybe Clause))
     (Maybe (IxValue (Map Variable (Bool, Maybe Clause))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index (Map Variable (Bool, Maybe Clause))
Index Assignment
i

assignVariable :: CNF.Literal -> Maybe CNF.Clause -> Assignment -> Assignment
assignVariable :: Literal -> Maybe Clause -> Assignment -> Assignment
assignVariable (CNF.Literal Positivity
CNF.Positive Variable
x) Maybe Clause
p = Index Assignment -> Lens' Assignment (Maybe (IxValue Assignment))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Assignment
Variable
x ((Maybe (Bool, Maybe Clause)
  -> Identity (Maybe (Bool, Maybe Clause)))
 -> Assignment -> Identity Assignment)
-> (Bool, Maybe Clause) -> Assignment -> Assignment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Bool
True, Maybe Clause
p)
assignVariable (CNF.Literal Positivity
CNF.Negative Variable
x) Maybe Clause
p = Index Assignment -> Lens' Assignment (Maybe (IxValue Assignment))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Assignment
Variable
x ((Maybe (Bool, Maybe Clause)
  -> Identity (Maybe (Bool, Maybe Clause)))
 -> Assignment -> Identity Assignment)
-> (Bool, Maybe Clause) -> Assignment -> Assignment
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ (Bool
False, Maybe Clause
p)

eraseVariables :: Set CNF.Variable -> Assignment -> Assignment
eraseVariables :: Set Variable -> Assignment -> Assignment
eraseVariables Set Variable
xs = Map Variable (Bool, Maybe Clause) -> Assignment
Assignment (Map Variable (Bool, Maybe Clause) -> Assignment)
-> (Assignment -> Map Variable (Bool, Maybe Clause))
-> Assignment
-> Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Variable (Bool, Maybe Clause)
 -> Set Variable -> Map Variable (Bool, Maybe Clause))
-> Set Variable
-> Map Variable (Bool, Maybe Clause)
-> Map Variable (Bool, Maybe Clause)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Map Variable (Bool, Maybe Clause)
-> Set Variable -> Map Variable (Bool, Maybe Clause)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Set Variable
xs (Map Variable (Bool, Maybe Clause)
 -> Map Variable (Bool, Maybe Clause))
-> (Assignment -> Map Variable (Bool, Maybe Clause))
-> Assignment
-> Map Variable (Bool, Maybe Clause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assignment -> Map Variable (Bool, Maybe Clause)
getAssignment

valueOfVariable :: CNF.Variable -> Traversal' Assignment Bool
valueOfVariable :: Variable -> Traversal' Assignment Bool
valueOfVariable Variable
x = Index Assignment -> Traversal' Assignment (IxValue Assignment)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Assignment
Variable
x (((Bool, Maybe Clause) -> f (Bool, Maybe Clause))
 -> Assignment -> f Assignment)
-> ((Bool -> f Bool)
    -> (Bool, Maybe Clause) -> f (Bool, Maybe Clause))
-> (Bool -> f Bool)
-> Assignment
-> f Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> f Bool) -> (Bool, Maybe Clause) -> f (Bool, Maybe Clause)
forall s t a b. Field1 s t a b => Lens s t a b
_1

valueOfLiteral :: CNF.Literal -> Traversal' Assignment Bool
valueOfLiteral :: Literal -> Traversal' Assignment Bool
valueOfLiteral (CNF.Literal Positivity
v Variable
x) = Variable -> Traversal' Assignment Bool
valueOfVariable Variable
x ((Bool -> f Bool) -> Assignment -> f Assignment)
-> ((Bool -> f Bool) -> Bool -> f Bool)
-> (Bool -> f Bool)
-> Assignment
-> f Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnIso Positivity Positivity Bool Bool
-> Iso Bool Bool Positivity Positivity
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso Positivity Positivity Bool Bool
Iso' Positivity Bool
CNF.isPositive ((Positivity -> f Positivity) -> Bool -> f Bool)
-> ((Bool -> f Bool) -> Positivity -> f Positivity)
-> (Bool -> f Bool)
-> Bool
-> f Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Positivity -> Bool)
-> (Bool -> Positivity) -> Iso' Positivity Bool
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (Positivity -> Positivity -> Bool
forall a. Eq a => a -> a -> Bool
== Positivity
v) (Positivity -> Positivity -> Bool -> Positivity
forall a. a -> a -> Bool -> a
bool (Positivity -> Positivity
CNF.negatePositivity Positivity
v) Positivity
v)

parentsOfLiteral :: CNF.Literal -> Traversal' Assignment (Maybe CNF.Clause)
parentsOfLiteral :: Literal -> Traversal' Assignment (Maybe Clause)
parentsOfLiteral (CNF.Literal Positivity
_ Variable
x) = Index Assignment -> Lens' Assignment (Maybe (IxValue Assignment))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at Index Assignment
Variable
x ((Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause)))
 -> Assignment -> f Assignment)
-> ((Maybe Clause -> f (Maybe Clause))
    -> Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause)))
-> (Maybe Clause -> f (Maybe Clause))
-> Assignment
-> f Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, Maybe Clause) -> f (Bool, Maybe Clause))
-> Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause))
forall a b. Prism (Maybe a) (Maybe b) a b
_Just (((Bool, Maybe Clause) -> f (Bool, Maybe Clause))
 -> Maybe (Bool, Maybe Clause) -> f (Maybe (Bool, Maybe Clause)))
-> ((Maybe Clause -> f (Maybe Clause))
    -> (Bool, Maybe Clause) -> f (Bool, Maybe Clause))
-> (Maybe Clause -> f (Maybe Clause))
-> Maybe (Bool, Maybe Clause)
-> f (Maybe (Bool, Maybe Clause))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Clause -> f (Maybe Clause))
-> (Bool, Maybe Clause) -> f (Bool, Maybe Clause)
forall s t a b. Field2 s t a b => Lens s t a b
_2