core.logic

Incorrect results with tabled resolution

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Major Major
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None
  • Environment:
    org.clojure/clojure "1.3.0"
    org.clojure/core.logic "0.8.0-rc2"
  • Patch:
    Code

Description

We (authors of damp.qwal and damp.ekeko) are trying to track the cause of some indeterminism with respect to the solutions to a path query over a control flow graph. To this end, we wrote a small test case that mimics the qwal part of the query. This test case works under core.logic 0.7.5, but exhibits incorrect behavior in the latest release.

The test case illustrates two problems:
First, the solutions to two logically equivalent path queries return differ. The query that uses predicate test-2 returns the correct amount of solutions (4 nodes encountered on the single path through a graph).
The query that uses predicate test-1 returns just 2 nodes.

damp.tabling-test> (test-1)
(:baz :quux)
damp.tabling-test> (test-2)
(:foo :bar :baz :quux)

Both queries skip an arbitrary number of nodes (using patho), capture a node to obtain a solution (through unification), and skip an arbitrary number of nodes.
The predicates only differ in the last step: either this is achieved by including 'patho' as the last element in the last that is passed to solve-goals, or by calling 'patho' separately after the call to solve-goals. Logic-wise, both queries should be equivalent. Note that omitting 'tabled' from the definition of 'patho' causes the tests to behave as expected.

Second, we encountered a minor issue concerning the number of results returned by the faulty query. This sometimes changes when the file is recompiled.

damp.tabling-test> (test-1)
(:quux)
;;recompile
damp.tabling-test> (test-1)
(:baz :quux)

More comments can be found in the code for the test case that is attached.

Activity

David Nolen made changes -
Field Original Value New Value
Description We (authors of damp.qwal and damp.ekeko) are trying to track the cause of some indeterminism with respect to the solutions to a path query over a control flow graph. To this end, we wrote a small test case that mimics the qwal part of the query. This test case works under core.logic 0.7.5, but exhibits incorrect behavior in the latest release.

The test case illustrates two problems:
First, the solutions to two logically equivalent path queries return differ. The query that uses predicate test-2 returns the correct amount of solutions (4 nodes encountered on the single path through a graph).
The query that uses predicate test-1 returns just 2 nodes.

damp.tabling-test> (test-1)
(:baz :quux)
damp.tabling-test> (test-2)
(:foo :bar :baz :quux)

Both queries skip an arbitrary number of nodes (using patho), capture a node to obtain a solution (through unification), and skip an arbitrary number of nodes.
The predicates only differ in the last step: either this is achieved by including 'patho' as the last element in the last that is passed to solve-goals, or by calling 'patho' separately after the call to solve-goals. Logic-wise, both queries should be equivalent. Note that omitting 'tabled' from the definition of 'patho' causes the tests to behave as expected.

Second, we encountered a minor issue concerning the number of results returned by the faulty query. This _sometimes_ changes when the file is recompiled.

damp.tabling-test> (test-1)
(:quux)
;;recompile
damp.tabling-test> (test-1)
(:baz :quux)


More comments can be found in the code for the test case that is attached.
We (authors of damp.qwal and damp.ekeko) are trying to track the cause of some indeterminism with respect to the solutions to a path query over a control flow graph. To this end, we wrote a small test case that mimics the qwal part of the query. This test case works under core.logic 0.7.5, but exhibits incorrect behavior in the latest release.

The test case illustrates two problems:
First, the solutions to two logically equivalent path queries return differ. The query that uses predicate test-2 returns the correct amount of solutions (4 nodes encountered on the single path through a graph).
The query that uses predicate test-1 returns just 2 nodes.

{code}
damp.tabling-test> (test-1)
(:baz :quux)
damp.tabling-test> (test-2)
(:foo :bar :baz :quux)
{code}

Both queries skip an arbitrary number of nodes (using patho), capture a node to obtain a solution (through unification), and skip an arbitrary number of nodes.
The predicates only differ in the last step: either this is achieved by including 'patho' as the last element in the last that is passed to solve-goals, or by calling 'patho' separately after the call to solve-goals. Logic-wise, both queries should be equivalent. Note that omitting 'tabled' from the definition of 'patho' causes the tests to behave as expected.

Second, we encountered a minor issue concerning the number of results returned by the faulty query. This _sometimes_ changes when the file is recompiled.

{code}
damp.tabling-test> (test-1)
(:quux)
;;recompile
damp.tabling-test> (test-1)
(:baz :quux)
{code}

More comments can be found in the code for the test case that is attached.
Hide
David Nolen added a comment -

Ok, I've confirmed the issue. Will look into it.

Show
David Nolen added a comment - Ok, I've confirmed the issue. Will look into it.
David Nolen made changes -
Status Open [ 1 ] In Progress [ 3 ]
Hide
David Nolen added a comment - - edited

I believe I have found the issue as well as the source of the nondeterminism. When we switched to sets away from lists for the cache I didn't fully think through the implications. The nondeterminism arises from the use of sets. We actually want a hybrid cache datatype that works like a list but can efficiently check for the existence of a cached answer w/o scanning the list.

Show
David Nolen added a comment - - edited I believe I have found the issue as well as the source of the nondeterminism. When we switched to sets away from lists for the cache I didn't fully think through the implications. The nondeterminism arises from the use of sets. We actually want a hybrid cache datatype that works like a list but can efficiently check for the existence of a cached answer w/o scanning the list.
David Nolen made changes -
Resolution Completed [ 1 ]
Status In Progress [ 3 ] Resolved [ 5 ]
Alex Miller made changes -
Patch None [ 10000 ] Code [ 10001 ]
David Nolen made changes -
Status Resolved [ 5 ] Closed [ 6 ]

People

Vote (0)
Watch (2)

Dates

  • Created:
    Updated:
    Resolved: