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

Question

Я смущен и стараюсь понять, как связаны два разных входных формата для двигателя с фиксированной точкой 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 означает, что решатель удалось найти интерпретацию (или инвариантны) satisfiying все утверждения для всех , а unsat означает, что таких функций нет. Другими словами, он пытается доказать, положив «доказательство» (инвариант) в модель (очевидно, когда sat).

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

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

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

Answer 1

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

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

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

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

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

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