Квантификатор в Z3

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

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

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

5
задан user1197891 16 February 2012 в 15:05
поделиться

0 ответов

Другие вопросы по тегам:

Похожие вопросы: