関係制約

以下の関数はすでに存在するCSint 変数間に制約を設定します。 これらの関数は呼び出し時に直ちにフェイルする (つまりFALSE を返す) ことがあります。

IZBOOL cs_Le(CSint *vint1, CSint *vint2)

vint1 はvint2 より小さいか等しくなければなりません。 (つまり cs_getMin(vint1) <= cs_getMin(vint2) でかつ cs_getMax(vint1) <= cs_getMax(vint2)).

IZBOOL cs_Ge(CSint *vint1, CSint *vint2)

vint1 は vint2 より大きいか等しくなくてはなりません。

IZBOOL cs_Lt(CSint *vint1, CSint *vint2)

vint1 はvint2 より小さくなければなりません。

IZBOOL cs_Gt(CSint *vint1, CSint *vint2)

vint1 は vint2 より大きくなくてはなりません。

IZBOOL cs_Eq(CSint *vint1, CSint *vint2)

vint1 と vint2 は常に等しくなくてはなりません。

IZBOOL cs_Neq(CSint *vint1, CSint *vint2)

vint1 と vint2 は異なった値を持たねばなりません。

以下の関数は、上述の対応する各関数における2つのオペランドのうち、一方が定数の場合に用いると便利です。

  • IZBOOL cs_LE(CSint *vint, int val)
  • IZBOOL cs_GE(CSint *vint, int val)
  • IZBOOL cs_LT(CSint *vint, int val)
  • IZBOOL cs_GT(CSint *vint, int val)
  • IZBOOL cs_EQ(CSint *vint, int val)
  • IZBOOL cs_NEQ(CSint *vint, int val)

例えば、cs_LE() は以下のように定義できるでしょう。:

IZBOOL cs_LE(CSint *vint, int val) {
  return(cs_Le(vint, CSINT(val));
}

<注意!>しかしながら、この例は実装を反映したものではありません。一方が定数であるような制約は、ある領域変数に対する 単項制約と考えることもでき、この場合、2つの領域変数に対する2項の関係制約とは異なるクラスに属する制約と考えられます。 iZ-Cでも、実装上は、この考え方に基づいています。 従って、例えば cs_LE() が呼ばれた場合には、第1引数の領域変数が 第2引数の値以下の領域を持つかどうかの検査を行うのであって、 第2引数の値で即値化された領域変数を作成し、第1引数の領域変数との間に制約を設定するわけではありません。 メモリの利用効率の面から、単項制約の方が有利であるのは明らかです。

IZBOOL cs_AllNeq(CSint **array, int size)

array に属するCSint 変数はすべて異なる値を持たねばなりません。 この制約は、以下のように書くこともできるでしょう。:

IZBOOL cs_AllNeq(CSint **array, int size) {
  int i, j;
  for (i = 0; i < size - 1; i++)
    for (j = i + 1; j < size; j++)
      cs_Neq(array[i], array[j]);
}

<注意!>この場合も実装上は、上記は等価ではありません。cs_AllNeq() は、複数の項に対するN-ary制約として実装されており、 2項制約の組み合わせで実装されているのではありません。この場合も、メモリの利用効率・制約伝播の点で、N-ary制約としての 実装が優れているのは明らかです。なお、iZ-CでのN-ary制約のクラスに属する他の制約としては、後述のwhen 制約(デモン)があります。

以下の制約では、すでに存在するCSint 型変数間の関係が成立するとき1、成立しないとき0という値をとるような新しいCSint 型変数が 作成されます。これらの制約は、設定されたときにはフェイルしません。

CSInt* cs_ReifLe(CSint *vint1, CSint *vint2)

vint1 が vint2より小さいか等しいとき1、そうでないときは0となるようなCSint 型変数を返します。

CSInt* cs_ReifGe(CSint *vint1, CSint *vint2)

vint1 が vint2より大きいか等しいとき1、そうでないときは0となるようなCSint 型変数を返します。

CSInt* cs_ReifLt(CSint *vint1, CSint *vint2)

vint1 が vint2より小さいとき1、そうでないときは0となるようなCSint 型変数を返します。

CSInt* cs_ReifGt(CSint *vint1, CSint *vint2)

vint1 が vint2より大きいとき1、そうでないときは0となるようなCSint 型変数を返します。

CSInt* cs_ReifEq(CSint *vint1, CSint *vint2)

vint1 と vint2 が等しいとき1、そうでないときは0となるようなCSint 型変数を返します。

CSInt* cs_ReifNeq(CSint *vint1, CSint *vint2)

vint1 と vint2 が異なるとき1、そうでないときは0となるようなCSint 型変数を返します。

以下の関数は、上述の対応する各関数における2つのオペランドのうち、一方が定数の場合に用いると便利です。

  • CSInt* cs_ReifLE(CSint *vint, int val)
  • CSInt* cs_ReifGE(CSint *vint, int val)
  • CSInt* cs_ReifLT(CSint *vint, int val)
  • CSInt* cs_ReifGT(CSint *vint, int val)
  • CSInt* cs_ReifEQ(CSint *vint, int val)
  • CSInt* cs_ReifNEQ(CSint *vint, int val)