{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# 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 Data.Array.IArray
import ToySolver.Converter.Base
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

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

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 [(Int, Formula)]
defs) Source TseitinInfo
m = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) (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 = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Int
1, Int
nv2) forall a b. (a -> b) -> a -> b
$
            forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Source TseitinInfo
m forall a. [a] -> [a] -> [a]
++ [(Int
v, forall m. IModel m => m -> Formula -> Bool
Tseitin.evalFormula Array Int Bool
a Formula
phi) | (Int
v, Formula
phi) <- [(Int, Formula)]
defs]

instance BackwardTransformer TseitinInfo where
  transformBackward :: TseitinInfo -> Target TseitinInfo -> Source TseitinInfo
transformBackward (TseitinInfo Int
nv1 Int
_nv2 [(Int, Formula)]
_defs) = Int -> Model -> Model
SAT.restrictModel Int
nv1

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