MiniZinc：打印出生成的约束？答案

【问题标题】：MiniZinc: print out generated constraints?MiniZinc：打印出生成的约束？
【发布时间】：2018-03-30 17:01:53
【问题描述】：

使用 MiniZinc，有没有办法打印出程序生成的约束？例如：

constraint exists (i in 1..3) (
     foo != i
);

我想确认它正在生成：

constraint (foo != 1 \/ foo != 2 \/ foo !=3);

【问题讨论】：

标签： constraint-programming minizinc

【解决方案1】：

尽管 MiniZinc 不提供直接打印约束。 MiniZinc 确实提供了trace(string: s, var $T: expr) 功能。可用于调试您的 MiniZinc 模型。 trace 是一个打印语句，它在编译器内进行评估时将其内容打印到命令行。因此，它可用于打印您希望看到的信息，但您必须自己格式化以显示约束。

如果是存在循环，您可以使用：

constraint exists(i in 1..3) (
    trace("foo != \(i)" ++ if i != max(1..3) then " \\/ " else "\n" endif,
    foo != i)
);

这会将foo != 1 \/ foo != 2 \/ foo != 3 打印到命令行。

【讨论】：

【解决方案2】：

要了解生成的约束，您可以查看生成的FlatZinc 文件。 MiniZinc 编译器将MiniZinc 源转换为FlatZinc。然后将其移交给求解器后端，例如 Gecode 或 Chuffed。

MiniZinc 输入：

var int: foo;

constraint exists (i in 1..3) (
     foo != i
);

solve satisfy;

创建FlatZinc:

var int: foo:: output_var;
var bool: X_INTRODUCED_0_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_1_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_2_ ::var_is_introduced :: is_defined_var;
constraint array_bool_or([X_INTRODUCED_2_,X_INTRODUCED_1_,X_INTRODUCED_0_],true);
constraint int_ne_reif(foo,1,X_INTRODUCED_0_):: defines_var(X_INTRODUCED_0_);
constraint int_ne_reif(foo,2,X_INTRODUCED_1_):: defines_var(X_INTRODUCED_1_);
constraint int_ne_reif(foo,3,X_INTRODUCED_2_):: defines_var(X_INTRODUCED_2_);
solve  satisfy;

要查看FlatZinc表单，可以在MiniZinc IDE的Configuration选项卡中添加参数--output-fzn-to-stdout：

【讨论】：

感谢您的及时回复，阿克塞尔！我知道 FlatZinc 的输出，但感谢您概述了机制。不过，我仍然希望我能看到 MiniZinc 约束......

【解决方案3】：

MiniZinc 在将表达式编译为 FlatZinc 时会经历一系列步骤，因此要决定在哪一步之后打印问题的中间表示并不容易。

要查看生成的 FlatZinc，您也可以简单地从 MiniZinc 菜单中选择“编译”，而不是使用--output-fzn-to-stdout 命令行选项。

【讨论】：