1

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

4

1 回答 1

2

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

干杯，乔什

于 2012-02-27T09:25:21.227 回答