首页 文章

订单理论的定制理论求解器?

提问于
浏览
2

我的程序,反应有限状态系统的有限合成器,产生SMT查询以注释(未解释的)系统的产品自动机和规范 . 本质上,它是一个使用未解释函数检查的模型 . 如果注释存在=> Z3找到的模型满足规范 . 查询包含:

  • 数据类型(用于编码系统和规范自动机的状态)

  • =(更大),>(严格地)(指定自动机系统*规范的状态的排序函数,用于搜索具有不良状态的套索)或换句话说,对该自动机的状态的排序,

  • 具有布尔域和范围的未解释函数

  • 所有条款都是角色条款

一个例子是https://dl.dropboxusercontent.com/u/444947/posts/full_arbiter2.smt2('forall'用于编码函数的"don't care"输入)

当前查询从整数算术中获取严格更大的 > 运算符(即排名函数具有 Int 范围) .

Question :是否值得在Z3中为此类查询开发自定义理论解算器?它可以利用基于DFS的lassos搜索,这可能比整数理论求解器(或差异策略)更快 .

或Z3已经有效地处理了这个问题? (有效地意味着“与基于图形的套索搜索相当”) .

1 回答

  • 1

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

    valgrind --tool=callgrind z3 full_arbiter2.smt2 
    kcachegrind
    

    大多数Linux发行版都提供Valgrind和kcachegrind . 因此,如果您为订单理论实现求解器,我认为您不会获得显着的性能提升 . 一个瓶颈是数据类型理论 . 如果使用位向量对Q和T类型进行编码,则可能会提高性能 . 另一个瓶颈是量词推理 . 在调用Z3之前,您是否尝试过扩展它们?在Z3中, qe (量词消除)策略将基本上扩展布尔量词 . 我通过更换获得了一个小的加速

    (check-sat)
    

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

相关问题