z3 - z3 战术无法通过在线界面获得

Question

我打印 Z3 中的战术列表。

for (int i=0;i < Z3_get_num_tactics(z3_cont);i++)
    cout<<"\n"<<Z3_get_tactic_name(z3_cont,i);

此外，我发现并非所有这些都可以通过在线界面使用。问题是：我在哪里可以找到关于它们的文档（可能是一些论文）？哪些在在线界面中可用？

score 1 · Accepted Answer

在http://rise4fun.com/z3py上有一个关于使用策略的完整在线教程。它包含指向论文的指针，包括：Leonardo de Moura 和 Grant Passmore。SMT 求解中的战略挑战，人工智能讲义第 7788 卷。Springer，2013。它解释了基本组合器的使用（失败、跳过和-然后等）。可从 http://research.microsoft.com/en-us/um/people/leonardo/publications/index.html访问

要获取有关每种策略的最详细信息，可以从http://z3.codeplex.com公开获得 Z3 源代码。

1 回答 1