-----------------------------------------------------------------------------
-- |
-- 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 forall a. Ord a => a -> a -> Bool
> Int
0
           then forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v forall a. Ord a => a -> a -> Bool
<= Int
n) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' 'forall a. a -> [a] -> [a]
: 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 forall a. Ord a => a -> a -> Bool
> Int
0
           then forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v forall a. Ord a => a -> a -> Bool
<= Int
n) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' ' forall a. a -> [a] -> [a]
: 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 forall a. Ord a => a -> a -> Bool
> Int
0
           then forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems Model
m
           else forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems Model
m
  Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ String
"v " 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 forall a. Ord a => a -> a -> Bool
> Int
0
           then forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\(Int
v,Bool
_) -> Int
v forall a. Ord a => a -> a -> Bool
<= Int
n) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
           else forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> [(i, e)]
assocs Model
m
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Int -> [a] -> [[a]]
split Int
10 [(Int, Bool)]
as) forall a b. (a -> b) -> a -> b
$ \[(Int, Bool)]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int, Bool)]
xs forall a b. (a -> b) -> a -> b
$ \(Int
var,Bool
val) -> Handle -> String -> IO ()
hPutStr Handle
h (String
" " forall a. [a] -> [a] -> [a]
++ (if Bool
val then String
"" else String
"-") forall a. [a] -> [a] -> [a]
++ String
"x" forall a. [a] -> [a] -> [a]
++ 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
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Int -> [a] -> [[a]]
split Int
10 [Int]
is) forall a b. (a -> b) -> a -> b
$ \[Int]
xs -> do
    Handle -> String -> IO ()
hPutStr Handle
h String
"v"
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
xs forall a b. (a -> b) -> a -> b
$ \Int
i -> Handle -> String -> IO ()
hPutStr Handle
h (Char
' 'forall a. a -> [a] -> [a]
: 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 = forall {a}. [a] -> [[a]]
go
  where
    go :: [a] -> [[a]]
go [] = []
    go [a]
xs =
      case forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [a]
xs of
        ([a]
ys, [a]
zs) -> [a]
ys forall a. a -> [a] -> [a]
: [a] -> [[a]]
go [a]
zs