1
SMT2标准（或其Z3扩展）是否提供等效于API调用“check_assumptions”的命令？根据Josh Berdine，与使用push-pop作用域相比，使用guard文字和check_assumptions通常更快。但是，现在我坚持使用Zdio通过stdio，并且使用(check-assumoptions p)仅产生unsupported。通过stdin/smt2的check_assumptions？
A
回答
2
如果您使用的是smt2命令语言，可能'z3 -smtc -in'提供的'get-core'命令可以完成这项工作吗？请注意，我认为该命令不在SMT-LIB 2标准中。
干杯，乔希
谢谢，这是诀窍！ SMT-LIB2标准确实没有提到，但我目前只针对Z3。 – 2012-02-27 12:44:18
快速注意：-smtc选项启用了不推荐的解析器（它不符合SMT 2.0标准）。这个前端将在未来版本的Z3中被删除。请参阅：http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3，了解新的SMT 2.0解析器中不存在的内核抽取问题。 – 2012-02-27 15:32:37
谢谢，符合SMT 2.0标准当然更好。 – 2012-02-28 13:19:09