По сути, я хочу попросить Z3 дать мне произвольное целое число, значение которого больше 10. Поэтому я пишу следующие утверждения:
(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))
Как я могу применить этот квантор к моей модели? Я знаю, что для этого можно написать (assert (> x 10)). Но я имею в виду, что мне нужен квантификатор в моей модели, поэтому каждый раз я объявляю целочисленную константу, значение которой гарантированно будет больше 10. Так что мне не нужно оператор вставки (assert (> x 10)) для каждой объявленной мной целочисленной константы.