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