通过标准输入/smt2 检查假设？

【问题标题】：check_assumptions via stdin/smt2?通过标准输入/smt2 检查假设？
【发布时间】：2012-02-27 08:50:51
【问题描述】：

SMT2 标准（或它的 Z3 扩展）是否提供与 API 调用“check_assumptions”等效的命令？根据Josh Berdine 的说法，使用保护文字和 check_assumptions 通常比使用 push-pop 范围更快。但是，我现在仍然坚持通过 stdio 使用 Z3，而使用 (check-assumoptions p) 只会产生 unsupported。

【问题讨论】：

标签： command z3 stdio

【解决方案1】：

如果您使用的是 smt2 命令语言，也许 'z3 -smtc -in' 提供的 'get-core' 命令可以完成这项工作？请注意，我认为此命令不在 SMT-LIB 2 标准中。

干杯，乔什

【讨论】：

谢谢，成功了！ SMT-LIB2标准中确实没有提到，但我目前只针对Z3。
快速说明：-smtc 选项启用已弃用的解析器（它不符合 SMT 2.0 标准）。此前端将在 Z3 的未来版本中移除。请参阅：stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3 以了解新 SMT 2.0 解析器中的未饱和内核提取。