{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
module ToySolver.Converter.GCNF2MaxSAT
( gcnf2maxsat
, GCNF2MaxSATInfo (..)
) where
import qualified Data.Vector.Generic as VG
import ToySolver.Converter.Base
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT
data GCNF2MaxSATInfo = GCNF2MaxSATInfo !Int
deriving (GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
(GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool)
-> (GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool)
-> Eq GCNF2MaxSATInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
$c/= :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
== :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
$c== :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
Eq, Int -> GCNF2MaxSATInfo -> ShowS
[GCNF2MaxSATInfo] -> ShowS
GCNF2MaxSATInfo -> String
(Int -> GCNF2MaxSATInfo -> ShowS)
-> (GCNF2MaxSATInfo -> String)
-> ([GCNF2MaxSATInfo] -> ShowS)
-> Show GCNF2MaxSATInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GCNF2MaxSATInfo] -> ShowS
$cshowList :: [GCNF2MaxSATInfo] -> ShowS
show :: GCNF2MaxSATInfo -> String
$cshow :: GCNF2MaxSATInfo -> String
showsPrec :: Int -> GCNF2MaxSATInfo -> ShowS
$cshowsPrec :: Int -> GCNF2MaxSATInfo -> ShowS
Show, ReadPrec [GCNF2MaxSATInfo]
ReadPrec GCNF2MaxSATInfo
Int -> ReadS GCNF2MaxSATInfo
ReadS [GCNF2MaxSATInfo]
(Int -> ReadS GCNF2MaxSATInfo)
-> ReadS [GCNF2MaxSATInfo]
-> ReadPrec GCNF2MaxSATInfo
-> ReadPrec [GCNF2MaxSATInfo]
-> Read GCNF2MaxSATInfo
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [GCNF2MaxSATInfo]
$creadListPrec :: ReadPrec [GCNF2MaxSATInfo]
readPrec :: ReadPrec GCNF2MaxSATInfo
$creadPrec :: ReadPrec GCNF2MaxSATInfo
readList :: ReadS [GCNF2MaxSATInfo]
$creadList :: ReadS [GCNF2MaxSATInfo]
readsPrec :: Int -> ReadS GCNF2MaxSATInfo
$creadsPrec :: Int -> ReadS GCNF2MaxSATInfo
Read)
instance Transformer GCNF2MaxSATInfo where
type Source GCNF2MaxSATInfo = SAT.Model
type Target GCNF2MaxSATInfo = SAT.Model
instance BackwardTransformer GCNF2MaxSATInfo where
transformBackward :: GCNF2MaxSATInfo -> Target GCNF2MaxSATInfo -> Source GCNF2MaxSATInfo
transformBackward (GCNF2MaxSATInfo Int
nv1) = Int -> Model -> Model
SAT.restrictModel Int
nv1
gcnf2maxsat :: CNF.GCNF -> (CNF.WCNF, GCNF2MaxSATInfo)
gcnf2maxsat :: GCNF -> (WCNF, GCNF2MaxSATInfo)
gcnf2maxsat
CNF.GCNF
{ gcnfNumVars :: GCNF -> Int
CNF.gcnfNumVars = Int
nv
, gcnfNumClauses :: GCNF -> Int
CNF.gcnfNumClauses = Int
nc
, gcnfLastGroupIndex :: GCNF -> Int
CNF.gcnfLastGroupIndex = Int
lastg
, gcnfClauses :: GCNF -> [GClause]
CNF.gcnfClauses = [GClause]
cs
}
=
( WCNF :: Int -> Int -> Weight -> [WeightedClause] -> WCNF
CNF.WCNF
{ wcnfTopCost :: Weight
CNF.wcnfTopCost = Weight
top
, wcnfClauses :: [WeightedClause]
CNF.wcnfClauses =
[(Weight
top, if Int
gInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then PackedClause
c else PackedLit -> PackedClause -> PackedClause
forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (- Int -> PackedLit
SAT.packLit (Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
g)) PackedClause
c) | (Int
g,PackedClause
c) <- [GClause]
cs] [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++
[(Weight
1, Clause -> PackedClause
SAT.packClause [Int
v]) | Int
v <- [Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
lastg]]
, wcnfNumVars :: Int
CNF.wcnfNumVars = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lastg
, wcnfNumClauses :: Int
CNF.wcnfNumClauses = Int
nc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lastg
}
, Int -> GCNF2MaxSATInfo
GCNF2MaxSATInfo Int
nv
)
where
top :: CNF.Weight
top :: Weight
top = Int -> Weight
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
lastg Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)