【发布时间】：2015-11-16 14:59:41
【问题描述】：
有没有办法使用 SMTLIB2 语法检索所有令人满意的分配？
我使用的求解器是 Z3 和 CVC4。
【问题讨论】：
【发布时间】：2015-11-16 14:59:41
【问题描述】：
虽然在“纯”SMTLIB2 中无法做到这一点，即仅使用单个文件且没有外部输入，但如果您有一个可以与求解器交互的应用程序，那么有一个标准技巧可以做到这一点。您在交互模式下运行求解器，您可以一次向其发送一个 SMTLIB2 命令，然后通过以下方式与其交互（伪代码）：
def get_all_assignments(instance):
create solver in interactive mode
for each declaration, assertion, etc. in instance:
send assertion to solver
let response := None
while response is not UNSAT:
send command '(check-sat)' to solver and get response
if response is SAT:
send command '(get-model)' to solver and get model
print model
send the solver a new assertion which is the negation of the model
实际上，每次找到令人满意的分配时，您都会向模型添加一个新约束，以防止求解器再次找到该分配，并要求它重新求解。当求解器返回 UNSAT 时，您就知道您已经找到了每一个令人满意的任务。
有关此主题和 Z3 实现的进一步阅读，请参阅 Z3: finding all satisfying models 和 Z3py: checking all solutions for equation。
【讨论】：