目的:Z3:战术和Z3：：目标

Question

我看到我可以创造目标，把它们添加到战术中，并从战术中创造出一个解决者。

与简单地创建z3::solver实例并将表达式添加到其中相比，这种方法的优点是什么？

Answer 1

战术有不同的目的。您可以创建一个包含断言/约束的目标，然后对目标运行一个策略，其结果将是一组新的(子)目标，即新的断言/约束。求解者决定可满足性，不会产生新的(子)目标。

战术可以转换为求解者，这样得到的解将运行策略，如果结果是决定性的(琐碎的sat/unsat)，它将返回该结果。如果该战术产生的子目标不是决定性的，它将返回“未知”。