При добавлении ограничений в мой код, я обнаружил, что мне нужно добавить одинаковые ограничения в вектор выражения несколько раз. Есть ли какой-либо API для определения того, являются ли два выражения одинаковыми, чтобы я мог удалить избыточные выражения?Z3 проверить, являются ли два выражения одинаковыми
Выражения всегда интернализируются до уникальных указателей. Поэтому, если вы создаете два выражения, используя одни и те же подвыражения, указатели на них будут одинаковыми. Вы можете просто использовать равенство указателя.
Выражения также имеют так называемые «идентификаторы». Вызов C для получения идентификаторов называется Z3_ast_get_id, есть соответствующие вызовы в других API для других языков программирования (из C++ вам все равно придется использовать Z3_ast_get_id, с C# и Java, он называется «Id»/«id»).
Еще один вопрос: я заметил, что возвращаемый тип ** Z3_get_ast_id ** не имеет знака, поэтому есть 2^32 идентификатора. Возможно ли, что два выражения будут иметь один и тот же идентификатор, так как может быть более 2^32 выражений? –