Как указать ограничения через универсальные квантификаторы? - PullRequest
Новая
       17

Как указать ограничения через универсальные квантификаторы?

0 голосов
/ 14 января 2019

Допустим, у меня есть такая матрица: 

M([[150, _],
   [130, _],
   [160, _],
   [100, _],
   [100, _],
   [100, _]])

И я хочу использовать второй столбец в качестве «порядка» этих строк, согласно некоторому правилу, которое включает элементы первого столбца.

Например, одним из таких правил будет: две соседние строки не могут иметь одинаковое значение в первом столбце.

Одним из возможных решений будет (строки уже отсортированы по второму столбцу): 

M([[150, 1],
   [100, 2], 
   [130, 3],
   [100, 4],
   [160, 5],
   [100, 6]]).

Я знаю, что могу использовать ins и all_distinct для ограничения значений, но неясно, как реализовать ограничение выше кратким образом. В логике первого порядка я бы написал что-то вроде: 

forall(X,Y) c2(X) == c2(Y) + 1 => c1(X) != c1(Y).

Где X и Y располагаются в разных строках, c1 - это значение первого столбца, а c2 - это значение второго столбца.

Один из способов, которым я думал, это просто сопоставить все значения ячеек с переменными и записать все возможные комбинации ограничений. Это может быть выполнимо, если я могу автоматически сгенерировать код, но, возможно, есть более краткий способ сделать это, подобный универсальному количественному определению выше?

...