module ToySolver.Converter.GCNF2MaxSAT
( convert
) where
import qualified ToySolver.Text.GCNF as GCNF
import qualified ToySolver.Text.MaxSAT as MaxSAT
convert :: GCNF.GCNF -> MaxSAT.WCNF
convert
GCNF.GCNF
{ GCNF.numVars = nv
, GCNF.numClauses = nc
, GCNF.lastGroupIndex = lastg
, GCNF.clauses = cs
}
=
MaxSAT.WCNF
{ MaxSAT.topCost = top
, MaxSAT.clauses = [(top, if g==0 then c else (nv+g) : c) | (g,c) <- cs] ++ [(1,[v]) | v <- [nv+1..nv+lastg]]
, MaxSAT.numVars = nv + lastg
, MaxSAT.numClauses = nc + lastg
}
where
top :: MaxSAT.Weight
top = fromIntegral (lastg + 1)