{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.Tseitin
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.Tseitin
  ( TseitinInfo (..)
  ) where

import qualified Data.Aeson as J
import qualified Data.Aeson.Types as J
import Data.Aeson ((.=), (.:))
import Data.Array.IArray
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Lazy as Map
import qualified Data.Text as T
import ToySolver.Converter.Base
import ToySolver.Internal.JSON
import qualified ToySolver.SAT.Formula as SAT
import ToySolver.SAT.Internal.JSON
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

data TseitinInfo = TseitinInfo !Int !Int (SAT.VarMap Tseitin.Formula)
  deriving (Int -> TseitinInfo -> ShowS
[TseitinInfo] -> ShowS
TseitinInfo -> String
(Int -> TseitinInfo -> ShowS)
-> (TseitinInfo -> String)
-> ([TseitinInfo] -> ShowS)
-> Show TseitinInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TseitinInfo -> ShowS
showsPrec :: Int -> TseitinInfo -> ShowS
$cshow :: TseitinInfo -> String
show :: TseitinInfo -> String
$cshowList :: [TseitinInfo] -> ShowS
showList :: [TseitinInfo] -> ShowS
Show, ReadPrec [TseitinInfo]
ReadPrec TseitinInfo
Int -> ReadS TseitinInfo
ReadS [TseitinInfo]
(Int -> ReadS TseitinInfo)
-> ReadS [TseitinInfo]
-> ReadPrec TseitinInfo
-> ReadPrec [TseitinInfo]
-> Read TseitinInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS TseitinInfo
readsPrec :: Int -> ReadS TseitinInfo
$creadList :: ReadS [TseitinInfo]
readList :: ReadS [TseitinInfo]
$creadPrec :: ReadPrec TseitinInfo
readPrec :: ReadPrec TseitinInfo
$creadListPrec :: ReadPrec [TseitinInfo]
readListPrec :: ReadPrec [TseitinInfo]
Read, TseitinInfo -> TseitinInfo -> Bool
(TseitinInfo -> TseitinInfo -> Bool)
-> (TseitinInfo -> TseitinInfo -> Bool) -> Eq TseitinInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TseitinInfo -> TseitinInfo -> Bool
== :: TseitinInfo -> TseitinInfo -> Bool
$c/= :: TseitinInfo -> TseitinInfo -> Bool
/= :: TseitinInfo -> TseitinInfo -> Bool
Eq)

instance Transformer TseitinInfo where
  type Source TseitinInfo = SAT.Model
  type Target TseitinInfo = SAT.Model

instance ForwardTransformer TseitinInfo where
  transformForward :: TseitinInfo -> Source TseitinInfo -> Target TseitinInfo
transformForward (TseitinInfo Int
_nv1 Int
nv2 VarMap Formula
defs) Source TseitinInfo
m = (Int, Int) -> [(Int, Bool)] -> UArray Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) (Array Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Array Int Bool
a)
    where
      -- Use BOXED array to tie the knot
      a :: Array SAT.Var Bool
      a :: Array Int Bool
a = (Int, Int) -> [(Int, Bool)] -> Array Int Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) ([(Int, Bool)] -> Array Int Bool)
-> [(Int, Bool)] -> Array Int Bool
forall a b. (a -> b) -> a -> b
$
            UArray Int Bool -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs UArray Int Bool
Source TseitinInfo
m [(Int, Bool)] -> [(Int, Bool)] -> [(Int, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Int
v, Array Int Bool -> Formula -> Bool
forall m. IModel m => m -> Formula -> Bool
Tseitin.evalFormula Array Int Bool
a Formula
phi) | (Int
v, Formula
phi) <- VarMap Formula -> [(Int, Formula)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList VarMap Formula
defs]

instance BackwardTransformer TseitinInfo where
  transformBackward :: TseitinInfo -> Target TseitinInfo -> Source TseitinInfo
transformBackward (TseitinInfo Int
nv1 Int
_nv2 VarMap Formula
_defs) = Int -> UArray Int Bool -> UArray Int Bool
SAT.restrictModel Int
nv1

instance J.ToJSON TseitinInfo where
  toJSON :: TseitinInfo -> Value
toJSON (TseitinInfo Int
nv1 Int
nv2 VarMap Formula
defs) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"TseitinInfo" :: J.Value)
    , Key
"num_original_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv1
    , Key
"num_transformed_variables" Key -> Int -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Int
nv2
    , Key
"definitions" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= [Pair] -> Value
J.object
        [ Int -> Key
forall a. IsString a => Int -> a
jVarName Int
v Key -> Formula -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= Formula
formula
        | (Int
v, Formula
formula) <- VarMap Formula -> [(Int, Formula)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList VarMap Formula
defs
        ]
    ]

instance J.FromJSON TseitinInfo where
  parseJSON :: Value -> Parser TseitinInfo
parseJSON = String
-> (Object -> Parser TseitinInfo) -> Value -> Parser TseitinInfo
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withTypedObject String
"TseitinInfo" ((Object -> Parser TseitinInfo) -> Value -> Parser TseitinInfo)
-> (Object -> Parser TseitinInfo) -> Value -> Parser TseitinInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj -> do
    Map Text Formula
defs <- Object
obj Object -> Key -> Parser (Map Text Formula)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"definitions"
    Int -> Int -> VarMap Formula -> TseitinInfo
TseitinInfo
      (Int -> Int -> VarMap Formula -> TseitinInfo)
-> Parser Int -> Parser (Int -> VarMap Formula -> TseitinInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"
      Parser (Int -> VarMap Formula -> TseitinInfo)
-> Parser Int -> Parser (VarMap Formula -> TseitinInfo)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
obj Object -> Key -> Parser Int
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_transformed_variables"
      Parser (VarMap Formula -> TseitinInfo)
-> Parser (VarMap Formula) -> Parser TseitinInfo
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([(Int, Formula)] -> VarMap Formula
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Formula)] -> VarMap Formula)
-> Parser [(Int, Formula)] -> Parser (VarMap Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, Formula) -> Parser (Int, Formula))
-> [(Text, Formula)] -> Parser [(Int, Formula)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Text, Formula) -> Parser (Int, Formula)
f (Map Text Formula -> [(Text, Formula)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text Formula
defs))
    where
      f :: (T.Text, SAT.Formula) -> J.Parser (SAT.Var, SAT.Formula)
      f :: (Text, Formula) -> Parser (Int, Formula)
f (Text
name, Formula
formula) = do
        Int
x <- Text -> Parser Int
parseVarNameText Text
name
        (Int, Formula) -> Parser (Int, Formula)
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
x, Formula
formula)

-- -----------------------------------------------------------------------------