【发布时间】：2020-06-22 10:37:04
【问题描述】：
SMT-LIB 标准支持任意属性，但只规定了很少的属性，例如:pattern。而 Z3 目前只支持少数选定的属性，并对无法识别的属性发出警告。
支持哪些属性，它们的典型用例是什么？
【问题讨论】：
标签： z3
【发布时间】：2020-06-22 10:37:04
【问题描述】：
属性
-
:named：命名术语可以包含在未饱和核心中 -
:weight：较重的量词使 Z3 更快地达到其量词实例化深度阈值 -
:qid：识别量词，例如获取实例化统计信息时 -
:pattern：何时在电子匹配中实例化量词的语法提示 -
:no-pattern: 防止 Z3 在推断模式时使用某些术语 -
:ex-act: 好像是死代码，要删除 -
:skolemid：专用于VCC/Boogie使用 -
:lblneg、:lblpos：关联Boogie标签，追踪反例来源
注意事项
- 部分信息由 Z3 自己的 Nikolaj Bjorner 提供，另请参阅 Z3 issue #4536。
- 另见 Z3 源文件smt2parser.cpp
【讨论】：