调试 minizinc（无论如何，我发现了一个错误吗？）

Question

我正在熟悉 MiniZinc 的基础知识。因此，借助 MiniZinc IDE，我编写了类似

的片段

solve satisfy;

string: s1 = "hello";
string: s2 = "world";

function list of int: cdr(list of int: v) =
  [v[i] | i in 1..length(v)];
function list of string: cdr(list of string: v) =
  [v[i] | i in 1..length(v)];

function string: concat(list of string: V) =
  if length(V) == 0 then "" else V[0] ++ concat(cdr(V)) endif;

output [concat([s1," ",s2])++" "++show(cdr([1,2,3]))];

显示

Compiling hello.mzn
Running hello.mzn
hello world [1, 2, 3]
----------
Finished in 49msec

现在，一个整数列表的cdr似乎是错误的。我认为这是我的错误，尽管我无法发现它。

可以 assertions 帮我吗？由于我要使用 Gecode（然后我有 Gist）实际将我的代码投入生产，我可以遵循这条路线吗？

感谢任何提示...

编辑这个片段

solve satisfy;

function list of string: cdr_s(list of string: v) =
  [v[i] | i in 2..length(v)];

function string: vcat(list of string: V) =
  if length(V) == 0 then "" else V[1] ++ vcat(cdr_s(V)) endif;

output [vcat(["hello"," ","world"])];

报告

MiniZinc: type error: no function or predicate with this signature found: `cdr_s(array[int] of string)'
/tmp/MiniZinc IDE-9nYiuF/hello.ozn:2

Answer 1

MiniZinc 是一种约束求解器，而不是一种普通的编程语言。它知道变量和参数。您定义约束以限定对形成解决方案的变量值的搜索 space。然后使用输出语句以格式化的方式显示解决方案。

您的代码既不包含变量定义也不包含约束。 MiniZinc 中使用断言作为特殊约束 ("constraint assert") 来检测无效参数。这类似于 C/C++.

中的 assert 宏

MiniZinc 2.0 中引入了用户定义的函数，以更优雅的方式编写约束。也支持递归。

看看tutorial and the examples。

Hakan Kjellerstrand 的 MiniZinc page 也是一个很好的开始。

您的 gecode 标签指的是 MiniZinc 支持的求解器后端之一。 MiniZinc IDE 允许 select 后端。一些后端需要安装外部包。 MiniZinc 编译器创建中间 FlatZinc 代码，最终由求解器后端之一解释和求解。

Answer 2

我对你认为的错误感到有点困惑，还有一些其他问题。

模型的输出似乎很好，"cdr([1,2,3])" 给出“[1,2,3]”。名称 "cdr" 表明您需要 "but first" 函数，但 MiniZinc 是默认的基于 1 的系统（而不是基于 0 的系统），因此您的函数可能应该是

 function list of int: cdr(list of int: v) =
   [v[i] | i in 2..length(v)];

由于可以定义数组的索引（例如起始索引为 0），因此更通用的定义是这样的（我对此不是很满意，但您可能明白我的意思）：

function list of int: cdr3(list of int: v) =
   [v[i] | i in index_set(v) diff {min(index_set(v))}];

所以现在你可以这样写：

% ...
array[int] of int: t = array1d(0..3, [1,2,3,4])
output [
   show(cdr3(t))
];

此外，您的 "concat" 函数根本没有被使用，而是它使用的内置 "concat" 。（尝试将您的版本重命名为 "concat1"。）这也是为什么您没有收到 "V[0]" 构造错误（应该给出越界错误）的原因。我原以为尝试重新定义内置函数会产生错误，但 MiniZinc 2.0 在某些方面比 1.6 版更宽松。

我同意 Axel 的一般性评论。作为一种通用的编程语言，MiniZinc 并不是很令人印象深刻（至少在我的书中）。当您向模型添加约束和决策变量时，真正的力量就来了。请注意 MiniZinc list/array 对决策变量的处理不像 Prolog 那样动态。通常，您应该始终将数组视为具有固定长度。

很高兴您开始研究 MiniZinc。希望这些评论对你学习 MiniZinc 有帮助。

/哈坎

调试 minizinc（无论如何，我发现了一个错误吗？）

debugging minizinc (anyway, did I found a bug?)

minizinc

gecode