conjure
conjure copied to clipboard
Refinement of matrix expression is not valid Essence'
Consider the following model:
language Essence 1.0
find x : matrix indexed by [int(1..10)] of int(1..10)
find m : matrix indexed by [int(1..55)] of int(1..10)
such that
x = [ sum([m[k] | k : int(i..j)]) | i,j : int(1..10), i <= j]
The constraint is refined to the basically identical:
x=[sum([m[k]|k : int(i..j), () ;int(1..)])|i : int(1..10), j : int(1..10), ((i<=j)) ;int(1..)]
But, Essence' doesn't do matrix equality.
I can fix this doing the horrible-at-first-glance:
forAll iter: int(1..sum([1 | i : int(1..10), j : int(1..10), i <= j])).
(x[iter] = [sum([m[k] | k : int(i..j)]) | i : int(1..10), j : int(1..10), i <= j][iter])