时间戳

首页 > 解决方案 > 处理 Z3 中的引用表达式

z3 - 处理 Z3 中的引用表达式

问题描述

我目前正在unsat_core大学的模型检查课程中使用 Z3 的功能。

当尝试使用 Z3 在核心中为我提供的假设时，就会出现问题：

例如：

z3::expr_vector unsat_core = exp_solver.unsat_core();
for(auto const c : unsat_core) {
  DEBUG << "\n" << c;
}

打印一个包含例如这样一个表达式的列表：

|(let ((a!1 (bvnot (ite (= current_state_V0 ((_ zero_extend 1) #b11)) #b1 #b0))))
 (let ((a!2 (bvnot (bvand a!1 (bvnot ((_ extract 2 2) current_state_V0))))))
 (let ((a!3 (bvor a!2
                 (ite (= next_state_V0 (bvadd current_state_V0 #b001)) #b1 #b0)
                 (bvnot #b1))))
  (= a!3 #b1))))|

我们通过这个包装器添加和跟踪表达式：

void add_and_track(z3::solver& s, z3::expr_vector const &v)
{
  check_context(s, v);
  for (unsigned i = 0; i < v.size(); ++i)
  {
    s.add(v[i], v[i].to_string().c_str());
  }
}

我现在需要用我的启动变量对这些假设进行编码，我打算使用z3::expr::substitute它，但这似乎不起作用。

DEBUG << unsat_core[0];
z3::expr foo = unsat_core[0].substitute(V0, V1);
DEBUG << unsat_core[0];
DEBUG << foo;

所有DEBUG调用都从上面打印出完全相同的（引用的）表达式。

V0并且V1是z3::expr_vectors 包含变量和引发变量，并且DEBUG是std::cout.

我最好的猜测是这些表达式被“引用” 了https://www.lri.fr/~conchon/TER/2013/2/SMTLIB2.pdf#page=22这是正确的吗？

我想要实现的是能够替换或提取表达式，正如我猜测的那样，引用。

标签： z3substitution

解决方案

推荐阅读