Details

Type: Defect

Status: Closed

Priority: Major

Resolution: Completed

Affects Version/s: None

Fix Version/s: None

Component/s: None

Labels:None
Description
Via this StackOverflow question http://stackoverflow.com/questions/15671823/unexpectedresultswithclojurecorelogicusingclpfd
(defn productpluso [factor1 factor2 number sum] (fd/eq (= sum (+ number (* factor1 factor2))))) (run* [x y] (fd/in x y (fd/interval 1 38)) (productpluso x y 2 40))
Returns too many answers. Even if we desugar into:
(run* [q] (fresh [x y p] (fd/in x y (fd/interval 1 38)) (fd/* x y p) (fd/+ p 2 40) (== q [x y p])))
We see results which clearly violate the fd/+ constraint.
Activity
David Nolen
made changes 
Field  Original Value  New Value 

Description 
Via this StackOverflow question http://stackoverflow.com/questions/15671823/unexpectedresultswithclojurecorelogicusingclpfd
{code} (defn productpluso [factor1 factor2 number sum] (fd/eq (= sum (+ number (* factor1 factor2))))) (run* [x y] (fd/in x y (fd/interval 1 38)) (productpluso x y 2 40)) {code} Returns to many answers even if we desugar into: {code} (run* [q] (fresh [x y p] (fd/in x y (fd/interval 1 38)) (fd/* x y p) (fd/+ p 2 40) (== q [x y p]))) {code} We see results which clearly violated the fd/+ constraint. 
Via this StackOverflow question http://stackoverflow.com/questions/15671823/unexpectedresultswithclojurecorelogicusingclpfd
{code} (defn productpluso [factor1 factor2 number sum] (fd/eq (= sum (+ number (* factor1 factor2))))) (run* [x y] (fd/in x y (fd/interval 1 38)) (productpluso x y 2 40)) {code} Returns too many answers even if we desugar into: {code} (run* [q] (fresh [x y p] (fd/in x y (fd/interval 1 38)) (fd/* x y p) (fd/+ p 2 40) (== q [x y p]))) {code} We see results which clearly violated the fd/+ constraint. 
David Nolen
made changes 
Description 
Via this StackOverflow question http://stackoverflow.com/questions/15671823/unexpectedresultswithclojurecorelogicusingclpfd
{code} (defn productpluso [factor1 factor2 number sum] (fd/eq (= sum (+ number (* factor1 factor2))))) (run* [x y] (fd/in x y (fd/interval 1 38)) (productpluso x y 2 40)) {code} Returns too many answers even if we desugar into: {code} (run* [q] (fresh [x y p] (fd/in x y (fd/interval 1 38)) (fd/* x y p) (fd/+ p 2 40) (== q [x y p]))) {code} We see results which clearly violated the fd/+ constraint. 
Via this StackOverflow question http://stackoverflow.com/questions/15671823/unexpectedresultswithclojurecorelogicusingclpfd
{code} (defn productpluso [factor1 factor2 number sum] (fd/eq (= sum (+ number (* factor1 factor2))))) (run* [x y] (fd/in x y (fd/interval 1 38)) (productpluso x y 2 40)) {code} Returns too many answers. Even if we desugar into: {code} (run* [q] (fresh [x y p] (fd/in x y (fd/interval 1 38)) (fd/* x y p) (fd/+ p 2 40) (== q [x y p]))) {code} We see results which clearly violate the fd/+ constraint. 
David Nolen
made changes 
Resolution  Completed [ 1 ]  
Status  Open [ 1 ]  Resolved [ 5 ] 
David Nolen
made changes 
Status  Resolved [ 5 ]  Closed [ 6 ] 
It seems like we should be able to fix this at the level of updatevardom by checking that the var doesn't already have a value in the substitution, but oddly by doing this we run into some strange nontermination behavior. I've experienced this before when trying to flip the order of checks in letdom, but at the time I was too busy with bigger problems to look at the issue more closely.