LogParser.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Test.SAT.LogParser (satLogParserTestGroup) where

import Data.Array.IArray
import qualified Data.ByteString.Lazy.Char8 as BL
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.TH

import ToySolver.SAT.LogParser

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

case_parseSATLog_SATISFIABLE :: Assertion
case_parseSATLog_SATISFIABLE = parseSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s SATISFIABLE"
      , "c bar"
      , "v -1 -2 3 4 -5"
      , "c baz"
      , "v 6 -7 8 9 -10"
      , "c quz"
      , "v 0"
      ]
    expected =
      ( "SATISFIABLE"
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

case_parseSATLog_UNSATISFIABLE :: Assertion
case_parseSATLog_UNSATISFIABLE = parseSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNSATISFIABLE"
      , "c bar"
      ]
    expected =
      ( "UNSATISFIABLE"
      , Nothing
      )

case_parseSATLog_UNKNOWN :: Assertion
case_parseSATLog_UNKNOWN = parseSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNKNOWN"
      , "c bar"
      ]
    expected =
      ( "UNKNOWN"
      , Nothing
      )

case_parseSATLog_UNKNOWN_implicit :: Assertion
case_parseSATLog_UNKNOWN_implicit = parseSATLog input @?= expected
  where
    input = BL.unlines ["c foo"]
    expected =
      ( "UNKNOWN"
      , Nothing
      )

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

case_parseMaxSATLog_UNSATISFIABLE :: Assertion
case_parseMaxSATLog_UNSATISFIABLE = parseMaxSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNSATISFIABLE"
      , "c bar"
      ]
    expected =
      ( "UNSATISFIABLE"
      , Nothing
      , Nothing
      )

case_parseMaxSATLog_UNKNOWN :: Assertion
case_parseMaxSATLog_UNKNOWN = parseMaxSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNKNOWN"
      , "c bar"
      ]
    expected =
      ( "UNKNOWN"
      , Nothing
      , Nothing
      )

case_parseMaxSATLog_UNKNOWN_implicit :: Assertion
case_parseMaxSATLog_UNKNOWN_implicit = parsePBLog input @?= expected
  where
    input = BL.unlines ["c foo"]
    expected =
      ( "UNKNOWN"
      , Nothing
      , Nothing
      )

case_parseMaxSATLog_OPTIMUM_FOUND_old :: Assertion
case_parseMaxSATLog_OPTIMUM_FOUND_old = parseMaxSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "o 4750"
      , "o 232"
      , "s OPTIMUM FOUND"
      , "c bar"
      , "v -1 -2 3 4 -5"
      , "c baz"
      , "v 6 -7 8 9 -10"
      , "c quz"
      ]
    expected =
      ( "OPTIMUM FOUND"
      , Just 232
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

case_parseMaxSATLog_OPTIMUM_FOUND_new :: Assertion
case_parseMaxSATLog_OPTIMUM_FOUND_new = parseMaxSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "o 4750"
      , "o 232"
      , "s OPTIMUM FOUND"
      , "c bar"
      , "v 00110"
      , "c baz"
      , "v 10110"
      , "c quz"
      ]
    expected =
      ( "OPTIMUM FOUND"
      , Just 232
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

-- Special Track on Incomplete Solvers allowed multiple v-lines
-- http://maxsat.ia.udl.cat/requirements/
case_parseMaxSATLog_multiple_vlines :: Assertion
case_parseMaxSATLog_multiple_vlines = parseMaxSATLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "o 4750"
      , "v 1 2 3 4 5 6 7 8 9 10"
      , "o 232"
      , "c bar"
      , "v -1 -2 3 4 -5 6 -7 8 9 -10"
      , "s SATISFIABLE"
      , "c quz"
      ]
    expected =
      ( "SATISFIABLE"
      , Just 232
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

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

case_parsePBLog_OPTIMUM_FOUND :: Assertion
case_parsePBLog_OPTIMUM_FOUND = parsePBLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "o 4750"
      , "o 232"
      , "s OPTIMUM FOUND"
      , "c bar"
      , "v -x1 -x2 x3 x4 -x5"
      , "c baz"
      , "v x6 -x7 x8 x9 -x10"
      , "c quz"
      ]
    expected =
      ( "OPTIMUM FOUND"
      , Just 232
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

case_parsePBLog_SATISFIABLE :: Assertion
case_parsePBLog_SATISFIABLE = parsePBLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "o 4750"
      , "o 232"
      , "s SATISFIABLE"
      , "c bar"
      , "v -x1 -x2 x3 x4 -x5"
      , "c baz"
      , "v x6 -x7 x8 x9 -x10"
      , "c quz"
      ]
    expected =
      ( "SATISFIABLE"
      , Just 232
      , Just $ array (1, 10) [(1, False), (2, False), (3, True), (4, True), (5, False), (6, True), (7, False), (8, True), (9, True), (10, False)]
      )

case_parsePBLog_UNSATISFIABLE :: Assertion
case_parsePBLog_UNSATISFIABLE = parsePBLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNSATISFIABLE"
      , "c bar"
      ]
    expected =
      ( "UNSATISFIABLE"
      , Nothing
      , Nothing
      )

case_parsePBLog_UNKNOWN :: Assertion
case_parsePBLog_UNKNOWN = parsePBLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNKNOWN"
      , "c bar"
      ]
    expected =
      ( "UNKNOWN"
      , Nothing
      , Nothing
      )

case_parsePBLog_UNKNOWN_implicit :: Assertion
case_parsePBLog_UNKNOWN_implicit = parsePBLog input @?= expected
  where
    input = BL.unlines ["c foo"]
    expected =
      ( "UNKNOWN"
      , Nothing
      , Nothing
      )

case_parsePBLog_UNSUPPORTED :: Assertion
case_parsePBLog_UNSUPPORTED = parsePBLog input @?= expected
  where
    input = BL.unlines
      [ "c foo"
      , "s UNSUPPORTED"
      , "c bar"
      ]
    expected =
      ( "UNSUPPORTED"
      , Nothing
      , Nothing
      )

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

satLogParserTestGroup :: TestTree
satLogParserTestGroup = $(testGroupGenerator)