-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Printer
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Printing utilities.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Printer
  ( satPrintModel
  , maxsatPrintModel
  , maxsatPrintModelCompact
  , pbPrintModel
  , musPrintSol
  ) where

import Control.Monad
import Data.Array.IArray
import Data.List
import System.IO
import ToySolver.SAT.Types

-- | Print a 'Model' in a way specified for SAT Competition.
-- See <http://www.satcompetition.org/2011/rules.pdf> for details.
satPrintModel :: Handle -> Model -> Int -> IO ()
satPrintModel :: Handle -> Model -> Int -> IO ()
satPrintModel Handle
h Model
m Int
n = do
  let as :: [(Int, Bool)]
as = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
           then ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n) ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  [[(Int, Bool)]] -> ([(Int, Bool)] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Bool)] -> [[(Int, Bool)]]
forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) (([(Int, Bool)] -> IO ()) -> IO ())
-> ([(Int, Bool)] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    [(Int, Bool)] -> ((Int, Bool) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs (((Int, Bool) -> IO ()) -> IO ())
-> ((Int, Bool) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' 'Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Int -> Bool -> Int
literal Int
var Bool
val))
    Handle -> String -> IO ()
hPutStrLn Handle
h String
""
  Handle -> String -> IO ()
hPutStrLn Handle
h String
"v 0"
  Handle -> IO ()
hFlush Handle
h

-- | Print a 'Model' in a way specified for Max-SAT Evaluation.
-- See <http://maxsat.ia.udl.cat/requirements/> for details.
maxsatPrintModel :: Handle -> Model -> Int -> IO ()
maxsatPrintModel :: Handle -> Model -> Int -> IO ()
maxsatPrintModel Handle
h Model
m Int
n = do
  let as :: [(Int, Bool)]
as = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
           then ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n) ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  [[(Int, Bool)]] -> ([(Int, Bool)] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Bool)] -> [[(Int, Bool)]]
forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) (([(Int, Bool)] -> IO ()) -> IO ())
-> ([(Int, Bool)] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    [(Int, Bool)] -> ((Int, Bool) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs (((Int, Bool) -> IO ()) -> IO ())
-> ((Int, Bool) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' ' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Int -> Bool -> Int
literal Int
var Bool
val))
    Handle -> String -> IO ()
hPutStrLn Handle
h String
""
  -- no terminating 0 is necessary
  Handle -> IO ()
hFlush Handle
h

-- | Print a 'Model' in the new compact way specified for Max-SAT Evaluation >=2020.
-- See <https://maxsat-evaluations.github.io/2020/vline.html> for details.
maxsatPrintModelCompact :: Handle -> Model -> Int -> IO ()
maxsatPrintModelCompact :: Handle -> Model -> Int -> IO ()
maxsatPrintModelCompact Handle
h Model
m Int
n = do
  let vs :: [Bool]
vs = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
           then Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
take Int
n ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ Model -> [Bool]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems Model
m
           else Model -> [Bool]
forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems Model
m
  Handle -> String -> IO ()
hPutStrLn Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"v " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [if Bool
v then Char
'1' else Char
'0' | Bool
v <- [Bool]
vs]
  Handle -> IO ()
hFlush Handle
h

-- | Print a 'Model' in a way specified for Pseudo-Boolean Competition.
-- See <http://www.cril.univ-artois.fr/PB12/format.pdf> for details.
pbPrintModel :: Handle -> Model -> Int -> IO ()
pbPrintModel :: Handle -> Model -> Int -> IO ()
pbPrintModel Handle
h Model
m Int
n = do
  let as :: [(Int, Bool)]
as = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
           then ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n) ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else Model -> [(Int, Bool)]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  [[(Int, Bool)]] -> ([(Int, Bool)] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [(Int, Bool)] -> [[(Int, Bool)]]
forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) (([(Int, Bool)] -> IO ()) -> IO ())
-> ([(Int, Bool)] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    [(Int, Bool)] -> ((Int, Bool) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs (((Int, Bool) -> IO ()) -> IO ())
-> ((Int, Bool) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
val then String
"" else String
"-") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
var)
    Handle -> String -> IO ()
hPutStrLn Handle
h String
""
  Handle -> IO ()
hFlush Handle
h

musPrintSol :: Handle -> [Int] -> IO ()
musPrintSol :: Handle -> [Int] -> IO ()
musPrintSol Handle
h [Int]
is = do
  [[Int]] -> ([Int] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> [Int] -> [[Int]]
forall a. Int -> [a] -> [[a]]
split Int
10 [Int]
is) (([Int] -> IO ()) -> IO ()) -> ([Int] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[Int]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
i -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' 'Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i)
    Handle -> String -> IO ()
hPutStrLn Handle
h String
""
  Handle -> String -> IO ()
hPutStrLn Handle
h String
"v 0"
  Handle -> IO ()
hFlush Handle
h

-- ------------------------------------------------------------------------

split :: Int -> [a] -> [[a]]
split :: forall a. Int -> [a] -> [[a]]
split Int
n = [a] -> [[a]]
forall {a}. [a] -> [[a]]
go
  where
    go :: [a] -> [[a]]
go [] = []
    go [a]
xs =
      case Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
xs of
        ([a]
ys, [a]
zs) -> [a]
ys [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [[a]]
go [a]
zs