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?

score 0 · Accepted Answer · edited May 23 '17 at 10:30

0

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.

edited May 23 '17 at 10:30

Community

1
1

answered Nov 18 '16 at 13:54

Patrick Trentin

7,126
3
23
40

2

Expressions are internalized into unique pointers. You could create a map from unsigned or pointers as the keys. Z3_get_ast_id retrieves the identifier of an AST as an unsigned and an operator on the expr class retrieves the AST pointer that is also unique. YOu will also want to pin the expressions in the map using some auxiliary method, e.g., an expr_vector. – Nikolaj Bjorner Nov 18 '16 at 21:42

score 0 · Answer 2 · answered Nov 13 '21 at 18:21

The idea is bad, since z3 is greedy and assumes it has ownership of all expressions/objects. Unfortunately you need to use z3::expr_vector and store the offset positions.

You also have an out of bounds error, because you did not use the correct API for insertion into map/z3::vector (insert()/push_back()).

Use Z3::expr as a map value

2 Answers2