toysolver-0.9.0: test/Test/Converter.hs
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Test.Converter (converterTestGroup) where
import Control.Monad
import qualified Data.Aeson as J
import Data.Array.IArray
import qualified Data.Foldable as F
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.String
import qualified Data.Vector.Generic as VG
import qualified Numeric.Optimization.MIP as MIP
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck hiding ((.&&.), (.||.))
import Test.Tasty.TH
import qualified Test.QuickCheck as QC
import qualified Test.QuickCheck.Monadic as QM
import ToySolver.Converter
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Graph.Base
import qualified ToySolver.Graph.MaxCut as MaxCut
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Types as SAT
import qualified Data.PseudoBoolean as PBFile
import Test.SAT.Utils
------------------------------------------------------------------------
case_identity_transformer_json :: Assertion
case_identity_transformer_json = do
let info :: IdentityTransformer SAT.Model
info = IdentityTransformer
json = J.encode info
J.eitherDecode json @?= Right info
case_reversed_transformer_json :: Assertion
case_reversed_transformer_json = do
let info :: ReversedTransformer (IdentityTransformer SAT.Model)
info = ReversedTransformer IdentityTransformer
json = J.encode info
J.eitherDecode json @?= Right info
------------------------------------------------------------------------
prop_sat2naesat_forward :: Property
prop_sat2naesat_forward = forAll arbitraryCNF $ \cnf ->
let ret@(nae,info) = sat2naesat cnf
in counterexample (show ret) $
forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
evalCNF m cnf === evalNAESAT (transformForward info m) nae
prop_sat2naesat_backward :: Property
prop_sat2naesat_backward = forAll arbitraryCNF $ \cnf ->
let ret@(nae,info) = sat2naesat cnf
in counterexample (show ret) $
forAllAssignments (fst nae) $ \m ->
evalCNF (transformBackward info m) cnf === evalNAESAT m nae
prop_sat2naesat_json :: Property
prop_sat2naesat_json = forAll arbitraryCNF $ \cnf ->
let ret@(_,info) = sat2naesat cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_naesat2sat_forward :: Property
prop_naesat2sat_forward = forAll arbitraryNAESAT $ \nae ->
let ret@(cnf,info) = naesat2sat nae
in counterexample (show ret) $
forAllAssignments (fst nae) $ \m ->
evalNAESAT m nae === evalCNF (transformForward info m) cnf
prop_naesat2sat_backward :: Property
prop_naesat2sat_backward = forAll arbitraryNAESAT $ \nae ->
let ret@(cnf,info) = naesat2sat nae
in counterexample (show ret) $
forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
evalNAESAT (transformBackward info m) nae === evalCNF m cnf
prop_naesat2sat_json :: Property
prop_naesat2sat_json = forAll arbitraryNAESAT $ \nae ->
let ret@(_,info) = naesat2sat nae
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_naesat2naeksat_forward :: Property
prop_naesat2naeksat_forward =
forAll arbitraryNAESAT $ \nae ->
forAll (choose (3,10)) $ \k ->
let ret@(nae',info) = naesat2naeksat k nae
in counterexample (show ret) $
property (all (\c -> VG.length c <= k) (snd nae'))
QC..&&.
(forAllAssignments (fst nae) $ \m ->
evalNAESAT m nae === evalNAESAT (transformForward info m) nae')
prop_naesat2naeksat_backward :: Property
prop_naesat2naeksat_backward =
forAll arbitraryNAESAT $ \nae ->
forAll (choose (3,10)) $ \k ->
let ret@(nae',info) = naesat2naeksat k nae
in counterexample (show ret) $
forAll (arbitraryAssignment (fst nae')) $ \m ->
evalNAESAT (transformBackward info m) nae || not (evalNAESAT m nae')
prop_naesat2naeksat_json :: Property
prop_naesat2naeksat_json =
forAll arbitraryNAESAT $ \nae ->
forAll (choose (3,10)) $ \k ->
let ret@(_,info) = naesat2naeksat k nae
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_naesat2maxcut_forward :: Property
prop_naesat2maxcut_forward =
forAll arbitraryNAESAT $ \nae ->
let ret@((maxcut, threshold), info) = naesat2maxcut nae
in counterexample (show ret) $
forAllAssignments (fst nae) $ \m ->
evalNAESAT m nae === (MaxCut.eval (transformForward info m) maxcut >= threshold)
prop_naesat2maxcut_backward :: Property
prop_naesat2maxcut_backward = forAll arbitraryNAESAT $ \nae ->
let ret@((g, threshold),info) = naesat2maxcut nae
in counterexample (show ret) $
forAll (arbitraryCut g) $ \cut ->
if MaxCut.eval cut g >= threshold then
evalNAESAT (transformBackward info cut) nae
else
True
prop_naesat2maxcut_json :: Property
prop_naesat2maxcut_json =
forAll arbitraryNAESAT $ \nae ->
let ret@(_, info) = naesat2maxcut nae
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_naesat2max2sat_forward :: Property
prop_naesat2max2sat_forward =
forAll arbitraryNAESAT $ \nae ->
let ret@((wcnf, threshold), info) = naesat2max2sat nae
in counterexample (show ret) $
forAllAssignments (fst nae) $ \m ->
case evalWCNF (transformForward info m) wcnf of
Nothing -> property False
Just v -> evalNAESAT m nae === (v <= threshold)
prop_naesat2max2sat_backward :: Property
prop_naesat2max2sat_backward =
forAll arbitraryNAESAT $ \nae ->
let ret@((wcnf, threshold), info) = naesat2max2sat nae
in counterexample (show ret) $
forAll (arbitraryAssignment (CNF.wcnfNumVars wcnf)) $ \m ->
case evalWCNF m wcnf of
Just v | v <= threshold -> evalNAESAT (transformBackward info m) nae
_ -> True
prop_naesat2max2sat_json :: Property
prop_naesat2max2sat_json =
forAll arbitraryNAESAT $ \nae ->
let ret@(_, info) = naesat2max2sat nae
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_sat2maxcut_forward :: Property
prop_sat2maxcut_forward =
forAll arbitraryCNF $ \cnf ->
let ret@((g, threshold), info) = sat2maxcut cnf
in counterexample (show ret) $
forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
evalCNF m cnf === (MaxCut.eval (transformForward info m) g >= threshold)
prop_sat2maxcut_backward :: Property
prop_sat2maxcut_backward = forAll arbitraryCNF $ \cnf ->
let ret@((g, threshold),info) = sat2maxcut cnf
in counterexample (show ret) $
forAll (arbitraryCut g) $ \cut ->
if MaxCut.eval cut g >= threshold then
-- TODO: maybe it's difficult to come here
evalCNF (transformBackward info cut) cnf
else
True
prop_sat2maxcut_json :: Property
prop_sat2maxcut_json =
forAll arbitraryCNF $ \cnf ->
let ret@(_, info) = sat2maxcut cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
arbitraryCut :: MaxCut.Problem a -> Gen MaxCut.Solution
arbitraryCut g = do
let b = bounds g
xs <- replicateM (rangeSize b) arbitrary
return $ array b (zip (range b) xs)
------------------------------------------------------------------------
prop_satToMaxSAT2_forward :: Property
prop_satToMaxSAT2_forward =
forAll arbitraryCNF $ \cnf ->
let ((wcnf, threshold), info) = satToMaxSAT2 cnf
in and
[ evalCNF m cnf == b2
| m <- allAssignments (CNF.cnfNumVars cnf)
, let m2 = transformForward info m
b2 = case evalWCNF m2 wcnf of
Nothing -> False
Just v -> v <= threshold
]
prop_satToMaxSAT2_json :: Property
prop_satToMaxSAT2_json =
forAll arbitraryCNF $ \cnf ->
let ret@(_, info) = satToMaxSAT2 cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_simplifyMaxSAT2_forward :: Property
prop_simplifyMaxSAT2_forward =
forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
let r@((_n,cs,th2), info) = simplifyMaxSAT2 (wcnf, th1)
in counterexample (show r) $ and
[ b1 == b2
| m1 <- allAssignments (CNF.wcnfNumVars wcnf)
, let o1 = fromJust $ evalWCNF m1 wcnf
b1 = o1 <= th1
m2 = transformForward info m1
o2 = fromIntegral $ length [()| (l1,l2) <- Set.toList cs, not (SAT.evalLit m2 l1), not (SAT.evalLit m2 l2)]
b2 = o2 <= th2
]
prop_simplifyMaxSAT2_json :: Property
prop_simplifyMaxSAT2_json =
forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
let ret@(_, info) = simplifyMaxSAT2 (wcnf, th1)
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_maxSAT2ToSimpleMaxCut_forward :: Property
prop_maxSAT2ToSimpleMaxCut_forward =
forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
let r@((maxcut, th2), info) = maxSAT2ToSimpleMaxCut (wcnf, th1)
in counterexample (show r) $ and
[ b1 == b2
| m <- allAssignments (CNF.wcnfNumVars wcnf)
, let o1 = fromJust $ evalWCNF m wcnf
b1 = o1 <= th1
sol2 = transformForward info m
o2 = MaxCut.eval sol2 maxcut
b2 = o2 >= th2
]
prop_maxSAT2ToSimpleMaxCut_backward :: Property
prop_maxSAT2ToSimpleMaxCut_backward =
forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
let r@((g, th2), info) = maxSAT2ToSimpleMaxCut (wcnf, th1)
in counterexample (show r) $
forAll (arbitraryCut g) $ \cut ->
if MaxCut.eval cut g >= th2 then
case evalWCNF (transformBackward info cut) wcnf of
Nothing -> False
Just v -> v <= th1
else
True
prop_maxSAT2ToSimpleMaxCut_json :: Property
prop_maxSAT2ToSimpleMaxCut_json =
forAll arbitraryMaxSAT2 $ \(wcnf, th1) ->
let ret@(_, info) = maxSAT2ToSimpleMaxCut (wcnf, th1)
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
-- -- Too Slow
-- prop_satToSimpleMaxCut_forward :: Property
-- prop_satToSimpleMaxCut_forward =
-- forAll arbitraryCNF $ \cnf ->
-- let ret@((g, threshold), info) = satToSimpleMaxCut cnf
-- in counterexample (show ret) $
-- forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
-- evalCNF m cnf === (MaxCut.eval (transformForward info m) g >= threshold)
-- -- Too Slow
-- prop_satToSimpleMaxCut_backward :: Property
-- prop_satToSimpleMaxCut_backward = forAll arbitraryCNF $ \cnf ->
-- let ret@((g, threshold),info) = satToSimpleMaxCut cnf
-- in counterexample (show ret) $
-- forAll (arbitraryCut g) $ \cut ->
-- if MaxCut.eval cut g >= threshold then
-- evalCNF (transformBackward info cut) cnf
-- else
-- True
prop_satToSimpleMaxCut_json :: Property
prop_satToSimpleMaxCut_json =
forAll arbitraryCNF $ \cnf ->
let ret@(_, info) = satToSimpleMaxCut cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
------------------------------------------------------------------------
prop_satToIS_forward :: Property
prop_satToIS_forward =
forAll arbitraryCNF $ \cnf -> do
let r@((g,k), info) = satToIS cnf
in counterexample (show r) $ conjoin
[ counterexample (show m) $ counterexample (show set) $
not (evalCNF m cnf) || (set `isIndependentSetOf` g && IntSet.size set >= k)
| m <- allAssignments (CNF.cnfNumVars cnf)
, let set = transformForward info m
]
prop_satToIS_backward :: Property
prop_satToIS_backward =
forAll arbitraryCNF $ \cnf -> do
let r@((g,k), info) = satToIS cnf
in counterexample (show r) $
forAll (oneof [arbitraryIndependentSet g, arbitraryIndependentSet' g k]) $ \set -> do
let m = transformBackward info set
in counterexample (show m) $
not (IntSet.size set >= k) || evalCNF m cnf
prop_satToIS_json :: Property
prop_satToIS_json =
forAll arbitraryCNF $ \cnf -> do
let r@(_, info) = satToIS cnf
json = J.encode info
in counterexample (show r) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_mis2MaxSAT_forward :: Property
prop_mis2MaxSAT_forward =
forAll arbitraryGraph $ \g -> do
let r@(wcnf, info) = mis2MaxSAT g
in counterexample (show r) $ conjoin
[ counterexample (show set) $ counterexample (show m) $ o1 === o2
| set <- map IntSet.fromList $ allSubsets $ range $ bounds g
, let m = transformForward info set
o1 = if set `isIndependentSetOf` g
then Just (transformObjValueForward info (IntSet.size set))
else Nothing
o2 = evalWCNF m wcnf
]
where
allSubsets :: [a] -> [[a]]
allSubsets = filterM (const [False, True])
prop_mis2MaxSAT_backward :: Property
prop_mis2MaxSAT_backward =
forAll arbitraryGraph $ \g -> do
let r@(wcnf, info) = mis2MaxSAT g
in counterexample (show r) $ conjoin
[ counterexample (show m) $ counterexample (show set) $ o1 === o2
| m <- allAssignments (CNF.wcnfNumVars wcnf)
, let set = transformBackward info m
o1 = if set `isIndependentSetOf` g
then Just (IntSet.size set)
else Nothing
o2 = fmap (transformObjValueBackward info) $ evalWCNF m wcnf
]
prop_mis2MaxSAT_json :: Property
prop_mis2MaxSAT_json =
forAll arbitraryGraph $ \g -> do
let r@(_, info) = mis2MaxSAT g
json = J.encode info
in counterexample (show r) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_is2pb_forward :: Property
prop_is2pb_forward =
forAll arbitraryGraph $ \g ->
forAll arbitrary $ \(Positive k) ->
let ret@(opb,info) = is2pb (g, k)
in counterexample (show ret) $ conjoin
[ counterexample (show set) $ counterexample (show m) $ o1 === o2
| set <- map IntSet.fromList $ allSubsets $ range $ bounds g
, let m = transformForward info set
o1 = set `isIndependentSetOf` g && IntSet.size set >= k
o2 = isJust $ SAT.evalPBFormula m opb
]
where
allSubsets :: [a] -> [[a]]
allSubsets = filterM (const [False, True])
prop_is2pb_backward :: Property
prop_is2pb_backward =
forAll arbitraryGraph $ \g ->
forAll arbitrary $ \(Positive k) ->
let ret@(opb,info) = is2pb (g, k)
in counterexample (show ret) $ conjoin
[ counterexample (show m) $ counterexample (show set) $ o1 === o2
| m <- allAssignments (PBFile.pbNumVars opb)
, let set = transformBackward info m
o1 = set `isIndependentSetOf` g && IntSet.size set >= k
o2 = isJust $ SAT.evalPBFormula m opb
]
prop_is2pb_json :: Property
prop_is2pb_json =
forAll arbitraryGraph $ \g ->
forAll arbitrary $ \(Positive k) ->
let ret@(_,info) = is2pb (g, k)
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
arbitraryGraph :: Gen Graph
arbitraryGraph = do
n <- choose (0, 8) -- inclusive range
es <- liftM concat $ forM [0..n-1] $ \v1 -> do
vs <- sublistOf [0..n-1]
return [(v1, v2, ()) | v2 <- vs]
return $ graphFromUnorderedEdges n es
arbitraryIndependentSet :: Graph -> Gen IntSet
arbitraryIndependentSet g = do
s <- arbitraryMaximalIndependentSet g
liftM IntSet.fromList $ sublistOf $ IntSet.toList s
arbitraryIndependentSet' :: Graph -> Int -> Gen IntSet
arbitraryIndependentSet' g k = go IntSet.empty (IntSet.fromList (range (bounds g)))
where
go s c
| IntSet.size s >= k = return s
| IntSet.null c = return s
| otherwise = do
a <- elements (IntSet.toList c)
go (IntSet.insert a s) (IntSet.delete a c IntSet.\\ (IntMap.keysSet (g ! a)))
arbitraryMaximalIndependentSet :: Graph -> Gen IntSet
arbitraryMaximalIndependentSet g = go IntSet.empty (IntSet.fromList (range (bounds g)))
where
go s c
| IntSet.null c = return s
| otherwise = do
a <- elements (IntSet.toList c)
go (IntSet.insert a s) (IntSet.delete a c IntSet.\\ (IntMap.keysSet (g ! a)))
------------------------------------------------------------------------
prop_sat2pb_forward :: Property
prop_sat2pb_forward = forAll arbitraryCNF $ \cnf ->
let ret@(opb,info) = sat2pb cnf
in counterexample (show ret) $
forAllAssignments (CNF.cnfNumVars cnf) $ \m ->
evalCNF m cnf === isJust (SAT.evalPBFormula (transformForward info m) opb)
prop_sat2pb_backward :: Property
prop_sat2pb_backward = forAll arbitraryCNF $ \cnf ->
let ret@(opb,info) = sat2pb cnf
in counterexample (show ret) $
forAllAssignments (PBFile.pbNumVars opb) $ \m ->
evalCNF (transformBackward info m) cnf === isJust (SAT.evalPBFormula m opb)
prop_sat2pb_json :: Property
prop_sat2pb_json = forAll arbitraryCNF $ \cnf ->
let ret@(_,info) = sat2pb cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_maxsat2wbo_forward :: Property
prop_maxsat2wbo_forward = forAll arbitraryWCNF $ \cnf ->
let ret@(wbo,info) = maxsat2wbo cnf
in counterexample (show ret) $
forAllAssignments (CNF.wcnfNumVars cnf) $ \m ->
fmap (transformObjValueForward info) (evalWCNF m cnf) === SAT.evalPBSoftFormula (transformForward info m) wbo
prop_maxsat2wbo_backward :: Property
prop_maxsat2wbo_backward = forAll arbitraryWCNF $ \cnf ->
let ret@(wbo,info) = maxsat2wbo cnf
in counterexample (show ret) $
forAllAssignments (PBFile.wboNumVars wbo) $ \m ->
evalWCNF (transformBackward info m) cnf === fmap (transformObjValueBackward info) (SAT.evalPBSoftFormula m wbo)
prop_maxsat2wbo_json :: Property
prop_maxsat2wbo_json = forAll arbitraryWCNF $ \cnf ->
let ret@(_,info) = maxsat2wbo cnf
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_pb2sat :: Property
prop_pb2sat = QM.monadicIO $ do
opb <- QM.pick arbitraryPBFormula
strategy <- QM.pick arbitrary
let (cnf, info) = pb2satWith strategy opb
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
ret1 <- QM.run $ solvePBFormula solver1 opb
ret2 <- QM.run $ solveCNF solver2 cnf
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just m1 -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, CNF.cnfNumVars cnf)
QM.assert $ evalCNF m2 cnf
case ret2 of
Nothing -> return ()
Just m2 -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, PBFile.pbNumVars opb)
QM.assert $ isJust $ SAT.evalPBFormula m1 opb
prop_pb2sat_json :: Property
prop_pb2sat_json =
forAll arbitraryPBFormula $ \opb ->
forAll arbitrary $ \strategy ->
let ret@(_, info) = pb2satWith strategy opb
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_wbo2maxsat :: Property
prop_wbo2maxsat = QM.monadicIO $ do
wbo <- QM.pick arbitraryPBSoftFormula
let (wcnf, info) = wbo2maxsat wbo
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
method <- QM.pick arbitrary
ret1 <- QM.run $ optimizePBSoftFormula solver1 method wbo
ret2 <- QM.run $ optimizeWCNF solver2 method wcnf
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just (m1,val) -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, CNF.wcnfNumVars wcnf)
QM.assert $ evalWCNF m2 wcnf == Just (transformObjValueForward info val)
case ret2 of
Nothing -> return ()
Just (m2,val) -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, PBFile.wboNumVars wbo)
QM.assert $ SAT.evalPBSoftFormula m1 wbo == Just (transformObjValueBackward info val)
prop_wbo2maxsat_json :: Property
prop_wbo2maxsat_json =
forAll arbitraryPBSoftFormula $ \wbo ->
let ret@(_, info) = wbo2maxsat wbo
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_pb2wbo :: Property
prop_pb2wbo = QM.monadicIO $ do
opb <- QM.pick arbitraryPBFormula
let (wbo, info) = pb2wbo opb
QM.monitor $ counterexample (show wbo)
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
method <- QM.pick arbitrary
ret1 <- QM.run $ optimizePBFormula solver2 method opb
ret2 <- QM.run $ optimizePBSoftFormula solver1 method wbo
QM.monitor $ counterexample (show ret1)
QM.monitor $ counterexample (show ret2)
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just (m1,val1) -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, PBFile.wboNumVars wbo)
QM.assert $ SAT.evalPBSoftFormula m2 wbo == Just (transformObjValueForward info val1)
case ret2 of
Nothing -> return ()
Just (m2,val2) -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, PBFile.wboNumVars wbo)
QM.assert $ SAT.evalPBFormula m1 opb == Just (transformObjValueBackward info val2)
prop_pb2wbo_json :: Property
prop_pb2wbo_json =
forAll arbitraryPBFormula $ \opb ->
let ret@(_, info) = pb2wbo opb
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_wbo2pb :: Property
prop_wbo2pb = QM.monadicIO $ do
wbo <- QM.pick arbitraryPBSoftFormula
let (opb, info) = wbo2pb wbo
QM.monitor $ counterexample (show opb)
-- no constant terms in objective function
QM.assert $ all (\(_,ls) -> length ls > 0) $ fromMaybe [] (PBFile.pbObjectiveFunction opb)
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
method <- QM.pick arbitrary
ret1 <- QM.run $ optimizePBSoftFormula solver1 method wbo
ret2 <- QM.run $ optimizePBFormula solver2 method opb
QM.monitor $ counterexample (show ret1)
QM.monitor $ counterexample (show ret2)
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just (m1,val1) -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, PBFile.pbNumVars opb)
QM.assert $ SAT.evalPBFormula m2 opb == Just (transformObjValueForward info val1)
case ret2 of
Nothing -> return ()
Just (m2,val2) -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, PBFile.wboNumVars wbo)
QM.assert $ SAT.evalPBSoftFormula m1 wbo == Just (transformObjValueBackward info val2)
prop_wbo2pb_json :: Property
prop_wbo2pb_json =
forAll arbitraryPBSoftFormula $ \wbo ->
let ret@(_, info) = wbo2pb wbo
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_sat2ksat :: Property
prop_sat2ksat = QM.monadicIO $ do
k <- QM.pick $ choose (3,10)
cnf1 <- QM.pick arbitraryCNF
let (cnf2, info) = sat2ksat k cnf1
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
ret1 <- QM.run $ solveCNF solver1 cnf1
ret2 <- QM.run $ solveCNF solver2 cnf2
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just m1 -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, CNF.cnfNumVars cnf2)
QM.assert $ evalCNF m2 cnf2
case ret2 of
Nothing -> return ()
Just m2 -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, CNF.cnfNumVars cnf1)
QM.assert $ evalCNF m1 cnf1
prop_sat2ksat_json :: Property
prop_sat2ksat_json =
forAll (choose (3,10)) $ \k ->
forAll arbitraryCNF $ \cnf1 ->
let ret@(_, info) = sat2ksat k cnf1
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_linearizePB_forward :: Property
prop_linearizePB_forward =
forAll arbitraryPBFormula $ \pb ->
forAll arbitrary $ \b ->
let ret@(pb2, info) = linearizePB pb b
in counterexample (show ret) $
forAllAssignments (PBFile.pbNumVars pb) $ \m ->
fmap (transformObjValueForward info) (SAT.evalPBFormula m pb) === SAT.evalPBFormula (transformForward info m) pb2
prop_linearizePB_backward :: Property
prop_linearizePB_backward =
forAll arbitraryPBFormula $ \pb ->
forAll arbitrary $ \b ->
let ret@(pb2, info) = linearizePB pb b
in counterexample (show ret) $
forAll (arbitraryAssignment (PBFile.pbNumVars pb2)) $ \m2 ->
case (SAT.evalPBFormula (transformBackward info m2) pb, SAT.evalPBFormula m2 pb2) of
pair@(Just val1, Just val2) -> counterexample (show pair) $ val1 <= transformObjValueBackward info val2
pair@(Nothing, Just _) -> counterexample (show pair) $ False
(_, Nothing) -> property True
prop_linearizePB_json :: Property
prop_linearizePB_json =
forAll arbitraryPBFormula $ \pb ->
forAll arbitrary $ \b ->
let ret@(_, info) = linearizePB pb b
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_linearizeWBO_forward :: Property
prop_linearizeWBO_forward =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(wbo2, info) = linearizeWBO wbo b
in counterexample (show ret) $
forAllAssignments (PBFile.wboNumVars wbo) $ \m ->
fmap (transformObjValueForward info) (SAT.evalPBSoftFormula m wbo) === SAT.evalPBSoftFormula (transformForward info m) wbo2
prop_linearizeWBO_backward :: Property
prop_linearizeWBO_backward =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(wbo2, info) = linearizeWBO wbo b
in counterexample (show ret) $
forAll (arbitraryAssignment (PBFile.wboNumVars wbo2)) $ \m2 ->
case (SAT.evalPBSoftFormula (transformBackward info m2) wbo, SAT.evalPBSoftFormula m2 wbo2) of
pair@(Just val1, Just val2) -> counterexample (show pair) $ val1 <= transformObjValueBackward info val2
pair@(Nothing, Just _) -> counterexample (show pair) $ False
(_, Nothing) -> property True
prop_linearizeWBO_json :: Property
prop_linearizeWBO_json =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(_, info) = linearizeWBO wbo b
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_quadratizePB :: Property
prop_quadratizePB =
forAll arbitraryPBFormula $ \pb ->
let ((pb2,th), info) = quadratizePB pb
in counterexample (show (pb2,th)) $
conjoin
[ property $ F.all (\t -> IntSet.size t <= 2) $ collectTerms pb2
, property $ PBFile.pbNumConstraints pb === PBFile.pbNumConstraints pb2
, forAll (arbitraryAssignment (PBFile.pbNumVars pb)) $ \m ->
fmap (transformObjValueForward info) (SAT.evalPBFormula m pb) === eval2 (transformForward info m) (pb2,th)
, forAll (arbitraryAssignment (PBFile.pbNumVars pb2)) $ \m ->
case eval2 m (pb2,th) of
Just o -> SAT.evalPBFormula (transformBackward info m) pb === Just (transformObjValueBackward info o)
Nothing -> property True
]
where
collectTerms :: PBFile.Formula -> Set IntSet
collectTerms formula = Set.fromList [t' | t <- terms, let t' = IntSet.fromList t, IntSet.size t' >= 3]
where
sums = maybeToList (PBFile.pbObjectiveFunction formula) ++
[lhs | (lhs,_,_) <- PBFile.pbConstraints formula]
terms = [t | s <- sums, (_,t) <- s]
eval2 :: SAT.IModel m => m -> (PBFile.Formula, Integer) -> Maybe Integer
eval2 m (pb,th) = do
o <- SAT.evalPBFormula m pb
guard $ o <= th
return o
prop_quadratizePB_json :: Property
prop_quadratizePB_json =
forAll arbitraryPBFormula $ \pb ->
let ret@(_, info) = quadratizePB pb
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_inequalitiesToEqualitiesPB :: Property
prop_inequalitiesToEqualitiesPB = QM.monadicIO $ do
opb <- QM.pick arbitraryPBFormula
let (opb2, info) = inequalitiesToEqualitiesPB opb
solver1 <- arbitrarySolver
solver2 <- arbitrarySolver
ret1 <- QM.run $ solvePBFormula solver1 opb
ret2 <- QM.run $ solvePBFormula solver2 opb2
QM.assert $ isJust ret1 == isJust ret2
case ret1 of
Nothing -> return ()
Just m1 -> do
let m2 = transformForward info m1
QM.assert $ bounds m2 == (1, PBFile.pbNumVars opb2)
QM.assert $ isJust $ SAT.evalPBFormula m2 opb2
case ret2 of
Nothing -> return ()
Just m2 -> do
let m1 = transformBackward info m2
QM.assert $ bounds m1 == (1, PBFile.pbNumVars opb)
QM.assert $ isJust $ SAT.evalPBFormula m1 opb
prop_inequalitiesToEqualitiesPB_json :: Property
prop_inequalitiesToEqualitiesPB_json = forAll arbitraryPBFormula $ \opb ->
let ret@(_, info) = inequalitiesToEqualitiesPB opb
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json == Right info
------------------------------------------------------------------------
prop_pb2ip_forward :: Property
prop_pb2ip_forward =
forAll arbitraryPBFormula $ \pb ->
let ret@(mip, info) = pb2ip pb
in counterexample (show ret) $
forAll (arbitraryAssignment (PBFile.pbNumVars pb)) $ \m ->
fmap (transformObjValueForward info) (SAT.evalPBFormula m pb)
===
evalMIP (transformForward info m) (fmap fromIntegral mip)
prop_pb2ip_backward :: Property
prop_pb2ip_backward =
forAll arbitraryPBFormula $ \pb ->
let ret@(mip, info) = pb2ip pb
in counterexample (show ret) $
forAll (arbitraryAssignmentBinaryIP mip) $ \sol ->
SAT.evalPBFormula (transformBackward info sol) pb
===
fmap (transformObjValueBackward info) (evalMIP sol (fmap fromIntegral mip))
prop_pb2ip_json :: Property
prop_pb2ip_json =
forAll arbitraryPBFormula $ \pb ->
let ret@(_, info) = pb2ip pb
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_wbo2ip_forward :: Property
prop_wbo2ip_forward =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(mip, info) = wbo2ip b wbo
in counterexample (show ret) $
forAll (arbitraryAssignment (PBFile.wboNumVars wbo)) $ \m ->
fmap (transformObjValueForward info) (SAT.evalPBSoftFormula m wbo)
===
evalMIP (transformForward info m) (fmap fromIntegral mip)
prop_wbo2ip_backward :: Property
prop_wbo2ip_backward =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(mip, info) = wbo2ip b wbo
in counterexample (show ret) $
forAll (arbitraryAssignmentBinaryIP mip) $ \sol ->
case evalMIP sol (fmap fromIntegral mip) of
Nothing -> True
Just val2 ->
case SAT.evalPBSoftFormula (transformBackward info sol) wbo of
Nothing -> False
Just val1 -> val1 <= transformObjValueBackward info val2
prop_wbo2ip_json :: Property
prop_wbo2ip_json =
forAll arbitraryPBSoftFormula $ \wbo ->
forAll arbitrary $ \b ->
let ret@(_, info) = wbo2ip b wbo
json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
prop_ip2pb_forward :: Property
prop_ip2pb_forward =
forAll arbitraryBoundedIP $ \ip ->
case ip2pb ip of
Left err -> counterexample err $ property False
Right ret@(pb, info) ->
counterexample (show ret) $
forAll (arbitraryAssignmentBoundedIP ip) $ \sol ->
fmap (transformObjValueForward info) (evalMIP sol ip)
===
SAT.evalPBFormula (transformForward info sol) pb
prop_ip2pb_backward :: Property
prop_ip2pb_backward =
forAll arbitraryBoundedIP $ \ip ->
case ip2pb ip of
Left err -> counterexample err $ property False
Right ret@(pb, info) ->
counterexample (show ret) $
forAll (arbitraryAssignment (PBFile.pbNumVars pb)) $ \m ->
case SAT.evalPBFormula m pb of
Nothing -> property True
Just val -> evalMIP (transformBackward info m) ip === Just (transformObjValueBackward info val)
prop_ip2pb_backward' :: Property
prop_ip2pb_backward' =
forAll arbitraryBoundedIP $ \ip ->
case ip2pb ip of
Left err -> counterexample err $ property False
Right ret@(pb, info) ->
counterexample (show ret) $
QM.monadicIO $ do
solver <- arbitrarySolver
-- Using optimizePBFormula is too slow for using in QuickCheck
ret2 <- QM.run $ solvePBFormula solver pb
case ret2 of
Nothing -> return ()
Just m -> QM.assert $ isJust $ evalMIP (transformBackward info m) ip
prop_ip2pb_json :: Property
prop_ip2pb_json =
forAll arbitraryBoundedIP $ \ip ->
case ip2pb ip of
Left err -> counterexample err $ property False
Right ret@(_, info) ->
let json = J.encode info
in counterexample (show ret) $ counterexample (show json) $
J.eitherDecode json === Right info
arbitraryBoundedIP :: Gen (MIP.Problem Rational)
arbitraryBoundedIP = do
nv <- choose (0,10)
bs <- liftM Map.fromList $ forM [0..nv-1] $ \(i :: Int) -> do
let v = fromString ("z" ++ show i)
b <- arbitrary
if b then
pure (v, (MIP.Finite 0, MIP.Finite 1))
else do
lb <- arbitrary
NonNegative w <- arbitrary
let ub = fromInteger (ceiling lb) + w
return (v, (MIP.Finite lb, MIP.Finite ub))
let vs = Map.keys bs
vs_bin = [v | (v, (MIP.Finite 0, MIP.Finite 1)) <- Map.toList bs]
dir <- elements [MIP.OptMin, MIP.OptMax]
obj <- arbitraryMIPExpr vs
nc <- choose (0,3)
cs <- replicateM nc $ do
ind <-
if null vs_bin then
pure Nothing
else do
b <- arbitrary
if b then
pure Nothing
else do
v <- elements vs_bin
rhs <- elements [0, 1]
pure $ Just (v, rhs)
e <- arbitraryMIPExpr vs
lb <- oneof [pure MIP.NegInf, MIP.Finite <$> arbitrary, pure MIP.PosInf]
ub <- oneof $ [pure MIP.NegInf, MIP.Finite <$> arbitrary, pure MIP.PosInf] ++ [pure lb | case lb of{ MIP.Finite _ -> True; _ -> False }]
isLazy <- arbitrary
return $ MIP.def
{ MIP.constrIndicator = ind
, MIP.constrExpr = e
, MIP.constrLB = lb
, MIP.constrUB = ub
, MIP.constrIsLazy = isLazy
}
sos <-
if length vs == 0 then
pure []
else do
n <- choose (0, 1)
replicateM n $ do
t <- elements [MIP.S1, MIP.S2]
m <- choose (0, length vs `div` 2)
xs <- liftM (take m) $ shuffle vs
ns <- shuffle (map fromIntegral [0 .. length xs - 1])
pure (MIP.SOSConstraint{ MIP.sosLabel = Nothing, MIP.sosType = t, MIP.sosBody = zip xs ns })
return $ MIP.def
{ MIP.objectiveFunction = MIP.def{ MIP.objDir = dir, MIP.objExpr = obj }
, MIP.varDomains = fmap (\b -> (MIP.IntegerVariable, b)) bs
, MIP.constraints = cs
, MIP.sosConstraints = sos
}
arbitraryMIPExpr :: [MIP.Var] -> Gen (MIP.Expr Rational)
arbitraryMIPExpr vs = do
let nv = length vs
nt <- choose (0,3)
liftM MIP.Expr $ replicateM nt $ do
ls <-
if nv==0
then return []
else do
m <- choose (0,2)
replicateM m (elements vs)
c <- arbitrary
return $ MIP.Term c ls
arbitraryAssignmentBinaryIP :: MIP.Problem a -> Gen (Map MIP.Var Rational)
arbitraryAssignmentBinaryIP mip = liftM Map.fromList $ do
forM (Map.keys (MIP.varTypes mip)) $ \v -> do
val <- choose (0, 1)
pure (v, fromInteger val)
arbitraryAssignmentBoundedIP :: RealFrac a => MIP.Problem a -> Gen (Map MIP.Var Rational)
arbitraryAssignmentBoundedIP mip = liftM Map.fromList $ do
forM (Map.toList (MIP.varBounds mip)) $ \case
(v, (MIP.Finite lb, MIP.Finite ub)) -> do
val <- choose (ceiling lb, floor ub)
pure (v, fromInteger val)
_ -> error "should not happen"
evalMIP :: Map MIP.Var Rational -> MIP.Problem Rational -> Maybe Rational
evalMIP = MIP.eval MIP.zeroTol
------------------------------------------------------------------------
converterTestGroup :: TestTree
converterTestGroup = $(testGroupGenerator)