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
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
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
""
Handle -> IO ()
hFlush Handle
h
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
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