z3 - 使用 Z3::expr 作为映射值

Question

我在使用 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值类型+[]运算符？

Answer 1

这是 map 的一个普遍问题:[] 需要实例类型的空构造函数，请参阅 this和 this .

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

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