Разве 'check-sat' не поддерживает булеву функцию в качестве предположения? - PullRequest
Новая
       4

Разве 'check-sat' не поддерживает булеву функцию в качестве предположения?

3 голосов
/ 28 марта 2012

В следующем примере я попытался использовать неинтерпретированную булеву функцию, например, "(Declare-Const P (Int) Bool)", а не одну логическую константу для каждого предположения. Но это не работает (это дает ошибку компиляции). 

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(declare-fun p (Int) Bool) 
             ;(declare-const p1 Bool) 
             ;(declare-const p2 Bool)
             ; (declare-const p3 Bool)

;; We assert (=> p C) to track C using p
(declare-const x Int)
(declare-const y Int)
(assert (=> (p 1) (> x 10)))
;; An Boolean constant may track more than one formula
(assert (=> (p 1) (> y x)))

(assert (=> (p 2) (< y 5)))
(assert (=> (p 3) (> y 0)))

(check-sat (p 1) (p 2) (p 3))
(get-unsat-core)

выход 

Z3(18, 16): ERROR: invalid check-sat command, 'not' expected, assumptions must be Boolean literals
Z3(19, 19): ERROR: unsat core is not available

Я понимаю, что невозможно (не поддерживается) использовать булеву функцию. Есть ли причина этого? Есть ли другой способ сделать это?

1 Ответ

3 голосов
/ 28 марта 2012

У нас есть это ограничение, потому что Z3 применяет много упрощений, прежде чем решит проблему.Некоторые из них перепишут формулы и термины.Проблема, которая фактически решается с помощью Z3, очень часто сильно отличается от проблемы ввода.Мы должны были бы проследить упрощенные предположения до исходных предположений или ввести вспомогательные переменные.Ограничение логических литералов позволяет избежать этой проблемы и делает интерфейс очень чистым.Обратите внимание, что это ограничение не ограничивает выразительность.Если вы считаете, что слишком сложно объявлять множество логических переменных для отслеживания различных утверждений.Я предлагаю вам взглянуть на новый внешний интерфейс Python для Z3 под названием Z3Py.Это намного удобнее в использовании, чем SMT 2.0.Вот ваш пример в Z3Py: http://rise4fun.com/Z3Py/cL В этом примере вместо создания неинтерпретируемого предиката p создается «вектор» (фактически, это список Python) o логические константы.

Онлайн-учебник Z3Py содержит много примеров.

В Z3Py также можно реализовать подход, который создает вспомогательные переменные.Вот сценарий, который делает свое дело.Я определил функцию check_ext, которая выполняет всю сантехнику.http://rise4fun.com/Z3Py/B4

...