letmaik
Divergence When Using @/=
This might qualify more as a question than a bug report. I tried writing the following model, which creates two variables ranging over {1,2} and constrains them with @/= so that it is not the case that (a,b) = (1,2). Then it branches on the values of the first variable. When I evaluate solve_not_12, the program diverges -- when compiled with GHC 7.6.3 -O2, it doesn't finish and allocates up to at least 700MB. However, if I evaluate solve_not_12', which states the constraint in a slightly different way, it succeeds and returns (10,[[1,1]]). Is this a bug or am I something wrong? I'm using monadiccp-0.7.6 compiled without any special flags (i.e. just cabal install monadiccp).
not_12 :: Tree (FDInstance OvertonFD) [Int]
not_12 =
exist 2 $ \[a,b] -> do
a @: (cte 1, cte 2)
b @: (cte 1, cte 2)
a @/= b - 1
a @= 1 \/ a @= 2
assignments [a,b]
solve_not_12 = solve dfs fs not_12
not_12' :: Tree (FDInstance OvertonFD) [Int]
not_12' =
exist 2 $ \[a,b] -> do
a @: (cte 1, cte 2)
b @: (cte 1, cte 2)
a + 1 @/= b
a @= 1 \/ a @= 2
assignments [a,b]
solve_not_12' = solve dfs fs not_12'
Hmm, looks indeed like a bug. Unfortunately I don't have much knowledge of the internals to help you there.
Ouch, that's too bad. I posted here because this repo was linked from the Hackage page. Is there some place else I should report this bug to?
This is the right place, there's just no active developer at the moment :/ I took over maintainance of this project so that at least it has a home and gets adapted to newer GHC versions should something break.