2

我熟悉 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 似乎是错误的。我认为这是我的错误，尽管我无法发现它。

断言可以在这里帮助我吗？由于我将使用 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
4

2 回答 2

4

我对您认为是错误的内容有些困惑，并且还有其他一些问题。

模型的输出似乎很好，“cdr([1,2,3])”给出“[1,2,3]”。名称“cdr”表明您想要“但首先”功能，但 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 对决策变量的列表/数组处理不像 Prolog 那样动态。通常，您应该始终将数组视为具有固定长度。

很高兴您开始研究 MiniZinc。我希望这些评论在你学习 MiniZinc 时能真正帮助到你。

/哈坎

于 2015-01-23T07:02:49.970 回答
3

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

您的代码既不包含变量定义也不包含约束。断言被用作MiniZinc特殊约束（“约束断言”）来检测无效参数。这类似于assert.C/C++

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

查看教程和示例。

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

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

于 2015-01-22T23:59:45.430 回答