CNF.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Test.CNF (cnfTestGroup) where

import Data.ByteString.Builder
import qualified Data.ByteString.Lazy.Char8 as BL
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import Test.Tasty.TH
import ToySolver.FileFormat
import qualified ToySolver.FileFormat.CNF as CNF

import Test.SAT.Utils

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

prop_CNF_ReadWrite_Invariance :: Property
prop_CNF_ReadWrite_Invariance = forAll arbitraryCNF $ \cnf ->
  CNF.parse (toLazyByteString (CNF.render cnf)) == Right cnf

prop_GCNF_ReadWrite_Invariance :: Property
prop_GCNF_ReadWrite_Invariance = forAll arbitraryGCNF $ \gcnf ->
  CNF.parse (toLazyByteString (CNF.render gcnf)) == Right gcnf

prop_WCNF_ReadWrite_Invariance :: Property
prop_WCNF_ReadWrite_Invariance = forAll arbitraryWCNF $ \wcnf ->
  CNF.parse (toLazyByteString (CNF.render wcnf)) == Right wcnf

prop_NewWCNF_ReadWrite_Invariance :: Property
prop_NewWCNF_ReadWrite_Invariance = forAll arbitraryNewWCNF $ \wcnf ->
  CNF.parse (toLazyByteString (CNF.render wcnf)) == Right wcnf

prop_QDimacs_ReadWrite_Invariance :: Property
prop_QDimacs_ReadWrite_Invariance = forAll arbitraryQDimacs $ \qdimacs ->
  CNF.parse (toLazyByteString (CNF.render qdimacs)) == Right qdimacs

prop_GCNF_from_CNF :: Property
prop_GCNF_from_CNF = forAll arbitraryCNF $ \cnf ->
  case CNF.parse (toLazyByteString (CNF.render cnf)) of
    Left _ -> False
    Right gcnf -> and
      [ CNF.gcnfNumVars gcnf == CNF.cnfNumVars cnf
      , CNF.gcnfNumClauses gcnf == CNF.cnfNumClauses cnf
      , CNF.gcnfLastGroupIndex gcnf == CNF.cnfNumClauses cnf
      , CNF.gcnfClauses gcnf == zip [1..] (CNF.cnfClauses cnf)
      ]

prop_WCNF_from_CNF :: Property
prop_WCNF_from_CNF = forAll arbitraryCNF $ \cnf ->
  case CNF.parse (toLazyByteString (CNF.render cnf)) of
    Left _ -> False
    Right wcnf -> and
      [ CNF.wcnfNumVars wcnf == CNF.cnfNumVars cnf
      , CNF.wcnfNumClauses wcnf == CNF.cnfNumClauses cnf
      , CNF.wcnfTopCost wcnf > fromIntegral (CNF.cnfNumClauses cnf)
      , CNF.wcnfClauses wcnf == map (\c -> (1,c)) (CNF.cnfClauses cnf)
      ]

prop_QDimacs_from_CNF :: Property
prop_QDimacs_from_CNF = forAll arbitraryCNF $ \cnf ->
  case CNF.parse (toLazyByteString (CNF.render cnf)) of
    Left _ -> False
    Right qdimacs -> and
      [ CNF.qdimacsNumVars qdimacs == CNF.cnfNumVars cnf
      , CNF.qdimacsNumClauses qdimacs == CNF.cnfNumClauses cnf
      , CNF.qdimacsPrefix qdimacs == []
      , CNF.qdimacsMatrix qdimacs == CNF.cnfClauses cnf
      ]

-- example from https://maxsat-evaluations.github.io/2021/format.html
case_parse_new_WCNF_as_old :: IO ()
case_parse_new_WCNF_as_old = parse s @?= Right expected
  where
    s = BL.pack $ unlines
        [ "c This is a comment"
        , "c Example 1...another comment"
        , "h 1 2 3 4 0"
        , "1 -3 -5 6 7 0"
        , "6 -1 -2 0"
        , "4 1 6 -7 0"
        ]
    h = 12
    expected =
      CNF.WCNF
      { CNF.wcnfNumVars = 7
      , CNF.wcnfNumClauses = 4
      , CNF.wcnfTopCost = h
      , CNF.wcnfClauses =
          [ (h, CNF.packClause [1,2,3,4])
          , (1, CNF.packClause [-3,-5,6,7])
          , (6, CNF.packClause [-1,-2])
          , (4, CNF.packClause [1,6,-7])
          ]
      }

-- example from https://maxsat-evaluations.github.io/2021/format.html
case_parse_old_WCNF_as_new :: IO ()
case_parse_old_WCNF_as_new = parse s @?= Right expected
  where
    s = BL.pack $ unlines
        [ "c This is a comment"
        , "c Example 1...another comment"
        , "p wcnf 7 4 12 "
        , "12 1 2 3 4 0"
        , "1 -3 -5 6 7 0"
        , "6 -1 -2 0"
        , "4 1 6 -7 0"
        ]
    expected =
      CNF.NewWCNF
        [ (Nothing, CNF.packClause [1,2,3,4])
        , (Just 1, CNF.packClause [-3,-5,6,7])
        , (Just 6, CNF.packClause [-1,-2])
        , (Just 4, CNF.packClause [1,6,-7])
        ]

------------------------------------------------------------------------
-- Test harness

cnfTestGroup :: TestTree
cnfTestGroup = $(testGroupGenerator)