如何在Z3＆＃x27的SMT2语法中使用策略？
我通过其SMT2接口与Z3进行交互。假设，我写下了以下命令：
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun r () Int)
(assert (and (<= (+ (* 4 p) (* 3 q)) (- r 10)) (<= (+ (* 4 p) (* 3 q)) (- r 12))))
(apply simplify)
现在，我在形式中获得了一个目标列表，
(goals
(goal …)
(goal …)
…
)
该怎么办？
另一个问题，有什么文件吗？我应该在哪里寻找它？
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
战术是Z3发明；因此，您将找不到有关如何从Smtlib角度使用它们的任何正式文档。
通常，您不仅使用
应用。相反，您使用方法check-sat-using，将战术作为参数。通常，check-sat使用（使用smt），即使用smttactic。就您的示例而言，您可以说：
这将使问题降低到
SAT。这个想法是，您可以使用这些“策略”来指导求解器找到解决方案（或更快）。策略通常旨在从C/C ++/Java等高级接口中使用，不幸的是，它们的记录并不那么充分。通过
策略也记录在，尽管它再次使用python接口而不是smtlib。
Tactics are a z3 invention; so you will not find any official documentation on how they should be used from an SMTLib perspective.
In general, you don't just use
apply. Instead, you use the methodcheck-sat-using, that takes a tactic as an argument. In general,check-satis equivalent to(check-sat-using smt), i.e., using thesmttactic.For your example, you can say:
this would reduce the problem to
sat. The idea is that you can use these "tactics" to guide the solver to find a solution (or go faster).Tactics are usually intended to be used from higher-level interfaces, such as C/C++/Java etc., and unfortunately they aren't all that well documented. Read through http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm, which is using the Python interface, but you can use the same ideas directly from smtLib as well.
Tactics are also documented at https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-tactics, though again it uses the Python interface not SMTLib.