z3::tactic和z3::goal的目的是什么？

Question

3

我看到可以创建目标，将它们添加到策略中，并从策略创建求解器。

这种方法相比于直接创建 z3::solver 实例并将表达式添加到其中有什么优势呢？

- user3703887

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Christoph Wintersteiger · Accepted Answer

战术有不同的目的。您可以创建一个包含您的断言/约束条件的目标，然后在目标上运行战术，其结果将是一组新的（子）目标，即新的断言/约束条件。求解器确定可满足性并不会产生新的（子）目标。

战术可以转换为求解器，使得生成的求解器将运行战术，如果结果是明确的（平凡的sat/unsat），它将返回该结果。如果战术产生的子目标不确定，它将返回“未知”。