Доступен ли обратный вызов при удалении объекта Z3_ast?

Question

Я использую C++ API для z3, поэтому мне не нужно беспокоиться о подсчете ссылок или управлении памятью.

Тем не менее, я хотел бы хранить информацию о z3 AST, используя std::map вдоль линий std::map<Z3_ast, some_struct>,

Когда конкретный объект Z3_ast удаляется, я хотел бы удалить его запись из этой карты.

Есть ли способ настроить функцию обратного вызова, которая будет вызываться, когда счетчик ссылок на объект Z3_ast возвращается к 0, а объект Z3_ast удаляется?

Answer 1

Нет, такого обратного вызова нет, но можно предположить, что вы могли бы взломать API для его предоставления. Однако до тех пор, пока существует хотя бы одна ссылка на Z3_ast, счетчик ссылок никогда не должен уменьшаться до 0 в любом случае (и ваша карта содержит ссылку, т. е. ссылку на карте).

Если вы не увеличиваете счетчик ссылок в то время, когда Z3_ast хранится на карте, парадигма подсчета ссылок нарушена, что, вероятно, приведет к ошибкам, которые очень трудно отладить.