{-# LANGUAGE ViewPatterns #-} module Satyros.QFIDL.Conversion ( ConversionTable , toCNF , fromAssignment ) where import Control.Applicative (liftA2) import Control.Lens (_1, at, over, view, (&), (?~)) import Data.Coerce (coerce) import Data.List (mapAccumL) import Data.Map (Map) import qualified Data.Map as Map import Data.Monoid (Ap (..), getAp) import Data.Tuple (swap) import qualified Satyros.CNF as CNF import Satyros.QFIDL.Expressed (Expressed (..)) import Satyros.QFIDL.Expressible (Expressible (..), Operator (..)) import Satyros.QFIDL.Variable (Variable (ZeroVariable)) type ConversionTable = (Map CNF.Variable Expressed, Map Expressed CNF.Literal) toCNF :: CNF.FormulaLike Expressible -> (CNF.Formula, ConversionTable) toCNF :: FormulaLike Expressible -> (Formula, ConversionTable) toCNF = ([ClauseLike Expressible] -> ([Clause], ConversionTable)) -> FormulaLike Expressible -> (Formula, ConversionTable) coerce (([ClauseLike Expressible] -> ([Clause], ConversionTable)) -> FormulaLike Expressible -> (Formula, ConversionTable)) -> ([ClauseLike Expressible] -> ([Clause], ConversionTable)) -> FormulaLike Expressible -> (Formula, ConversionTable) forall a b. (a -> b) -> a -> b $ (ConversionTable, [Clause]) -> ([Clause], ConversionTable) forall a b. (a, b) -> (b, a) swap ((ConversionTable, [Clause]) -> ([Clause], ConversionTable)) -> ([ClauseLike Expressible] -> (ConversionTable, [Clause])) -> [ClauseLike Expressible] -> ([Clause], ConversionTable) forall b c a. (b -> c) -> (a -> b) -> a -> c . [ClauseLike Expressible] -> (ConversionTable, [Clause]) toCNF' where toCNF' :: [CNF.ClauseLike Expressible] -> (ConversionTable, [CNF.Clause]) toCNF' :: [ClauseLike Expressible] -> (ConversionTable, [Clause]) toCNF' = ([[Expressed]] -> (ConversionTable, [[Literal]])) -> [ClauseLike Expressed] -> (ConversionTable, [Clause]) coerce ( ASetter ((ConversionTable, [Variable]), [[Literal]]) (ConversionTable, [[Literal]]) (ConversionTable, [Variable]) ConversionTable -> ((ConversionTable, [Variable]) -> ConversionTable) -> ((ConversionTable, [Variable]), [[Literal]]) -> (ConversionTable, [[Literal]]) forall s t a b. ASetter s t a b -> (a -> b) -> s -> t over ASetter ((ConversionTable, [Variable]), [[Literal]]) (ConversionTable, [[Literal]]) (ConversionTable, [Variable]) ConversionTable forall s t a b. Field1 s t a b => Lens s t a b _1 (Getting ConversionTable (ConversionTable, [Variable]) ConversionTable -> (ConversionTable, [Variable]) -> ConversionTable forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a view Getting ConversionTable (ConversionTable, [Variable]) ConversionTable forall s t a b. Field1 s t a b => Lens s t a b _1) (((ConversionTable, [Variable]), [[Literal]]) -> (ConversionTable, [[Literal]])) -> ([[Expressed]] -> ((ConversionTable, [Variable]), [[Literal]])) -> [[Expressed]] -> (ConversionTable, [[Literal]]) forall b c a. (b -> c) -> (a -> b) -> a -> c . ((ConversionTable, [Variable]) -> [Expressed] -> ((ConversionTable, [Variable]), [Literal])) -> (ConversionTable, [Variable]) -> [[Expressed]] -> ((ConversionTable, [Variable]), [[Literal]]) forall (t :: * -> *) a b c. Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) mapAccumL @[] (((ConversionTable, [Variable]) -> Expressed -> ((ConversionTable, [Variable]), Literal)) -> (ConversionTable, [Variable]) -> [Expressed] -> ((ConversionTable, [Variable]), [Literal]) forall (t :: * -> *) a b c. Traversable t => (a -> b -> (a, c)) -> a -> t b -> (a, t c) mapAccumL @[] (ConversionTable, [Variable]) -> Expressed -> ((ConversionTable, [Variable]), Literal) go) ((Map Variable Expressed forall k a. Map k a Map.empty, Map Expressed Literal forall k a. Map k a Map.empty), Word -> Variable CNF.Variable (Word -> Variable) -> [Word] -> [Variable] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Word 1..]) ) ([ClauseLike Expressed] -> (ConversionTable, [Clause])) -> ([ClauseLike Expressible] -> [ClauseLike Expressed]) -> [ClauseLike Expressible] -> (ConversionTable, [Clause]) forall b c a. (b -> c) -> (a -> b) -> a -> c . (ClauseLike Expressible -> [ClauseLike Expressed]) -> [ClauseLike Expressible] -> [ClauseLike Expressed] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap ClauseLike Expressible -> [ClauseLike Expressed] transformClauseLike go :: (ConversionTable, [CNF.Variable]) -> Expressed -> ((ConversionTable, [CNF.Variable]), CNF.Literal) go :: (ConversionTable, [Variable]) -> Expressed -> ((ConversionTable, [Variable]), Literal) go s :: (ConversionTable, [Variable]) s@((Map Variable Expressed v2e, Map Expressed Literal e2l), [Variable] newVs) Expressed e | Just Literal l <- Expressed -> Map Expressed Literal -> Maybe Literal forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup Expressed e Map Expressed Literal e2l = ((ConversionTable, [Variable]) s, Literal l) | Variable newV:[Variable] newVs' <- [Variable] newVs = (((Map Variable Expressed v2e Map Variable Expressed -> (Map Variable Expressed -> Map Variable Expressed) -> Map Variable Expressed forall a b. a -> (a -> b) -> b & Index (Map Variable Expressed) -> Lens' (Map Variable Expressed) (Maybe (IxValue (Map Variable Expressed))) forall m. At m => Index m -> Lens' m (Maybe (IxValue m)) at Index (Map Variable Expressed) Variable newV ((Maybe Expressed -> Identity (Maybe Expressed)) -> Map Variable Expressed -> Identity (Map Variable Expressed)) -> Expressed -> Map Variable Expressed -> Map Variable Expressed forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t ?~ Expressed e , Map Expressed Literal e2l Map Expressed Literal -> (Map Expressed Literal -> Map Expressed Literal) -> Map Expressed Literal forall a b. a -> (a -> b) -> b & Index (Map Expressed Literal) -> Lens' (Map Expressed Literal) (Maybe (IxValue (Map Expressed Literal))) forall m. At m => Index m -> Lens' m (Maybe (IxValue m)) at Index (Map Expressed Literal) Expressed e ((Maybe Literal -> Identity (Maybe Literal)) -> Map Expressed Literal -> Identity (Map Expressed Literal)) -> Literal -> Map Expressed Literal -> Map Expressed Literal forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t ?~ Positivity -> Variable -> Literal CNF.Literal Positivity CNF.Positive Variable newV Map Expressed Literal -> (Map Expressed Literal -> Map Expressed Literal) -> Map Expressed Literal forall a b. a -> (a -> b) -> b & Index (Map Expressed Literal) -> Lens' (Map Expressed Literal) (Maybe (IxValue (Map Expressed Literal))) forall m. At m => Index m -> Lens' m (Maybe (IxValue m)) at (Expressed -> Expressed negateExpressed Expressed e) ((Maybe Literal -> Identity (Maybe Literal)) -> Map Expressed Literal -> Identity (Map Expressed Literal)) -> Literal -> Map Expressed Literal -> Map Expressed Literal forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t ?~ Positivity -> Variable -> Literal CNF.Literal Positivity CNF.Negative Variable newV), [Variable] newVs'), Positivity -> Variable -> Literal CNF.Literal Positivity CNF.Positive Variable newV) | Bool otherwise = [Char] -> ((ConversionTable, [Variable]), Literal) forall a. HasCallStack => [Char] -> a error [Char] "toCNF: impossible case!" fromAssignment :: ConversionTable -> [(CNF.Variable, Bool)] -> [Expressed] fromAssignment :: ConversionTable -> [(Variable, Bool)] -> [Expressed] fromAssignment = ((Variable, Bool) -> Expressed) -> [(Variable, Bool)] -> [Expressed] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (((Variable, Bool) -> Expressed) -> [(Variable, Bool)] -> [Expressed]) -> (ConversionTable -> (Variable, Bool) -> Expressed) -> ConversionTable -> [(Variable, Bool)] -> [Expressed] forall b c a. (b -> c) -> (a -> b) -> a -> c . ConversionTable -> (Variable, Bool) -> Expressed fromVariable fromVariable :: ConversionTable -> (CNF.Variable, Bool) -> Expressed fromVariable :: ConversionTable -> (Variable, Bool) -> Expressed fromVariable (Map Variable Expressed m, Map Expressed Literal _) ((Map Variable Expressed m Map Variable Expressed -> Variable -> Expressed forall k a. Ord k => Map k a -> k -> a Map.!) -> Expressed e, Bool v) | Bool v = Expressed e | Bool otherwise = Expressed -> Expressed negateExpressed Expressed e negateExpressed :: Expressed -> Expressed negateExpressed :: Expressed -> Expressed negateExpressed (LessThanEqualTo Variable v1 Variable v2 Int n) = Variable -> Variable -> Int -> Expressed LessThanEqualTo Variable v2 Variable v1 (- Int n Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) transformClauseLike :: CNF.ClauseLike Expressible -> [CNF.ClauseLike Expressed] transformClauseLike :: ClauseLike Expressible -> [ClauseLike Expressed] transformClauseLike = ([Expressible] -> [[Expressed]]) -> ClauseLike Expressible -> [ClauseLike Expressed] coerce [Expressible] -> [[Expressed]] go where go :: [Expressible] -> [[Expressed]] go :: [Expressible] -> [[Expressed]] go = Ap [] [Expressed] -> [[Expressed]] forall k (f :: k -> *) (a :: k). Ap f a -> f a getAp (Ap [] [Expressed] -> [[Expressed]]) -> ([Expressible] -> Ap [] [Expressed]) -> [Expressible] -> [[Expressed]] forall b c a. (b -> c) -> (a -> b) -> a -> c . [Ap [] [Expressed]] -> Ap [] [Expressed] forall a. Monoid a => [a] -> a mconcat ([Ap [] [Expressed]] -> Ap [] [Expressed]) -> ([Expressible] -> [Ap [] [Expressed]]) -> [Expressible] -> Ap [] [Expressed] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Expressible -> Ap [] [Expressed]) -> [Expressible] -> [Ap [] [Expressed]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap ([[Expressed]] -> Ap [] [Expressed] forall k (f :: k -> *) (a :: k). f a -> Ap f a Ap ([[Expressed]] -> Ap [] [Expressed]) -> (Expressible -> [[Expressed]]) -> Expressible -> Ap [] [Expressed] forall b c a. (b -> c) -> (a -> b) -> a -> c . Expressible -> [[Expressed]] transformExpressible) transformExpressible :: Expressible -> [[Expressed]] transformExpressible :: Expressible -> [[Expressed]] transformExpressible (Singleton Variable v Operator op Double n) = Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v Variable ZeroVariable Operator op Double n) transformExpressible (Difference Variable v1 Variable v2 Operator (::<?) Double x) = [[Variable -> Variable -> Int -> Expressed LessThanEqualTo Variable v1 Variable v2 (Double -> Int forall a b. (RealFrac a, Integral b) => a -> b ceiling (Double x Double -> Double -> Double forall a. Num a => a -> a -> a - Double 1))]] transformExpressible (Difference Variable v1 Variable v2 Operator (::<=?) Double x) = [[Variable -> Variable -> Int -> Expressed LessThanEqualTo Variable v1 Variable v2 (Double -> Int forall a b. (RealFrac a, Integral b) => a -> b floor Double x)]] transformExpressible (Difference Variable v1 Variable v2 Operator (::>?) Double x) = Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v2 Variable v1 Operator (::<?) (- Double x)) transformExpressible (Difference Variable v1 Variable v2 Operator (::>=?) Double x) = Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v2 Variable v1 Operator (::<=?) (- Double x)) transformExpressible (Difference Variable v1 Variable v2 Operator (::=?) Double x) = Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v1 Variable v2 Operator (::<=?) Double x) [[Expressed]] -> [[Expressed]] -> [[Expressed]] forall a. [a] -> [a] -> [a] ++ Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v2 Variable v1 Operator (::<=?) (- Double x)) transformExpressible (Difference Variable v1 Variable v2 Operator (::<>?) Double x) = ([Expressed] -> [Expressed] -> [Expressed]) -> [[Expressed]] -> [[Expressed]] -> [[Expressed]] forall (f :: * -> *) a b c. Applicative f => (a -> b -> c) -> f a -> f b -> f c liftA2 [Expressed] -> [Expressed] -> [Expressed] forall a. Semigroup a => a -> a -> a (<>) (Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v1 Variable v2 Operator (::<?) Double x)) (Expressible -> [[Expressed]] transformExpressible (Variable -> Variable -> Operator -> Double -> Expressible Difference Variable v2 Variable v1 Operator (::<?) (- Double x)))