Сохранение «состояния» решателя Z3 в формате SMT2

возможно ли, используя Z3 API (например, API Python), сохранить текущее состояние решателя, в том числе то, что понял решатель (в SAT-решении мы сказали бы «выученные фразы») в файле в формате SMT2?

Потому что я хотел бы иметь возможность сохранить состояние решателя во временном файле, чтобы возобновить решение позже, чтобы иметь некоторое время, чтобы понять, какие дальнейшие запросы я должен сделать для него.

Спасибо заранее…

    2 Solutions collect form web for “Сохранение «состояния» решателя Z3 в формате SMT2”

    У SMT2 нет никаких условий для сохранения данного состояния решателей, которое, несомненно, будет отличаться от решателя до решателя. Однако у каждого решателя могут быть разные механизмы, но это определенно не будет в формате SMTLib2.

    Поскольку ваш вопрос полностью задан Z3, я рекомендую просить его на https://github.com/Z3Prover/z3/issues, чтобы узнать, могут ли они что-нибудь интересное. Насколько мне известно, в настоящее время это невозможно.

    В конце концов Левент был прав 🙂

    Ниже приведены некоторые замечания Николая Бьорнера, с сайта Z3 github.

    « Состояние решателя не полностью сериализуется в формате SMT2. Вы можете распечатать решатель в формате smt2 на основе текущих утверждений, но не изучать предложения / единицы, используя метод sexpr () на объекте Solver».

    «Мы не раскрываем способы печати внутреннего состояния. Возможно, вы можете прервать решатель, затем клонировать его, используя методы« перевести »и получить доступ к переведенному состоянию решателя с помощью внутренних утилит печати. ​​Вам придется немного изменить код, чтобы получить к этому состоянию. Функции печати на решателях не имеют доступа к внутреннему состоянию любого из решателей, вместо этого они смотрят на утверждённые формулы и печатают их. Я не переводил изученные лемм . Например, код в smt_context.cpp строка 176 отключена, поскольку она не помогла ни в каких улучшениях производительности. Аналогичным образом, код копирования в sat_solver не копирует извлеченные статьи, даже если он сохраняет отдельные литералы и двоичные статьи, которые были изучены ».

    Вы можете увидеть приведенные выше комментарии Nicolaj по этой ссылке .

      Python - лучший язык программирования в мире.