Как добавить новое ограничение для существующей объявленной функции в z3, используя c ++?

Question

Я хотел бы знать, есть ли способ добавить некоторые новые ограничения для существующих объявленных переменных в решателе, не получая модель.

Например, если у меня есть 2 функции объявления:

(declare-fun k!648 () (_ BitVec 8))
(declare-fun k!647 () (_ BitVec 8))

и некоторые ограничения с ним.

Как я могу получить их объявленные имена вообще?

Ситуация в том, что я хочу добавить больше ограничений для существующих "переменных?" в ограничении и решить их вместе. Но я не понимаю, как получить существующие «переменные»? и затем сформируйте новое ограничение, которое также верно для решателя.

Answer 1

Непонятно, о чем ты спрашиваешь. Обратите внимание, что k!648 и k!647 в вашем примере на самом деле не являются функциями, это просто 8-битные векторы. (Имя declare-fun сбивает с толку, по общему признанию.)

Первое, что нужно понять, это откуда эти имена? Это в сценарии вы кормите z3? Тогда вы спрашиваете не ту сторону: вам следует спросить программу / систему, которая сгенерировала этот тест. z3 может генерировать такие имена, но только в моделях.

Попробуйте указать MCVE: https://stackoverflow.com/help/minimal-reproducible-example