z3 - 如何让z3命令行输出模式（或unsat core）而不是sat/unsat？

Question

z3 -smt2 <filename>只输出“sat”或“unsat”。如果满足约束，我希望 Z3 输出模型，如果不满足，则输出 unsat 核心。我应该使用 Z3 的哪些选项？

Answer 1

没有命令行选项，因为在 SMTLIB2 中它们是单独的命令，(get-model)并且仅在分别返回 sat 或 unsat(get-unsat-core)时才定义。(check-sat)

无论是否使用这些或其他命令，都必须启用选项model和，以使求解器跟踪正确的信息，否则和命令以后可能会失败。unsat-core(get-model)(get-unsat-core)