{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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.Aeson as J
import Data.Aeson ((.=), (.:))
import qualified Data.Vector.Generic as VG
import ToySolver.Converter.Base
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Internal.JSON
import qualified ToySolver.SAT.Types as SAT

newtype 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
$c== :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
== :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
$c/= :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
/= :: GCNF2MaxSATInfo -> GCNF2MaxSATInfo -> Bool
Eq, GroupIndex -> GCNF2MaxSATInfo -> ShowS
[GCNF2MaxSATInfo] -> ShowS
GCNF2MaxSATInfo -> String
(GroupIndex -> GCNF2MaxSATInfo -> ShowS)
-> (GCNF2MaxSATInfo -> String)
-> ([GCNF2MaxSATInfo] -> ShowS)
-> Show GCNF2MaxSATInfo
forall a.
(GroupIndex -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: GroupIndex -> GCNF2MaxSATInfo -> ShowS
showsPrec :: GroupIndex -> GCNF2MaxSATInfo -> ShowS
$cshow :: GCNF2MaxSATInfo -> String
show :: GCNF2MaxSATInfo -> String
$cshowList :: [GCNF2MaxSATInfo] -> ShowS
showList :: [GCNF2MaxSATInfo] -> ShowS
Show, ReadPrec [GCNF2MaxSATInfo]
ReadPrec GCNF2MaxSATInfo
GroupIndex -> ReadS GCNF2MaxSATInfo
ReadS [GCNF2MaxSATInfo]
(GroupIndex -> ReadS GCNF2MaxSATInfo)
-> ReadS [GCNF2MaxSATInfo]
-> ReadPrec GCNF2MaxSATInfo
-> ReadPrec [GCNF2MaxSATInfo]
-> Read GCNF2MaxSATInfo
forall a.
(GroupIndex -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: GroupIndex -> ReadS GCNF2MaxSATInfo
readsPrec :: GroupIndex -> ReadS GCNF2MaxSATInfo
$creadList :: ReadS [GCNF2MaxSATInfo]
readList :: ReadS [GCNF2MaxSATInfo]
$creadPrec :: ReadPrec GCNF2MaxSATInfo
readPrec :: ReadPrec GCNF2MaxSATInfo
$creadListPrec :: ReadPrec [GCNF2MaxSATInfo]
readListPrec :: ReadPrec [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

instance J.ToJSON GCNF2MaxSATInfo where
  toJSON :: GCNF2MaxSATInfo -> Value
toJSON (GCNF2MaxSATInfo GroupIndex
nv) =
    [Pair] -> Value
J.object
    [ Key
"type" Key -> Value -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= (Value
"GCNF2MaxSATInfo" :: J.Value)
    , Key
"num_original_variables" Key -> GroupIndex -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= GroupIndex
nv
    ]

instance J.FromJSON GCNF2MaxSATInfo where
  parseJSON :: Value -> Parser GCNF2MaxSATInfo
parseJSON = String
-> (Object -> Parser GCNF2MaxSATInfo)
-> Value
-> Parser GCNF2MaxSATInfo
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withTypedObject String
"GCNF2MaxSATInfo" ((Object -> Parser GCNF2MaxSATInfo)
 -> Value -> Parser GCNF2MaxSATInfo)
-> (Object -> Parser GCNF2MaxSATInfo)
-> Value
-> Parser GCNF2MaxSATInfo
forall a b. (a -> b) -> a -> b
$ \Object
obj ->
    GroupIndex -> GCNF2MaxSATInfo
GCNF2MaxSATInfo (GroupIndex -> GCNF2MaxSATInfo)
-> Parser GroupIndex -> Parser GCNF2MaxSATInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
obj Object -> Key -> Parser GroupIndex
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"num_original_variables"

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
gGroupIndex -> GroupIndex -> Bool
forall a. Eq a => a -> a -> Bool
==GroupIndex
0 then PackedClause
c else PackedLit -> PackedClause -> PackedClause
forall (v :: * -> *) a. Vector v a => a -> v a -> v a
VG.cons (- GroupIndex -> PackedLit
SAT.packLit (GroupIndex
nvGroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+GroupIndex
g)) PackedClause
c) | (GroupIndex
g,PackedClause
c) <- [GClause]
cs] [WeightedClause] -> [WeightedClause] -> [WeightedClause]
forall a. [a] -> [a] -> [a]
++
        [(Weight
1, Clause -> PackedClause
SAT.packClause [GroupIndex
v]) | GroupIndex
v <- [GroupIndex
nvGroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+GroupIndex
1..GroupIndex
nvGroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+GroupIndex
lastg]]
    , wcnfNumVars :: GroupIndex
CNF.wcnfNumVars = GroupIndex
nv GroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+ GroupIndex
lastg
    , wcnfNumClauses :: GroupIndex
CNF.wcnfNumClauses = GroupIndex
nc GroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+ GroupIndex
lastg
    }
  , GroupIndex -> GCNF2MaxSATInfo
GCNF2MaxSATInfo GroupIndex
nv
  )
  where
    top :: CNF.Weight
    top :: Weight
top = GroupIndex -> Weight
forall a b. (Integral a, Num b) => a -> b
fromIntegral (GroupIndex
lastg GroupIndex -> GroupIndex -> GroupIndex
forall a. Num a => a -> a -> a
+ GroupIndex
1)