<< Back to previous view

[LOGIC-112] Incorrect results with tabled resolution Created: 05/Feb/13  Updated: 28/Jul/13  Resolved: 13/Mar/13

Status: Closed
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Major
Reporter: Reinout Stevens Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None

org.clojure/clojure "1.3.0"
org.clojure/core.logic "0.8.0-rc2"

Attachments: File tabling-test.clj    
Patch: Code


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)
damp.tabling-test> (test-1)
(:baz :quux)

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

Comment by David Nolen [ 13/Feb/13 3:10 PM ]

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

Comment by David Nolen [ 11/Mar/13 8:37 AM ]

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.

Comment by David Nolen [ 13/Mar/13 8:51 AM ]

fixed, http://github.com/clojure/core.logic/commit/53cbfca4b7062e09d7c7ff43fccec70e46d36ea1

Generated at Tue Oct 17 08:27:52 CDT 2017 using JIRA 4.4#649-r158309.