Trying to parse non-DNF disjunctions

Argc0 commented 5 years ago

I was trying myself somes examples of disjunction of non-DNF form. An examples is:

.decl AMethod(?simplename:symbol, ?descriptor:symbol, ?type:symbol, ?method:symbol)
.decl BMethod(?class:symbol, ?superclass:symbol)
.decl CMethod(?ref:symbol, ?interface:symbol)

AMethod(?simplename, ?descriptor, ?type, ?method) :-
    AMethod(?simplename, ?descriptor, ?supertype, ?method),
    (BMethod(?type, ?supertype) ; CMethod(?type, ?supertype)).

So, I started from uncommenting the line from the grammar rule in souffle-grammar.pg:

Term: Literal
    | "!" Term
    | "(" Body ")" // TODO
    ;

When I was trying to simple run the souffle_python.py, to see if the example can pass the parglare an error appeared:

...
In state 74:FunctionCall and input symbol ')' can't decide which reduction to perform: '133: Literal = FunctionCall' or '107: Arg = FunctionCall'.
Traceback (most recent call last):
  File "souffle_converter.py", line 1400, in <module>
    main()
  File "souffle_converter.py", line 1396, in main
    convert(args.input, args.out, args.prefix, args.d)
  File "souffle_converter.py", line 1354, in convert
    parser = getParser(debug)
  File "souffle_converter.py", line 114, in getParser
    parglareParser = parglare.Parser(g, build_tree=True, debug=debugParser)
  File "/home/argc0/.local/lib/python2.7/site-packages/parglare/parser.py", line 88, in __init__
    self._check_parser()
  File "/home/argc0/.local/lib/python2.7/site-packages/parglare/parser.py", line 118, in _check_parser
    raise RRConflicts(unhandled_conflicts)
parglare.exceptions.RRConflicts: 
Reduce/Reduce conflicts in following states: set([74])

It seems that when I uncomment the line obove the grammar rule Literal and Arg are conflicted for the reduction of FunctionCall.

I do not understand why exactly this error appeared, but I solved it temporarily by changing the rule:

Literal : Arg Relop Arg
        | Atom
        | FunctionCall
        | TRUE
        | FALSE
        ;

to:

Literal : Arg Relop Arg
        | Atom
        | Arg
        | TRUE
        | FALSE
        ;

and it pass the parglare parser, but I am not sure how fair this change would be and I am trying to find a way so the grammar you wrote won't need a lot of changes, so at least can accept parentheses with or without disjunction.

ryzhyk commented 5 years ago

@mbudiu-vmw should be able to help with the parser question, but I am a bit confused as to what you are trying to accomplish. Even if the parser can recognize parentheses, disjunction, etc., DDlog does not support them at the moment (we are hoping to add support for arbitrary Boolean structure in the rules soon). It seems, the only situation where parsing parenthesis could be useful is in Boolean expressions like (x = 5; y > z), since DDlog does support those.

gfour commented 5 years ago

@ryzhyk Doop contains many rules like the following:

_MethodLookup_WithLen(?simplename, ?descriptor, ?type, ?method, n + 1) :-
    (DirectSuperclass(?type, ?supertype) ;
     DirectSuperinterface(?type, ?supertype)),
    _MethodLookup_WithLen(?simplename, ?descriptor, ?supertype, ?method, n),
    !MethodImplemented(?simplename, ?descriptor, ?type, _).

These are not in DNF form but can be converted by a preprocessor in the Souffle converter that feeds the converted DNF rules to the rest of the conversion process (@Argc0 is working on that). I think this preprocessor would also address #98.

ryzhyk commented 5 years ago

Understood. We considered doing the same, but held back, since we plan to support disjunctions in DDlog eventually; however if it is an important feature for you, I agree it makes sense to have at least a temporary implementation in the converter. Again, @mbudiu-vmw should be able to recommend the best way to do it.

Note, for performance, you do not want to compile:

X :- (A;B),C,D.

into

X :- A,C,D.
X :- B,C,D.

but rather

Y :- A.
Y :- B.
X :- Y,C,D.