Z3 版本 2.19 和 3.2 w.r.t. 之间有什么区别吗?SMTLIB-2 代码语法?

问题描述

安装 Z3 V3.1 后，以下 SMT-LIB 代码不起作用.在我之前的版本(Z3 V2.19)中已经相当不错了.

After installing Z3 V3.1, following SMT-LIB code is not working. It was quite good in my earlier version (Z3 V2.19).

(define-fun getIP ((o0 Int) (o1 Int) (o2 Int) (o3 Int)) BitVec[32]

     (bvor (bvshl (int2bv[32] o0) (int2bv[32] 24))

          (bvshl (int2bv[32] o1) (int2bv[32] 16))))       

(declare-funs ((dip BitVec[32]) (m BitVec[32])))

(declare-funs ((s Bool) (d Bool) (y Int) (z Int)))

(declare-funs ((r0 Bool) (r1 Bool) (f Bool)))

(declare-funs ((r0do0 Int) (r0do1 Int) (r0do2 Int) (r0do3 Int) (r0m Int) (r0nh Int)))

(declare-funs ((r1do0 Int) (r1do1 Int) (r1do2 Int) (r1do3 Int) (r1m Int) (r1nh Int)))

(declare-funs ((fso0 Int) (fso1 Int) (fso2 Int) (fso3 Int) (fsm Int)))

(declare-funs ((fdo0 Int) (fdo1 Int) (fdo2 Int) (fdo3 Int) (fdm Int) (fp Int) (fnh Int)))

(declare-funs ((so0 Int) (so1 Int) (so2 Int) (so3 Int)))

(declare-funs ((do0 Int) (do1 Int) (do2 Int) (do3 Int)))

(assert (=> f (and (= fso0 172) (= fso1 16) (= fso2 0) (= fso3 0) (= fsm 16) 

          (= fdo0 150) (= fdo1 96) (= fdo2 1) (= fdo3 0) (= fdm 24) 

          (= fp 0))))

(assert (=> r0 (and (= r0do0 150) (= r0do1 96) (= r0do2 0) (= r0do3 0) (= r0m 16))))

(assert (=> r1 (and (= r1do0 172) (= r1do1 16) (= r1do2 0) (= r1do3 0) (= r1m 16))))

(assert (=> s (and (= so0 172) (= so1 16) (= so2 0) (= so3 1))))

(assert (=> d (and (= do0 150) (= do1 96) (= do2 1) (= do3 120))))

(assert (= m (int2bv[32] 16)))


(assert ((= dip (getIP so0 so1 so2 so3))))

(check-sat) ; sat

(model)

我需要在上面的代码中更改什么才能在 3.1 版本中运行它.

What do I need to change in the above code to run it in the version 3.1.

推荐答案

Z3 3.x 符合 SMT 2.0 标准.版本 2.x 不是.例如，SMT 2.0 中没有declare-funs 命令；32 位向量排序是 (_ BitVec 32) 而不是 BitVec[32].Z3 仍然支持旧的不兼容的 SMT 2.0 解析器.您只需要提供命令行选项 -smtc.话虽如此，我建议您转向 SMT 2.0 标准.SMT 2.0 输入语言是 Z3 的官方输入语言.此外，许多新功能仅在此前端可用(例如:参数类型).

Z3 3.x is compliant with the SMT 2.0 standard. Versions 2.x were not. For example, there is no declare-funs command in SMT 2.0; the 32-bitvector sort is (_ BitVec 32) instead of BitVec[32]. Z3 still supports the old non-compliant SMT 2.0 parser. You just have to provide the command line option -smtc. That being said, I suggest you move to SMT 2.0 standard. The SMT 2.0 input language is the official input language for Z3. Moreover, many new features are only available in this frontend (Example: parametric types).

这篇关于Z3 版本 2.19 和 3.2 w.r.t. 之间有什么区别吗?SMTLIB-2 代码语法?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！