{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Data.Function ((&))
import qualified Data.List as List
import Data.Aeson (FromJSON(..), ToJSON(..), (.=), (.:))
import qualified Data.Aeson as Aeson
import Data.Hashable (Hashable(..))
import Control.Monad.IO.Class (liftIO)
import Control.Monad (when)
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Test.Hspec (describe, it, hspec)
import Test.Hspec.Hedgehog (hedgehog)
import Process.Minizinc
data Input001 = Input001 { input001X :: Int }
deriving (Show,Eq,Ord)
instance Hashable Input001 where
hashWithSalt s (Input001 x) = hashWithSalt s x
instance ToJSON Input001 where
toJSON (Input001 x) = Aeson.object [ "x" .= x ]
data Output001 = Output001 { output001Y :: Int }
deriving (Show,Eq,Ord)
instance FromJSON Output001 where
parseJSON = Aeson.withObject "output001" $ \v -> Output001 <$> v .: "y"
solver :: MonadGen m => m Solver
solver = Gen.element [ Gecode, Chuffed, COIN_BC ]
mipSolver :: MonadGen m => m Solver
mipSolver = Gen.element [ COIN_BC ]
cpSolver :: MonadGen m => m Solver
cpSolver = Gen.element [ Gecode, Chuffed ]
mzncall_t001_01 = do
x <- forAll $ Gen.integral (Range.linear (-100) 100)
s <- forAll solver
let mzn = simpleMiniZinc @Input001 @Output001 "models/test001_01.mzn" 1000 s
let input = Input001 x
outy <- liftIO $ runLastMinizincJSON mzn input
liftIO $ cleanTmpFile mzn input
Just x === fmap output001Y outy
mzncall_t001_02 = do
x <- forAll $ Gen.integral (Range.linear (-100) 100)
s <- forAll solver
let mzn = simpleMiniZinc @Input001 @Output001 "models/test001_02.mzn" 1000 s
let input = Input001 x
outy <- liftIO $ runLastMinizincJSON mzn input
liftIO $ cleanTmpFile mzn input
Nothing === outy
mzncall_t001_03 = do
x <- forAll $ Gen.integral (Range.linear (-100) 100)
s <- forAll cpSolver
let mzn = simpleMiniZinc @Input001 @Output001 "models/test001_03.mzn" 3000 s
& withArgs ["-a"]
let input = Input001 x
outputs <- liftIO $ runMinizincJSON mzn input [] collectResults
let (exhaustives,nonExhaustives) = List.partition isExhaustive outputs
when (length outputs == 7) $ do
liftIO $ cleanTmpFile mzn input
length outputs === 7
length nonExhaustives === 6
length exhaustives === 1
where
isExhaustive (Exhausted a) = True
isExhaustive _ = False
prop_mzncall_t001_01 :: Property
prop_mzncall_t001_01 =
property mzncall_t001_01
prop_mzncall_t001_02 :: Property
prop_mzncall_t001_02 =
property mzncall_t001_02
prop_mzncall_t001_03 :: Property
prop_mzncall_t001_03 =
property mzncall_t001_03
tests :: IO Bool
tests = checkParallel $$(discover)
main :: IO ()
main = hspec $ do
describe "output-input json reading" $ do
it "should solve trivial problems" $ hedgehog $ do
mzncall_t001_01
it "should not solve unsatisfiable problems" $ hedgehog $ do
mzncall_t001_02
it "should find seven satisfiable answers to y in [x-3 .. x+3]" $ hedgehog $ do
mzncall_t001_03