change SAT2KSATInfo into TseitinInfo

src/ToySolver/Converter/SAT2KSAT.hs

@@ -16,7 +16,6 @@
 -----------------------------------------------------------------------------
 module ToySolver.Converter.SAT2KSAT
   ( sat2ksat
-  , SAT2KSATInfo (..)
   ) where
 
 import Control.Monad
@@ -29,12 +28,14 @@ import qualified Data.Sequence as Seq
 import Data.STRef
 
 import ToySolver.Converter.Base
+import ToySolver.Converter.Tseitin
 import qualified ToySolver.FileFormat.CNF as CNF
+import ToySolver.SAT.Formula
 import qualified ToySolver.SAT.Types as SAT
 import ToySolver.SAT.Store.CNF
 
 
-sat2ksat :: Int -> CNF.CNF -> (CNF.CNF, SAT2KSATInfo)
+sat2ksat :: Int -> CNF.CNF -> (CNF.CNF, TseitinInfo)
 sat2ksat k _ | k < 3 = error "ToySolver.Converter.SAT2KSAT.sat2ksat: k must be >=3"
 sat2ksat k cnf = runST $ do
   let nv1 = CNF.cnfNumVars cnf
@@ -55,32 +56,4 @@ sat2ksat k cnf = runST $ do
     loop $ Seq.fromList $ SAT.unpackClause clause
   cnf2 <- getCNFFormula db
   defs <- readSTRef defsRef
-  return (cnf2, SAT2KSATInfo nv1 (CNF.cnfNumVars cnf2) defs)
-
-
-data SAT2KSATInfo = SAT2KSATInfo !Int !Int (Seq.Seq (SAT.Var, [SAT.Lit]))
-  deriving (Eq, Show, Read)
-
-instance Transformer SAT2KSATInfo where
-  type Source SAT2KSATInfo = SAT.Model
-  type Target SAT2KSATInfo = SAT.Model
-
-instance ForwardTransformer SAT2KSATInfo where
-  transformForward (SAT2KSATInfo nv1 nv2 defs) m = runSTUArray $ do
-    m2 <- newArray_ (1,nv2)
-    forM_ [1..nv1] $ \v -> do
-      writeArray m2 v (SAT.evalVar m v)
-    forM_ (toList defs) $ \(v, clause) -> do
-      let f lit =
-            if lit > 0 then
-              readArray m2 lit
-            else
-              liftM not (readArray m2 (- lit))
-      val <- liftM or (mapM f clause)
-      writeArray m2 v val
-    return m2
-
-instance BackwardTransformer SAT2KSATInfo where
-  transformBackward (SAT2KSATInfo nv1 _nv2 _defs) = SAT.restrictModel nv1
-
--- -----------------------------------------------------------------------------
+  return (cnf2, TseitinInfo nv1 (CNF.cnfNumVars cnf2) [(v, Or [Atom lit | lit <- clause]) | (v, clause) <- toList defs])

src/ToySolver/Converter/SAT2MIS.hs

@@ -31,6 +31,7 @@ import qualified Data.PseudoBoolean as PBFile
 
 import ToySolver.Converter.Base
 import ToySolver.Converter.SAT2KSAT
+import ToySolver.Converter.Tseitin
 import qualified ToySolver.FileFormat.CNF as CNF
 import ToySolver.Graph.Base
 import ToySolver.SAT.Store.CNF
@@ -45,7 +46,7 @@ satToIS x = (x2, (ComposedTransformer info1 info2))
     (x1, info1) = sat2ksat 3 x
     (x2, info2) = sat3ToIS x1
 
-type SAT2ISInfo = ComposedTransformer SAT2KSATInfo SAT3ToISInfo
+type SAT2ISInfo = ComposedTransformer TseitinInfo SAT3ToISInfo
 
 -- ------------------------------------------------------------------------
 

src/ToySolver/Converter/SAT2MaxSAT.hs

@@ -65,13 +65,14 @@ import qualified Data.Set as Set
 import qualified ToySolver.FileFormat.CNF as CNF
 import ToySolver.Converter.Base
 import ToySolver.Converter.SAT2KSAT
+import ToySolver.Converter.Tseitin
 import ToySolver.Graph.Base
 import qualified ToySolver.Graph.MaxCut as MaxCut
 import qualified ToySolver.SAT.Types as SAT
 
 -- ------------------------------------------------------------------------
 
-type SATToMaxSAT2Info = ComposedTransformer SAT2KSATInfo SAT3ToMaxSAT2Info
+type SATToMaxSAT2Info = ComposedTransformer TseitinInfo SAT3ToMaxSAT2Info
 
 satToMaxSAT2 :: CNF.CNF -> ((CNF.WCNF, Integer), SATToMaxSAT2Info)
 satToMaxSAT2 x = (x2, (ComposedTransformer info1 info2))