z3:在断言中添加变量声明

Question

有没有办法将函数定义作为断言添加到求解器中？

我目前正在研究C++文件的有界模型检查，能够将定义添加为断言语句，这将为求解器断言和代码行提供一种一对一的对应关系。

例如，我有以下玩具程序：

int x, y;
x = y + 1;
assert(x != 0)

CBMC生成以下smt2文件：

(declare-fun |main::1::y!0@1#1| () (_ BitVec 32))
(define-fun |main::1::x!0@1#2| () (_ BitVec 32) (bvadd (_ bv1 32) |main::1::y!0@1#1|))
(define-fun |B0| () Bool (= |main::1::y!0@1#1| |main::1::y!0@1#1|))
(assert (not (not (= |main::1::x!0@1#2| (_ bv0 32)))))

z3_parse_string返回以下公式。

Not(Not(1 + main::1::y!0@1#1 == 0))

我想知道是否有可能将函数声明也添加到求解器中，类似于：

(x!0@1#2 == 1 + y!0@1#1) AND !(x!0@1#2 == 0)

因此，每个子句松散地对应一行源代码。

据我所知，目前z3_parse_string应用程序接口只访问(断言...行并从那里进行折叠(如果我错了，请纠正我)我能想到的唯一解决方案是修改文件，这样定义就变成了declare-fun，并将定义推到一个新的断言行中，如下所示：

(declare-fun |main::1::x!0@1#2| () (_ BitVec 32))
(assert (= |main::1::x!0@1#2| (bvadd (_ bv1 32) |main::1::y!0@1#1|)))

在此之前，非常感谢您。

Answer 1

如果没有看到更多的示例或实际代码(CBMC或Z3)，我也没有更好的解决方案。一般来说，我会劝阻人们完全不要使用Z3_parse_string，因为它通常会造成更多的混乱。最好是通过命令行切换到完整的smt2文件，或者一直将问题转换为Z3-API调用(不包括字符串解析等)。据我所知，CBMC有一个用于Z3的API后端，所以这应该很简单。