From 22ae1bed2ee360774afa35a807781fdf33fdcaca Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Thu, 30 Jun 2022 16:55:42 -0600 Subject: [PATCH] stash --- .devcontainer/Dockerfile | 2 +- .gitignore | 2 + .vscode/launch.json | 2 +- NOTES.md | 14 +- __pycache__/ontology.cpython-39.pyc | Bin 1298 -> 1496 bytes example.py | 21 +- logic/Makefile | 18 + logic/O.g4 | 14 + logic/__init__.py | 0 logic/__pycache__/__init__.cpython-39.pyc | Bin 0 -> 138 bytes logic/__pycache__/logic.cpython-39.pyc | Bin 0 -> 4865 bytes logic/grammars/O.interp | 30 ++ logic/grammars/O.tokens | 16 + logic/grammars/OLexer.interp | 44 +++ logic/grammars/OLexer.py | 70 ++++ logic/grammars/OLexer.tokens | 16 + logic/grammars/OParser.py | 368 ++++++++++++++++++ logic/grammars/OVisitor.py | 48 +++ logic/grammars/__init__.py | 0 .../__pycache__/OLexer.cpython-39.pyc | Bin 0 -> 4030 bytes .../__pycache__/OParser.cpython-39.pyc | Bin 0 -> 11716 bytes .../__pycache__/__init__.cpython-39.pyc | Bin 0 -> 147 bytes logic/logic.py | 104 +++++ ontology.py | 6 +- programs/a.ont | 1 + programs/a.py | 7 - programs/b.ont | 1 + programs/b.py | 6 - programs/c.lp | 3 + programs/c.ont | 1 + propagator.py | 23 +- test_output/a.accept | 2 + test_output/a.out | 2 + test_output/b.accept | 2 + test_output/b.out | 2 + test_output/c.accept | 2 + test_output/c.out | 2 + tests.py | 28 +- 38 files changed, 819 insertions(+), 38 deletions(-) create mode 100644 logic/Makefile create mode 100644 logic/O.g4 create mode 100644 logic/__init__.py create mode 100644 logic/__pycache__/__init__.cpython-39.pyc create mode 100644 logic/__pycache__/logic.cpython-39.pyc create mode 100644 logic/grammars/O.interp create mode 100644 logic/grammars/O.tokens create mode 100644 logic/grammars/OLexer.interp create mode 100644 logic/grammars/OLexer.py create mode 100644 logic/grammars/OLexer.tokens create mode 100644 logic/grammars/OParser.py create mode 100644 logic/grammars/OVisitor.py create mode 100644 logic/grammars/__init__.py create mode 100644 logic/grammars/__pycache__/OLexer.cpython-39.pyc create mode 100644 logic/grammars/__pycache__/OParser.cpython-39.pyc create mode 100644 logic/grammars/__pycache__/__init__.cpython-39.pyc create mode 100644 logic/logic.py create mode 100644 programs/a.ont delete mode 100644 programs/a.py create mode 100644 programs/b.ont delete mode 100644 programs/b.py create mode 100644 programs/c.lp create mode 100644 programs/c.ont create mode 100644 test_output/a.accept create mode 100644 test_output/a.out create mode 100644 test_output/b.accept create mode 100644 test_output/b.out create mode 100644 test_output/c.accept create mode 100644 test_output/c.out mode change 100644 => 100755 tests.py diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 455dbfa..f6bd83f 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -1,6 +1,6 @@ FROM sjkillen/clyngor -RUN apt-get -qq update; apt-get -qq install sudo +RUN apt-get -qq update; apt-get -qq install sudo default-jdk make ARG USERNAME=asp ARG USER_UID=1000 diff --git a/.gitignore b/.gitignore index bfa6551..94c5c73 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ notes +antlr4.jar +logic/.antlr diff --git a/.vscode/launch.json b/.vscode/launch.json index 3cbc94b..5a5ba32 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -9,7 +9,7 @@ "type": "python", "request": "launch", "program": "${file}", - "args": ["programs/a.lp"], + "args": ["programs/c.lp"], "console": "integratedTerminal", "justMyCode": true } diff --git a/NOTES.md b/NOTES.md index 1e76147..d2306ee 100644 --- a/NOTES.md +++ b/NOTES.md @@ -1,4 +1,16 @@ # Technical issues - Clingo may or may not choose to propagate DL atoms before the ontology tells it to. - Symbols for atoms are not always present in the control object (E.g. a rule `a :- a`) -Current workaround is to use signature (which don't get removed). This may have implications about what can be grounded. \ No newline at end of file +Current workaround is to use signature (which don't get removed). This may have implications about what can be grounded. + +- Minimality checking +- The solver should never "decide" to propagate theory atoms, but it does +This might be blockable with tagged clauses, but since the solver unifies solver literals with their theory literals, this may block the regular atoms sometimes. + + +- CLingo unifying the atoms is a big problem + + +- If theory atoms are false, then it didn't come from ontology +Maybe this will work: +if the final model is not minimal, then it can't have come from the ontology \ No newline at end of file diff --git a/__pycache__/ontology.cpython-39.pyc b/__pycache__/ontology.cpython-39.pyc index e77b37255be579d868c6d7e19a4f2ab87de73aec..cae9399037d9b5044aba44adbed53d42e0f8c27e 100644 GIT binary patch delta 751 zcmY*X&ubGw6n^i`Y<`EdMKD`UX{DemSj3yP6vdo-2?(x=B%P@SvZl^%!NZ0K?ZK<= z)q|cSn18|lL-y*)lQ%D3d^1Uxc3{4Jv+sT1`{u`|+Rys5-)z=^NAK^C!F>Vn%PuYs zj~5Sl#wmjWg(HYC#E3$QL?|K|N(4oHPllP>$fh`OvRN92PKN`5BgsnVGYt6I3c zLsjPgyA@UCL~WUni?1R}bpW_U1zK;*P@ zH<$fn9GNOq0ZfBgrjfnI$9OZFW9QM%-Yfk^zdJVj2La_G)=BOS6CK4fGEFYdy=biT zXi2o}mW36Dx(!ydZ`fTa+i;<6qgM70JGh?tG{5btTxu delta 660 zcmY*X%}N|W5U#538E0oTZk9#YB$!JsBSFNY5fO6FMer~X!fN*>l3k-UBSca55MRKI zN3R|>Un5>Pe;AExfEpGUjN=}DS$uTnO<6) zZP`UBV8Gx2hM41!avG{!AsFguqk54=8!v%i_%4CbH)J9cU+R3uQpg1~GZIfsL*j{j zJxQoZfuTML(HEqqDFqEfJCM!(6=}%S)vwW(vcTFaE{+_7Z8rgzz&S@ zU4~8-wj7hA)ioClzZg3h1J74?__pfP_G&C_p0A-LmP>{4A(R%0_=UeYP>Q@*-P6w% zKc)#~R;)2{w+?tZKNSc@yZWKlH#$D%n{@inel58vW~KruPm7bIM$3SYsKfD(iS-D?tilTpQ~f)j1-4(-9kpS?%t#Bw4ktE6xfSm z7U6%u6cg0gMt&)=EOl{tdUSC3kx5+kufTpj;fCymWZ)&UKY%xuJ$l~Mi0igpvMED8 S8Q3k9ilEjZO skip; + +expr: + '(' expr ')' # parenth + | '-' expr # log_neg + | expr op = '->' expr # log_impl + | expr op = '<->' expr # log_iff + | expr op = '|' expr # log_or + | expr op = '&' expr # log_and + | ATOM # atom; + +ATOM: [a-z][a-zA-Z0-9]*; diff --git a/logic/__init__.py b/logic/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/logic/__pycache__/__init__.cpython-39.pyc b/logic/__pycache__/__init__.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..6128a482a2032c2cb4fe2ce420e2150b8954e378 GIT binary patch literal 138 zcmYe~<>g`kg2I=3lR)%i5P=LBfgA@QE@lA|DGb33nv8xc8Hzx{2;!H%etCXTc5y*s za%!=Da!zJmdcJN(ZgyUpZb@o!iGEIgdSvf%&TWKdOvJnS->!aS4)6-I1pmJyIwFjWC#fp(P78Xnkq@N>Ykph zE-h=t=rnsG0xn!RNH_E&{73o-Cr5DOwkN)D!SLyMb%^PUOXaY`qX$qp$SBW_3=$4&1kGmb6 zmEY4+h5M1r>|IIh=5Iok$~`6JhuyTR6P4B8>-A6cu2wRPv-w9!94EcKB7WLGhzL!}SPPN>d1H*Scgom)0fEoK!{!Y7SgAUo@}Yy#L2U z9jE=UBh&kxsM|YC?j6O)y@PvNruu%A9CkZ-yV?IFbL8_df`3`5nU$YbNTE&Q?zGBT zx!vxCv23@qYP%f+*ogXmyZ!7WjPemh4=QrU%!XkyXFo|IwOr^k(M&B7ua1U1+bpKc zI5V6ZXxb2YKw@vADbW0#MR*FfWdT!rgenKBws7DmCE)^7FDt*JlbDu~Ii#X$;1xGO zC9Mspq|AT~tf$sGpjAzfEv8<_O)XF}MmE=<7Dfxn@nWa-VzL4=wL(v=QnN* z-41)bM2EVY^wM_Q;H5Tb{8pr1!zgKEkgD=BSH$^0kn&{7_}>Jn@(8KYPNH+5B;cA2 z6j{OmMKBUf=WM_(m_G)KtFK`sU&n2Tk>&+r{%Fz>V3q5Dk%y?SP(w~-@cSI3z6v=4 ze1a5lZbxbhqceTV5#0EeBW&C~_*jmd10QpR2Oleo5`3(jl^%9`205PeGbfSD@h|8Qh=Lt+br(H$&I!)`9rW$Izne>NNIafMBoA*$*pN7yNcdL&;D(F? znLkZrCgaC^*94Q6yYq?-Ua>b$`MvE^d+XkI%TZs4n(8h!#y!75z1wX2O$?^ws1~cT zwb8YK`>8(y={8H#*2pbwY;Mf`-}l5FJVCZi%V@AC82(%l_jYUl1fy52y^i={qKJn( zS-gb5vyK2DY*^Y6uCcTSOP8|JlSIWQQJ9s(sDBjhOPx6?Ni>4Cr=&hny$%KF;zyRI zg^)h!uh3|+CL6Ldrnz9+9-uGypZR0!3L+~JHL*7022KEJ08w2}8 z#Q$d-6!u}M7Tp{gb%(Cx^C#YXn<~jo-_2EXo7Bno;UQoSOC2M zdeP8}VhQvT=w(Ca)zgYt6>FGhRbaoj*0Tb%hbP@gNM-QfQ7u~Hv>Q`@oFaV?+8V;2 z+Nf%ZB*~HQr8X}>!ZgO5AWC3T_0a8gb-Vp@P(}D(9a(Lpz-A$X+REerNY>}2J1$eA>B$#YG9geRs9Y}E0M7|J&kSw|12RC?{2O4D*T^r6UO z^dVQq=4MaXQ$DcHv9Zrln_S>OrZ`bU8^GH;iXi=rnwG2X;AVns=4kmsE81as8l`A8 zTk-aOx7SYk??Rx!a;D-Vxf_a8R5FTFAg8EAiTs=sl*2KYwxaO*h4gtpIc)dj;V(Z= zpOM@Ree6OXQ-N7z*s)PBnW7}EW}#6t=ApMH>eo|~Z_Kh{F7`jot+sEQxjvq`8~3A~ zskvXjZEh0$l4j4{mlo7LIQZ?<cWIHHvPO z(oUDIDP}}kYuAh8YZ>i_G%1DWpfQSTkCL8=C~wmU?V+GSu7HhNjQot4^?YL#JPOdk zobeerY{7jnejFZGFy9$7Vd8>G(KM(Ljs@p2IO+*Clf|2!NwYt|04Zk*l`8Xj!*1GT zT;sp1NCt_8?0Y3O5d>pTq5wg$%+yziXSj1s=0P0=Z^CzpGiTtOJMc7DyF&|gm3zU? zya9^4{H#|}6}&^y8CX#yGH~W*BMryyR&R2UYlK3Gn0!WFS^RybD3ejZH}mfrX7$0!^)a{< zEr|TfoYKwa%M-*M;u)7WAel;@w4Yk<*xFfnEB|z`P1!G{V}*~s=#T0+-)?xEEfiOi Kv!>tt)_(w<(!gZ^ literal 0 HcmV?d00001 diff --git a/logic/grammars/O.interp b/logic/grammars/O.interp new file mode 100644 index 0000000..dd48b21 --- /dev/null +++ b/logic/grammars/O.interp @@ -0,0 +1,30 @@ +token literal names: +null +'(' +')' +'-' +'->' +'<->' +'|' +'&' +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +WS +ATOM + +rule names: +expr + + +atn: +[4, 1, 9, 30, 2, 0, 7, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 3, 0, 11, 8, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 5, 0, 25, 8, 0, 10, 0, 12, 0, 28, 9, 0, 1, 0, 0, 1, 0, 1, 0, 0, 0, 34, 0, 10, 1, 0, 0, 0, 2, 3, 6, 0, -1, 0, 3, 4, 5, 1, 0, 0, 4, 5, 3, 0, 0, 0, 5, 6, 5, 2, 0, 0, 6, 11, 1, 0, 0, 0, 7, 8, 5, 3, 0, 0, 8, 11, 3, 0, 0, 6, 9, 11, 5, 9, 0, 0, 10, 2, 1, 0, 0, 0, 10, 7, 1, 0, 0, 0, 10, 9, 1, 0, 0, 0, 11, 26, 1, 0, 0, 0, 12, 13, 10, 5, 0, 0, 13, 14, 5, 4, 0, 0, 14, 25, 3, 0, 0, 6, 15, 16, 10, 4, 0, 0, 16, 17, 5, 5, 0, 0, 17, 25, 3, 0, 0, 5, 18, 19, 10, 3, 0, 0, 19, 20, 5, 6, 0, 0, 20, 25, 3, 0, 0, 4, 21, 22, 10, 2, 0, 0, 22, 23, 5, 7, 0, 0, 23, 25, 3, 0, 0, 3, 24, 12, 1, 0, 0, 0, 24, 15, 1, 0, 0, 0, 24, 18, 1, 0, 0, 0, 24, 21, 1, 0, 0, 0, 25, 28, 1, 0, 0, 0, 26, 24, 1, 0, 0, 0, 26, 27, 1, 0, 0, 0, 27, 1, 1, 0, 0, 0, 28, 26, 1, 0, 0, 0, 3, 10, 24, 26] \ No newline at end of file diff --git a/logic/grammars/O.tokens b/logic/grammars/O.tokens new file mode 100644 index 0000000..b586e7c --- /dev/null +++ b/logic/grammars/O.tokens @@ -0,0 +1,16 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +WS=8 +ATOM=9 +'('=1 +')'=2 +'-'=3 +'->'=4 +'<->'=5 +'|'=6 +'&'=7 diff --git a/logic/grammars/OLexer.interp b/logic/grammars/OLexer.interp new file mode 100644 index 0000000..97660a2 --- /dev/null +++ b/logic/grammars/OLexer.interp @@ -0,0 +1,44 @@ +token literal names: +null +'(' +')' +'-' +'->' +'<->' +'|' +'&' +null +null + +token symbolic names: +null +null +null +null +null +null +null +null +WS +ATOM + +rule names: +T__0 +T__1 +T__2 +T__3 +T__4 +T__5 +T__6 +WS +ATOM + +channel names: +DEFAULT_TOKEN_CHANNEL +HIDDEN + +mode names: +DEFAULT_MODE + +atn: +[4, 0, 9, 50, 6, -1, 2, 0, 7, 0, 2, 1, 7, 1, 2, 2, 7, 2, 2, 3, 7, 3, 2, 4, 7, 4, 2, 5, 7, 5, 2, 6, 7, 6, 2, 7, 7, 7, 2, 8, 7, 8, 1, 0, 1, 0, 1, 1, 1, 1, 1, 2, 1, 2, 1, 3, 1, 3, 1, 3, 1, 4, 1, 4, 1, 4, 1, 4, 1, 5, 1, 5, 1, 6, 1, 6, 1, 7, 4, 7, 38, 8, 7, 11, 7, 12, 7, 39, 1, 7, 1, 7, 1, 8, 1, 8, 5, 8, 46, 8, 8, 10, 8, 12, 8, 49, 9, 8, 0, 0, 9, 1, 1, 3, 2, 5, 3, 7, 4, 9, 5, 11, 6, 13, 7, 15, 8, 17, 9, 1, 0, 3, 3, 0, 9, 10, 13, 13, 32, 32, 1, 0, 97, 122, 3, 0, 48, 57, 65, 90, 97, 122, 51, 0, 1, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 5, 1, 0, 0, 0, 0, 7, 1, 0, 0, 0, 0, 9, 1, 0, 0, 0, 0, 11, 1, 0, 0, 0, 0, 13, 1, 0, 0, 0, 0, 15, 1, 0, 0, 0, 0, 17, 1, 0, 0, 0, 1, 19, 1, 0, 0, 0, 3, 21, 1, 0, 0, 0, 5, 23, 1, 0, 0, 0, 7, 25, 1, 0, 0, 0, 9, 28, 1, 0, 0, 0, 11, 32, 1, 0, 0, 0, 13, 34, 1, 0, 0, 0, 15, 37, 1, 0, 0, 0, 17, 43, 1, 0, 0, 0, 19, 20, 5, 40, 0, 0, 20, 2, 1, 0, 0, 0, 21, 22, 5, 41, 0, 0, 22, 4, 1, 0, 0, 0, 23, 24, 5, 45, 0, 0, 24, 6, 1, 0, 0, 0, 25, 26, 5, 45, 0, 0, 26, 27, 5, 62, 0, 0, 27, 8, 1, 0, 0, 0, 28, 29, 5, 60, 0, 0, 29, 30, 5, 45, 0, 0, 30, 31, 5, 62, 0, 0, 31, 10, 1, 0, 0, 0, 32, 33, 5, 124, 0, 0, 33, 12, 1, 0, 0, 0, 34, 35, 5, 38, 0, 0, 35, 14, 1, 0, 0, 0, 36, 38, 7, 0, 0, 0, 37, 36, 1, 0, 0, 0, 38, 39, 1, 0, 0, 0, 39, 37, 1, 0, 0, 0, 39, 40, 1, 0, 0, 0, 40, 41, 1, 0, 0, 0, 41, 42, 6, 7, 0, 0, 42, 16, 1, 0, 0, 0, 43, 47, 7, 1, 0, 0, 44, 46, 7, 2, 0, 0, 45, 44, 1, 0, 0, 0, 46, 49, 1, 0, 0, 0, 47, 45, 1, 0, 0, 0, 47, 48, 1, 0, 0, 0, 48, 18, 1, 0, 0, 0, 49, 47, 1, 0, 0, 0, 3, 0, 39, 47, 1, 6, 0, 0] \ No newline at end of file diff --git a/logic/grammars/OLexer.py b/logic/grammars/OLexer.py new file mode 100644 index 0000000..2e8be2c --- /dev/null +++ b/logic/grammars/OLexer.py @@ -0,0 +1,70 @@ +# Generated from O.g4 by ANTLR 4.10.1 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + + +def serializedATN(): + return [ + 4,0,9,50,6,-1,2,0,7,0,2,1,7,1,2,2,7,2,2,3,7,3,2,4,7,4,2,5,7,5,2, + 6,7,6,2,7,7,7,2,8,7,8,1,0,1,0,1,1,1,1,1,2,1,2,1,3,1,3,1,3,1,4,1, + 4,1,4,1,4,1,5,1,5,1,6,1,6,1,7,4,7,38,8,7,11,7,12,7,39,1,7,1,7,1, + 8,1,8,5,8,46,8,8,10,8,12,8,49,9,8,0,0,9,1,1,3,2,5,3,7,4,9,5,11,6, + 13,7,15,8,17,9,1,0,3,3,0,9,10,13,13,32,32,1,0,97,122,3,0,48,57,65, + 90,97,122,51,0,1,1,0,0,0,0,3,1,0,0,0,0,5,1,0,0,0,0,7,1,0,0,0,0,9, + 1,0,0,0,0,11,1,0,0,0,0,13,1,0,0,0,0,15,1,0,0,0,0,17,1,0,0,0,1,19, + 1,0,0,0,3,21,1,0,0,0,5,23,1,0,0,0,7,25,1,0,0,0,9,28,1,0,0,0,11,32, + 1,0,0,0,13,34,1,0,0,0,15,37,1,0,0,0,17,43,1,0,0,0,19,20,5,40,0,0, + 20,2,1,0,0,0,21,22,5,41,0,0,22,4,1,0,0,0,23,24,5,45,0,0,24,6,1,0, + 0,0,25,26,5,45,0,0,26,27,5,62,0,0,27,8,1,0,0,0,28,29,5,60,0,0,29, + 30,5,45,0,0,30,31,5,62,0,0,31,10,1,0,0,0,32,33,5,124,0,0,33,12,1, + 0,0,0,34,35,5,38,0,0,35,14,1,0,0,0,36,38,7,0,0,0,37,36,1,0,0,0,38, + 39,1,0,0,0,39,37,1,0,0,0,39,40,1,0,0,0,40,41,1,0,0,0,41,42,6,7,0, + 0,42,16,1,0,0,0,43,47,7,1,0,0,44,46,7,2,0,0,45,44,1,0,0,0,46,49, + 1,0,0,0,47,45,1,0,0,0,47,48,1,0,0,0,48,18,1,0,0,0,49,47,1,0,0,0, + 3,0,39,47,1,6,0,0 + ] + +class OLexer(Lexer): + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + T__0 = 1 + T__1 = 2 + T__2 = 3 + T__3 = 4 + T__4 = 5 + T__5 = 6 + T__6 = 7 + WS = 8 + ATOM = 9 + + channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] + + modeNames = [ "DEFAULT_MODE" ] + + literalNames = [ "", + "'('", "')'", "'-'", "'->'", "'<->'", "'|'", "'&'" ] + + symbolicNames = [ "", + "WS", "ATOM" ] + + ruleNames = [ "T__0", "T__1", "T__2", "T__3", "T__4", "T__5", "T__6", + "WS", "ATOM" ] + + grammarFileName = "O.g4" + + def __init__(self, input=None, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache()) + self._actions = None + self._predicates = None + + diff --git a/logic/grammars/OLexer.tokens b/logic/grammars/OLexer.tokens new file mode 100644 index 0000000..b586e7c --- /dev/null +++ b/logic/grammars/OLexer.tokens @@ -0,0 +1,16 @@ +T__0=1 +T__1=2 +T__2=3 +T__3=4 +T__4=5 +T__5=6 +T__6=7 +WS=8 +ATOM=9 +'('=1 +')'=2 +'-'=3 +'->'=4 +'<->'=5 +'|'=6 +'&'=7 diff --git a/logic/grammars/OParser.py b/logic/grammars/OParser.py new file mode 100644 index 0000000..77a4898 --- /dev/null +++ b/logic/grammars/OParser.py @@ -0,0 +1,368 @@ +# Generated from O.g4 by ANTLR 4.10.1 +# encoding: utf-8 +from antlr4 import * +from io import StringIO +import sys +if sys.version_info[1] > 5: + from typing import TextIO +else: + from typing.io import TextIO + +def serializedATN(): + return [ + 4,1,9,30,2,0,7,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,3,0,11,8,0,1,0, + 1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,5,0,25,8,0,10,0,12,0, + 28,9,0,1,0,0,1,0,1,0,0,0,34,0,10,1,0,0,0,2,3,6,0,-1,0,3,4,5,1,0, + 0,4,5,3,0,0,0,5,6,5,2,0,0,6,11,1,0,0,0,7,8,5,3,0,0,8,11,3,0,0,6, + 9,11,5,9,0,0,10,2,1,0,0,0,10,7,1,0,0,0,10,9,1,0,0,0,11,26,1,0,0, + 0,12,13,10,5,0,0,13,14,5,4,0,0,14,25,3,0,0,6,15,16,10,4,0,0,16,17, + 5,5,0,0,17,25,3,0,0,5,18,19,10,3,0,0,19,20,5,6,0,0,20,25,3,0,0,4, + 21,22,10,2,0,0,22,23,5,7,0,0,23,25,3,0,0,3,24,12,1,0,0,0,24,15,1, + 0,0,0,24,18,1,0,0,0,24,21,1,0,0,0,25,28,1,0,0,0,26,24,1,0,0,0,26, + 27,1,0,0,0,27,1,1,0,0,0,28,26,1,0,0,0,3,10,24,26 + ] + +class OParser ( Parser ): + + grammarFileName = "O.g4" + + atn = ATNDeserializer().deserialize(serializedATN()) + + decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ] + + sharedContextCache = PredictionContextCache() + + literalNames = [ "", "'('", "')'", "'-'", "'->'", "'<->'", + "'|'", "'&'" ] + + symbolicNames = [ "", "", "", "", + "", "", "", "", + "WS", "ATOM" ] + + RULE_expr = 0 + + ruleNames = [ "expr" ] + + EOF = Token.EOF + T__0=1 + T__1=2 + T__2=3 + T__3=4 + T__4=5 + T__5=6 + T__6=7 + WS=8 + ATOM=9 + + def __init__(self, input:TokenStream, output:TextIO = sys.stdout): + super().__init__(input, output) + self.checkVersion("4.10.1") + self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache) + self._predicates = None + + + + + class ExprContext(ParserRuleContext): + __slots__ = 'parser' + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + + def getRuleIndex(self): + return OParser.RULE_expr + + + def copyFrom(self, ctx:ParserRuleContext): + super().copyFrom(ctx) + + + class Log_negContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.copyFrom(ctx) + + def expr(self): + return self.getTypedRuleContext(OParser.ExprContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLog_neg" ): + return visitor.visitLog_neg(self) + else: + return visitor.visitChildren(self) + + + class ParenthContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.copyFrom(ctx) + + def expr(self): + return self.getTypedRuleContext(OParser.ExprContext,0) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitParenth" ): + return visitor.visitParenth(self) + else: + return visitor.visitChildren(self) + + + class Log_orContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.op = None # Token + self.copyFrom(ctx) + + def expr(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(OParser.ExprContext) + else: + return self.getTypedRuleContext(OParser.ExprContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLog_or" ): + return visitor.visitLog_or(self) + else: + return visitor.visitChildren(self) + + + class Log_implContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.op = None # Token + self.copyFrom(ctx) + + def expr(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(OParser.ExprContext) + else: + return self.getTypedRuleContext(OParser.ExprContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLog_impl" ): + return visitor.visitLog_impl(self) + else: + return visitor.visitChildren(self) + + + class AtomContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.copyFrom(ctx) + + def ATOM(self): + return self.getToken(OParser.ATOM, 0) + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitAtom" ): + return visitor.visitAtom(self) + else: + return visitor.visitChildren(self) + + + class Log_iffContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.op = None # Token + self.copyFrom(ctx) + + def expr(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(OParser.ExprContext) + else: + return self.getTypedRuleContext(OParser.ExprContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLog_iff" ): + return visitor.visitLog_iff(self) + else: + return visitor.visitChildren(self) + + + class Log_andContext(ExprContext): + + def __init__(self, parser, ctx:ParserRuleContext): # actually a OParser.ExprContext + super().__init__(parser) + self.op = None # Token + self.copyFrom(ctx) + + def expr(self, i:int=None): + if i is None: + return self.getTypedRuleContexts(OParser.ExprContext) + else: + return self.getTypedRuleContext(OParser.ExprContext,i) + + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitLog_and" ): + return visitor.visitLog_and(self) + else: + return visitor.visitChildren(self) + + + + def expr(self, _p:int=0): + _parentctx = self._ctx + _parentState = self.state + localctx = OParser.ExprContext(self, self._ctx, _parentState) + _prevctx = localctx + _startState = 0 + self.enterRecursionRule(localctx, 0, self.RULE_expr, _p) + try: + self.enterOuterAlt(localctx, 1) + self.state = 10 + self._errHandler.sync(self) + token = self._input.LA(1) + if token in [OParser.T__0]: + localctx = OParser.ParenthContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + + self.state = 3 + self.match(OParser.T__0) + self.state = 4 + self.expr(0) + self.state = 5 + self.match(OParser.T__1) + pass + elif token in [OParser.T__2]: + localctx = OParser.Log_negContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + self.state = 7 + self.match(OParser.T__2) + self.state = 8 + self.expr(6) + pass + elif token in [OParser.ATOM]: + localctx = OParser.AtomContext(self, localctx) + self._ctx = localctx + _prevctx = localctx + self.state = 9 + self.match(OParser.ATOM) + pass + else: + raise NoViableAltException(self) + + self._ctx.stop = self._input.LT(-1) + self.state = 26 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,2,self._ctx) + while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: + if _alt==1: + if self._parseListeners is not None: + self.triggerExitRuleEvent() + _prevctx = localctx + self.state = 24 + self._errHandler.sync(self) + la_ = self._interp.adaptivePredict(self._input,1,self._ctx) + if la_ == 1: + localctx = OParser.Log_implContext(self, OParser.ExprContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_expr) + self.state = 12 + if not self.precpred(self._ctx, 5): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 5)") + self.state = 13 + localctx.op = self.match(OParser.T__3) + self.state = 14 + self.expr(6) + pass + + elif la_ == 2: + localctx = OParser.Log_iffContext(self, OParser.ExprContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_expr) + self.state = 15 + if not self.precpred(self._ctx, 4): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 4)") + self.state = 16 + localctx.op = self.match(OParser.T__4) + self.state = 17 + self.expr(5) + pass + + elif la_ == 3: + localctx = OParser.Log_orContext(self, OParser.ExprContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_expr) + self.state = 18 + if not self.precpred(self._ctx, 3): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 3)") + self.state = 19 + localctx.op = self.match(OParser.T__5) + self.state = 20 + self.expr(4) + pass + + elif la_ == 4: + localctx = OParser.Log_andContext(self, OParser.ExprContext(self, _parentctx, _parentState)) + self.pushNewRecursionContext(localctx, _startState, self.RULE_expr) + self.state = 21 + if not self.precpred(self._ctx, 2): + from antlr4.error.Errors import FailedPredicateException + raise FailedPredicateException(self, "self.precpred(self._ctx, 2)") + self.state = 22 + localctx.op = self.match(OParser.T__6) + self.state = 23 + self.expr(3) + pass + + + self.state = 28 + self._errHandler.sync(self) + _alt = self._interp.adaptivePredict(self._input,2,self._ctx) + + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.unrollRecursionContexts(_parentctx) + return localctx + + + + def sempred(self, localctx:RuleContext, ruleIndex:int, predIndex:int): + if self._predicates == None: + self._predicates = dict() + self._predicates[0] = self.expr_sempred + pred = self._predicates.get(ruleIndex, None) + if pred is None: + raise Exception("No predicate with index:" + str(ruleIndex)) + else: + return pred(localctx, predIndex) + + def expr_sempred(self, localctx:ExprContext, predIndex:int): + if predIndex == 0: + return self.precpred(self._ctx, 5) + + + if predIndex == 1: + return self.precpred(self._ctx, 4) + + + if predIndex == 2: + return self.precpred(self._ctx, 3) + + + if predIndex == 3: + return self.precpred(self._ctx, 2) + + + + + diff --git a/logic/grammars/OVisitor.py b/logic/grammars/OVisitor.py new file mode 100644 index 0000000..0c85df3 --- /dev/null +++ b/logic/grammars/OVisitor.py @@ -0,0 +1,48 @@ +# Generated from O.g4 by ANTLR 4.10.1 +from antlr4 import * +if __name__ is not None and "." in __name__: + from .OParser import OParser +else: + from OParser import OParser + +# This class defines a complete generic visitor for a parse tree produced by OParser. + +class OVisitor(ParseTreeVisitor): + + # Visit a parse tree produced by OParser#log_neg. + def visitLog_neg(self, ctx:OParser.Log_negContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#parenth. + def visitParenth(self, ctx:OParser.ParenthContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#log_or. + def visitLog_or(self, ctx:OParser.Log_orContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#log_impl. + def visitLog_impl(self, ctx:OParser.Log_implContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#atom. + def visitAtom(self, ctx:OParser.AtomContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#log_iff. + def visitLog_iff(self, ctx:OParser.Log_iffContext): + return self.visitChildren(ctx) + + + # Visit a parse tree produced by OParser#log_and. + def visitLog_and(self, ctx:OParser.Log_andContext): + return self.visitChildren(ctx) + + + +del OParser \ No newline at end of file diff --git a/logic/grammars/__init__.py b/logic/grammars/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/logic/grammars/__pycache__/OLexer.cpython-39.pyc b/logic/grammars/__pycache__/OLexer.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..1ae18ead8f0b39875a7359a2f53ffa9b1d0289a4 GIT binary patch literal 4030 zcmaJ^&2!tv72gF&2&5>A@(hQME{E3FuCQllVfhVr0@M85+a8vIQZdx?0dWKW0!!puuv6r zefPtE9zLlE@jWx=uM#nTpgaCMff7oFqRmeulwHFyB-3VSI;L+vDyh;{p~{a-(FY{8 z!gAMgEGc?5aB~@_=9K+RIQE}}s;KHSp{jo6)O4!KJP?g}O|yuGOy%1I_CXQ_y`#PT zmX;*e;ENd&4EO4LtzU24ui$;GhLc( zGws}nifT;3Y++1627qkLYLkaRw#XC|a0MAC$T)^<94N@R0+|dHWH8HtWt!v4#w{^5 zj%b>KVhZ3CvYf(7A)7^E&CvdT3UOduP9YA+aw<;*Q~E6q0datxAH}A};p_T1O4!0* zPUSfOg~^%H>toMgu>uUaI8x|MrjSl3xGhlqOooX7c`e}{ELMP&zyTD??0_fI&@yOv z#tNXtU^vBWa0LJh?FxIjG6MYuQ!g`&&9q0X9{+8MN@R+i_#_pRE=D*ZL~3Iiw%Jt z0MFZ#+D&G$IcL?Ek0t#Y4}tC0q%ChI{rX5dJ@0$0{l!?ze=+AWd5hV?zT#l?n`UPf_Lo_-TdjVSXeV!7S{k|w0FvDJ$begpQ znh*{OwdlH8T2|=7>SIc{pJj`}BLrkTABWV9WBXP_I~>>;e!8{sWj}fxAA21?-spt% z9@by`y!*I!xR&^FvJv)=g3iWKd{gqvr{cMEEG3okO!#xY^~gSzO>runisCoM zk~6Q$PEA?Pf|_#{mF+C4igQ6#onhAuaQ?$D~qwiIU8Lj5gY-B z7V{Q95<~IX#ZQf|>;}rI%W>d1t3#rpEe>R0fWr;ymZkAIU>n z-3o&^>GZqD+t-Nyk!~?qK1*<}%XTC>6g9><%WKI_P4q8LIsVs4SDL$bc0Rt_cH8@Z z-fg+JKiX-vcJHRvM|;iYZY!;g)c5wAyAAuN%GO@%!Oq>i=Jvp>U#}B17}n~8QhjZ^ zJ}B3>_+i$E3~$vNW^|9IF+Mp+OFQlTdyPt3YP;?Y;3n`L;Jd(^!1sW+q86`upI}hh zUq8CpqAXecljQg$>2QKa*C^TijJc5$L2V+3a%eoK50Rnx#!&LPlp-;Q#62p}T~4f1 zaY~dsr%2}7z={(1G8kAl*EeshZ#JrFIX*e|qttfYpcf>ro7Os?`<=%R{3s6ky>uD< zO$~hzbWcJr=|`#QCB1Y}`JI4A#O*#6HeJ0R`6}onB)Q%1CG??k+apKm9Jx*W=-9Dc z58Bw7caJgFqy0n;QHuTWFf9i?3Oo9QqWe~+71!;AUL3n_)+F2?(ccL85Q=#R3%Mw( za#dP#uyocUqX-(Wb2L4#>r*sU*X{PzNyv1~b-y_A!ZXbh1=aM&n>I@4)j5tEJNlF$ zt@yo@t{>5A)1^_+?fyYRg6K0Ib)Vrc41Z-fU}!UZ%-Bnm*rMgdPKDOy zgG_5-Kn}f3L5IoH?!$fFnsa6J(OqjGxA-6(@>1C*lt~Br07vOJT$UWpCNNAI&H|UOeyV=H~aoH%zsh?pRmSLOxD;W`6H0D#w>m^}yGc|&K#7!CX z3DVj>vYw%eANEr#d3sD|CsyQCGG?8|b7Ipnx(e>jodQ@MjskltE84a}qhsFYwya5; LYQAXHOnc>j0Bonb literal 0 HcmV?d00001 diff --git a/logic/grammars/__pycache__/OParser.cpython-39.pyc b/logic/grammars/__pycache__/OParser.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..0227aabcdecccd082f0a679feea96cb0046c610d GIT binary patch literal 11716 zcmc&)U2I%QR=$7z-?lrBW9L84uhW@{|S>0>FK(*+wQ-q zd!0#|_GlSLEC>PS1q6zay+T5M0IiUCTONc>eSzr~Y}b?Tf`=hUrp%R@t14cEW@*WZ2m!?!i<-wBCd7Lc2`-A@37CiI#%NB>4m zuN$_ZQ`xMUw&|ElmavX#BC%}AcTt?# zto}d;Nn`f%2|T?`6OjbAGXzc(peH1gPK71z!gU8z+BQSV+c_GNcsoGyKLe8_MSs%A zs5Bg*WC(skJ}RB0(jcBmY6A!72A1i$kcuqyc8ZA!dU$!#uMF zyU%tTB6j`9xC=iqMnt(3&CTz^4MV$eMT+v}!q4`RXMypveGN>MWyP)hY*%#56$^rS z>6=Wql?UIomFW#?r6ISE?>3`D)XH2j2h3Vmk`vU*)8dBiTHr26iRcJ{0rTCahHWOw zpzm2?XqyK2wa_>232GQbnfh&y5;#mM27UoLfLM5}usW#Vu92!V0x!j$`L zW0G1)BtFlqk1pl2)G&x=;%}Q}#q%AcBVG`^=yq-8^|ov485(?0D>Fm_8`#QI<-rF% zORd|iib1XCBcg*^c}ONdsFhX5BId!V-N&1=t=3$qR<13`a=l)b?zM-H03A8qdZ~u+UoF?FZAaXin((QI94wjp!`E^AHONI1zgZBw^X!Vu;w%}G0{rOcXsM_beFtdm>Q>^vfh z^#k1=!hZt)!y;*qh}42^7o0;&qxPss+lNKQ9urynh{)OFB5zNKA^WHpwvUMs`?x6B zC!CW@r{;C%v~xxrdTo4Po7cstIQ(kJo13xN` z0YAq01>ncU3E(FfzX<%KI0gI^! zrx&hQXtjhFg+CJgZQL%og9WXleLVVIV^v=@JgsAN^flv;jL)nmzEL3Tn|JQrDw@ie zo>6)gI&!<#A}@l1%HF6|U9Zxtx89=_@!z<$_GoAt-Ns`2Cz%`fXP@4BaR1JGZFB1K z6hM){)v2~Mb@jcec4F!V{h3o80+*(WS$P%I_5qaf?1{2&%{}~(LyEGT7cJ>8zbLB7 zZj53F)eS7<$BTwaR2!`oPbHfx9{wvNtndm2NB{1-0Gt>+R5wFZ_P}~%0cDBKIn9r`e)2 zkl0ZBa5(B+Xf>FmO19Yf%t{I%&>rDV!&5`m#`ESfJl7KsGp>*;3@<9v&03`B5NOfp zn5;z|S~5sWTl#F#l<%Mi%R&A!N<~ZFpb9F>n*?qV_$2}t2t;DL3(VzlA-49(0nATF z;)}0ND${+No~JFCr!8UAEZ;}5Xviu2sm$Y#9^5UFb#LiDKRkBCfXXj8-s6>;bH5>+ z7r#Q3d_UZt9K=VwGc3WZcrPm49}m(+Ws(+4jDkmK_hjoNsgOC6l}cBdt(W&?vkq=q zR^LKxzl1(O-7M~quYvOE5(@O2rA5*x*Bva9Y^hXl3e1rfOsVwQO1T!az>?is(}N|e zL;l(!QG^y_VnO)&Bn?SoL=6SDUvX-+(EeGNtXER0%EhdXRKY7Ety{);B5lb>sHx!Y zxmfwAVOJ3@0>>13VB!?k@;2VkL;`PL2zMe0XHV~9mYrh5Ps8vt?eS1&51I?5hO-dN zMBW4K9sViO6FK&{p2$1FPsKI16}N5@1S-1LJxFcj59V+OhMm{jX9hF3yKR$HZW9UG z-GV92)0fC?8dz|~EIaNkQyqp)&b@3oBBnaFeHOL6gJ=Eq#%dxB$r*re;|@*g#4eoq z%SNT1!*{}$4zzS;@EnLC9O?q$P>ywUczWzdo}dPjVbDnEtcJ~=SfNY zs3C5>y;!XY_@=F3RXjse-xO4`T&XxM@4GY$TKXFNZPsX?+GQqw@2!lyPqb*6%U>n% zApueq%S07;5zI-)dFoGD(g5-y0Tv&FuBi|A+Sz0DV{X#Ms0CXu0src49X!L2FCLh! z%U`4E(p>so5edq{J;0`WnfRG(T0Ws6Y0d0vv{f3M{jJ`PjJ9uRGFtf*9S_c2gAowo zzC+x7Lck{Q>jb)n!HbJ5rjC1{S@!Yjo2C4?mrTsQdi#?t#qFyMe0Tf0iPk-QX%3r< z1iUD=6xcE+9e7h-$oKvx?qC{eJ#Vy+51z(>T5>LOyiFMz@*?rKry+mY z<&^zvwD};%7a7B}Z^uP_b}PHPhowynyIJ`gRNC9K4)qM+g>1mFCJHIJ1pF&E{E4_$ zs`XZFe;#%cyzR^M<)`SmtEvAU8snxOZAVEkF>boXE(IPrFjJT0=;Z=|J_kn@ypB6= z!98{n=k7pl*xw$60tl^mnRwjOivOg`En9Jq+lX@;*|DTZ6PtL~C69!|2iEYrA??64 zYruCmO?nmH!zcf={cZGOcgt(m_h*j#*xc?N@Hc3J^VE3H?zpk z?%ct0w8sW8P5!jG>@<8IdJRtv4FA;d7r4Xle>7a3aYpz+c4=t@h%GV*&drwmcl-~WG+Vb&%>d4^J&T^@ZAmZCR+C}#Qkm#dS1Ay^Yi<& z$w>@;050-}AQN|yJug^YW+L;P{ds!GzwI)|F+SR^vj2!AHGQBCvio+0>4#R^0w;T0 z?T@;=?tF`i334Cqk>7~AkNkB=Iq;630sr|LWw{X^^BvTdb?>4XOy2ydw9iK)4!y7XEu;!+N6?JLaxd0+aryMjic003{f9Q zINeE$p=ER3l7&v%JGOK@EDK}VSU2T=qTdO;$my8d-#{`aH*q%1vKrolI%$)rXF3_C zW5`c1pHm$Tkn~F@-8k!p?6r;4kUylll-M+JmOB#6?+j58$xUP3aNiZWDAXqFXIHZr z8xjzQ){HNaC5y@89A<5m&I`yaF4c9t@!Q~G2y-#ye_-?r```icWEwsX3FhHPJ9s$4 zJdDS9xESy-5%G{D4S@#(JXkExdGK&)A3Q)yF&<#2>!y2i2M@=XhvP9GrUD*LL_8$e zO1=jU623;k!R38$aI%MkA?Dy8c5rZtIXE5Tpcrrf=>?jwhyyX{<9l1l0o9Ev*f zu~S*$h5z) zNYZ(X500xJri#Rfo$BuO_cgW717IeV3psSLk7y(mRrNXOgyQj9=%Y z7A}5GQk>-CFQ_q$&|E+c7ADi3W5x;1Nadu{YD$mks}!uM`5fY%SZT;+t=7+;Tg>~} z6guazvov8$30k%DL78)tDqU+<$~CG_Q;zmIm2xF0UV46qghy|ZwpA+EJlm|5Oa9CZ z>BQdUFVYNW0R9!X`(pqN8?~ff&@KE%b?l6Q<%3@mi7UdANHEa9fgB}a7GqS~TVoh$ zqrh!rNC0Qi7pboRr<5?Y6;MmmhH+;>|NmBR4DN3ccPDx5Vf~VERBz|QS7h4GVdM43 zn5oLhFxjaxw8A;>*^~7pe-gd8({VgUIBnUGqn^G740{j_N23(?^c&nt$GSrE_b7ar zde6g7$4hjKHGP6(ej|(MsdvmZB(FFZWcnVheRQ@tNqlg=ee(0Fw>Vj)RO~m4N%@P! zu!Sa1f)!%0DIWXZ$!l(5HQs3J5*HAq8jGD1AhF z9|jyX+9RRlf_}))GFhTnF#*Dh%8{(-L=$q*At^-L4U&vb`#t2rkibMOB0^A$ILWn$ zbn^YE7P|gT4f7s0yLWpmlt5hWMV*t5#hJcCUNsVY;&cx|Wfn{Ho=%310{4oKzVIonODCavt6 zZ{+Akk=G^FrVYy&HpYykkv7v7ycGNtd9a?JaXeEf6b|8c1iu3A@j`nv%an>aq)|B< zD5KhxWXtle0Fb2hKd3<%oNub6_p*i0LwL4!#z&^npR}lw$WTGee%!r46uRIdbx7av Wzdd-5$n#pGbp}h*hmE|E9{yjM`&w53 literal 0 HcmV?d00001 diff --git a/logic/grammars/__pycache__/__init__.cpython-39.pyc b/logic/grammars/__pycache__/__init__.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..463ccca7afaf606c4c615c6048a30983cd489214 GIT binary patch literal 147 zcmYe~<>g`kf;+GGCV}Y3AOaaM0yz#qT+9L_QW%06G#UL?G8BP?5yUSG{qp>x?BasN z": + return (not self.left.eval(assignment)) or self.right.eval(assignment) + if self.op == "<->": + return self.left.eval(assignment) == self.right.eval(assignment) + + +@dataclass +class Formula: + alphabet: Set[str] + root: Expr + + def models(self) -> Iterable[Iterable[str]]: + alphabet = tuple(self.alphabet) + for bools in product((True, False), repeat=len(alphabet)): + assignment = {atom: v for atom, v in zip(alphabet, bools)} + if self.root.eval(assignment): + yield assignment + + +class FormulaBuilder(ParseTreeVisitor): + alphabet: Set[str] + + def __init__(self) -> None: + self.alphabet = set() + + def visitParenth(self, ctx: OParser.ParenthContext): + return self.visit(ctx.expr()) + + def visit_bin_op(self, ctx): + return BinExpr(ctx.op.text, self.visit(ctx.expr(0)), self.visit(ctx.expr(1))) + + def visitLog_neg(self, ctx:OParser.Log_negContext): + return NotExpr(self.visit(ctx.expr())) + + def visitLog_or(self, ctx: OParser.Log_orContext): + return self.visit_bin_op(ctx) + + def visitLog_impl(self, ctx: OParser.Log_implContext): + return self.visit_bin_op(ctx) + + def visitLog_iff(self, ctx: OParser.Log_iffContext): + return self.visit_bin_op(ctx) + + def visitLog_and(self, ctx: OParser.Log_andContext): + return self.visit_bin_op(ctx) + + def visitAtom(self, ctx: OParser.AtomContext): + text = ctx.getText() + self.alphabet.add(text) + return AtomExpr(text) + + def build(self, tree): + expr = self.visit(tree) + return Formula(self.alphabet, expr) + + +def parse(text: str): + input_stream = InputStream(text) + lexer = OLexer(input_stream) + stream = CommonTokenStream(lexer) + parser = OParser(stream) + tree = parser.expr() + formula = FormulaBuilder().build(tree) + return formula diff --git a/ontology.py b/ontology.py index 2872ba0..d6da9b3 100644 --- a/ontology.py +++ b/ontology.py @@ -1,14 +1,14 @@ -from typing import Iterable, Set, Union +from typing import Dict, Iterable, Set, Union models = None DL_ATOMS = "abc" -def set_models(alphabet: Iterable[str], v: Iterable[Iterable[str]]): +def set_models(alphabet: Iterable[str], v: Iterable[Dict[str, bool]]): global models, DL_ATOMS DL_ATOMS = "".join(alphabet) - models = tuple(set(model) for model in v) + models = tuple(set(atom for atom, v in model.items() if v) for model in v) def propagate(atoms: Set[str]) -> Set[str]: diff --git a/programs/a.ont b/programs/a.ont new file mode 100644 index 0000000..835e57f --- /dev/null +++ b/programs/a.ont @@ -0,0 +1 @@ +((a | -a) & (b | -b)) \ No newline at end of file diff --git a/programs/a.py b/programs/a.py deleted file mode 100644 index 0e3a59b..0000000 --- a/programs/a.py +++ /dev/null @@ -1,7 +0,0 @@ -"ab" -( -"", -"a", -"b", -"ab", -) \ No newline at end of file diff --git a/programs/b.ont b/programs/b.ont new file mode 100644 index 0000000..66d32a4 --- /dev/null +++ b/programs/b.ont @@ -0,0 +1 @@ +a | b \ No newline at end of file diff --git a/programs/b.py b/programs/b.py deleted file mode 100644 index ea92ebc..0000000 --- a/programs/b.py +++ /dev/null @@ -1,6 +0,0 @@ -"ab" -( -"a", -"b", -"ab", -) \ No newline at end of file diff --git a/programs/c.lp b/programs/c.lp new file mode 100644 index 0000000..cc84761 --- /dev/null +++ b/programs/c.lp @@ -0,0 +1,3 @@ +a, b. +a :- x. +b :- y. diff --git a/programs/c.ont b/programs/c.ont new file mode 100644 index 0000000..7613ee5 --- /dev/null +++ b/programs/c.ont @@ -0,0 +1 @@ +(b -> x) & (a -> y) diff --git a/propagator.py b/propagator.py index d9ae52b..0458d98 100644 --- a/propagator.py +++ b/propagator.py @@ -46,6 +46,11 @@ class OntologyPropagator: self.symbolic_atoms_inv = {v: k for k, v in self.symbolic_atoms.items()} self.theory_atoms_inv = {v: k for k, v in self.theory_atoms.items()} + + # Make false always false + false_lit = self.theory_atoms_inv["false"] + init.add_clause([-false_lit]) + # Might only need to watch just theory atoms / just symbol atoms but for now # watching everything is easier for lit in chain(self.symbolic_atoms, self.theory_atoms): @@ -165,7 +170,8 @@ class OntologyPropagator: if shrink is None: self.conflict(pcontrol) return - shrink = tuple(self.theory_atoms_inv[atom] for atom in shrink) + # Theory atom might not be present if it was removed by clingo for some reason... + shrink = tuple(self.theory_atoms_inv[atom] for atom in shrink if atom in self.theory_atoms) if any(self.assignment.get(abs(lit)) for lit in shrink): self.conflict(pcontrol) return @@ -220,8 +226,11 @@ def add_external_atoms(program: str) -> str: """ # Using .signatures here because symbols is unreliable # E.g. a rule with the single rule `a :- a.` will not generate a symbol for an atom + # Dummy rules of the form atom :- &o{false} must be added for atoms that do not appear + # In the head of a rule as Clingo may decide to unify these with theory atoms for whatever reason + # This seems to be a fix for now external_atoms = "\n".join( - f"{atom} :- &o{{{atom}}}." + f"{atom} :- &o{{{atom}}}. {atom} :- &o{{false}}." for atom in (sig for sig, _, _ in control.symbolic_atoms.signatures) ) return theory_grammar + program + "\n" + external_atoms @@ -259,15 +268,17 @@ def solve(program: str, O_alphabet: Iterable[str], O_models: Iterable[Iterable[s def main(): from sys import argv from os.path import splitext + from logic import logic assert len(argv) == 2, "Please provide an .lp file as an argument" lp_filename = argv[1] - models_filename = splitext(lp_filename)[0] + ".py" + models_filename = splitext(lp_filename)[0] + ".ont" with open(lp_filename, "rt", encoding="utf8") as lp_fo: with open(models_filename, "rt", encoding="utf8") as models_fo: - alphabet = eval(models_fo.readline()) - models = eval(models_fo.read()) - solve(lp_fo.read(), alphabet, models) + models_text = models_fo.read() + formula = logic.parse(models_text) + models = tuple(formula.models()) + solve(lp_fo.read(), formula.alphabet, models) if __name__ == "__main__": diff --git a/test_output/a.accept b/test_output/a.accept new file mode 100644 index 0000000..ddd45bf --- /dev/null +++ b/test_output/a.accept @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +b a diff --git a/test_output/a.out b/test_output/a.out new file mode 100644 index 0000000..ddd45bf --- /dev/null +++ b/test_output/a.out @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +b a diff --git a/test_output/b.accept b/test_output/b.accept new file mode 100644 index 0000000..ddd45bf --- /dev/null +++ b/test_output/b.accept @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +b a diff --git a/test_output/b.out b/test_output/b.out new file mode 100644 index 0000000..ddd45bf --- /dev/null +++ b/test_output/b.out @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +b a diff --git a/test_output/c.accept b/test_output/c.accept new file mode 100644 index 0000000..adcac42 --- /dev/null +++ b/test_output/c.accept @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +a b x y diff --git a/test_output/c.out b/test_output/c.out new file mode 100644 index 0000000..adcac42 --- /dev/null +++ b/test_output/c.out @@ -0,0 +1,2 @@ +ALL FINISHED, ALL ANSWER SETS: +a b x y diff --git a/tests.py b/tests.py old mode 100644 new mode 100755 index 426ae83..f9f2a60 --- a/tests.py +++ b/tests.py @@ -1,10 +1,11 @@ #!/usr/bin/env python3 from glob import glob -from os import system +from os import remove, system from functools import partial +from pathlib import Path from sys import argv, stderr -from os.path import splitext +from os.path import splitext, basename eprint = partial(print, file=stderr) @@ -14,7 +15,26 @@ if len(argv) >= 2 and argv[1] == "-a": else: accept = False -system("mkdir -p tests") +TEST_FOLDER = "test_output" + +system(f"mkdir -p {TEST_FOLDER}") + +system(f"rm -rf {TEST_FOLDER}/*.out") for lp in glob("programs/*.lp"): - base = splitext(lp)[0] + base = basename(splitext(lp)[0]) + out_path = Path() / TEST_FOLDER / f"{base}.out" + accept_path = Path() / TEST_FOLDER / f"{base}.accept" + diff_path = Path() / TEST_FOLDER / f"{base}.diff" + system(f"python3 propagator.py {lp} > {out_path}") + + if accept: + system(f"cp {out_path} {accept_path}") + else: + system(f"diff {out_path} {accept_path} > {diff_path}") + + +for diff in glob(f"{TEST_FOLDER}/*.diff"): + with open(diff, "tr", encoding="utf8") as diff_fo: + if diff_fo.read(1) == "": + remove(diff)