По умолчанию глобальные переменные рассматриваются как экзистенциально квантифицированные. Например.

(declare-const x Int)
(assert (exists ((y Int)) (and (= x y) (= x y))))
(check-sat)
(get-model)

Дает

sat
(model 
  (define-fun y!0 () Int
    0)
  (define-fun x () Int
    0)
)

Как заставить его рассматривать x как forall x, как в этом запросе:

(assert (forall ((x Int)) (exists ((y Int)) (and (= x y) (= x y)))))
(check-sat)
(get-model)

Чтобы получить значение y, зависит от x:

sat
(model 
  (define-fun y!0 ((x!1 Int)) Int
    x!1)
)

Это должно быть просто вопросом синтаксиса. Возможно ли это в z3? В другом решателе SMT?

Редактировать:

Чего я хочу добиться, так это выполнить скрипт, например:

(declare-forall-const x Int)
(declare-const y Int)
(assert (and (= x y) (= x y)))
(check-sat)
(get-model)

И получить ответ вида:

sat
(model 
  (define-fun y!0 ((x!1 Int)) Int
    x!1)
)

Другими словами, я хочу объявить параметр forall глобально и ссылаться на него в последующих утверждениях.