Souffle Converter to DNF does not handle some programs

[mihaibudiu]

For example the following program:

.decl A(a: number)
.decl B(b: number)
.decl C(c: number)
.decl R(r: number)

R(X) :- A(X) , ! (B(X), C(X)).

[mihaibudiu]

@Argc0 : do you mean to support such programs as well? The DNF converter does not seem to handle this case.

[mihaibudiu]

BTW: the error is:

Traceback (most recent call last):
  File "../tools/souffle_converter.py", line 1428, in <module>
    main()
  File "../tools/souffle_converter.py", line 1424, in main
    convert(args.input, args.out, options, args.d)
  File "../tools/souffle_converter.py", line 1386, in convert
    converter.process(tree)
  File "../tools/souffle_converter.py", line 1362, in process
    self.process_decl(decl)
  File "../tools/souffle_converter.py", line 1299, in process_decl
    self.process_rule(rule)
  File "../tools/souffle_converter.py", line 1173, in process_rule
    convertedDisjunctions += [self.convert_terms(x)]
  File "../tools/souffle_converter.py", line 1051, in convert_terms
    (term, postpone) = self.convert_term(t)
  File "../tools/souffle_converter.py", line 1034, in convert_term
    (not_term, postpone) = self.convert_term(not_term)
  File "../tools/souffle_converter.py", line 1038, in convert_term
    raise Exception("Disjunction not yet handled")

[gfour]

The DNF converter in souffle_converter.py does not currently handle all patterns of DNF conversion. We added it as a temporary/cheap workaround to support the non-DNF patterns found in Doop, until proper support for full disjunction is added (#98). When that support arrives, I understand that DNF conversion should be done differently (if at all).

Of course, handling more or all non-DNF patterns would be nice to have. This particular pattern !(A and B) should become (!A or !B), which means the transformer must apply De Morgan's laws to fix this issue.

[Argc0]

In case, you wish to solve temporarly this problem by having some changes in souffle_convert.py I suggest:

def convert_term(self, term):
        """Convert a Souffle term.  Returns a tuple with two fields:
        - the first field is the string list representing the conversion of multiple or not conjunctions
        # the first field is the string representing the conversion
        - the second field is a boolean indicating whether the term evaluation should be postponed.
          This is because in Souffle the order is irrelevant, but in DDlog is not.
        """
        # print term.tree_str()
        lit = getOptField(term, "Literal")
        if lit is not None:
            (lit_term, postpone) = self.convert_literal(lit)
            return ([lit_term], postpone)
           #return self.convert_literal(lit)
        not_term = getOptField(term, "Term")
        if not_term is not None:
            (not_term, postpone) = self.convert_term(not_term)
            listnot_term = []
            for n in not_term:
                listnot_term.append("not " + n)
            return (listnot_term, postpone)
            #return ("not " + not_term, postpone)
        disj = getOptField(term, "Disjunction")
        if disj is not None:
            #it is a conjunction because a check for a disjunction has already been done in process_rule
            termsAst = getListField(disj, "Term", "Conjunction")
            terms = self.convert_terms(termsAst)
            #returns postpone False because in convert_terms the order has been restored
            return (terms, False)
            #raise Exception("Disjunction not yet handled")
        raise Exception("Unhandled term " + term.tree_str())

    def convert_terms(self, terms):
        result = []
        tail = []
        for t in terms:
            (term, postpone) = self.convert_term(t)
            for ter in term:
                if postpone:
                    tail.append(ter)
                else:
                    result.append(ter)
        return result + tail

It solves this bug for the moment.