Menu ▾ ▴

#103 forall bug

open
nobody
query language (13)
5
2008-09-10
2008-09-10
Jonathan Kilgour
No

Previously listed as a lazy loading bug, there is actually a logical bug in the processing of some forall queries. Consider the two queries:

Q1 ($w word)(forall $t turn): $t^$w
Q2 ($w word)(forall $t turn): !$t^$w

In the attached corpus, both queries should return one result: there is in fact one word that is contained within the only turn in the corpus, and one word that is not a descendant of any turn. Q2 does return the correct result, but Q1 always returns zero results: this query does cause the correct files to be loaded, but it is not a lazy loading problem: it occurs when the appropriate files are pre-loaded too.

Discussion

  • Jonathan Kilgour

    Jonathan Kilgour - 2008-09-10
     
    bugreport.zip

  • Jonathan Kilgour

    Jonathan Kilgour - 2008-09-10

    Agh! The bug report should read...

    ..Q1 always returns zero results: this query does *not* cause the
    correct files to be loaded, but it is not a lazy loading problem..

     

  • Jonathan Kilgour

    Jonathan Kilgour - 2008-09-10

    Bug present back to at least v1.2.9 (2004).

     

  • Jonathan Kilgour

    Jonathan Kilgour - 2008-09-15

    Debugging observations:

    On execution, Q1's main iterator runs over all elements that dominate each word. If an element is found that dominates a word but is not a turn, the word is removed from the result list. Obviously an incorrect algorithm!

    My first attempt to fix was to ignore element pairs that fail if they do not match their type declarations. But though that improves matters, internal bookkeeping is affected, and anyway the algorithm still fails to iterate over all turns (only those that dominate a word which defeats the purpose!).

    Engine.java (stage 1) always puts type iterators at the end of the dnf. Moving them to the start doesn't appear to help (maybe they are still reordered) but in any case it seems an odd approach. Perhaps more importantly it seems type conditions are treated in exactly the same manner to the conditions on the right side of the colon (that is clearly invalid for forall queries).

    Engine.java (stage 4) fails to use quantified variables when it attempts to order iterators, explicitly ordering only 'free' variables. I don't understand why. Adding the quantified variables means that the correct files are lazy loaded but the search algorithm still fails.

    ...