{-# 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)))