Добавление предложений непосредственно к решателю z3

Question

У меня есть AIG (и-инверторный график), который я продолжаю изменять, и выполнимость которого я должен проверить инкрементным образом с помощью Z3. Я могу генерировать CNF-представление AIG и в идеале хотел бы передать эти предложения непосредственно решателю и называть его повторно из моего кода. Есть ли способ, с помощью которого я могу напрямую добавлять предложения (или AIG) к решателю Z3 через API C/C++?

Answer 1

Да, вы можете просто утверждать новые утверждения, которые внутренне переведены в пункты.

Обратите внимание, что для многих задач с постепенным решением Z3 не использует готовый SAT-решатель, но это собственный SMT-решатель, который включает в себя некоторые функции SAT-решателей, но не все, и которые изначально обрабатывает небулевые задачи. Таким образом, не обязательно, что взлом решателя для инъекционных предложений напрямую приведет к значительному повышению производительности.

У Z3 также есть выделенный логический SAT-ресивер, и если вы решаете чисто логические задачи, этот решатель, скорее всего, будет намного быстрее. Вы можете заставить его использовать этот решатель, заменив (check-sat) на (check-sat-using sat) или выполнив тактику «sat». Реализация этого решателя находится в sat_solver.h/.cpp, и это будет отличное место, чтобы начать оглядываться, если вы хотите его взломать.

Z3 также использует собственную реализацию AIG как шаг предварительной обработки в некоторых тактиках, см. aig_tactic.h/.cpp.