如何将旧的 z3::expr(Oldvec) 更改为新的 z3::expr(Vec)？答案

【问题标题】：How to change an old z3::expr(Oldvec) to a new z3::expr(Vec)?如何将旧的 z3::expr(Oldvec) 更改为新的 z3::expr(Vec)？
【发布时间】：2020-04-14 14:32:39
【问题描述】：

我想像这样更改旧的 z3::expr(Oldvec)：

OldVec is:(and (= (= R4 0) true) (= (= R6 R7) true))

到一个新的 z3::expr(Vec) 像这样：

Vec is:(and (= (= R4 0) false) (= (= R6 R7) true))

我曾尝试将字符串更改为 z3::expr，如下所示：

void changeZ3(z3::expr &OldVec) {
    std::string s="(set-info :status unknown)\n"
                  "(declare-fun R4 () Int)\n"
                  "(declare-fun R7 () Int)\n"
                  "(declare-fun R6 () Int)\n"
                  "(assert\n"
                  " (= (= R4 0) false))\n"
                  "(assert\n"
                  " (= (= R6 R7) true))\n"
                  "(check-sat)";
    std::cout<<"OldVec is:"<<OldVec<<"\n";
    z3::expr Vec=C.parse_string(s.data());
    std::cout<<"Vec is:"<<Vec<<"\n";
    OldVec=Vec;
}

我打印了 Oldvec 和 Vec，它们看起来一样：

OldVec is:(and (= (= R4 0) true) (= (= R6 R7) true))    
Vec is:(and (= (= R4 0) false) (= (= R6 R7) true))

changeZ3返回后，我做了Solver.add(Vec)这样的操作：

z3::expr Vec = Ctx.parse_file(FormulaFile); //FormulaFile save z3::expr which looked like "s" on the top|^    
changeZ3(Vec);
Solver.add(Vec);

然后当我像这样Solver.add(Vec) 时遇到异常：

terminate called after throwing an instance of 'z3::exception'

为什么会这样？还有其他方法可以更改 z3::expr 吗？

【问题讨论】：

标签： c++ z3

【解决方案1】：

一般来说，对parse_file 的调用需要被告知范围内的排序和声明。也就是说，虽然您在 Vec 中成功构造了“表达式”，但您仍然需要将排序 Int 以及 R4、R7 和 R6 的声明插入到上下文中。

这是 z3 编程中的一个常见问题：您必须记住，当您调用 Solver.add 时，必须适当设置 Ctx 以使这些公式“有意义”。

一般来说，您应该避免像这样“解析”字符串并将它们添加到求解器中。相反，您应该在已有的上下文中工作，并使用表达式 AST 直接创建表达式。

【讨论】：