z3 - 剂量 SMTLIB 1.2 具有（获取值）功能，如 SMTLIB 2

Question

我想知道是否SMTLIB1.2有等价于SMTLIB2's ( get-value)。我正在使用and运行不同的SMT编码测试，问题出在输出中，我不断获取模型与 100 多个辅助变量值混合的所有值。Z3 SMT solverSMTLIB1.2

谢谢

Answer 1

抱歉，SMTLIB 1.2 没有获取值。

SMTLIB 1.2 已被弃用，您可以使用具有 2.0 格式的 SMTLIB 1.2 来做所有可能的事情，因此应该没有真正的理由使用 v1.2 的语法。