import Picosat
import Control.Monad.IO.Class (liftIO)
import Control.Monad (when)
import qualified Data.Set as S

printAllSolutions = do
  xs <- scopedAllSolutions
  liftIO $ mapM_ print xs

expectSolutions expected = do
  real <- scopedAllSolutions
  when (S.fromList expected /= S.fromList real) $ liftIO $ do
    print ("expected", expected)
    print ("real", real)
    error "test failed"

main =
  evalScopedPicosat $ do
    addBaseClauses [[1, 2, 3]]
    
    liftIO $ putStrLn "base cnf [[1, 2, 3]]"
    printAllSolutions
    expectSolutions [Solution [1,2,3],
                     Solution [1,2,-3],
                     Solution [1,-2,3],
                     Solution [1,-2,-3],
                     Solution [-1,-2,3],
                     Solution [-1,2,-3],
                     Solution [-1,2,3]]

    withScopedClauses [[-2,-3]] $ do
      liftIO $ putStrLn "\nwith [-2,-3]"
      printAllSolutions
      expectSolutions [Solution [-1,2,-3],
                       Solution [-1,-2,3],
                       Solution [1,-2,-3],
                       Solution [1,-2,3],
                       Solution [1,2,-3]]

    withScopedClauses [[-1,-2]] $ do
      liftIO $ putStrLn "\nwith [-1,-2]"
      printAllSolutions
      expectSolutions [Solution [1,-2,3],
                       Solution [1,-2,-3],
                       Solution [-1,-2,3],
                       Solution [-1,2,-3],
                       Solution [-1,2,3]]

    addBaseClauses [[-1,-3]]
    expectSolutions [Solution [-1,2,-3],
                     Solution [-1,2,3],
                     Solution [-1,-2,3],
                     Solution [1,-2,-3],
                     Solution [1,2,-3]]

    withScopedClauses [[-2,-3]] $ do
      expectSolutions [Solution [1,-2,-3],
                       Solution [1,2,-3],
                       Solution [-1,-2,3],
                       Solution [-1,2,-3]]

    withScopedClauses [[-1,-2], [1,-3]] $ do
      expectSolutions [Solution [-1,2,-3],
                       Solution [1,-2,-3]]

      let printSolutionsWithAssumptions as = do
            liftIO $ putStrLn ("\nwith assumptions " ++ show as)
            res <- scopedSolutionWithAssumptions as
            liftIO $ print res

      printSolutionsWithAssumptions [1]
      printSolutionsWithAssumptions [-1]
      printSolutionsWithAssumptions [2]
      printSolutionsWithAssumptions [-2]
      printSolutionsWithAssumptions [3]
      printSolutionsWithAssumptions [-3]