Квантор в Z3 - PullRequest
Новая
       36

Квантор в Z3

5 голосов
/ 16 февраля 2012

По сути, я хочу попросить Z3 дать мне произвольное целое число, значение которого больше 10. Поэтому я пишу следующие утверждения: 

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

Как я могу применить этот квантификатор к моей модели? Я знаю, что вы можете написать (assert (> x 10)), чтобы достичь этого. Но я хочу сказать, что мне нужен квантификатор в моей модели, поэтому каждый раз, когда я объявляю целочисленную константу, значение которой гарантированно будет больше 10. Поэтому мне не нужно вставлять оператор (assert (> x 10)) для каждой целочисленной константы, которую я объявлен.

1 Ответ

5 голосов
/ 16 февраля 2012

Когда вы используете (assert (forall ((i Int)) (> i 10))), i является ограниченной переменной, и квантифицированная формула эквивалентна истинному значению, которое в данном случае false.

Я думаю, что вы хотите определить макрос с помощью квантификаторов: 

(declare-fun greaterThan10 (Int) Bool)
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10))))

И вы можете использовать их, чтобы избежать повторения кода: 

(declare-const x (Int))
(declare-const y (Int))
(assert (greaterThan10 x))
(assert (greaterThan10 y))
(check-sat)

По сути, это способ определения макросов с использованием неинтерпретированных функций при работе с Z3 API. Обратите внимание, что вы должны установить (set-option :macro-finder true), чтобы Z3 заменял универсальные квантификаторы телами этих функций.

Однако, если вы работаете с текстовым интерфейсом, макрос define-fun в SMT-LIB v2 - более простой способ сделать то, что вы хотите: 

(define-fun greaterThan10 ((i Int)) Bool
  (> i 10))
...