clojure.core.logic.fd
clojure.core.logic.fd 中的变量
*^%
- !=
- 有限域约束。u 和 v 不能相等。如果 u 和 v 是变量,则最终必须给它们指定域。
- *
- 用于乘法和除法的有限域约束。如果 x、y 和 product 是变量,则最终必须给它们指定域。
- +
- 用于加法和减法的有限域约束。如果 x、y 和 sum 是变量,则最终必须给它们指定域。
- -distinctc
- 真正的 *独立* distinct 约束。x 是一个现在绑定到单个值的变量。y* 是在约束构建时存在的非单例绑定变量。n* 是在约束构建时存在的单例域值集合。我们使用 categorize 来确定当前的非单例绑定变量和单例值。如果 x 在 n* 或新的单例中,则我们失败了。如果不是,我们只需从绑定到变量的剩余非单例域中删除 x 的值。
- <
- 有限域约束。u 必须小于 v。如果 u 和 v 是变量,则最终必须给它们指定域。
- <=
- 有限域约束。u 必须小于或等于 v。如果 u 和 v 是变量,则最终必须给它们指定域。
- ==
- 有限域约束。u 和 v 必须相等。如果 u 和 v 是变量,则最终必须给它们指定域。
- >
- 有限域约束。u 必须大于 v。如果 u 和 v 是变量,则最终必须给它们指定域。
- >=
- 有限域约束。u 必须大于或等于 v。如果 u 和 v 是变量,则最终必须给它们指定域。
d
- distinct
- 一个有限域约束,它将保证出现在 v* 中的所有变量都将与唯一值统一。v* 不需要是接地的。v* 中的任何变量最终都应该被赋予一个域。
- distinctc
- 真正的 distinct 约束。v* 可以是逻辑变量和值的序列,也可以是逻辑变量本身。此约束在 v* 接地之前不会运行。当它接地后,我们将 v* 分组为一组逻辑变量和一组已排序的已知单例值。然后,我们为每个变量构造单独的约束。
- domain
- 构造要分配给变量的域。参数应该是按排序顺序给出的整数。当只有几个可能的值时,域可能比区间更有效。
i
- interval
- 构造要分配给变量的区间。当可能性范围很大时,区间可能比域类型更有效。
p
- process-dom
- 如果 x 是变量,我们更新它的域。如果它是一个整数,我们检查它是否是给定域的成员。dom 则是新的域,它应该已经从之前的域 domp 计算出来。