Skip to content
Snippets Groups Projects
Commit f71032c3 authored by Thorsten Wißmann's avatar Thorsten Wißmann
Browse files

Add smallest DL98 testcases to testsuite

parent 7fe1f7bb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/testsuite/DL98TestCases.ml 0 → 100644
+ 61
− 0
View file @ f71032c3
open Testsuite
let satCasesString =
"
(~(~(((P100)&(~(P101)))&((((((P100)|(~(P101)))&((P101)|(~(P102))))&((((([R1]((P0)|(~(P100))))|(~(P0)))&(([R1]((~(P0))|(~(P100))))|(~(~(P0)))))|(~(P100)))&(((([R1]((P1)|(~(P101))))|(~(P1)))&(([R1]((~(P1))|(~(P101))))|(~(~(P1)))))|(~(P101)))))&(((<R1>(((P101)&(~(P102)))&(P1)))&(<R1>(((P101)&(~(P102)))&(~(P1)))))|(~((P100)&(~(P101))))))&([R1](((((P100)|(~(P101)))&((P101)|(~(P102))))&((((([R1]((P0)|(~(P100))))|(~(P0)))&(([R1]((~(P0))|(~(P100))))|(~(~(P0)))))|(~(P100)))&(((([R1]((P1)|(~(P101))))|(~(P1)))&(([R1]((~(P1))|(~(P101))))|(~(~(P1)))))|(~(P101)))))&(((<R1>(((P101)&(~(P102)))&(P1)))&(<R1>(((P101)&(~(P102)))&(~(P1)))))|(~((P100)&(~(P101)))))))))))
(~((((((([R1](([R1](P0))|([R1](<R1>(~(P0))))))|(<R1>([R1](False))))|(<R1>(([R1](P0))&(<R1>(<R1>(~(P0)))))))|(<R1>(([R1](<R1>(P0)))&(<R1>(<R1>([R1](~(P0))))))))|(<R1>(([R1](P0))&([R1](~(P0))))))|(<R1>(([R1](([R1](~(P0)))|(P0)))&(<R1>(<R1>((<R1>(P0))&(~(P0))))))))|(<R1>(([R1]((<R1>(~(P0)))|(P0)))&(<R1>(<R1>(([R1](P0))&(~(P0)))))))))
(~(((<R1>(<R1>(~((((([R1]([R1]((P0)|(~([R1](([R1](P0))|(~(P0))))))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0)))))))))&([R1](([R1]([R1](P0)))|(~([R1](P0))))))&((((P0)|([R1](P0)))|(~(<R1>([R1](P0)))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0))))))))))&((((([R1](P0))|(~(P0)))|([R1](([R1](P0))|(~(P0)))))|(~(<R1>([R1](([R1](P0))|(~(P0)))))))|(~([R1]((([R1](P0))|(~(P0)))|(~([R1](([R1](([R1](P0))|(~(P0))))|(~(([R1](P0))|(~(P0)))))))))))))))|(False))|(~((True)&(~([R1]([R1](((P0)|(~(<R1>([R1](P0)))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0))))))))))))))))
(~(((((P1)|(~([R1]((P1)|(~([R1](([R1](P1))|(~(P1)))))))))|((P2)|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))|((P3)|(~([R1]((P3)|(~([R1](([R1](P3))|(~(P3))))))))))|(~((([R1](([R1](P2))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))&(True))&(([R1](((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2)))))))))))|(~([R1]((((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))|(~([R1](([R1](((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2)))))))))))|(~(((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))))))))))))))
(~(((False)|(([R1]((P1)|(~([R1](P1)))))|([R1]((P1)|(~([R1](P1)))))))|(False)))
(~(((((([R1](P1))|([R1](P2)))|([R1](P3)))|([R1](P5)))|((((((((((((((<R1>((~(P1))&([R1](P1))))|(<R1>((~(P1))&([R1](P3)))))|(False))|((False)|(False)))|(((<R1>((~(P3))&([R1](P1))))|(<R1>((~(P3))&([R1](P3)))))|(False)))|((False)|(False)))|(((<R1>((~(P5))&([R1](P1))))|(<R1>((~(P5))&([R1](P3)))))|(False)))|((False)|(False)))|((False)|(False)))|((False)|((<R1>((~(P4))&([R1](P2))))|(<R1>((~(P6))&([R1](P2)))))))|((False)|(False)))|((False)|((<R1>((~(P4))&([R1](P4))))|(<R1>((~(P6))&([R1](P4)))))))|((False)|(False)))|((False)|((<R1>((~(P4))&([R1](P6))))|(<R1>((~(P6))&([R1](P6))))))))|((((<R1>(<R1>(~(P2))))|(<R1>(<R1>(~(P4)))))|(<R1>(<R1>(~(P5)))))|(<R1>(<R1>(~(P6)))))))
(~((<R1>((~(P101))&(P201)))|(~(<R1>((P101)&(P201))))))
(~((([R1]([R1]([R1]([R1]([R1](((((P1)&(P2))&(P3))&(P4))&(P5)))))))|((<R1>(((<R1>(((<R1>(((<R1>((False)|(<R1>(((P1)&(P2))|((~(P1))&(~(P2)))))))|([R1](P3)))|(<R1>(<R1>(((P2)&(P3))|((~(P2))&(~(P3))))))))|([R1](P4)))|(<R1>(<R1>(<R1>(((P3)&(P4))|((~(P3))&(~(P4)))))))))|([R1](P5)))|(<R1>(<R1>(<R1>(<R1>(((P4)&(P1))|((~(P4))&(~(P1))))))))))|([R1](P6))))|([R1]([R1]([R1]([R1]([R1](((((~(P2))&(~(P4)))&(~(P6)))&(~(P8)))&(~(P10))))))))))
(~(((((<R1>(~(([R1]([R1](~(P1))))|(~([R1](~(P1)))))))|([R1](<R1>([R1](P0)))))|([R1](([R1](~([R1](P1))))|(~(~([R1](P1)))))))|(((<R1>(([R1](P1))&(<R1>(<R1>(~(P1))))))|(<R1>((((([R1](<R1>(P0)))&([R1]((~(P0))|([R1](P3)))))|(<R1>(([R1](<R1>([R1]((~(P0))|([R1](P3))))))&([R1](<R1>(P0))))))|(([R1](<R1>(P0)))&(<R1>(<R1>([R1]((~(P0))|([R1](P3))))))))|(<R1>(((<R1>([R1](<R1>(P0))))&(P0))&(<R1>((~(P0))|([R1](P3)))))))))|(<R1>(([R1](<R1>(P1)))&(<R1>(<R1>([R1](~(P1)))))))))|(<R1>(P4))))
(~(~((p100&(~p101))&(((((p101=>p100)&(p102=>p101))&((p100=>((p0=>([r](p100=>p0)))&((~p0)=>([r](p100=>(~p0))))))&(p101=>((p1=>([r](p101=>p1)))&((~p1)=>([r](p101=>(~p1))))))))&((p100&(~p101))=>((<r>((p101&(~p102))&p1))&(<r>((p101&(~p102))&(~p1))))))&([r]((((p101=>p100)&(p102=>p101))&((p100=>((p0=>([r](p100=>p0)))&((~p0)=>([r](p100=>(~p0))))))&(p101=>((p1=>([r](p101=>p1)))&((~p1)=>([r](p101=>(~p1))))))))&((p100&(~p101))=>((<r>((p101&(~p102))&p1))&(<r>((p101&(~p102))&(~p1)))))))))))
(~((((((([r](([r]p0)|([r](<r>(~p0)))))|(<r>([r]False)))|(<r>(([r]p0)&(<r>(<r>(~p0))))))|(<r>(([r](<r>p0))&(<r>(<r>([r](~p0)))))))|(<r>(([r]p0)&([r](~p0)))))|(<r>(([r](([r](~p0))|p0))&(<r>(<r>((<r>p0)&(~p0)))))))|(<r>(([r]((<r>(~p0))|p0))&(<r>(<r>(([r]p0)&(~p0))))))))
(~((True&(~([r]([r](([r](([r](p0=>([r]p0)))=>p0))=>((<r>([r]p0))=>p0))))))=>((<r>(<r>(~((((([r](([r](p0=>([r]p0)))=>p0))=>([r]([r](([r](p0=>([r]p0)))=>p0))))&([r](([r]p0)=>([r]([r]p0)))))&(([r](([r](p0=>([r]p0)))=>p0))=>((<r>([r]p0))=>(p0|([r]p0)))))&(([r](([r]((p0=>([r]p0))=>([r](p0=>([r]p0)))))=>(p0=>([r]p0))))=>((<r>([r](p0=>([r]p0))))=>((p0=>([r]p0))|([r](p0=>([r]p0))))))))))|False)))
(~(((([r](([r](([r](p2=>([r]p2)))=>p2))=>([r]p2)))&True)&(([r](([r](((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2)))))=>([r]((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2))))))))=>((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2)))))))=>([r]((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2))))))))=>(((([r](([r](p1=>([r]p1)))=>p1))=>p1)|(([r](([r](p2=>([r]p2)))=>p2))=>p2))|(([r](([r](p3=>([r]p3)))=>p3))=>p3))))
(~((False|(([r](([r]p1)=>p1))|([r](([r]p1)=>p1))))|False))
(~(((((([r]p1)|([r]p2))|([r]p3))|([r]p5))|((((((((((((((<r>((~p1)&([r]p1)))|(<r>((~p1)&([r]p3))))|False)|(False|False))|(((<r>((~p3)&([r]p1)))|(<r>((~p3)&([r]p3))))|False))|(False|False))|(((<r>((~p5)&([r]p1)))|(<r>((~p5)&([r]p3))))|False))|(False|False))|(False|False))|(False|((<r>((~p4)&([r]p2)))|(<r>((~p6)&([r]p2))))))|(False|False))|(False|((<r>((~p4)&([r]p4)))|(<r>((~p6)&([r]p4))))))|(False|False))|(False|((<r>((~p4)&([r]p6)))|(<r>((~p6)&([r]p6)))))))|((((<r>(<r>(~p2)))|(<r>(<r>(~p4))))|(<r>(<r>(~p5))))|(<r>(<r>(~p6))))))
(~((<r>(p101&p201))=>(<r>((~p101)&p201))))
(~((([r]([r]([r]([r]([r]((((p1&p2)&p3)&p4)&p5))))))|((<r>(((<r>(((<r>(((<r>(False|(<r>(p1<=>p2))))|([r]p3))|(<r>(<r>(p2<=>p3)))))|([r]p4))|(<r>(<r>(<r>(p3<=>p4))))))|([r]p5))|(<r>(<r>(<r>(<r>(p4<=>p1)))))))|([r]p6)))|([r]([r]([r]([r]([r](((((~p2)&(~p4))&(~p6))&(~p8))&(~p10)))))))))
(~(((((<r>(~(([r](~p1))=>([r]([r](~p1))))))|([r](<r>([r]p0))))|([r]((~([r]p1))=>([r](~([r]p1))))))|(((<r>(([r]p1)&(<r>(<r>(~p1)))))|(<r>((((([r](<r>p0))&([r]((~p0)|([r]p3))))|(<r>(([r](<r>([r]((~p0)|([r]p3)))))&([r](<r>p0)))))|(([r](<r>p0))&(<r>(<r>([r]((~p0)|([r]p3)))))))|(<r>(((<r>([r](<r>p0)))&p0)&(<r>((~p0)|([r]p3))))))))|(<r>(([r](<r>p1))&(<r>(<r>([r](~p1))))))))|(<r>p4)))
"
let unsatCasesString =
"
(~((~(((P100)&(~(P101)))&((((((P100)|(~(P101)))&((P101)|(~(P102))))&((((([R1]((P0)|(~(P100))))|(~(P0)))&(([R1]((~(P0))|(~(P100))))|(~(~(P0)))))|(~(P100)))&(((([R1]((P1)|(~(P101))))|(~(P1)))&(([R1]((~(P1))|(~(P101))))|(~(~(P1)))))|(~(P101)))))&(((<R1>(((P101)&(~(P102)))&(P1)))&(<R1>(((P101)&(~(P102)))&(~(P1)))))|(~((P100)&(~(P101))))))&([R1](((((P100)|(~(P101)))&((P101)|(~(P102))))&((((([R1]((P0)|(~(P100))))|(~(P0)))&(([R1]((~(P0))|(~(P100))))|(~(~(P0)))))|(~(P100)))&(((([R1]((P1)|(~(P101))))|(~(P1)))&(([R1]((~(P1))|(~(P101))))|(~(~(P1)))))|(~(P101)))))&(((<R1>(((P101)&(~(P102)))&(P1)))&(<R1>(((P101)&(~(P102)))&(~(P1)))))|(~((P100)&(~(P101))))))))))|(~([R1](P1)))))
(~(((((([R1]((<R1>(~(P0)))|(P0)))|(<R1>([R1](False))))|(<R1>(([R1](P0))&(<R1>(<R1>(~(P0)))))))|(<R1>(([R1](<R1>(P0)))&(<R1>(<R1>([R1](~(P0))))))))|(<R1>((P0)&(<R1>([R1](~(P0)))))))|(<R1>((~(P0))&(<R1>([R1](P0)))))))
(~(((<R1>(~((((([R1]([R1]((P0)|(~([R1](([R1](P0))|(~(P0))))))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0)))))))))&([R1](([R1]([R1](P0)))|(~([R1](P0))))))&(((P0)|(~(<R1>([R1](P0)))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0))))))))))&(((([R1](P0))|(~(P0)))|(~(<R1>([R1](([R1](P0))|(~(P0)))))))|(~([R1]((([R1](P0))|(~(P0)))|(~([R1](([R1](([R1](P0))|(~(P0))))|(~(([R1](P0))|(~(P0))))))))))))))|(False))|(~((True)&(~([R1]((([R1](P0))|(~(<R1>([R1](P0)))))|(~([R1]((P0)|(~([R1](([R1](P0))|(~(P0)))))))))))))))
(~((((([R1](P1))|(~([R1]((P1)|(~([R1](([R1](P1))|(~(P1)))))))))|(([R1](P2))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))|(([R1](P3))|(~([R1]((P3)|(~([R1](([R1](P3))|(~(P3))))))))))|(~((([R1]((P2)|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))&(True))&((((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))|(~([R1]((((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))|(~([R1](([R1](((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2)))))))))))|(~(((P2)|(~([R1](([R1](P2))|(~(P2))))))&(([R1]([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))|(~([R1]((P2)|(~([R1](([R1](P2))|(~(P2))))))))))))))))))))))
(~(((False)|(([R1]((P1)|(~((P1)&([R1](P1))))))|([R1]((P1)|(~((P1)&([R1](P1))))))))|(~((([R1]((P2)|(~(((P1)&([R1](P1)))&(P1)))))|([R1]((~(([R1](P2))&(P2)))|(~(~(P1))))))|(~((([R1](((P2)|(~(((P1)&([R1](P1)))&(P1))))|((~(([R1](P2))&(P2)))|(~(~(P1))))))&([R1](([R1]((P2)|(~(((P1)&([R1](P1)))&(P1)))))|((~(([R1](P2))&(P2)))|(~(~(P1)))))))&([R1](((P2)|(~(((P1)&([R1](P1)))&(P1))))|([R1]((~(([R1](P2))&(P2)))|(~(~(P1)))))))))))))
(~(((((([R1](P1))|([R1](P2)))|([R1](P3)))|([R1](P5)))|(((((((False)|(False))|((False)|(False)))|((False)|(False)))|((False)|(False)))|((False)|(False)))|((False)|(False))))|((((<R1>(~(P2)))|(<R1>(~(P4))))|(<R1>(~(P2))))|(<R1>(~(P6))))))
(~((<R1>((P101)&(P201)))|(~(<R1>((P101)&(P201))))))
(~((([R1]([R1]([R1]([R1]((((P1)&(P2))&(P3))&(P4))))))|((<R1>(((<R1>(((<R1>((False)|(<R1>(((P1)&(P2))|((~(P1))&(~(P2)))))))|([R1](P3)))|(<R1>(<R1>(((P2)&(P3))|((~(P2))&(~(P3))))))))|([R1](P4)))|(<R1>(<R1>(<R1>(((P3)&(P1))|((~(P3))&(~(P1)))))))))|([R1](P5))))|([R1]([R1]([R1]([R1]((((~(P2))&(~(P4)))&(~(P6)))&(~(P8)))))))))
(~(((((<R1>(~(([R1]([R1](~(P1))))|(~([R1](~(P1)))))))|([R1](<R1>([R1](P0)))))|([R1](([R1](~([R1](P1))))|(~(~([R1](P1)))))))|(((<R1>(([R1](P1))&(<R1>(<R1>(~(P1))))))|(<R1>(((((([R1](<R1>(P0)))&([R1]((~(P0))|([R1](P3)))))|(<R1>(([R1](<R1>([R1]((~(P0))|([R1](P3))))))&([R1](<R1>(P0))))))|(([R1](<R1>(P0)))&(<R1>(<R1>([R1]((~(P0))|([R1](P3))))))))|(<R1>(((<R1>([R1](<R1>(P0))))&(P0))&(<R1>((~(P0))|([R1](P3)))))))|(<R1>([R1]((~(P0))|([R1](P3))))))))|(<R1>(([R1](<R1>(P1)))&(<R1>(<R1>([R1](~(P1)))))))))|(<R1>(P4))))
(~((~((p100&(~p101))&(((((p101=>p100)&(p102=>p101))&((p100=>((p0=>([r](p100=>p0)))&((~p0)=>([r](p100=>(~p0))))))&(p101=>((p1=>([r](p101=>p1)))&((~p1)=>([r](p101=>(~p1))))))))&((p100&(~p101))=>((<r>((p101&(~p102))&p1))&(<r>((p101&(~p102))&(~p1))))))&([r]((((p101=>p100)&(p102=>p101))&((p100=>((p0=>([r](p100=>p0)))&((~p0)=>([r](p100=>(~p0))))))&(p101=>((p1=>([r](p101=>p1)))&((~p1)=>([r](p101=>(~p1))))))))&((p100&(~p101))=>((<r>((p101&(~p102))&p1))&(<r>((p101&(~p102))&(~p1))))))))))|(~([r]p1))))
(~(((((([r]((<r>(~p0))|p0))|(<r>([r]False)))|(<r>(([r]p0)&(<r>(<r>(~p0))))))|(<r>(([r](<r>p0))&(<r>(<r>([r](~p0)))))))|(<r>(p0&(<r>([r](~p0))))))|(<r>((~p0)&(<r>([r]p0))))))
(~((True&(~([r](([r](([r](p0=>([r]p0)))=>p0))=>((<r>([r]p0))=>([r]p0))))))=>((<r>(~((((([r](([r](p0=>([r]p0)))=>p0))=>([r]([r](([r](p0=>([r]p0)))=>p0))))&([r](([r]p0)=>([r]([r]p0)))))&(([r](([r](p0=>([r]p0)))=>p0))=>((<r>([r]p0))=>p0)))&(([r](([r]((p0=>([r]p0))=>([r](p0=>([r]p0)))))=>(p0=>([r]p0))))=>((<r>([r](p0=>([r]p0))))=>(p0=>([r]p0)))))))|False)))
(~(((([r](([r](([r](p2=>([r]p2)))=>p2))=>p2))&True)&(([r](([r](((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2)))))=>([r]((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2))))))))=>((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2)))))))=>((([r](p2=>([r]p2)))=>p2)&(([r](([r](p2=>([r]p2)))=>p2))=>([r]([r](([r](p2=>([r]p2)))=>p2)))))))=>(((([r](([r](p1=>([r]p1)))=>p1))=>([r]p1))|(([r](([r](p2=>([r]p2)))=>p2))=>([r]p2)))|(([r](([r](p3=>([r]p3)))=>p3))=>([r]p3)))))
(~((False|(([r]((p1&([r]p1))=>p1))|([r]((p1&([r]p1))=>p1))))|(~(((([r]((((p1&([r]p1))&p1)=>p2)|((~p1)=>(~(([r]p2)&p2)))))&([r](([r](((p1&([r]p1))&p1)=>p2))|((~p1)=>(~(([r]p2)&p2))))))&([r]((((p1&([r]p1))&p1)=>p2)|([r]((~p1)=>(~(([r]p2)&p2)))))))=>(([r](((p1&([r]p1))&p1)=>p2))|([r]((~p1)=>(~(([r]p2)&p2)))))))))
(~(((((([r]p1)|([r]p2))|([r]p3))|([r]p5))|((((((False|False)|(False|False))|(False|False))|(False|False))|(False|False))|(False|False)))|((((<r>(~p2))|(<r>(~p4)))|(<r>(~p2)))|(<r>(~p6)))))
(~((<r>(p101&p201))=>(<r>(p101&p201))))
(~((([r]([r]([r]([r](((p1&p2)&p3)&p4)))))|((<r>(((<r>(((<r>(False|(<r>(p1<=>p2))))|([r]p3))|(<r>(<r>(p2<=>p3)))))|([r]p4))|(<r>(<r>(<r>(p3<=>p1))))))|([r]p5)))|([r]([r]([r]([r]((((~p2)&(~p4))&(~p6))&(~p8))))))))
(~(((((<r>(~(([r](~p1))=>([r]([r](~p1))))))|([r](<r>([r]p0))))|([r]((~([r]p1))=>([r](~([r]p1))))))|(((<r>(([r]p1)&(<r>(<r>(~p1)))))|(<r>(((((([r](<r>p0))&([r]((~p0)|([r]p3))))|(<r>(([r](<r>([r]((~p0)|([r]p3)))))&([r](<r>p0)))))|(([r](<r>p0))&(<r>(<r>([r]((~p0)|([r]p3)))))))|(<r>(((<r>([r](<r>p0)))&p0)&(<r>((~p0)|([r]p3))))))|(<r>([r]((~p0)|([r]p3)))))))|(<r>(([r](<r>p1))&(<r>(<r>([r](~p1))))))))|(<r>p4)))
"
let k = [| (CoAlgMisc.MultiModalK, [0]) |]
let getCases (lines:string) (res:testResult) : satCheck list =
let lineList = Str.split (Str.regexp "[\n]+") lines in
let f line : satCheck = (res, k, line) in
List.map f lineList
let satCasesList : satCheck list =
getCases satCasesString Sat
let unsatCasesList : satCheck list =
getCases unsatCasesString Unsat
src/testsuite/DL98TestCases.mli 0 → 100644
+ 6
− 0
View file @ f71032c3
open Testsuite
val satCasesList : satCheck list
val unsatCasesList : satCheck list
src/testsuite/Testsuite.ml
+ 12
− 3
View file @ f71032c3
......@@ -13,7 +13,8 @@ type testResult = | Sat
| Unsat
| ParseError
type satCheck = testResult * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
(* sat * functors * formula *)
type satCheck = testResult * (CoAlgMisc.sortTable) * string
......@@ -42,13 +43,21 @@ let runSatCheck (_,logic,input) =
with | Stream.Error _ -> ParseError
| CoAlgFormula.CoAlgException _ -> ParseError
let stringCrop width str =
if (String.length str <= width) then str
else ((Str.string_before str (width-1)) ^ "…")
let columnCreate width str =
let shorten = (stringCrop width str) in
let pad = String.make (max 0 (width - (String.length shorten))) ' ' in
(shorten ^ pad)
let runSatCheckVerbose (sc:satCheck) =
let cs = colored_string in
let sotr = terminal_string_of_testResult in
let (expectation,_,title) = sc in
PF.printf "Is %-50s " (cs "1" title);
PF.printf "%s?… " (sotr expectation);
PF.printf "Is %s " (cs "1" (columnCreate 50 title));
PF.printf "%s? → " (sotr expectation);
let res = runSatCheck sc in
(if (res = expectation)
then PF.printf "%s\n" (cs "1;32" "Yes")
......
src/testsuite/Testsuite.mli
+ 2
− 1
View file @ f71032c3
......@@ -9,7 +9,8 @@ type testResult = | Sat
| Unsat
| ParseError
type satCheck = testResult * (CoAlgMisc.sortTable) * string (* expected * functors * formula *)
(* expected * functors * formula *)
type satCheck = testResult * (CoAlgMisc.sortTable) * string
val runSatCheck : satCheck -> testResult
val runSatCheckVerbose : satCheck -> testResult
......
src/testsuite/cool-testsuite.ml
+ 10
− 2
View file @ f71032c3
open CoolUtils
open Testsuite
module DL98 = DL98TestCases
module CF = CoAlgFormula
module CR = CoAlgReasoner
module CM = CoAlgMisc
......@@ -19,6 +20,11 @@ let k_testcases: satCheck list =
; c Unsat "<R> True & [R] False"
; c Unsat "C |- <R> ~C"
; c Sat "C |- [R] ~C"
; c Unsat "<R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
(* Some DL98-Testcases *)
]
......@@ -41,7 +47,7 @@ let kd_testcases =
; c Unsat "C |- [R] ~C"
]
let cl_testcases =
let cl_testcases : satCheck list =
let c a b = (a,cl,b) in
[ c Unsat "[{1}] C & [{ 2 }] ~C"
; c Sat "[{1}] C & <{ 2 }> ~C"
......@@ -53,7 +59,9 @@ let cl_testcases =
let testcases =
let c name table = (name,table) in
[ c "K" k_testcases
[ c "DL98 (Sat)" DL98.satCasesList
; c "DL98 (Unsat)" DL98.unsatCasesList
; c "K" k_testcases
; c "Nominals" nominal_testcases
; c "KD" kd_testcases
; c "CL" cl_testcases
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment