7c4b45011ca12526ec6438c0459ff75ffe106e26Christian Maeder{- |

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescu test module similar to GUI_tests, but tests CMDL functions

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescu-}

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescumodule Main where

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescu

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport Interfaces.GenericATPState

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport qualified Logic.Prover as LProver

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescu

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport SoftFOL.Sign

180e4a3b6c3d466a44f6e01d1eb611dc13fdb0c5Corneliu-Claudiu Prodescuimport SoftFOL.ProveSPASS

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport SoftFOL.ProveVampire

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport SoftFOL.ProveMathServ

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport SoftFOL.ProveDarwin

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescu

651b65d88715480a474041557bee863ea8b10fbaCorneliu-Claudiu Prodescuimport System.IO (stdout, hSetBuffering, BufferMode(NoBuffering))

7c4b45011ca12526ec6438c0459ff75ffe106e26Christian Maederimport System.Environment (getArgs)

7c4b45011ca12526ec6438c0459ff75ffe106e26Christian Maederimport System.Exit

7c4b45011ca12526ec6438c0459ff75ffe106e26Christian Maeder

00fd29f7901da09a256b431aa3a7d2f844658c7eChristian Maederimport Common.AS_Annotation

c7cf09ae27e389e401f2532c87656121e9f1d0a5Christian Maederimport Common.Id

d529781ea5bd4e2c934f9b8d4c74406864ffd8d4Christian Maederimport Common.ProofTree

00fd29f7901da09a256b431aa3a7d2f844658c7eChristian Maederimport Common.Result

00fd29f7901da09a256b431aa3a7d2f844658c7eChristian Maeder

092300709012b3bd88bf22c38fa50115115470b4Christian Maederimport qualified Data.Set as Set

b4fb21fff7d47eb6a57aadd6f58aeb7cb72808baChristian Maederimport qualified Data.Map as Map

76401eac18c41270987ffe3e774d65665bfd0dd7Christian Maederimport qualified Control.Concurrent as Concurrent

ddeca6263879fce60a36ea00492ed1c8e1fc331fChristian Maederimport Control.Monad

f161f9015db69629c035851e94380fec712598c2Corneliu-Claudiu Prodescu

f161f9015db69629c035851e94380fec712598c2Corneliu-Claudiu Prodescu-- * Definitions of test theories

76401eac18c41270987ffe3e774d65665bfd0dd7Christian Maeder

ddeca6263879fce60a36ea00492ed1c8e1fc331fChristian Maedersign1 :: SoftFOL.Sign.Sign

820ea965b34b93faf555c668a55bccb232b709e0Christian Maedersign1 = emptySign

b4fb21fff7d47eb6a57aadd6f58aeb7cb72808baChristian Maeder { sortMap = Map.insert (mkSimpleId "s") Nothing Map.empty

961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner , predMap = Map.fromList (map (\ (x,y) ->

b4fb21fff7d47eb6a57aadd6f58aeb7cb72808baChristian Maeder (mkSimpleId x, Set.singleton $ map mkSimpleId y))

b4fb21fff7d47eb6a57aadd6f58aeb7cb72808baChristian Maeder [("p",["s"]),("q",["s"]),("r",["s"]),("a",["s"])])}

820ea965b34b93faf555c668a55bccb232b709e0Christian Maeder

b4fb21fff7d47eb6a57aadd6f58aeb7cb72808baChristian Maederterm_x :: SPTerm

term_x = simpTerm (mkSPCustomSymbol "X")

axiom1 :: Named SPTerm

axiom1 = makeNamed "ax" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPEquiv [SPComplexTerm (mkSPCustomSymbol "p") [term_x],SPComplexTerm (mkSPCustomSymbol "q") [term_x]]))

axiom2 :: Named SPTerm

axiom2 = makeNamed "ax2" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x],SPComplexTerm (mkSPCustomSymbol "r") [term_x]]))

axiom3 :: Named SPTerm

axiom3 = makeNamed "b$$-3" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x],SPComplexTerm (mkSPCustomSymbol "a") [term_x]]))

goal1 :: Named SPTerm

goal1 = (makeNamed "go" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x],SPComplexTerm (mkSPCustomSymbol "p") [term_x] ])) { isAxiom = False }

goal2 :: Named SPTerm

goal2 = (makeNamed "go2" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "p") [term_x],SPComplexTerm (mkSPCustomSymbol "r") [term_x] ])) { isAxiom = False }

goal3 :: Named SPTerm

goal3 = (makeNamed "go3" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "p") [term_x],SPComplexTerm (mkSPCustomSymbol "a") [term_x] ])) { isAxiom = False }

theory1 :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theory1 = (LProver.Theory sign1 $ LProver.toThSens [axiom1,-- axiom2,

goal1,goal2])

theory2 :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theory2 = (LProver.Theory sign1 $ LProver.toThSens [axiom1,axiom2,axiom3,

goal1,goal2,goal3])

-- A more complicated theory including ExtPartialOrder from Basic/RelationsAndOrders.casl

signExt :: SoftFOL.Sign.Sign

signExt = emptySign {sortMap = {- Map.insert "Elem" Nothing -} Map.empty,

funcMap = Map.fromList (map (\ (x, (y, z)) -> (mkSimpleId x,

Set.singleton (map mkSimpleId y, mkSimpleId z)))

[("gn_bottom",([],"Elem")),

("inf",(["Elem", "Elem"],"Elem")),

("sup",(["Elem", "Elem"],"Elem"))]),

predMap = Map.fromList (map (\ (x,y) -> (mkSimpleId x,

Set.singleton $ map mkSimpleId y))

[ ("gn_defined",["Elem"]),

("p__LtEq__",["Elem", "Elem"])] )}

ga_nonEmpty :: Named SPTerm

ga_nonEmpty = makeNamed "ga_nonEmpty" SPQuantTerm {quantSym = SPExists, variableList = [simpTerm (mkSPCustomSymbol "X")], qFormula = SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}}

ga_notDefBottom :: Named SPTerm

ga_notDefBottom = makeNamed "ga_notDefBottom" SPComplexTerm {symbol = SPNot, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_bottom", arguments = []}]}]}

ga_strictness :: Named SPTerm

ga_strictness = makeNamed "ga_strictness" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")]}]},SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

ga_strictness_one :: Named SPTerm

ga_strictness_one = makeNamed "ga_strictness_one" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")]}]},SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

ga_predicate_strictness :: Named SPTerm

ga_predicate_strictness = makeNamed "ga_predicate_strictness" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X_one"),simpTerm (mkSPCustomSymbol "X_two")]},SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

antisym :: Named SPTerm

antisym = makeNamed "antisym" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "X")]}]},SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]}]}]}}

trans :: Named SPTerm

trans = makeNamed "trans" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]},SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "Z")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Z")]}]}]}}

refl :: Named SPTerm

refl = makeNamed "refl" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "X")]}]}}

inf_def_ExtPartialOrder :: Named SPTerm

inf_def_ExtPartialOrder = makeNamed "inf_def_ExtPartialOrder" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]},SPComplexTerm {symbol = SPEquiv, arguments = [SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},simpTerm (mkSPCustomSymbol "Z")]},SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"),simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"),simpTerm (mkSPCustomSymbol "Y")]}]},SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "T")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "T")]},SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"),simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"),simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"),simpTerm (mkSPCustomSymbol "Z")]}]}]}}]}]}]}}

sup_def_ExtPartialOrder :: Named SPTerm

sup_def_ExtPartialOrder = makeNamed "sup_def_ExtPartialOrder" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]},SPComplexTerm {symbol = SPEquiv, arguments = [SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},simpTerm (mkSPCustomSymbol "Z")]},SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Z")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "Z")]}]},SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "T")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "T")]},SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "T")]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "T")]}]},SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"),simpTerm (mkSPCustomSymbol "T")]}]}]}}]}]}]}}

ga_comm_sup :: Named SPTerm

ga_comm_sup = (makeNamed "ga_comm_sup" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "X")]}]}]}}) { isAxiom = False }

ga_comm_inf :: Named SPTerm

ga_comm_inf = (makeNamed "ga_comm_inf" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]},SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]},SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X"),simpTerm (mkSPCustomSymbol "Y")]},SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "Y"),simpTerm (mkSPCustomSymbol "X")]}]}]}}) { isAxiom = False }

gone :: Named SPTerm

gone = (makeNamed "gone" $ simpTerm SPTrue) { isAxiom = False }

theoryExt :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theoryExt = (LProver.Theory signExt $ LProver.toThSens [ga_nonEmpty, ga_notDefBottom, ga_strictness, ga_strictness_one, ga_predicate_strictness, antisym, trans, refl, inf_def_ExtPartialOrder, sup_def_ExtPartialOrder, gone, ga_comm_sup, ga_comm_inf])

-- * Testing functions

main :: IO ()

main = do

args <- getArgs

hSetBuffering stdout NoBuffering

if null args

then runAllTests

else case args of

["batch"] -> runBatchTests

_ -> runMathServTest

exitOnBool :: Bool -> IO ()

exitOnBool b = if b

then exitWith ExitSuccess

else exitWith (ExitFailure 9)

runBatchTests :: IO ()

runBatchTests =

sequence

[runTestBatch2 True Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved Nothing))

,runTestBatch2 True Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved (Just True)))

,runTestBatch2 True Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved Nothing))

,runTestBatch2 True (Just 12) spassProveCMDLautomaticBatch "SPASS"

"[Test]ExtPartialOrder" theoryExt

(("gone",LProver.Proved Nothing) :

zip ["ga_comm_inf","ga_comm_sup"] (repeat LProver.openGoalStatus))

,runTestBatch2 True (Just 12) darwinCMDLautomaticBatch "Darwin"

"[Test]ExtPartialOrder" theoryExt

(("gone", LProver.Proved (Just True)):

(zip ["ga_comm_sup"] (repeat LProver.openGoalStatus)))

,runTestBatch2 True (Just 20) vampireCMDLautomaticBatch "Vampire"

"[Test]ExtPartialOrder" theoryExt

(zip ["gone","ga_comm_sup"] (repeat LProver.openGoalStatus))

] >>= (exitOnBool . and)

runMathServTest :: IO ()

runMathServTest = do

pass1 <-

runTest mathServBrokerCMDLautomatic "MathServ" "[Test]Foo1" theory1

[("go",LProver.Proved Nothing)]

pass2 <-

runTest vampireCMDLautomatic "Vampire" "[Test]Foo1" theory1

[("go",LProver.Proved Nothing)]

exitOnBool (pass1 && pass2)

{- |

Main function doing all tests (combinations of theory and prover) in a row.

Outputs status lines with information whether test passed or failed.

-}

runAllTests :: IO ()

runAllTests = do

sequence

[runTest spassProveCMDLautomatic "SPASS" "[Test]Foo1" theory1

[("go",LProver.Proved Nothing)]

,runTest darwinCMDLautomatic "Darwin" "[Test]Foo1" theory1

[("go",LProver.Proved (Just True))]

,runTest vampireCMDLautomatic "Vampire" "[Test]Foo1" theory1

[("go",LProver.Proved Nothing)]

,runTest mathServBrokerCMDLautomatic "MathServ" "[Test]Foo1" theory1

[("go",LProver.Proved Nothing)]

,runTest spassProveCMDLautomatic "SPASS" "[Test]Foo2" theory2

[("go",LProver.Proved Nothing)]

,runTest darwinCMDLautomatic "Darwin" "[Test]Foo2" theory2

[("go",LProver.Proved (Just True))]

,runTest vampireCMDLautomatic "Vampire" "[Test]Foo2" theory2

[("go",LProver.Proved Nothing)]

,runTest mathServBrokerCMDLautomatic "MathServ" "[Test]Foo2" theory2

[("go",LProver.Proved Nothing)]

,runTest spassProveCMDLautomatic "SPASS" "[Test]ExtPartialOrder" theoryExt

[("gone",LProver.Proved Nothing)]

,runTest darwinCMDLautomatic "Darwin" "[Test]Foo2" theoryExt

[("gone",LProver.Proved (Just True))]

,runTest vampireCMDLautomatic "Vampire" "[Test]ExtPartialOrder" theoryExt

[("gone",LProver.openGoalStatus)]

,runTest mathServBrokerCMDLautomatic "MathServ"

"[Test]ExtPartialOrder" theoryExt

[("gone",LProver.Proved Nothing)]

,runTestBatch Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo1" theory1

[("go",LProver.Proved Nothing),

("go2",LProver.Disproved)]

,runTestBatch Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo1" theory1

[("go",LProver.Proved (Just True)),

("go2",LProver.Disproved)]

,runTestBatch Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo1" theory1

[("go",LProver.Proved Nothing),

("go2",LProver.Disproved)]

,runTestBatch Nothing mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]Foo1" theory1

[("go",LProver.Proved Nothing),

("go2",LProver.Disproved)]

,runTestBatch Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved Nothing))

,runTestBatch Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved (Just True)))

,runTestBatch Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved Nothing))

,runTestBatch Nothing mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]Foo2" theory2

(zip ["go","go2","go3"] $ repeat (LProver.Proved Nothing))

,runTestBatch (Just 12) spassProveCMDLautomaticBatch "SPASS"

"[Test]ExtPartialOrder" theoryExt

(("gone",LProver.Proved Nothing) :

zip ["ga_comm_inf","ga_comm_sup"] (repeat LProver.openGoalStatus))

,runTestBatch (Just 20) darwinCMDLautomaticBatch "Darwin"

"[Test]ExtPartialOrder" theoryExt

(("gone", LProver.Proved (Just True)):

(zip ["ga_comm_sup"] (repeat LProver.openGoalStatus)))

,runTestBatch (Just 20) vampireCMDLautomaticBatch "Vampire"

"[Test]ExtPartialOrder" theoryExt

(zip ["gone","ga_comm_sup"] (repeat LProver.openGoalStatus))

,runTestBatch (Just 25) mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]ExtPartialOrder" theoryExt

(("gone",LProver.Proved Nothing) :

zip ["ga_comm_inf","ga_comm_sup"] (repeat LProver.openGoalStatus))

] >>= (exitOnBool . and)

{- |

Runs a CMDL automatic function (given as parameter) over a given theory.

The result will be output as status message.

-}

runTest :: (String

-> LProver.Tactic_script

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Result ([LProver.Proof_status ProofTree]))

)

-> String -- ^ prover name for proof status in case of error

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String,LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTest runCMDLProver prName thName th expStatus = do

putStrLn $ "Trying " ++ thName ++ "(automatic) with prover " ++ prName ++ " ... "

putStrLn $ show $ ATPTactic_script { ts_timeLimit = 20, ts_extraOpts = [] }

m_result <- runCMDLProver

thName

(LProver.Tactic_script (show $ ATPTactic_script {

ts_timeLimit = 20, ts_extraOpts = [] }))

th []

stResult <- maybe (return [LProver.openProof_status ""

prName (ProofTree "")])

return (maybeResult m_result)

putStrLn $ if (succeeded stResult expStatus)

then "passed"

else ("failed\n"++ (unlines $ map show $ diags m_result))

return (succeeded stResult expStatus)

{- |

Runs a CMDL automatic batch function (given as parameter) over a given

theory. The result will be output as status message.

-}

runTestBatch :: Maybe Int -- ^ seconds to pass before thread will be killed

-> (Bool

-> Bool

-> Concurrent.MVar

(Result [LProver.Proof_status ProofTree])

-> String

-> LProver.Tactic_script

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Concurrent.ThreadId,Concurrent.MVar ())

)

-> String -- ^ prover name

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String,LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTestBatch waitsec runCMDLProver prName thName th expStatus =

runTestBatch2 False waitsec runCMDLProver prName thName th expStatus

{- |

Runs a CMDL automatic batch function (given as parameter) over a given

theory. The result will be output as status message.

-}

runTestBatch2 :: Bool -- ^ True means try to read intermediate results

-> Maybe Int -- ^ seconds to pass before thread will be killed

-> (Bool

-> Bool

-> Concurrent.MVar

(Result [LProver.Proof_status ProofTree])

-> String

-> LProver.Tactic_script

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Concurrent.ThreadId,Concurrent.MVar ())

)

-> String -- ^ prover name

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String,LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTestBatch2 intermRes waitsec runCMDLProver prName thName th expStatus = do

putStr $ "Trying " ++ thName ++ "(automaticBatch"++

(if intermRes then " reading intermediate results" else "")++

") with prover " ++ prName ++ " ... "

resultMVar <- if intermRes

then Concurrent.newEmptyMVar

else Concurrent.newMVar (return [])

(threadID, mvar) <- runCMDLProver

False False resultMVar thName

(LProver.Tactic_script (show $ ATPTactic_script {

ts_timeLimit = 10, ts_extraOpts = [] }))

th []

maybe (return ()) (\ ws -> do

Concurrent.threadDelay (ws*1000000)

Concurrent.killThread threadID) waitsec

(stResult,diaStr):: ([LProver.Proof_status ProofTree],String)

<- if intermRes

then do -- reading intermediate results

iResMV <- Concurrent.newMVar []

putStrLn ""

let isReady = do

mReady <- Concurrent.tryTakeMVar mvar

maybe (return True)

(const $ Concurrent.putMVar mvar () >> return False)

mReady

waitForEachResult = do

-- Concurrent.yield

mRes <- Concurrent.takeMVar resultMVar

oldRes <- Concurrent.takeMVar iResMV

putStrLn (unlines $ map show $ diags mRes)

newRes <- maybe (return [])

(mapM (\ res -> do

putStrLn $ "Proof status of goal \""++

LProver.goalName res++ "\": "++

show (LProver.goalStatus res)

return res))

(maybeResult mRes)

Concurrent.putMVar iResMV (oldRes++newRes)

isReady

-- external reader thread

Concurrent.forkIO (

foldM_ (\ run ac ->

if run then ac

else return False) True $

map (const waitForEachResult) expStatus)

-- wait for prover to complete

Concurrent.takeMVar mvar

mmRes <- Concurrent.tryTakeMVar resultMVar

mRes <- maybe (return $ return [])

(\mR -> do putStrLn (unlines $ map show $ diags mR)

return mR)

mmRes

res <- Concurrent.takeMVar iResMV

putStr "... "

return (res++maybe [] id (maybeResult mRes),"")

else do -- only read at the end of a batch run

Concurrent.takeMVar mvar

m_result <- Concurrent.takeMVar resultMVar

return ( maybe [] id (maybeResult m_result)

, (unlines $ map show $ diags m_result)++"\n"++ show m_result)

putStrLn $ if (succeeded stResult expStatus)

then "passed"

else ("failed\n" ++ diaStr)

return (succeeded stResult expStatus)

{- |

Checks if a prover run's result matches expected result.

-}

succeeded :: [LProver.Proof_status ProofTree]

-> [(String,LProver.GoalStatus)]

-> Bool

succeeded stResult expStatus =

(length stResult == length expStatus)

&& (foldl (\b givenRes -> maybe False (==(LProver.goalStatus givenRes))

(lookup (LProver.goalName givenRes)

expStatus)

&& b)

True stResult)