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'
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).