Рекомендации по настройке создания квантификатора Z3 (с интерфейсом SMT-LIB)

Я пытаюсь настроить z3 на машинные проблемы, которые

  • являются неудовлетворительными,
  • содержат утверждения, не имеющие отношения к доказательству
  • нерелевантные утверждения содержат кванторы
  • где z3 не может найти доказательство невыполнимости из-за этих нерелевантных утверждений (удаление их вручную показывает это).

Есть ли какие-то общие рекомендации, как поступить в этой ситуации?

Просматривая параметры командной строки, я подумал, что могу попробовать:

mbqi.id (строка) Использовать экземпляр на основе модели только для квантификаторов с идентификатором, начинающимся со строки (по умолчанию: )

Тем не менее я не вижу, как я могу прикрепить идентификатор к квантификатору, используя синтаксис SMT-LIB. Может ли кто-нибудь с подсказкой поделиться им со мной?


z3 smt
person dde    schedule 10.06.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Упомянутый здесь идентификатор — это просто имя квантифицированной переменной. Если у вас есть:

(declare-sort S 0)
(declare-fun gt (S S) bool)

(assert (forall ((inst_a S) (inst_b S))
          (or (gt inst_a inst_b) (gt inst_b inst_a))))

(check-sat)

Тогда вы можете сказать:

z3 smt.mbqi=true smt.mbqi.id=inst a.smt2

Не забудьте использовать smt.mbqi=true для включения MBQI. Если вы используете этот вызов, то z3 создаст шаблон только в том случае, если квантифицированная переменная начинается с inst в приведенном выше примере.

person alias    schedule 10.06.2020