conjure icon indicating copy to clipboard operation
conjure copied to clipboard

Refinement of matrix expression is not valid Essence'

Open ChrisJefferson opened this issue 11 months ago • 0 comments

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])

ChrisJefferson avatar Mar 14 '24 04:03 ChrisJefferson