<< Back to previous view

[LOGIC-165] Add non-interleaving version of conde Created: 21/Dec/14  Updated: 21/Dec/14

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

Type: Enhancement Priority: Major
Reporter: David Nolen Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

For validation use cases having depth first search as an option would be very useful.






[LOGIC-162] FD logic doesn't always return all solutions Created: 20/Oct/14  Updated: 09/Nov/14

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

Type: Defect Priority: Major
Reporter: Viktar Basharymau Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: finite-domains
Environment:

org.clojure/core.logic 0.8.8



 Description   

Given the following code

(run* [x11 x12 x13 
       x21 x22     x24
       x31     x33 x34
           x42 x43 x44]
      (fd/in x11 x12 x13 x21 x22 x24 x31 x33 x34 x42 x43 x44 (fd/interval 1 9))
      (fd/eq (= (+ x11 (/ x12 x13))   5)
             (= (+ x21 (/ x22   2)) x24)
             (= (+ x31 (/   6 x33)) x34)
             (= (+   4 (/ x42 x43)) x44)
             (= (+ x11 (/ x21 x31))   4)
             (= (* x12 (/ x22   6)) x42)
             (= (+ x13 (-   2 x33)) x43)
             (= (+ (-  5 x24) x34)  x44)))

I have {{([1 4 1 3 6 6 1 1 7 4 2 6] [2 6 2 4 6 7 2 1 8 6 3 6])}} as a result.

However, as soon as I change (fd/interval 1 9) to (fd/interval 0 9), the result becomes an empty sequence. However, I expect it to include at least the two aforementioned solutions.



 Comments   
Comment by David Nolen [ 21/Oct/14 4:34 AM ]

It would help if you could confirm that the issue is present without using fd/eq - which is just macro sugar. Writing out the long form is tedious but it will help isolate the issue. Thanks.

Comment by Viktar Basharymau [ 21/Oct/14 8:08 AM ]

I actually suspect that the bug is in `fd/eq`. Here is a smaller test case:

(run* [q]
      (fd/in q (fd/interval 1 2))
      (fd/eq (= (/ q q) 1)))

It returns `(1 2)` as expected, but as soon as I change `fd/interval` to `0 2`, it returns an empty seq.

Comment by David Nolen [ 09/Nov/14 6:09 PM ]

Thanks for the minimal case, yeah looks like an issue with fd/eq as it works fine if you write it out long hand.





[LOGIC-156] Two consecutive calls to run* return different results Created: 22/Feb/14  Updated: 05/Mar/14

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

Type: Defect Priority: Major
Reporter: Mauro Lopes Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: bug

Attachments: File core.clj     File core.clj    

 Description   

Calling run* twice with the same input may return different results for no apparent reason.
See attachment.



 Comments   
Comment by David Nolen [ 05/Mar/14 9:19 AM ]

The problematic code incorrectly uses finite domain operations on fresh variables that have not be assigned domains. Can we get an updated version of the problematic code that demonstrate the issue after the corrections?

Comment by Mauro Lopes [ 05/Mar/14 9:25 PM ]

Sure. I have just added a new code version with finite domains assigned to each variable that is involved in an fd operation. The problem persists.





[LOGIC-154] walk* of an empty set overflows the stack Created: 31/Dec/13  Updated: 31/Dec/13

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

Type: Defect Priority: Major
Reporter: Kevin Downey Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

I noticed this issue when asserting a relation with an empty set in it in the new pldb stuff, the minimal case I have is (walk* empty-s #{})






[LOGIC-144] Extending cljs.core.logic with all of the functionality from clojure.core.logic Created: 19/Nov/13  Updated: 04/Dec/13

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

Type: Enhancement Priority: Major
Reporter: Adrian Medina Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

Repo I've been working from is here: https://github.com/aamedina/cljs.core.logic

I've followed the code layout in clojure.core.logic pretty much verbatim, compensating for ClojureScript necessities, moved macros into sister .clj files. I have no hard opinions about the best way to organize the macros for each file, the way I do it is just the way I've found easiest, because then you don't have to namespace qualify every syntax quoted form that references a function in the sister .cljs file.

Additionally I ported all of the clojure.core.logic tests with clojurescript.test.



 Comments   
Comment by Adrian Medina [ 27/Nov/13 10:43 PM ]

So I've updated the repo to reflect a more faithful adherence to the existing cljs.core.logic code conventions and organization. I'd appreciate any insight into how to potentially optimize the code to run more on par with the JVM.

Comment by David Nolen [ 04/Dec/13 1:09 AM ]

What kinds of performance problems are you observing? Do you have a particular benchmark that you're running?

Comment by Adrian Medina [ 04/Dec/13 12:18 PM ]

Appendo and membero are particularly slow.

(dotimes [i ie5] (run* [q] (== q true))) takes around ~4500ms, which is about 10x slower than the JVM.

After profiling, I've discovered the problem - pretty standard recursion optimizations are necessary, it's re-walking (by reunifying) lvars recursively as the code is executed. E.g.,
for appendo, (run 5 [q] (fresh [x y] (appendo x y q))) will expand into something like..

((_0) (_0 . _1) (_0 _1 . _2) ... ))

and it's slow because every new list is actually re-walking every previously unified lvar again.

I'll have more time to investigate this over the weekend, but I think it might be as simple as not generating unique lvars by default, since then the identical? for unification check should catch any attempted walk.





[LOGIC-142] Unified map values are returned as LVar rather than the unified value in ClojureScript Created: 29/Sep/13  Updated: 29/Sep/13

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

Type: Defect Priority: Major
Reporter: Darrick Wiebe Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None
Environment:

ClojureScript



 Description   

This works correctly in core.logic for clojure:

(run 1 [q]
     (fresh [v]
            (== v 1)
            (== {:x v} q)))

In ClojureScript, I get this though:

({:x <lvar:v_4>})





[LOGIC-140] compile time occurs check for pattern matching Created: 25/Jun/13  Updated: 25/Jun/13

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

Type: Defect Priority: Major
Reporter: David Nolen Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

Claire Alvis correctly pointed out that it's easy to make a mistake when you have many clauses and accidentally use parameter name in a match for that parameter - we could easily do a compile time occurs check for these cases.






[LOGIC-136] Make benchmark suite as easy to run as `lein test` Created: 09/May/13  Updated: 09/May/13

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

Type: Enhancement Priority: Major
Reporter: Austin Haas Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

`lein benchmark` (or some other non-lein-based incantation) prints a report listing the name of each benchmark and its timing.

Example:

$ lein benchmark
membero 2839
zebra 152738
$ lein benchmark comparison-report {:baseline "benchmark-5.9.2013-1"
                                    :runs 5
                                    :diffs-only true
                                    :threshold 25} ; only consider different if the delta is > 25 ms.                                     
membero +68ms
zebra -122ms
$ lein benchmark {:pretty true}
Thu May  9 11:21:41 PDT 2013

Linux mars 2.6.32-5-amd64 #1 SMP Fri Feb 15 15:39:52 UTC 2013 x86_64 GNU/Linux

java version "1.7.0_21"
Java(TM) SE Runtime Environment (build 1.7.0_21-b11)
Java HotSpot(TM) 64-Bit Server VM (build 23.21-b01, mixed mode)

membero     2839 ms
zebra     152738 ms

I haven't looked for any Clojure benchmarking libs, but ideally this would be a trivial script that automates the repetitive manual task of running benchmark tests. Unlike the test suite, we aren't looking for binary success or failure. Every run will generate unique results, so the script should accommodate a fuzzier comparison.

A "pretty" output that includes system info would be great for bug reports.



 Comments   
Comment by David Nolen [ 09/May/13 1:44 PM ]

Sounds like an excellent enhancement to me. Patch welcome for this.





[LOGIC-133] Add label goal Created: 29/Apr/13  Updated: 11/Jan/14

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

Type: Defect Priority: Major
Reporter: David Nolen Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

This goal should enumerate any fd vars found in a fresh/ground var bound to a sequence. This would avoid some unintuitive behavior that came up on the mailing list:

(defne weighted-listo [l w]
  ([() _] (fd/== w 0))
  ([[h . t] _]
    (fresh [n]
      (fd/in n (fd/interval 0 java.lang.Integer/MAX_VALUE))
      (fd/in h (fd/interval 1 java.lang.Integer/MAX_VALUE))
      (fd/+ h n w)
      (weighted-listo t n))))


 Comments   
Comment by Austin Haas [ 11/Jan/14 10:23 PM ]

Here is a link to the discussion on the mailing list: https://groups.google.com/forum/#!topic/minikanren/MgcvtkA6_EI





[LOGIC-129] matcha/matchu are not faithful to the semantics of conda/condu Created: 04/Apr/13  Updated: 09/Jun/13

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

Type: Defect Priority: Major
Reporter: Austin Haas Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

The semantics of conda and condu give special importance to the head of each clause, but the pattern matching macros in core.logic that are built on top of them merge the body into the head. That means that every expression in a body position is considered when deciding which line is chosen, rather than just the expression in the head position. This is because the entire clause is wrapped in a fresh expression to bind the implicitly specified lvars that appear in the pattern.

To illustrate:

(matcha ['a]
    [['a] u#]
    [['a] s#])

;; expands to:

(conda
  [(fresh [] (== 'a 'a) u#)]
  [(fresh [] (== 'a 'a) s#)])

;; which has a different meaning than:

(conda
  [(== 'a 'a) u#]
  [(== 'a 'a) s#])

Ideally, we could devise a new system to marry the semantics of conda with pattern matching. At the very least, I think the offending macros should carry a warning in their docstring, stating this semantic difference.

I suspect this would also cause the "Third Commandment" warning to apply to the entire line, rather than just the head/question, but I have not investigated that issue.

Here's an example that demonstrates the difference in meaning:

;; This does not succeed, because we commit to the first line, 
;; since the question succeeds, but then fail in the body.

(run* [q]
  (conda
   [(== 'a 'a) u#]
   [(== 'a 'a) s#]))

;; => ()

;; This succeeds, because the whole line is used to determine which line to commit to, 
;; rather than just the pattern matching clause at the head. So when the first line fails,
;; the second line is tried.

(run* [q]
  (matcha ['a]
   [['a] u#]
   [['a] s#]))

;; => (_0)


 Comments   
Comment by Austin Haas [ 04/Apr/13 2:35 PM ]

For reference:

The Third Commandment

If prior to determining the question of a conda (or condu) line a variable is fresh, it must remain fresh in the question of that line.

From The Reasoned Schemer.

Comment by David Nolen [ 04/Apr/13 5:16 PM ]

Good catch I need to think about this one.

Comment by David Nolen [ 09/Jun/13 12:11 PM ]

The issue is that we rely on the `conde` macro which isn't very flexible. We should probably do something one step lower so can wrap each conde line in a `let` that constructs the logic vars and then ensure that all the head unifications are wrapped in one `fresh` so that the semantics of conda/u are preserved.





[LOGIC-119] tie disequality Created: 12/Mar/13  Updated: 12/Mar/13

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

Type: Defect Priority: Major
Reporter: Nada Amin Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   
(deftest test-tie-disequality
  (is (= (run* [q]
           (nom/fresh [a b]
             (!= (nom/tie a a) 'hello)))
        '(_0)))
  (is (= (run* [q]
           (nom/fresh [a b]
             (!= (nom/tie a a) (nom/tie b b))))
        ())))

Currently, the first causes an error, because IPersistentMap (which gets called because Tie is a record!) assumes that the the other term is also a record (that seems like a bug). If we revert the commit which makes Tie a record, this works.

The other one succeeds, when it should fail. This is regardless of whether Tie is a record or not.



 Comments   
Comment by Nada Amin [ 12/Mar/13 5:52 AM ]

quick fix in https://github.com/clojure/core.logic/commit/8af0f45f8d1cb515ec7a00e5acd751562a31bb37

for actually doing != modulo alpha equivalence requires the opposite of nom/hash.





[LOGIC-117] one-shot constraints with multiple rands may run more than once Created: 11/Mar/13  Updated: 19/Mar/13

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

Type: Defect Priority: Major
Reporter: Nada Amin Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   

Here are two examples using fixc:

(run* [q]
  (fresh [x y]
    (fixc [x y]
      (fn [[x y] a _] (!= x 1))
      (fn [[x y] a] (= (walk a x) (walk a y)))
      '...)
    (== x y)))

(run* [q]
  (fresh [x y c d]
    (fixc [x y]
      (fn [[x y] a _] (!= x y))
      (fn [[x y] a] (or (not (lvar? (walk a x))) (not (lvar? (walk a y)))))
      '...)
    (== [x y] [[c] [d]])))

The constraint != is reified twice in each example, showing that the fixc constraint indeed ran twice.



 Comments   
Comment by David Nolen [ 17/Mar/13 7:27 PM ]

For the first example I see the following as a result on master:

((_0 :- (!= (_1 1))))

Is this what you're seeing? As x isn't even part of the answer I wonder if we should show these constraints?

Comment by Nada Amin [ 19/Mar/13 1:36 AM ]

I changed the reifier by setifying the set of constraints, hence you get only one result now. So my illustration is now out-of-date but the problem remains. It's a separate issue to filter out irrelevant constraints, and I agree it should be done (I try to do it for the nominal constraints).





[LOGIC-114] stack overflow with conda/u Created: 14/Feb/13  Updated: 17/Mar/13

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

Type: Defect Priority: Major
Reporter: Austin Haas Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   
(ns test
  (:refer-clojure :exclude [==])
  (:require
   [clojure.core.logic :refer :all]))
 
(defn foo [in out]
  (matcha 
   [in out]
   ([('and a b . ()) ('and x y . ())] (foo a x) (foo b y))
   ([a ('bar ('baz a . ()) . ())])))
 
;; I get a stack overflow with the following, but if I remove one conjunct, then it will run.
 
(run 1 [q] (foo
            '(and p
                  (and p
                       (and p
                            (and p
                                 (and p
                                      (and p
                                           (and p
                                                (and p
                                                     (and p
                                                          (and p
                                                               (and p p)))))))))))
            q))


 Comments   
Comment by David Nolen [ 14/Feb/13 1:22 PM ]

It looks this issue still exists even if you swap the matcha with matche

Comment by Austin Haas [ 14/Feb/13 8:06 PM ]

I think the overflow is occurring during reification.

I was getting this error when returning a result from run, but now that I'm using the same value as the input to another goal there is no overflow.

If you replace q in the foo call with a fresh variable, it will not overflow.

Comment by David Nolen [ 17/Mar/13 7:30 PM ]

This works for me on master. Can you give me more specifics about your setup so I can try to recreate? I'm on OS X 10.8 running JDK 7 64bit.

Comment by Austin Haas [ 17/Mar/13 8:50 PM ]

I don't see the issue anymore, but I believe I was using Java 1.6 when I reported it and now I am using:

$ java -version
java version "1.7.0_15"
Java(TM) SE Runtime Environment (build 1.7.0_15-b03)
Java HotSpot(TM) 64-Bit Server VM (build 23.7-b01, mixed mode)

Comment by David Nolen [ 17/Mar/13 9:02 PM ]

OK, thanks for the quick response, I'll double check how things look under 1.6.





[LOGIC-99] StackOverflow for large `appendo` Created: 05/Jan/13  Updated: 07/Jan/13

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

Type: Defect Priority: Major
Reporter: David Nolen Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None


 Description   
(def l (range 0 2000))
(run* [q] (appendo l l q))

Stacktrace

user=> (def l (range 0 2000))
#'user/l
user=> (run* [q] (appendo l l q))
StackOverflowError   clojure.core.logic.LVar (logic.clj:1307)
user=> (pst)
StackOverflowError 
    clojure.core.logic.LVar (logic.clj:1307)
    clojure.lang.KeywordLookupSite$1.get (KeywordLookupSite.java:45)
    clojure.core.logic.LVar (logic.clj:1325)
    clojure.lang.Util.equiv (Util.java:32)
    clojure.lang.PersistentHashMap$BitmapIndexedNode.find (PersistentHashMap.java:601)

    clojure.lang.PersistentHashMap$ArrayNode.find (PersistentHashMap.java:370)
    clojure.lang.PersistentHashMap$ArrayNode.find (PersistentHashMap.java:370)
    clojure.lang.PersistentHashMap.entryAt (PersistentHashMap.java:133)
    clojure.lang.RT.find (RT.java:720)
    clojure.core/find (core.clj:1432)
    clojure.core.logic.Substitutions (logic.clj:1134)
    clojure.core.logic/walk*/fn--2847 (logic.clj:1005)


 Comments   
Comment by David Nolen [ 05/Jan/13 2:44 PM ]

I cannot recreate on my machine but should try a large N & wait and see.





Generated at Mon Dec 22 09:43:54 CST 2014 using JIRA 4.4#649-r158309.