使用 Z3::expr 作为地图值答案

【问题标题】：Use Z3::expr as a map value使用 Z3::expr 作为地图值
【发布时间】：2017-04-01 15:13:51
【问题描述】：

我在使用 Z3::expr 作为地图值类型时遇到了困难。编译器抱怨不能使用默认构造函数。一个玩具示例如下所示。

#include <z3++.h>
#include <map>
//#include <vector>

using namespace std;
using namespace z3;

int main() {
  map <int, expr> m;
  context c;
  m[1] = c.bool_const("x");
  return 0;
}

编译器（Clang++）抱怨

no matching constructor for initialization of 'mapped_type' (aka 'z3::expr')
      __i = insert(__i, value_type(__k, mapped_type()));

in instantiation of member function 'std::map<int, z3::expr, std::less<int>,
std::allocator<std::pair<const int, z3::expr> > >::operator[]' requested here
m[1] = c.bool_const("x");

/usr/include/z3++.h:562:9: note: candidate constructor not viable: requires single argument 'c', but no arguments were provided
    expr(context & c):ast(c) {}
    ^
/usr/include/z3++.h:564:9: note: candidate constructor not viable: requires single argument 'n', but no arguments were provided
    expr(expr const & n):ast(n) {}
    ^
/usr/include/z3++.h:563:9: note: candidate constructor not viable: requires 2 arguments, but 0 were provided
    expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}

使用向量将 expr 或 find 方法包装在 map 中作为替代方法似乎很好。有没有办法直接用expr作为map值类型+[]操作符？

【问题讨论】：

标签： z3

【解决方案1】：

这是 map 的一般问题：[] 要求实例类型的构造函数为空，请参阅 this 和 this。

（丑陋的）调整。 您可能想要派生map 的子类，添加对z3 context 的本地引用，并通过map_subclass 的构造函数或方法提供此参数。然后，您应该重写 [] 以便它使用此引用来创建具有构造函数 expr(context &c) 的新 expr 实例，而不是尝试使用 expr()。

我对 z3 内部结构的了解有限，但据我所知这不会破坏任何东西。

【讨论】：

表达式被内化为唯一的指针。您可以从无符号或指针作为键创建映射。 Z3_get_ast_id 检索作为无符号的 AST 标识符，并且 expr 类上的运算符检索也是唯一的 AST 指针。您还需要使用一些辅助方法（例如 expr_vector）将表达式固定在地图中。

【解决方案2】：

这个想法很糟糕，因为 z3 是贪婪的，并假设它拥有所有表达式/对象的所有权。不幸的是，您需要使用 z3::expr_vector 并存储偏移位置。

您还有一个越界错误，因为您没有使用正确的 API 来插入 map/z3::vector (insert()/push_back())。

【讨论】：