Use Z3::expr as a map value

Question

I got difficulties in using Z3::expr as a map value type. The compiler complains no default constructor can be used. A toy example looks like the following.

#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;
}

The Compiler(Clang++) complains

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)) {}

Using a vector to wrap the expr or find method in map as alternatives seems to be fine. Is there any way to use expr as a map value type + [] operator directly?

Answer 1

This is a general issue with map: [] requires an empty constructor for the instance type, see this and this.

(Ugly) Tweak. You might want to derive a sub-class of map, add a local reference to a z3 context and provide this parameter either through the constructor of map_subclass or a method. Then, you should override [] so that it uses this reference to create a new expr instance with the constructor expr(context &c), instead of attempting to use expr().

My knowledge of z3's internals is limited, but as far as I know this should not break anything.