{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
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
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