Динамически вызывать get-value только тогда, когда check-sat возвращает "sat"

ProgramBox

Динамически вызывать get-value только тогда, когда check-sat возвращает «sat»

Post author:admin
Запись опубликована:4 февраля, 2023
Post category:Вопросы по программированию

#z3 #smt #cvc4

Вопрос:

Стандарт SMT2 гласит, что вызов get-value разрешен только после вызова check-sat и только тогда, когда check-sat возвращает «sat» или «неизвестно».

Вот простой пример нерешенной проблемы:

 (set-option :produce-models true)
(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(declare-fun a ()(_ BitVec 4))
(declare-fun b ()(_ BitVec 4))
(declare-fun c ()(_ BitVec 4))
(declare-fun z ()(_ BitVec 4))
(assert (= #b1111 z))
(assert (= a b))
(assert (= (bvxor a z) c))
(assert (= b c))
(check-sat)
(get-value ( a ))
(get-value ( b ))
(get-value ( c ))

Поскольку проблема не решена, команды get-value являются незаконными. Удалите любое утверждение, и оно станет sat, а команды get-value станут законными. Итак, мой вопрос в том, как вы пишете скрипт SMT2, который проверяет возвращаемое значение check-sat и вызывает get-value только в том случае, если он вернул sat?

Незаконный вызов get-value является проблемой для меня, поскольку я запускаю разные решатели smt в потоке и проверяю возвращаемое значение программы, а затем анализирую их вывод. CVC4 переводит возвращаемое значение в состояние ошибки, если get-value вызывается незаконно.

Ответ №1:

Я не думаю, что есть хороший способ, если вы хотите иметь один файл «SMT» для управления всей транзакцией.

Эта проблема часто возникает при взаимодействии с SMT-решателями с других языков. Решение, которое я принял, заключается в том, что я сохраняю открытый канал с решателем и передаю ему строки скрипта, читаю ответы и решаю, что отправлять дальше, на основе полученных ответов. По сути, запрограммированное взаимодействие. (Например, это то, что делает библиотека SBV Haskell.)

Тем не менее, я согласен, что это боль; и было бы неплохо, если бы существовал санкционированный SMT2-lib способ обработки такого общего взаимодействия.

1. Это предполагаемая модель взаимодействия, к лучшему или к худшему. Однако не совсем ясно, что следует добавить в SMT. Циклы явно выходят за рамки предполагаемой области языка, но как насчет «(check-sat :print-model-if-sat)»? Я уверен, что Кларк и Чезаре были бы признательны за предложения по добавлению простых функций удобства использования, если они могут аккуратно вписаться в рамки.

Ответ №2:

Для CVC4, запускаемого из командной строки, добавьте флаг

 --dump-models          output models after every SAT/INVALID/UNKNOWN
                       response [*]

Это не так конкретно, как get-value . Эта опция является нестандартной, и CVC4 в настоящее время не поддерживает установку этого флага в анализаторе SMT2. (Дайте нам знать, если вы хотите, чтобы это поддерживалось.)

1. Спасибо, Тим. Это решает мою проблему, хотя первоначальный вопрос все еще остается в силе. Я полагаю, что у каждого решателя будет свое собственное решение. Следует отметить одну вещь, которая --dump-models требует, чтобы параметр produce-models также был установлен из командной строки, а не из синтаксического анализатора, т.Е. -m --dump-models Требуется. Это ошибка? Несмотря на это, для меня это не проблема, но мне потребовалось немного времени, чтобы понять, почему --dump-models сначала не работало. Также: CVC4 -h абсолютно ничего не говорит об этой --dump-models опции. Может быть, стоит добавить его?

2. Неважно, CVC4 -h содержит сообщение о --dump-models , я просто пропустил его изначально.

3. Да, у каждого решателя будет свое собственное решение. Вы всегда можете реализовать предложение Левента для текстового взаимодействия. На данный момент это предполагаемая модель использования.