高水準制約
以下の制約は、今までのものに比べてより複雑なものです。 これらは、これまでに述べてきたプリミティブとデモン(デモン 参照)により実現することができます。
<注意!>実際のiZ-Cにおける実装では、以下の制約は既述のプリミティブとデモンの組み合わせによるのではなく、 独自の実現方式を持ちます。
特定の関係を満たす CSint を返す制約では、制約設定時にフェイルした場合には NULL が返されます。
-
IZBOOL cs_IfEq(CSint *vint1, CSint *vint2, int val1, int val2)
vint1 が値 val1 に即値化されたら、vint2 を val2 に即値化します。
vint2 が値 val2 に即値化されたら、vint1 を val1 に即値化します。
-
IZBOOL cs_IfNeq(CSint *vint1, CSint *vint2, int val1, int val2)
CSint 型変数の組(vint1, vint2) は値 (val1, val2)を持つことができません。
-
CSint *cs_Occur(CSint *vint, int val, CSint **array, int size)
値 val は vint 回 array 中に出現しなくてはなりません。
<注意!>旧バージョンでは実装に不備がありました。本来ならば返り値は値 val が vint 回 array 中に出現する (TRUE)かしない(FALSE)かを返す必要がありました。
旧バージョンとの互換性のため返り値は変更しませんが、 今後は
cs_OccurConstraints()を使ってください。本APIは将来削除する予定です。
-
CSint *cs_OccurDomain(int val, CSint **array, int size)
array 中に値 val となりうる個数の範囲を返します。
-
IZBOOL cs_OccurConstraints(CSint *vint, int val, CSint **array, int size)
値 val は vint 回 array 中に出現しなくてはなりません。
-
CSint *cs_Index(CSint **array, int size, int val)
返されるCSint 型変数を Index とすると、長さ size の配列 array に対して要素制約 array [ Index ] = val が設定されます。
i \(\in\) domain( Index ) \(\Leftrightarrow\) val \(\in\) domain( array [ i ])
-
CSint *cs_Element(CSint *index, int *values, int size)
返される CSint 型変数を Element とすると、長さ size の配列 values について、 Element = values [ index ]が設定されます。
-
CSint *cs_VarElement(CSint *index, CSint **array, int size)
返されるCSint 型変数を Element とすると、長さ size の領域変数の配列 array について、 Element = array [ index ] が設定されます。
-
CSint *cs_VarElementRange(CSint *index, CSint **array, int size)
CSint 型変数を
cs_VarElement()と同様に制約します。ただし、array 内の変数については上限と下限のみに基づいて制約伝播を行います。
-
CSint *cs_Min(CSint **array, int size)
array により参照されるCSint 型変数のうち最小のものの値と等しいCSint 型変数を返します。
-
CSint *cs_VMin(int nbVars, CSint *vint, ...)
cs_VMin() は可変長引数をとります(引数の数は最初の引数 nbVars に指定されます)。
-
CSint *cs_Max(CSint **array, int size)
array により参照されるCSint 変数のうち最大のものの値と等しいCSint 型変数を返します。
-
CSint *cs_VMax(int nbVars, CSint *vint, ...)
cs_VMax() は可変長引数をとります(引数の数は最初の引数 nbVars に指定されます)。
-
IZBOOL cs_Cumulative(CSint **startVars, CSint **durationVars, CSint **resourceVars, int size, CSint *limitVar)
スケジューリング等で使用される制約です。 size 個のタスクの i 番目について、開始時刻を startVars [i]、 継続時間を durationVars [i]、必要なリソースを resourceVars [i] としたとき、同時に実行されるタスクの resourceVars の合計が limitVar 以下になるように制約します。
-
IZBOOL cs_Disjunctive(CSint **startVars, CSint **durationVars, int size)
スケジューリング等で使用される制約です。 size 個のタスクの i 番目について、開始時刻を startVars [i]、 継続時間を durationVars [i] としたとき、タスクが同一時刻に 実行されないように制約します。
-
IZBOOL cs_Regular(CSint **array, int size, const int *d, int Q, int S, int q0, const int *F, int fsize)
array により参照される CSint 型変数配列を、d, Q, S, q0, F で定義されるオートマトンで受理される 記号列となるように制約します。
d は \(Q \times S\) の大きさを持つ配列です。状態 q で入力 s を受け取った時の次の遷移先が位置 \(q \times S + s\) に格納されている必要があります。(遷移先がない場合は、-1)
Q は状態数です。
S は入力の種類数です。
q0 は初期状態です。
F は受理状態を格納した配列で、その長さは fsize です。