∃-запросы и ∀-запросы с движком фиксированной точки Z3

Я смущен и изо всех сил пытаюсь понять, как связаны два разных формата ввода для движка с фиксированной точкой Z3. Краткий пример: предположим, я хочу доказать существование отрицательных чисел. Я объявляю функцию, которая возвращает 1 для неотрицательных чисел и 0 для отрицательных, а затем запрашивает решающую программу об отказе, если есть аргументы, для которых функция возвращает 0. Но есть одно ограничение: я хочу, чтобы решатель отвечал sat, когда существует хотя бы один отрицательное число и unsat, если все числа неотрицательны.

Это тривиально с использованием формата declare-rel и query:

(declare-rel f (Int Int))
(declare-rel fail ())
(declare-var n Int)
(declare-var m Int)

(rule (=> (< n 0) (f n 0)))
(rule (=> (>= n 0) (f n 1)))

(rule (=> (and (f n m) (= m 0)) fail))
(query fail)

Но при использовании чистого формата SMT-LIB2 (с forall) это становится непросто. Например, простой

(set-logic HORN)
(declare-fun f (Int Int) Bool)
(declare-fun fail () Bool)

(assert (forall ((n Int)) 
    (=> (< n 0) (f n 0))))
(assert (forall ((n Int)) 
    (=> (>= n 0) (f n 1))))

(assert (forall ((n Int) (m Int)) 
    (=> (and (f n m) (= m 0)) fail)))
(assert (not fail))

(check-sat)

возвращает unsat. Неудивительно, что изменение (= m 0) на (= m 1) приводит к тому же. Мы можем получить sat, только подразумевая fail из (= m 2). Проблема в том, что я не могу понять, как задать решателю, используя этот формат.

Насколько я понимаю сейчас, при использовании forall-формы мы можем попросить найти только ∀-решения, т.е. ответ sat означает, что решателю удалось найти интерпретацию (или инвариант), удовлетворяющую всем утверждениям для всех values, а unsat означает, что таких функций нет. Другими словами, он пытается доказать, помещая «доказательство» (инвариант) в модель (очевидно, когда sat).

Напротив, когда query поиск решения в решателе формата declare-rel ищет в решении некоторые переменные, точно так же, как ограничения находятся под ∃-квантификатором. Другими словами, это контрпример. Он может вывести инвариант только в случае unsat.

У меня есть пара вопросов:

  1. Я правильно понимаю? Я чувствую, что упускаю некоторые ключевые идеи. Например, общее представление о том, как выразить (query ...) через (assert (forall ...)), будет действительно полезным (и ответит на вопрос 2 автоматически).
  2. Есть ли способ решить такие ∃-ограничения (вывод sat при обнаружении контрпримера) с помощью чистого формата SMT-LIB2? Если да, то как?

z3 smt
person dvvrd    schedule 09.09.2016    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Прежде всего, формат, в котором используются «declare-rel», «declare-var», «rule» и «query», является настраиваемым расширением SMT-LIB2. Функция «declare-var» удобна для исключения связанных переменных из нескольких правил. Это также позволяет формулировать правила Datalog со стратифицированным отрицанием, и семантика этого - то, что вы должны ожидать от стратифицированного отрицания. По соглашению он использует «sat», чтобы указать, что запрос имеет производную, и «unsat», что для запроса не существует производной.

Оказывается, стандартный SMT-LIB2 может выражать почти все, что вы хотите для предложений Horn, без отрицания. Правила становятся следствиями, а запросы - следствиями формы: (=> запрос неверен) или в том виде, в каком вы его написали (не запрос). Вывод в настраиваемом формате соответствует доказательству пустого предложения (например, доказательству «запроса», которое затем доказывает «ложность»). Таким образом, наличие деривации означает, что утверждения SMT-LIB2 «неподходящие». И наоборот, если существует интерпретация (модель) для предложений Хорна, то такая модель устанавливает отсутствие вывода. Пункты "сат".

Другими словами:

 "sat" for datalog extension   <=> "unsat" for SMT-LIB2 formulation
 "unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation

Преимущество использования чистого формата SMT-LIB2, когда он применяется, заключается в отсутствии специальных расширений синтаксиса. Это простые формулы SMT, и другим, кто хочет решить этот класс формул, не нужно писать специальные расширения, им просто нужно убедиться, что решатели, настроенные на предложения Horn, распознают соответствующий класс формул. (Реализация фрагмента HORN в Z3 действительно допускает некоторую гибкость при записи предложений Horn. У вас могут быть дизъюнкции в телах, и вы можете иметь последствия Карри).

У использования формата SMT-LIB2 есть один недостаток, с которым помогает формат на основе правил: когда есть производный запрос, то формат на основе правил имеет прагмы для печати элементов кортежа. Обратите внимание, что в общем случае отношение запроса может принимать аргументы. Эта функция полезна для отношений конечной области. В приведенном выше примере используются целые числа, поэтому отношения не являются конечной областью, но примеры в онлайн-руководстве содержат конечные экземпляры домена. Теперь вывод запроса также соответствует доказательству разрешения. Вы можете извлечь доказательство разрешения из случая SMT-LIB2, но я должен сказать, что он довольно запутан, и я не нашел способа эффективно использовать его. Механизм «двойственности» для предложений Хорна генерирует производные в более доступном формате, чем формат доказательства по умолчанию Z3. В любом случае вполне вероятно, что пользователи столкнутся с препятствиями, если попытаются работать с сертификатами подтверждения, потому что они редко используются. Формат на основе правил имеет еще одну функцию, которая объединяет набор предикатов с экземплярами, которые соответствуют следу происхождения. На этот вывод легче смотреть.

person Nikolaj Bjorner    schedule 09.09.2016
comment
Николай, большое спасибо за четкий и полный ответ. - person dvvrd; 09.09.2016