Z3 Java API: когда нужно размещать выражения/объекты Z3?

Question

В моем Java-коде я вызываю Z3 в цикле, чтобы проверить формулу (которая зависит от индекса цикла и отличается для каждой итерации), пока формула не станет выполнимой, как указано в следующем фрагменте псевдокода:

Тем не менее, я быстро сталкиваюсь с проблемами памяти (т. Е. Вызывается Z3Exception с сообщением «из памяти»), и я чувствую, что я, вероятно, неправильно размещаю созданные Z3Objects.

Поскольку я не нашел информации об этом (я только что нашел Z3 Java API documentation or tutorial и Performance issues about Z3 for Java), мои вопросы:

1. При вызове solver.dispose(), все содержащиеся BoolExpr расположены так или мне нужно помнить о них где-то и звоните .dispose() на любой из них?
2. Было бы более сложно перенести создание и удаление контекста и решателя из цикла и вместо этого использовать solver.push() и solver.pop() внутри цикла?
3. Что еще Z3Objects должен ли я «вручную» в данном случае?

Answer 1

Когда выбрано сообщение Z3Exception с сообщением «из памяти», это означает, что на родной libz3.dll закончилась нехватка памяти. Устранение как решателя, так и контекста в каждой итерации цикла действительно лучшее, что можно сделать (некоторые вещи все еще остаются в памяти, например, символы). Однако обратите внимание, что объекты Solver и Context выглядят как крошечные объекты для сборщика мусора (они всего лишь указатель, а Java не может видеть, что находится за указателем). Итак, первое, что нужно попробовать, это добавить звонок в System.gc() в надежде, что все объекты Z3 будут фактически собраны в этот момент. Кроме того, я, похоже, напоминаю, что виртуальная машина Java имеет ограничение по умолчанию для памяти, которое меньше, чем можно было бы ожидать, но они могут быть установлены с помощью опцийи -Xmx.