Question

迭代约束让我们能够使用循环变量和索引表达式以一种参数化的方式约束数组变量。

定义一个迭代约束的语法如下：

constraint_expression ::=     // 引用自附录A.1.9
    ...
  | foreach (array_identifier [loop_variables]) constraint_set

loop_variables ::= [index_variable_identifier] {, [index_variable_identifier]}
                                                              // 引用自附录A.6.8

语法12-6 — foreach迭代约束语法（摘录自附录A）

foreach结构指定了数组元素上的迭代。它的参数是一个标识符跟着一个包围在方括号中的循环变量，这个标识符说明了任意类型的数组（固定尺寸、动态数组、联合数组、或队列）。每一个循环变量均对应于数组的某一维。

例如：

class C;
    rand byte A[];
    constraint C1 {foreach (A[i]) A[i] inside {2,4,8,16};}
    constraint C2 {foreach (A[j]) A[j] > 2*j;}
endclass

C1将数组A的每一个元素约束成位于集合[2,4,8,16]之内。C2将数组A中的每一个元素约束成大于其索引值的两倍。

循环变量的数目不能超过数组变量的维数。每一个循环变量的作用范围是foreach约束结构，包括它的constraint_set。每一个循环变量的类型被隐含地声明成与数组索引类型一致。一个空的循环变量指示在数组的该维上没有迭代。与缺省参数一样，尾部的逗号列表可以被忽略，因此，foreach(arr[j])等价于foreach(arr[j, , , ,])。任何循环变量都不能与数组具有相同的标识符。

循环变量与数组索引的映射由维基数确定，参见23.7节。

//    1  2  3         3    4      1   2   -> Dimension numbers
int A[2][3][4]; bit [3:0][2:1] B[5:1][4];
foreach(A[i,j,k]) ...
foreach(B[q,r, ,s]) ...

第一个foreach引起i从0到1迭代，j从0到2迭代，k从0到3迭代。第二个foreach引起q从5到1迭代，r从0到3迭代，s从2到1迭代。

迭代约束可以包含判定条件。例如：

class C;
    rand int A[];
    constraint c1 {arr.size inside {[1:10]};}
    constraint c2 {foreach (A[k]) (k < A.size-1) -> A[k+1] > A[k];}
endclass

第一个约束，c1将数组A的尺寸约束在1到10之间。第二个约束，c2将每一个数组值约束成大于前面一个的值，也就是数组按降序排列。

在一个foreach结构内，仅包含常量、状态变量、对象句柄比较、循环变量、正在被迭代的数组的尺寸的判定表达式的作用是作为产生约束的守卫者，而不是作为逻辑关系操作。例如，上面例子中约束c2中的蕴涵仅包括一个循环变量和正在被迭代的数组的尺寸，它仅当k < A.size-1时才允许产生一个约束，这样可以阻止约束中的越界访问。有关约束守卫的更多细节在12.4.12节中描述。

索引表达式可以包含循环变量、常量、和状态变量。无效或越界的数组索引不会被自动地消除；用户必须使用判定条件来显式地排除这些索引。

动态数组或联合数组的size方法可以被用来约束数组的尺寸（参见上面例子中的c1）。如果一个数组既被尺寸约束所约束也被迭代约束所约束，那么尺寸约束首先被解析，然后才是迭代约束。作为尺寸约束和迭代约束间隐含排序的结果，size方法应该被当作对应数组的foreach块内的状态变量。例如，表达式A.size被当作约束c1中的一个随机变量，并被作为约束c2中的一个状态变量。这个隐含的排序在某些情况下会导致求解器失败。