Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
z3 -smt2 <filename>只输出“sat”或“unsat”。如果满足约束,我希望 Z3 输出模型,如果不满足,则输出 unsat 核心。我应该使用 Z3 的哪些选项?
z3 -smt2 <filename>
没有命令行选项,因为在 SMTLIB2 中它们是单独的命令,(get-model)并且仅在分别返回 sat 或 unsat(get-unsat-core)时才定义。(check-sat)
(get-model)
(get-unsat-core)
(check-sat)
无论是否使用这些或其他命令,都必须启用选项model和,以使求解器跟踪正确的信息,否则和命令以后可能会失败。unsat-core(get-model)(get-unsat-core)
model
unsat-core