{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
----------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Solver.SLS.UBCSAT
-- Copyright   :  (c) Masahiro Sakai 2017
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
----------------------------------------------------------------------
module ToySolver.SAT.Solver.SLS.UBCSAT
  ( ubcsatBest
  , ubcsatBestFeasible
  , ubcsatMany
  , Options (..)
  ) where

import Control.Exception
import Control.Monad
import Data.Array.IArray
import Data.Char
import Data.Default
import Data.Either
import Data.Function
import Data.List
import Data.Void
import System.Directory
import System.IO
import System.IO.Temp
import System.Process
import Text.Megaparsec hiding (try)
import Text.Megaparsec.Char

import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT

data Options
  = Options
  { Options -> String
optCommand :: FilePath
  , Options -> Maybe String
optTempDir :: Maybe FilePath
  , Options -> WCNF
optProblem :: CNF.WCNF
  , Options -> Maybe String
optProblemFile :: Maybe FilePath
  , Options -> [Lit]
optVarInit :: [SAT.Lit]
  }

instance Default Options where
  def :: Options
def = Options
        { optCommand :: String
optCommand = String
"ubcsat"
        , optTempDir :: Maybe String
optTempDir = forall a. Maybe a
Nothing
        , optProblem :: WCNF
optProblem =
            CNF.WCNF
            { wcnfNumVars :: Lit
CNF.wcnfNumVars    = Lit
0
            , wcnfNumClauses :: Lit
CNF.wcnfNumClauses = Lit
0
            , wcnfTopCost :: Integer
CNF.wcnfTopCost    = Integer
1
            , wcnfClauses :: [WeightedClause]
CNF.wcnfClauses    = []
            }
        , optProblemFile :: Maybe String
optProblemFile   = forall a. Maybe a
Nothing
        , optVarInit :: [Lit]
optVarInit = []
        }

ubcsatBestFeasible :: Options -> IO (Maybe (Integer, SAT.Model))
ubcsatBestFeasible :: Options -> IO (Maybe (Integer, Model))
ubcsatBestFeasible Options
opt = do
  Maybe (Integer, Model)
ret <- Options -> IO (Maybe (Integer, Model))
ubcsatBest Options
opt
  case Maybe (Integer, Model)
ret of
    Maybe (Integer, Model)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Just (Integer
obj,Model
_) ->
      if Integer
obj forall a. Ord a => a -> a -> Bool
< WCNF -> Integer
CNF.wcnfTopCost (Options -> WCNF
optProblem Options
opt) then
        forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Integer, Model)
ret
      else
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

ubcsatBest :: Options -> IO (Maybe (Integer, SAT.Model))
ubcsatBest :: Options -> IO (Maybe (Integer, Model))
ubcsatBest Options
opt = do
  [(Integer, Model)]
sols <- Options -> IO [(Integer, Model)]
ubcsatMany Options
opt
  case [(Integer, Model)]
sols of
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    [(Integer, Model)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) [(Integer, Model)]
sols

ubcsatMany :: Options -> IO [(Integer, SAT.Model)]
ubcsatMany :: Options -> IO [(Integer, Model)]
ubcsatMany Options
opt = do
  String
dir <- case Options -> Maybe String
optTempDir Options
opt of
           Just String
dir -> forall (m :: * -> *) a. Monad m => a -> m a
return String
dir
           Maybe String
Nothing -> IO String
getTemporaryDirectory

  let f :: String -> IO [(Integer, Model)]
f String
fname
        | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Options -> [Lit]
optVarInit Options
opt) = Options -> String -> Maybe String -> IO [(Integer, Model)]
ubcsat' Options
opt String
fname forall a. Maybe a
Nothing
        | Bool
otherwise = do
            forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
String -> String -> (String -> Handle -> m a) -> m a
withTempFile String
dir String
".txt" forall a b. (a -> b) -> a -> b
$ \String
varInitFile Handle
h -> do
              Handle -> Bool -> IO ()
hSetBinaryMode Handle
h Bool
True
              Handle -> BufferMode -> IO ()
hSetBuffering Handle
h (Maybe Lit -> BufferMode
BlockBuffering forall a. Maybe a
Nothing)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Lit -> [a] -> [[a]]
split Lit
10 (Options -> [Lit]
optVarInit Options
opt)) forall a b. (a -> b) -> a -> b
$ \[Lit]
xs -> do
                Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Lit]
xs)
              Handle -> IO ()
hClose Handle
h
              Options -> String -> Maybe String -> IO [(Integer, Model)]
ubcsat' Options
opt String
fname (forall a. a -> Maybe a
Just String
varInitFile)

  case Options -> Maybe String
optProblemFile Options
opt of
    Just String
fname -> String -> IO [(Integer, Model)]
f String
fname
    Maybe String
Nothing -> do
      forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
String -> String -> (String -> Handle -> m a) -> m a
withTempFile String
dir String
".wcnf" forall a b. (a -> b) -> a -> b
$ \String
fname Handle
h -> do
        Handle -> IO ()
hClose Handle
h
        forall a (m :: * -> *).
(FileFormat a, MonadIO m) =>
String -> a -> m ()
CNF.writeFile String
fname (Options -> WCNF
optProblem Options
opt)
        String -> IO [(Integer, Model)]
f String
fname

ubcsat' :: Options -> FilePath -> Maybe FilePath -> IO [(Integer, SAT.Model)]
ubcsat' :: Options -> String -> Maybe String -> IO [(Integer, Model)]
ubcsat' Options
opt String
fname Maybe String
varInitFile = do
  let wcnf :: WCNF
wcnf = Options -> WCNF
optProblem Options
opt
  let args :: [String]
args =
        [ String
"-w" | String
".wcnf" forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
fname] forall a. [a] -> [a] -> [a]
++
        [ String
"-alg", String
"irots"
        , String
"-seed", String
"0"
        , String
"-runs", String
"10"
        , String
"-cutoff", forall a. Show a => a -> String
show (WCNF -> Lit
CNF.wcnfNumVars WCNF
wcnf forall a. Num a => a -> a -> a
* Lit
50)
        , String
"-timeout", forall a. Show a => a -> String
show (Lit
10 :: Int)
        , String
"-gtimeout", forall a. Show a => a -> String
show (Lit
30 :: Int)
        , String
"-solve"
        , String
"-r", String
"bestsol"
        , String
"-inst", String
fname
        ] forall a. [a] -> [a] -> [a]
++
        (case Maybe String
varInitFile of
           Maybe String
Nothing -> []
           Just String
fname2 -> [String
"-varinitfile", String
fname2])
      stdinStr :: String
stdinStr = String
""

  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"c Running " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Options -> String
optCommand Options
opt) forall a. [a] -> [a] -> [a]
++ String
" with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [String]
args
  Either IOError String
ret <- forall e a. Exception e => IO a -> IO (Either e a)
try forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> IO String
readProcess (Options -> String
optCommand Options
opt) [String]
args String
stdinStr
  case Either IOError String
ret of
    Left (IOError
err :: IOError) -> do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (String -> [String]
lines (forall a. Show a => a -> String
show IOError
err)) forall a b. (a -> b) -> a -> b
$ \String
l -> do
        String -> IO ()
putStr String
"c " forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn String
l
      forall (m :: * -> *) a. Monad m => a -> m a
return []
    Right String
s -> do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (String -> [String]
lines String
s) forall a b. (a -> b) -> a -> b
$ \String
l -> String -> IO ()
putStr String
"c " forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn String
l
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Lit -> String -> [(Integer, Model)]
scanSolutions (WCNF -> Lit
CNF.wcnfNumVars WCNF
wcnf) String
s

scanSolutions :: Int -> String -> [(Integer, SAT.Model)]
scanSolutions :: Lit -> String -> [(Integer, Model)]
scanSolutions Lit
nv String
s = forall a b. [Either a b] -> [b]
rights forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse (forall (m :: * -> *).
MonadParsec Void String m =>
Lit -> m (Integer, Model)
solution Lit
nv) String
"") forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
s

solution :: MonadParsec Void String m => Int -> m (Integer, SAT.Model)
solution :: forall (m :: * -> *).
MonadParsec Void String m =>
Lit -> m (Integer, Model)
solution Lit
nv = do
  forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipSome forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
digitChar
  forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Token String
_ <- forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'0' forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'1'
  forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Integer
obj <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Read a => String -> a
read forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
digitChar
  forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  [Bool]
values <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ((forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'0' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'1' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True))
  let m :: Model
m = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [(i, e)] -> a i e
array (Lit
1, Lit
nv) (forall a b. [a] -> [b] -> [(a, b)]
zip [Lit
1..] [Bool]
values)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
obj, Model
m)


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