我的程序,反应有限状态系统的有限合成器,产生SMT查询以注释(未解释的)系统的产品自动机和规范 . 本质上,它是一个使用未解释函数检查的模型 . 如果注释存在=> Z3找到的模型满足规范 . 查询包含:
-
数据类型(用于编码系统和规范自动机的状态)
-
=(更大),>(严格地)(指定自动机系统*规范的状态的排序函数,用于搜索具有不良状态的套索)或换句话说,对该自动机的状态的排序,
-
具有布尔域和范围的未解释函数
-
所有条款都是角色条款
一个例子是https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2('forall'用于编码函数的"don't care"输入)
当前查询从整数算术中获取严格更大的 >
运算符(即排名函数具有 Int
范围) .
Question :是否值得在Z3中为此类查询开发自定义理论解算器?它可以利用基于DFS的lassos搜索,这可能比整数理论求解器(或差异策略)更快 .
或Z3已经有效地处理了这个问题? (有效地意味着“与基于图形的套索搜索相当”) .
1 回答
算术不是您的基准测试的瓶颈 . 我们可以通过使用来检查
大多数Linux发行版都提供Valgrind和kcachegrind . 因此,如果您为订单理论实现求解器,我认为您不会获得显着的性能提升 . 一个瓶颈是数据类型理论 . 如果使用位向量对Q和T类型进行编码,则可能会提高性能 . 另一个瓶颈是量词推理 . 在调用Z3之前,您是否尝试过扩展它们?在Z3中,
qe
(量词消除)策略将基本上扩展布尔量词 . 我通过更换获得了一个小的加速同