订单理论的自定义理论求解器？

Question

我的程序，反应式有限状态系统的有界合成器，生成 SMT 查询来注释（未解释的）系统的产品自动机和规范。本质上，它是一个带有未解释功能的模型检查。如果注释存在 => Z3 找到的模型满足规范。查询包含：

• 数据类型（用于编码系统和规范自动机的状态）
• >= (greater), > (strictly) (指定自动机系统*spec的状态排序函数，用于搜索状态不佳的lassos)，或者换句话说，自动机的状态排序，
• 具有布尔域和范围的未解释函数
• 所有子句都是喇叭子句

一个例子是https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2 （'forall' 用于对函数的“无关”输入进行编码）

目前查询从整数算术中采用严格更大的> 运算符（即排名函数具有Int 范围）。

问题：是否值得在 Z3 中为此类查询开发自定义理论求解器？它可以利用基于 DFS 的套索搜索，这可能比整数理论求解器（或 diff-neg 策略）更快。

或者 Z3 已经有效地处理了这个问题？ （有效地意味着“类似于基于图的套索搜索”）。

Answer 1

算术不是基准测试的瓶颈。 我们可以通过使用来检查

valgrind --tool=callgrind z3 full_arbiter2.smt2 
kcachegrind

Valgrind 和 kcachegrind 在大多数 Linux 发行版中都可用。 所以，我认为如果你为顺序理论实施求解器，你不会获得显着的性能提升。 一个瓶颈是数据类型理论。如果您使用位向量对类型 Q 和 T 进行编码，您可能会获得性能提升。另一个瓶颈是量词推理。在调用 Z3 之前，您是否尝试过扩展它们？ 在 Z3 中，qe（消除量词）策略本质上将扩展布尔量词。 通过替换，我得到了一点加速

(check-sat)

与

(check-sat-using (then qe smt))