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 api只访问（assert…行，并从那里进行折叠（如果我错了，请纠正我）我能想到的唯一解决方案是修改文件，使define-fun变成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-files，或者一直将问题转化为Z3-API调用（不包括字符串解析等）。上次我检查过，CBMC有一个Z3的API后端，所以这应该很简单。