Question

约束守卫者是一些判决表达式，它的作用并不是为了求解约束需要满足的逻辑关系，而是作为产生约束的守卫者。这些判决表达式在约束被求解之前计算，并且只能调用下列条目：

• 常量
• 状态变量
• 对象句柄比较（两个句柄之间比较或者在句柄与常量null之间比较）

除了上面描述的条目外，迭代约束（参见12.4.7节）还会将循环变量以及正在被迭代的数组的尺寸当作状态变量。

将这些判决表达式作为约束守卫者能够在某些表面上看起来正确的约束上失败，因此也就可以防止求解器产生计算错误。这就使得用户能够编写约束来防止由于无效句柄或越界的数组索引导致的错误。例如，下面的例子实现了一个singlylinked链表（名字为SList），使用它的sort约束能够赋值一个按降序排列的数字随机序列。然而，对于最后一个元素，next.n会由于无效句柄产生一个计算错误，因此约束表达式会在最后一个元素失败。

class SList;
    rand int n;
    rand Slist next;
    constraint sort {n < next.n;}
endclass

上面例子中的错误条件可以通过编写一个守卫这个条件的判决表达式来避免：

constraint sort {if(next != null) n < next.n;}

在上面例子中的sort约束中，if会防止在next==null的时候产生一个约束，因此，在这种情况下可以避免访问一个无效对象。无论是蕴含（->）还是if...else都可以用作约束守卫者。

守卫表达式本身可以包含会引起计算错误的子表达式（例如空引用），并且它们还被守卫以免产生错误。通过使用下列的四态表示来计算判决子表达式可以完成这个逻辑转移：

• 0 FALSE子表达式计算成FALSE
• 1 TRUE子表达式计算成TRUE
• E ERROR子表达式引起一个计算错误
• R RANDOM表达式包含随机变量并且不能被计算

判决表达式内的每一个子表达式都会被计算以便产生上述四个值中的一个。子表达式以任意顺序计算，并且计算结果加上逻辑操作以四态表示形式定义了结果。子表达式的联合（&&）、分离（||）或非（!）可以包含某些（或许所有）守卫子表达式。下列规则说明了守卫的结果值：

• 联合（&&）：如果任意一个子表达式计算成FALSE，那么守卫会被计算成FALSE。另外，如果任意一个子表达式计算成ERROR，那么守卫计算成ERROR，否则计算成TRUE。
  • 如果守卫计算成FALSE，那么约束会被消除。
  • 如果守卫计算成TRUE，那么会产生一个约束（可能是有条件的）。
  • 如果守卫计算成ERROR，那么会产生一个错误并且随机化会失败。
• 分离（||）：如果任何一个子表达式计算成TRUE，那么守卫会被计算成TRUE。另外，如果任意个子表达式计算成ERROR的话，那么守卫会被计算成ERROR，否则守卫计算成FALSE。
  • 如果守卫计算成FALSE，那么会产生一个约束（可能是有条件的）。
  • 如果守卫计算成TRUE，那么会产生一个无条件的约束。
  • 如果守卫计算成ERROR，那么会产生一个错误并且随机化会失败。
• 非（!）：如果子表达式计算成ERROR，那么守卫计算成ERROR。另外，如果子表达式计算成TRUE或FALSE，那么守卫会被分别计算成FALSE或TRUE。

这些规则可以使用下列的真值表表示：

上述规则会被递归地应用直到所有的子表达式被计算。判决表达式的最终值按下列规则确定结果：

• 如果结果为TRUE，那么会产生一个无条件约束。
• 如果结果为FALSE，那么约束会被消除并且不会产生错误。
• 如果结果为ERROR，那么会产生一个无条件错误并且约束会失败。
• 如果最终的计算结果为RANDOM，那么会产生一个有条件约束。

当最终结果是RANDOM的时候，需要遍历判决表达式树以便收集计算成RANDOM的所有有条件守卫。当最终结果为ERROR的时候，不需要遍历后续的表达式树，这就使得实现时只发布一个错误。

例子1：

class D;
    int x;
endclass

class C;
    rand int x, y;
    D a, b;
    constraint c1 {(x < y || a.x > b.x || a.x == 5) -> x+y == 10;}
endclass

在上面的例子中，判决表达式为(x < y)、(a.x > b.x)、以及(a.x == 5)，它们被分离（||）连接起来。一些可能的情况有：

• 情况1：a为非空，b为null，a.x为5。

因为(a.x == 5)为真，所以b.x产生错误的事实不会导致一个错误。

无条件约束(x+y == 10)会被产生。

• 情况2：a为null

这种情况总会导致错误而不管其它的条件。

• 情况3：a为非空，b为非空，a.x为10，b.x为20

所有的守卫子表达式计算成FALSE。

产生有条件约束(x<y) -> (x+y) == 10。

例子2：

class D;
    int x;
endclass

class C;
    rand int x, y;
    D a, b;
    constraint c1 {(x < y && a.x > b.x && a.x == 5) -> x+y == 10;}
endclass

在上面的例子中，判决表达式为(x < y)、(a.x > b.x)、以及(a.x == 5)，它们被联合（&&）连接起来。一些可能的情况为：

• 情况1：a为非空，b为null，a.x为6。

因为(a.x==5)为假，b.x产生一个错误的事实不会导致一个错误。

约束被消除。

• 情况2：a为null

这种情况总会导致错误而不管其它的条件。

• 情况3：a为非空，b为非空，a.x为5，b.x为2。

所有的守卫子表达式计算成TRUE，产生有条件约束(x<y) -> (x+y) == 10。

例子3：

class D;
    int x;
endclass

class C;
    rand int x, y;
    D a, b;
    constraint c1 {(x < y && (a.x > b.x || a.x == 5)) -> x+y == 10;}
endclass

在上面的例子中，判决表达式为(x < y)以及(a.x > b.x || a.x == 5)，有一个表达式使用分离（||）连接起来。一些可能的情况如下：

• 情况1：a为非空，b为null，a.x为5。

守卫表达式计算成(ERROR || a.x==5)，进一步计算成(ERROR || TRUE)。

守卫子表达式计算成TRUE。

产生有条件约束(x<y) -> (x+y) == 10。

• 情况2：a为非空，b为null，a.x为8。

守卫表达式计算成(ERROR || FALSE)，并产生一个错误。

• 情况3：a为null

这种情况总会导致错误而不管其它的条件。

• 情况4：a为非空，b为非空，a.x为5，b.x为2。

所有的守卫子表达式计算成TRUE。

产生有条件约束(x<y) -> (x+y) == 10。