{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.GCNF2MaxSAT
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
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)