我发现我可以创建目标，将它们添加到策略中，然后根据策略创建求解器。
与简单地创建 z3::solver 实例并将我的表达式添加到其中相比，这种方法有什么优势？
最佳答案
战术有不同的目的。您可以创建一个包含您的断言/约束的目标，然后在该目标上运行一个策略，其结果将是一组新的(子)目标，即新的断言/约束。求解器确定可满足性并且不会产生新的(子)目标。
策略可以转换为求解器，这样生成的求解器将运行策略，如果结果是确定的(平凡的 sat/unsat)，它将返回该结果。如果该策略产生的子目标不是决定性的，它将返回“未知”。
关于z3 - z3::tactic 和 z3::goal 的用途，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/36236232/