{-# 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
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, GroupIndex -> GCNF2MaxSATInfo -> ShowS
[GCNF2MaxSATInfo] -> ShowS
GCNF2MaxSATInfo -> String
forall a.
(GroupIndex -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GCNF2MaxSATInfo] -> ShowS
$cshowList :: [GCNF2MaxSATInfo] -> ShowS
show :: GCNF2MaxSATInfo -> String
$cshow :: GCNF2MaxSATInfo -> String
showsPrec :: GroupIndex -> GCNF2MaxSATInfo -> ShowS
$cshowsPrec :: GroupIndex -> GCNF2MaxSATInfo -> ShowS
Show, ReadPrec [GCNF2MaxSATInfo]
ReadPrec GCNF2MaxSATInfo
GroupIndex -> ReadS GCNF2MaxSATInfo
ReadS [GCNF2MaxSATInfo]
forall a.
(GroupIndex -> 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 :: GroupIndex -> ReadS GCNF2MaxSATInfo
$creadsPrec :: GroupIndex -> 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 GroupIndex
nv1) = GroupIndex -> Model -> Model
SAT.restrictModel GroupIndex
nv1
gcnf2maxsat :: CNF.GCNF -> (CNF.WCNF, GCNF2MaxSATInfo)
gcnf2maxsat :: GCNF -> (WCNF, GCNF2MaxSATInfo)
gcnf2maxsat
CNF.GCNF
{ gcnfNumVars :: GCNF -> GroupIndex
CNF.gcnfNumVars = GroupIndex
nv
, gcnfNumClauses :: GCNF -> GroupIndex
CNF.gcnfNumClauses = GroupIndex
nc
, gcnfLastGroupIndex :: GCNF -> GroupIndex
CNF.gcnfLastGroupIndex = GroupIndex
lastg
, gcnfClauses :: GCNF -> [GClause]
CNF.gcnfClauses = [GClause]
cs
}
=
( CNF.WCNF
{ wcnfTopCost :: Weight
CNF.wcnfTopCost = Weight
top
, wcnfClauses :: [WeightedClause]
CNF.wcnfClauses =
[(Weight
top, if GroupIndex
gforall a. Eq a => a -> a -> Bool
==GroupIndex
0 then PackedClause
c else forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (- GroupIndex -> PackedLit
SAT.packLit (GroupIndex
nvforall a. Num a => a -> a -> a
+GroupIndex
g)) PackedClause
c) | (GroupIndex
g,PackedClause
c) <- [GClause]
cs] forall a. [a] -> [a] -> [a]
++
[(Weight
1, Clause -> PackedClause
SAT.packClause [GroupIndex
v]) | GroupIndex
v <- [GroupIndex
nvforall a. Num a => a -> a -> a
+GroupIndex
1..GroupIndex
nvforall a. Num a => a -> a -> a
+GroupIndex
lastg]]
, wcnfNumVars :: GroupIndex
CNF.wcnfNumVars = GroupIndex
nv forall a. Num a => a -> a -> a
+ GroupIndex
lastg
, wcnfNumClauses :: GroupIndex
CNF.wcnfNumClauses = GroupIndex
nc forall a. Num a => a -> a -> a
+ GroupIndex
lastg
}
, GroupIndex -> GCNF2MaxSATInfo
GCNF2MaxSATInfo GroupIndex
nv
)
where
top :: CNF.Weight
top :: Weight
top = forall a b. (Integral a, Num b) => a -> b
fromIntegral (GroupIndex
lastg forall a. Num a => a -> a -> a
+ GroupIndex
1)