{-# 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
(TseitinInfo -> TseitinInfo -> Bool)
-> (TseitinInfo -> TseitinInfo -> Bool) -> Eq TseitinInfo
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
(Int -> TseitinInfo -> ShowS)
-> (TseitinInfo -> String)
-> ([TseitinInfo] -> ShowS)
-> Show TseitinInfo
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]
(Int -> ReadS TseitinInfo)
-> ReadS [TseitinInfo]
-> ReadPrec TseitinInfo
-> ReadPrec [TseitinInfo]
-> Read 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 = (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) <- [(Int, Formula)]
defs]

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

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