Квантификаторы в 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)) для каждого целочисленная константа, которую я объявил. Если мне приходится использовать макросы для предотвращения повторения кода, то каково фактическое использование квантификаторов?


z3 quantifiers
person Mahsa    schedule 24.08.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вам нужно будет ограничить каждый int, который вы объявляете индивидуально. x > 10 это правильный способ сделать это.

Вы можете использовать макросы или любую другую технику codegen. В решателе SMT все это расширяется до обычных ограничений. Это не влияет на время выполнения.

forall ((i Int)) (> i 10)) означает "Все целые больше 10?" что неверно.

Квантификаторы не определяют количество всех переменных, которые вы объявили. Они дают количественную оценку только по связанным переменным, здесь i.

person usr    schedule 24.08.2015