<< Back to previous view

[LOGIC-162] FD logic doesn't always return all solutions Created: 20/Oct/14  Updated: 21/Oct/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.





[LOGIC-161] fd/eq returns strange results Created: 13/Oct/14  Updated: 16/Oct/14  Resolved: 16/Oct/14

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

Type: Defect Priority: Major
Reporter: Dustin Conrad Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None
Environment:

clojure.core.logic 0.8.8 on mac osx 10.9



 Description   
(logic/run* [q]
  (logic/fresh [a b]
    (fd/in a b (fd/interval 0 10))
    (fd/eq (= 4 (* (- a b) 2)))
    (logic/== q [a b])))

I am fairly new to logic programming, but it seems to me this should return a result. I believe it is equivalent to

(logic/run* [q]
  (logic/fresh [a b]
    (fd/in a b (fd/interval 0 10))
    (fd/eq (= 2 (- a b)))
    (logic/== q [a b])))

which does return 9 results



 Comments   
Comment by Dustin Conrad [ 13/Oct/14 10:37 PM ]

I apologize for the formatting, I am unable to edit the description after posting.

Comment by David Nolen [ 15/Oct/14 6:01 PM ]

This appears to be a problem with the sugar `fd/eq`. If you stick to the primitives you should see the results that you expect.

Comment by David Nolen [ 15/Oct/14 6:02 PM ]

My suspicion is that some of the implicitly constructed logic vars are not getting assigned FD intervals.

Comment by David Nolen [ 15/Oct/14 8:10 PM ]

I dug into this quite a bit. The specific issue with this code example is that the multiplication will set the domain of a logic var such that negative values leak into the domain calculation causing the spurious appearance of negative values where they should not exist. We should think quite a bit more about the appearance of negative values.

Comment by Dustin Conrad [ 15/Oct/14 10:35 PM ]

Thanks for looking at this David.

Comment by David Nolen [ 16/Oct/14 4:49 PM ]

fixed https://github.com/clojure/core.logic/commit/719c23f80280762ff20216a579d88efa32da2de7





[LOGIC-146] run macro should take * in addition to n Created: 26/Nov/13  Updated: 16/Oct/14

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

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





[LOGIC-128] add mod/rem/abs/min/max Created: 02/Apr/13  Updated: 15/Oct/14

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

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


 Description   

SWI-Prolog's CLP(FD) module has this functionality http://www.swi-prolog.org/man/clpfd.html






[LOGIC-89] Allow application again in pattern matches Created: 01/Jan/13  Updated: 15/Oct/14

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

Type: Enhancement Priority: Minor
Reporter: David Nolen Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: 0.8.0


 Description   

Perhaps we can support simple function application in the following manner.

(defne substo [e new a out]
  (['(var ~a) _ _ new])
  (['(var ~y) _ _ '(var ~y)] (nom/hash a y))
  (['(app ~rator ~rand) _ _ '(app ~rator-res ~rand-res)]
     (substo rator new a rator-res)
     (substo rand new a rand-res))
  (['(lam ~(nom/tie c body)) _ _ '(lam ~(nom/tie c body-res))]
     (nom/hash c a) (nom/hash c new)
     (substo body new a body-res)))

If we have a seq in an unquote then we know we have an application. All function symbols are left alone, all arguments are considered to be fresh vars or locals.






[LOGIC-68] add Prolog meta-logical predicates bagof, setof, findall Created: 16/Nov/12  Updated: 15/Oct/14

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

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

Attachments: Text File 0001-LOGIC-68-Add-run-a-run-a-logic-functions-to-support-.patch    

 Description   

This can be done by annotating logic variables and embedding a run within a run by passing in the current substitution, running on it, and extracting out the reified values and unifying it back into the current substitution.



 Comments   
Comment by Aaron Brooks [ 16/Nov/12 1:23 PM ]

I'm working on understanding the answers given for this StackOverflow question:

http://stackoverflow.com/questions/7647758/prolog-findall-implementation

Comment by Aaron Brooks [ 16/Nov/12 10:02 PM ]

For discussion — Initial working patch supporting nested version of 'run-a/'run-a*. Binding symbols must match existing lvars with which vectors of all returned values will be unified.

Comment by Aaron Brooks [ 17/Nov/12 4:07 PM ]

Should we provide wrappers that emulate each of bagof, setof and findall?

I'm still not sold on the current names run-a/run-a*. "a" is really an internal implementation detail. Expect a revised patch with better names when I think of them (any ideas?).

Comment by David Nolen [ 17/Nov/12 8:32 PM ]

Yes please. Yeah I don't think the names of run-a/etc are critical - implementation details for now until we really understand the implications and it gets some use.

Comment by Aaron Brooks [ 21/Nov/12 10:51 AM ]

I'm considering simply making run/run* conditionalized on the first argument, using the nesting form if we are being called with a substitution map as the first argument.

My current understanding of bagof and findall makes me think they're not worth implementing beyond the nesting run functionality.

I'm still thinking about setof which is quite useful and will want help from the infrastructure to be fully efficient.

I'll submit a new patch after Thanksgiving.

Comment by David Nolen [ 21/Nov/12 10:57 AM ]

Excellent, thanks much.

Comment by Aaron Brooks [ 06/Dec/12 12:30 AM ]

I have not forgotten, I've just gotten swamped.

There's a small chance I'll get to this before Christmas, otherwise, it's after the new year.

Comment by Aaron Brooks [ 04/Feb/13 5:50 PM ]

After a car accident, travel to London and Morocco, getting caught up at work and getting caught up on the apparently very busy stream of core.logic activity (great work!), I'm back on this.

I found some bugs in my implementation after porting the patch forwards and realized these issues highlighted my sloppy understanding of some of the semantics I had created.

I'm fairly convinced now that we don't want to name this after run or run*. It's too much of a strain to try to make it mean the same thing in a nested context.

The current mechanism is still not quite a match for findall/bagof/setof, however, so I'm seeing what a good fit would be. I'll post meaningful thoughts for review as I have them.

Comment by David Nolen [ 13/Feb/13 1:50 PM ]

Glad to hear you're OK! No worries, will take a patch whenever you get around to one.

Comment by Aaron Brooks [ 12/Jun/13 9:03 PM ]

Having switched to Datomic which has bagof/setof type aggregation and subqueries (though the switch wasn't for those specifically) I don't know if or when I'll get back to this. Sorry!

Comment by David Nolen [ 13/Jun/13 1:36 AM ]

No worries! Glad Datomic is working out for you





[LOGIC-47] is macro needs to be improved Created: 30/Aug/12  Updated: 15/Oct/14

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

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


 Description   

the is macro should work like the following:

(is x (- (+ a b) c))

All locals appearing in the right expression should be walked.






[LOGIC-38] Logic Threading Macro Created: 13/May/12  Updated: 15/Oct/14

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

Type: Enhancement Priority: Minor
Reporter: Jason Jackson Assignee: David Nolen
Resolution: Unresolved Votes: 0
Labels: None

Attachments: Text File 0001-added-logic-threading-macro.patch     Text File 0001-added-logic-threading-macro.patch    

 Description   

This macro was somewhat useful when I was implementing static analysis for a compiler with core.logic.

(defmacro ==>> [expr-in & rel-forms]
"Thread the expr-in through rel-forms then unify with last rel-forms
(the 'out expression').

Example:
(==>> [[1]] (firsto) (firsto) x))
;; 'x' will become bound to value 1

This macro expands to:
(fresh [_A _B]
(firsto [[1]] _A)
(firsto _A _B)
(== _B q))

If you imagine that the 'return value' of firsto is its last parameter,
then it works just like clojure.core/-> as return value of each form is
first argument of the following form."



 Comments   
Comment by Jason Jackson [ 13/May/12 11:08 AM ]

There might be a better name, not sure.

Comment by Jason Jackson [ 13/May/12 11:18 AM ]

renamed ==>> to ==->





[LOGIC-158] membero documentation does not describe arguments Created: 30/May/14  Updated: 15/Oct/14  Resolved: 15/Oct/14

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

Type: Defect Priority: Major
Reporter: Phillip Lord Assignee: David Nolen
Resolution: Completed Votes: 0
Labels: None

Attachments: Text File 0001-Change-defnm-to-add-arglists-metadata-to-defined-var.patch    

 Description   

(doc clojure.core.logic/membero)
-------------------------
clojure.core.logic/membero
A relation where l is a collection, such that l contains x.

Membero documentation is rather unhelpful because it doesn't
describe the order of the arguments (i.e. which is l and which
is x). appendo and permuteo are similarly affected, so it appears
to be a weakness in defne



 Comments   
Comment by Tobias Kortkamp [ 15/Aug/14 12:45 PM ]

defnm does not add :arglists to the var's metadata.

I've attached a patch that fixes this.

Comment by David Nolen [ 15/Oct/14 6:04 PM ]

fixed https://github.com/clojure/core.logic/commit/fa9451ed57ba9647399e1e6e1d5a723e422d7c6b





Generated at Wed Oct 22 16:46:10 CDT 2014 using JIRA 4.4#649-r158309.