From dd1d3fca0a472d04862429e39ee9b9ba261a02e9 Mon Sep 17 00:00:00 2001 From: JoKurth <71062996+JoKurth@users.noreply.github.com> Date: Sat, 6 Jul 2024 19:19:40 +0200 Subject: [PATCH] implemented testing for sublogics in propositional --- Makefile | 4 +- Propositional/Makefile | 4 + Propositional/test/Makefile | 9 + Propositional/test/TestSublogics.hs | 251 ++++++++++++++++++++++++++++ Propositional/test/runcheck.sh | 13 ++ 5 files changed, 279 insertions(+), 2 deletions(-) create mode 100644 Propositional/Makefile create mode 100644 Propositional/test/Makefile create mode 100644 Propositional/test/TestSublogics.hs create mode 100755 Propositional/test/runcheck.sh diff --git a/Makefile b/Makefile index d050b25cfc..101a0ffc22 100755 --- a/Makefile +++ b/Makefile @@ -130,11 +130,11 @@ TESTTARGETFILES += Scratch.hs CASL/fromKif.hs CASL/capa.hs HasCASL/hacapa.hs \ Comorphisms/test/sublogicGraph.hs PGIP/ParseProofScript.hs \ Common/testxupdate.hs Common/testxpath.hs \ SoftFOL/dfg.hs Adl/adl.hs GUI/displayDependencyGraph.hs \ - OWL2/scripts/runTest.hs + OWL2/scripts/runTest.hs Propositional/test/TestSublogics.hs ### list of directories to run checks in TESTDIRS += Common CASL Fpl/test HasCASL test ExtModal/Tries \ - CommonLogic/TestData OWL2/tests + CommonLogic/TestData OWL2/tests Propositional/test hs_clean_files = Haskell/TiATC.hs Haskell/TiDecorateATC.hs \ Haskell/TiPropATC.hs Haskell/ATC_Haskell.der.hs diff --git a/Propositional/Makefile b/Propositional/Makefile new file mode 100644 index 0000000000..de2f3c083f --- /dev/null +++ b/Propositional/Makefile @@ -0,0 +1,4 @@ +# $Id$ + +%: + (cd test; $(MAKE) $@) diff --git a/Propositional/test/Makefile b/Propositional/test/Makefile new file mode 100644 index 0000000000..5dc751d13f --- /dev/null +++ b/Propositional/test/Makefile @@ -0,0 +1,9 @@ +# $Id$ + +.PHONY: check + +check: Propositional/test/TestSublogics + ./runcheck.sh + +%: + (cd ../..; $(MAKE) $@) diff --git a/Propositional/test/TestSublogics.hs b/Propositional/test/TestSublogics.hs new file mode 100644 index 0000000000..b59b1d5446 --- /dev/null +++ b/Propositional/test/TestSublogics.hs @@ -0,0 +1,251 @@ +module Main where + +import Propositional.AS_BASIC_Propositional +import Propositional.Sublogic +import qualified Common.Id as Id + +import qualified Data.Set as Set + +import Control.Monad (unless) +import System.Exit (exitFailure) + +import Debug.Trace + + +main :: IO () +main = do + let tests = [testPlain, testNNF, testCNF, testDNF, testCnfDnf, testHorn] + let testSuccess = and tests + unless testSuccess exitFailure + + +-- We use the same range and token for all tests because it does not matter for our results + +r :: Id.Range +r = Id.Range {Id.rangeToList = []} + +t :: Id.Token +t = Id.Token { + Id.tokStr = "", + Id.tokPos = r +} + + +testPlain :: Bool +testPlain = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip plainDesc $ map (Set.null . format . sl_form bottom) plain + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notPlainDesc $ map (not . Set.null . format . sl_form bottom) notPlain + + f1 = Negation (Disjunction [Predication t, Predication t] r) r + f1' = "Plain_f1: ¬(A ∨ B)" + f2 = Conjunction [f1, Negation (Predication t) r, f1] r + f2' = "Plain_f2: (¬(A ∨ B)) ∧ ¬C ∧ (¬(D ∨ E))" + f3 = Conjunction [Negation f1 r, f2] r + f3' = "Plain_f3: ¬(¬(A ∨ B)) ∧ ((¬(A ∨ B)) ∧ ¬C ∧ (¬(D ∨ E)))" + f4 = Implication (Negation (Predication t) r) (Predication t) r + f4' = "Plain_f4: ¬A -> B" + f5 = Equivalence f1 f2 r + f5' = "Plain_f5: (A ∨ B) <-> ()" + + f11 = Conjunction [Predication t, Predication t] r + f11' = "Plain_f11: A ∧ B" + f12 = Disjunction [Negation (Predication t) r, Predication t] r + f12' = "Plain_f12: ¬A ∨ B" + f13 = Predication t + f13' = "Plain_f13: A" + f14 = Conjunction [f11, f12, f11] r + f14' = "Plain_f14: (A ∧ B) ∧ (¬C ∨ D) ∧ (E ∧ F)" + f15 = True_atom r + f15' = "Plain_f15: True" + + plain = [f1, f2, f3, f4, f5] + plainDesc = [f1', f2', f3', f4', f5'] + notPlain = [f11, f12, f13, f14, f15] + notPlainDesc = [f11', f12', f13', f14', f15'] + +testNNF :: Bool +testNNF = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip nnfDesc $ map (isNNF . sl_form bottom) nnf + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notNnfDesc $ map (not . isNNF . sl_form bottom) notNnf + + f1 = Conjunction [Predication t, Predication t] r + f1' = "Nnf_f1: A ∧ B" + f2 = Disjunction [Negation (Predication t) r, Predication t] r + f2' = "Nnf_f1: ¬C ∨ D" + f3 = Predication t + f3' = "Nnf_f1: A" + f4 = Conjunction [f1, f2, f1] r + f4' = "Nnf_f1: (A ∧ B) ∧ (¬C ∨ D) ∧ (E ∧ F)" + f5 = True_atom r + f5' = "Nnf_f1: True" + + f11 = Negation (Disjunction [f2, f2] r) r + f11' = "Nnf_f11: ¬((¬A ∨ B) ∨ (¬C ∨ D))" + f12 = Conjunction [f1, Negation f2 r, f1] r + f12' = "Nnf_f12: (A ∧ B) ∧ ¬(C ∨ D) ∧ (A ∧ B)" + f13 = Conjunction [Negation f1 r, f2] r + f13' = "Nnf_f13: ¬(A ∧ B) ∧ (C ∨ D)" + f14 = Implication (Predication t) (Predication t) r + f14' = "Nnf_f14: A -> B" + f15 = Equivalence f1 f2 r + f15' = "Nnf_f15: A <-> B" + + nnf = [f1, f2, f3, f4, f5] + nnfDesc = [f1', f2', f3', f4', f5'] + notNnf = [f11, f12, f13, f14, f15] + notNnfDesc = [f11', f12', f13', f14', f15'] + +testCNF :: Bool +testCNF = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip cnfDesc $ map (isCNF . sl_form bottom) cnf + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notCnfDesc $ map (not . isCNF . sl_form bottom) notCnf + + f1 = Conjunction [Predication t, Predication t] r + f1' = "Cnf_f1: A ∧ B" + f2 = Disjunction [Negation (Predication t) r, Predication t] r + f2' = "Cnf_f1: ¬A ∨ B" + f3 = Predication t + f3' = "Cnf_f1: A" + f4 = Conjunction [f2, f2, f2] r + f4' = "Cnf_f1: (¬A ∨ B) ∧ (¬C ∨ D) ∧ (¬E ∨ F)" + f5 = True_atom r + f5' = "Cnf_f1: True" + + f11 = Disjunction [f2, f2] r + f11' = "Cnf_f1: (¬A ∨ B) ∨ (¬C ∨ D)" + f12 = Conjunction [f1, f1] r + f12' = "Cnf_f1: (A ∧ B) ∧ (C ∧ D)" + f13 = Conjunction [f1, f2] r + f13' = "Cnf_f1: (A ∧ B) ∧ (C ∨ D)" + f14 = Implication (Predication t) (Predication t) r + f14' = "Cnf_f1: A -> B" + f15 = Equivalence f1 f2 r + f15' = "Cnf_f1: A <-> B" + + cnf = [f1, f2, f3, f4, f5] + cnfDesc = [f1', f2', f3', f4', f5'] + notCnf = [f11, f12, f13, f14, f15] + notCnfDesc = [f11', f12', f13', f14', f15'] + +testDNF :: Bool +testDNF = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip dnfDesc $ map (isDNF . sl_form bottom) dnf + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notDnfDesc $ map (not . isDNF . sl_form bottom) notDnf + + f1 = Conjunction [Predication t, Predication t] r + f1' = "Dnf_f1: A ∧ B" + f2 = Disjunction [Negation (Predication t) r, Predication t] r + f2' = "Dnf_f2: ¬A ∨ B" + f3 = Predication t + f3' = "Dnf_f3: A" + f4 = Disjunction [f1, f1, f1] r + f4' = "Dnf_f4: (A ∧ B) ∨ (C ∧ D) ∨ (E ∧ F)" + f5 = True_atom r + f5' = "Dnf_f5: True" + + f11 = Conjunction [f2, f2] r + f11' = "Dnf_f11:(¬A ∨ B) ∧ (¬C ∨ D)" + f12 = Disjunction [f1, f2] r + f12' = "Dnf_f12: (A ∧ B) ∨ (¬C ∨ D)" + f13 = Conjunction [f1, f2] r + f13' = "Dnf_f13: (A ∧ B) ∧ (¬C ∨ D)" + f14 = Implication (Predication t) (Predication t) r + f14' = "Dnf_f14: A -> B" + f15 = Equivalence f1 f2 r + f15' = "Dnf_f15: A <-> B" + + dnf = [f1, f2, f3, f4, f5] + dnfDesc = [f1', f2', f3', f4', f5'] + notDnf = [f11, f12, f13, f14, f15] + notDnfDesc = [f11', f12', f13', f14', f15'] + +testCnfDnf :: Bool +testCnfDnf = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip cnfDnfDesc $ map ((\x -> isCNF x && isDNF x) . sl_form bottom) cnfDnf + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notCnfDnfDesc $ map ((\x -> not (isCNF x && isDNF x)) . sl_form bottom) notCnfDnf + + f1 = Conjunction [Predication t, Predication t] r + f1' = "CnfDnf_f1: A ∧ B" + f2 = Disjunction [Negation (Predication t) r, Predication t] r + f2' = "CnfDnf_f1: ¬A ∨ B" + f3 = Predication t + f3' = "CnfDnf_f1: A" + f4 = Negation (Predication t) r + f4' = "CnfDnf_f1: ¬A" + f5 = True_atom r + f5' = "CnfDnf_f1: True" + + f11 = Conjunction [f2, f2] r + f11' = "CnfDnf_f11: (¬A ∨ B) ∧ (¬C ∨ D)" + f12 = Disjunction [f1, f1] r + f12' = "CnfDnf_f12: (A ∧ B) ∨ (C ∧ D)" + f13 = Conjunction [f1, f2] r + f13' = "CnfDnf_f13: (A ∧ B) ∧ (¬C ∨ D)" + f14 = Implication (Predication t) (Predication t) r + f14' = "CnfDnf_f14: A -> B" + f15 = Equivalence f1 f2 r + f15' = "CnfDnf_f15: A <-> B" + + cnfDnf = [f1, f2, f3, f4, f5] + cnfDnfDesc = [f1', f2', f3', f4', f5'] + notCnfDnf = [f11, f12, f13, f14, f15] + notCnfDnfDesc = [f11', f12', f13', f14', f15'] + +testHorn :: Bool +testHorn = testPos && testNeg + where + testPos = all (\x -> printIfFailed (snd x) (fst x)) $ zip hornDesc $ map (isHC . sl_form bottom) hornFormulas + testNeg = all (\x -> printIfFailed (snd x) (fst x)) $ zip notHornDesc $ map (not . isHC . sl_form bottom) notHornFormulas + + f1 = Implication (Predication t) (Predication t) r + f1' = "Horn_f1: A -> B" + f2 = Implication (Conjunction [Predication t, Predication t, Predication t, True_atom r] r) (Predication t) r + f2' = "Horn_f2: (A ∧ B ∧ C ∧ True) -> D" + f3 = True_atom r + f3' = "Horn_f3: True" + f4 = Negation (Predication t) r + f4' = "Horn_f4: ¬A" + f5 = Conjunction [f1, f2] r + f5' = "Horn_f5: (A -> B) ∧ ((C ∧ D ∧ E ∧ True) -> F)" + f6 = Conjunction [Disjunction [Negation (Predication t) r, Predication t] r] r + f6' = "Horn_f6: ∧(¬A ∨ B)" + f7 = Conjunction [Disjunction [Negation (Predication t) r, Negation (Predication t) r] r] r + f7' = "Horn_f7: ∧(¬A ∨ ¬B)" + f8 = Conjunction [Disjunction [Negation (Predication t) r, Negation (Predication t) r, Negation (Predication t) r, Negation (Predication t) r, Predication t] r, Disjunction [Negation (Predication t) r, Predication t] r, f1] r + f8' = "Horn_f8: (¬A ∨ ¬B ∨ ¬C ∨ ¬D ∨ E) ∧ (¬F ∨ G) ∧ (H -> I)" + f9 = Disjunction [Negation (Predication t) r, Negation (Predication t) r, Negation (Predication t) r, Negation (Predication t) r, Predication t] r + f9' = "Horn_f9: ¬A ∨ ¬B ∨ ¬C ∨ ¬D ∨ E" + + f11 = Implication (Disjunction [Predication t, Predication t] r) (Predication t) r + f11' = "Horn_f11: (A ∨ B) -> C" + f12 = Implication (Conjunction [Predication t, Negation (Predication t) r, Predication t, True_atom r] r) (Predication t) r + f12' = "Horn_f12: (A ∧ ¬B ∧ C ∧ True) -> D" + f13 = Disjunction [True_atom r, False_atom r] r + f13' = "Horn_f13: True ∨ False" + f14 = Conjunction [f11, f2] r + f14' = "Horn_f14: ((A ∨ G) -> B) ∧ ((C ∧ D ∧ E ∧ True) -> F)" + f15 = Conjunction [Disjunction [Predication t, Predication t] r] r + f15' = "Horn_f15: ∧(A ∨ B)" + f16 = Conjunction [Disjunction [Predication t, Predication t, Negation (Predication t) r, Negation (Predication t) r, Predication t] r, Disjunction [Negation (Predication t) r, Predication t] r, f1] r + f16' = "Horn_f16: (A ∨ B ∨ ¬C ∨ ¬D ∨ E) ∧ (¬F ∨ G) ∧ (H -> I)" + f17 = Disjunction [Negation (Predication t) r, Negation (Predication t) r, Negation (Predication t) r, Predication t, Predication t] r + f17' = "Horn_f17: ¬A ∨ ¬B ∨ ¬C ∨ D ∨ E" + + hornFormulas = [f1, f2, f3, f4, f5, f6, f7, f8, f9] + hornDesc = [f1', f2', f3', f4', f5', f6', f7', f8', f9'] + notHornFormulas = [f11, f12, f13, f14, f15, f16, f17] + notHornDesc = [f11', f12', f13', f14', f15', f16', f17'] + + +-- helper + +printIfFailed :: Bool -> String -> Bool +printIfFailed correct desc = + if not correct + then trace ("failed in test for: " ++ desc) correct + else correct diff --git a/Propositional/test/runcheck.sh b/Propositional/test/runcheck.sh new file mode 100755 index 0000000000..349b2653fd --- /dev/null +++ b/Propositional/test/runcheck.sh @@ -0,0 +1,13 @@ +#!/bin/ksh93 + +#first parameter is executable +#second parameter resets ouput files + +SD=$( cd ${ dirname $0; }; printf "$PWD" ) +BD=${SD%/*/*} + +. ${BD}/Common/test/checkFunctions.sh + +./TestSublogic || addErr + +(( ! ERR ))