发出多个 (check-sat) 调用直到 returns unsat
issuing multiple (check-sat) calls until it returns unsat
z3 版本 4.6 的发行说明提到了一项新功能 "issuing multiple (check-sat) calls until it returns unsat"。
这相当于 ALLSAT 吗？
在哪里可以找到有关此功能的更多文档或示例？
不，这是为了解决这个问题：https://github.com/Z3Prover/z3/issues/1008
z3 不支持 ALLSAT 命令；尽管使用 "assert the negation of the previous model and re-check" 循环对其进行编码很容易。大多数高级接口将此作为一个层提供在使用 SMT-Lib2 的可能性之上。如果您确实需要对此的支持，最好首先说服 SMTLib 人员 (http://smtlib.cs.uiowa.edu/)，这样就会开发出一种标准的方法，并且可以由多个求解器实施。
z3 版本 4.6 的发行说明提到了一项新功能 "issuing multiple (check-sat) calls until it returns unsat"。
这相当于 ALLSAT 吗？
在哪里可以找到有关此功能的更多文档或示例？
不，这是为了解决这个问题：https://github.com/Z3Prover/z3/issues/1008
z3 不支持 ALLSAT 命令；尽管使用 "assert the negation of the previous model and re-check" 循环对其进行编码很容易。大多数高级接口将此作为一个层提供在使用 SMT-Lib2 的可能性之上。如果您确实需要对此的支持，最好首先说服 SMTLib 人员 (http://smtlib.cs.uiowa.edu/)，这样就会开发出一种标准的方法，并且可以由多个求解器实施。