LogParser.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.LogParser
-- Copyright   :  (c) Masahiro Sakai 2025
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.SAT.LogParser
  ( parseSATLog
  , parseMaxSATLog
  , parsePBLog
  ) where

import Data.Array.IArray
import qualified Data.ByteString.Char8 as BS
import qualified Data.ByteString.Lazy.Char8 as BL
import Data.Char
import Data.Maybe (fromMaybe)
import qualified Data.Vector.Unboxed as VU

import ToySolver.SAT.Types as SAT

parseSATLog :: BL.ByteString -> (BS.ByteString, Maybe SAT.Model)
parseSATLog s = f "UNKNOWN" Nothing (BL.lines s)
  where
    f :: BS.ByteString -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe SAT.Model)
    f !status vlines (l : ls) =
      case BL.uncons l of
        Just ('c', _) -> f status vlines ls
        Just ('s', BS.toStrict -> BS.strip -> rest) -> f rest vlines ls
        Just ('v', rest) ->
          let vlines' = Just $ rest : fromMaybe [] vlines
           in f status vlines' ls
        Just (c, _) -> error ("unknown line type: " ++ show c)
        Nothing -> f status vlines ls
    f !status vlines [] =
      ( status
      , case vlines of
          Nothing -> Nothing
          Just lss ->
            let xs = VU.fromList $ map (read . BL.unpack) $ concat $ map BL.words $ reverse lss
                xs' = VU.init xs
                n = maximum $ map abs $ VU.toList xs'
             in if VU.last xs /= 0 then
                  error "vlines are not terminated with zero"
                else if 0 `VU.elem` xs' then
                  error "multiple zeros in vlines"
                else
                  Just $ array (1, n) [if lit > 0 then (lit, True) else (- lit, False) | lit <- VU.toList xs']
      )

parseMaxSATLog :: BL.ByteString -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)
parseMaxSATLog s = f "UNKNOWN" Nothing Nothing (BL.lines s)
  where
    f :: BS.ByteString -> Maybe Integer -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)
    f !status obj vlines (l : ls) =
      case BL.uncons l of
        Just ('c', _) -> f status obj vlines ls
        Just ('s', BL.toStrict -> BS.strip -> rest) -> f rest obj vlines ls
        Just ('v', rest) ->
          let vlines' = Just $ rest : fromMaybe [] vlines
           in f status obj vlines' ls
        Just ('o', BL.toStrict -> BS.strip -> rest) ->
          case BS.readInteger rest of
            Just (!val, "") -> f status (Just val) Nothing ls
            _ -> error "failed to parse o-line"
        Just (c, _) -> error ("unknown line type: " ++ show c)
        Nothing -> f status obj vlines ls
    f !status obj vlines [] =
      ( status
      , obj
      , case vlines of
          Nothing -> Nothing
          Just lss ->
            let tmp1 = BL.filter (not . isSpace) $ BL.concat $ reverse lss
                tmp2 = map (read . BL.unpack) $ concat $ map BL.words $ reverse lss
             in if BL.all (\c -> c == '0' || c == '1') tmp1 then
                  Just $ array (1, fromIntegral (BL.length tmp1)) [(v, c=='1') | (v, c) <- zip [1..] (BL.unpack tmp1)]
                else
                  Just $ array (1, maximum (map abs tmp2)) [if lit > 0 then (lit, True) else (- lit, False) | lit <- tmp2]
      )

parsePBLog :: BL.ByteString -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)
parsePBLog s = f "UNKNOWN" Nothing Nothing (BL.lines s)
  where
    f :: BS.ByteString -> Maybe Integer -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)
    f !status obj vlines (l : ls) =
      case BL.uncons l of
        Just ('c', _) -> f status obj vlines ls
        Just ('s', BL.toStrict -> BS.strip -> rest) -> f rest obj vlines ls
        Just ('v', rest) ->
          let vlines' = Just $ rest : fromMaybe [] vlines
           in f status obj vlines' ls
        Just ('o', BL.toStrict -> BS.strip -> rest) ->
          case BS.readInteger rest of
            Just (!val, "") -> f status (Just val) Nothing ls
            _ -> error "failed to parse o-line"
        Just (c, _) -> error ("unknown line type: " ++ show c)
        Nothing -> f status obj vlines ls
    f !status obj vlines [] =
      ( status
      , obj
      , case vlines of
          Nothing -> Nothing
          Just lss ->
            let lits = map (parseLit . BL.unpack) $ concat $ map BL.words $ reverse lss
             in Just $ array (1, maximum (map abs lits)) [if lit > 0 then (lit, True) else (- lit, False) | lit <- lits]
      )

    parseLit :: String -> SAT.Lit
    parseLit ('-' : 'x' : rest) | [(v, "")] <- reads rest = - v
    parseLit ('x' : rest) | [(v, "")] <- reads rest = v
    parseLit w = error ("failed to parse a literal: " ++ show w)