From 58ca00207de30c231b8ee0d0718e9c535c63261b Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Fri, 13 Dec 2024 08:35:02 +0900 Subject: [PATCH] add test cases for linearizeWBO --- test/Test/Converter.hs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/test/Test/Converter.hs b/test/Test/Converter.hs index 2429a592..6e368012 100644 --- a/test/Test/Converter.hs +++ b/test/Test/Converter.hs @@ -665,6 +665,36 @@ prop_linearizePB_json = 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 -> + 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 -> + if isJust (SAT.evalPBSoftFormula m2 wbo2) then + isJust (SAT.evalPBSoftFormula (transformBackward info m2) wbo) + else + 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 ->