WedX - журнал о программировании и компьютерных науках

Преобразование в формат SMTLib с опцией set-option

Я хочу преобразовать этот код z3py (онлайн-код) в стандартный формат SMTLib. Все конвертируется в формат SMTLib, за исключением установленных свойств параметров «(set-option: productions true) (set-option: timeout 4000)». Почему не работает? Код преобразования был предложен Леонардо де Моура.

Я хочу, чтобы результат был похож на -

; benchmark 
(set-info :status unknown)
(set-option :produce-models true)
(set-option :timeout 4000)
(set-logic QF_UFLIA)
(assert true)
(check-sat)

Спасибо

z3 z3py
11.09.2013

Ответы:


1

Параметры не печатаются принтером SMT-LIB2 pretty. Симпатичный принтер возвращает строку, и вы должны иметь возможность предварительно отложить параметры по вашему выбору.

11.09.2013
  • Спасибо за ваш быстрый ответ. Это правильный способ определить параметр для решателя. s = Решатель (); s.set (unsat_core = True) s.set (models = True); s.set (timeout = 4000) Потому что, если я установлю любое произвольное ключевое слово, z3py не выдаст никаких ошибок. Есть ли документация по ключевым словам, которые он поддерживает? 11.09.2013

    • 2

    Я запускаю ваш код и получаю

    ; benchmark
(set-info :status unknown)
(set-logic QF_UFLIA)
(assert true)
(check-sat)
    11.09.2013
    Новые материалы
    Объяснение документов 02: BERT
    BERT представил двухступенчатую структуру обучения: предварительное обучение и тонкая настройка. Во время предварительного обучения модель обучается на неразмеченных данных с помощью..
    Как проанализировать работу вашего классификатора?
    Не всегда просто знать, какие показатели использовать С развитием глубокого обучения все больше и больше людей учатся обучать свой первый классификатор. Но как только вы закончите..
    Работа с цепями Маркова, часть 4 (Машинное обучение)
    Нелинейные цепи Маркова с агрегатором и их приложения (arXiv) Автор : Бар Лайт Аннотация: Изучаются свойства подкласса случайных процессов, называемых дискретными нелинейными цепями Маркова..
    Crazy Laravel Livewire упростил мне создание электронной коммерции (панель администратора и API) [Часть 3]
    Как вы сегодня, ребята? В этой части мы создадим CRUD для данных о продукте. Думаю, в этой части я не буду слишком много делиться теорией, но чаще буду делиться своим кодом. Потому что..
    Использование машинного обучения и Python для классификации 1000 сезонов новичков MLB Hitter
    Чему может научиться машина, глядя на сезоны новичков 1000 игроков MLB? Это то, что исследует это приложение. В этом процессе мы будем использовать неконтролируемое обучение, чтобы..
    Учебные заметки: создание моего первого пакета Node.js
    Это мои обучающие заметки, когда я научился создавать свой самый первый пакет Node.js, распространяемый через npm. Оглавление Глоссарий I. Новый пакет 1.1 советы по инициализации..
    Забудьте о Matplotlib: улучшите визуализацию данных с помощью умопомрачительных функций Seaborn!
    Примечание. Эта запись в блоге предполагает базовое знакомство с Python и концепциями анализа данных. Привет, энтузиасты данных! Добро пожаловать в мой блог, где я расскажу о невероятных..
    Для любых предложений по сайту: [email protected]