Объявите символы, которые остаются действительными вне их области действия

Question

Z3 2.x имеет особенность (возможно, скорее, ошибку), что объявления символов не были удалены, например, Z3 2.x принимает следующий код:

(push)
(declare-fun x () Int)
; Assumptions made in this scope will be popped correctly
(pop)
(assert (= x x))

Z3 3.x больше не принимает этот код («неизвестная константа»).

Есть ли способ восстановить старое поведение?Или другой способ, как можно объявить символы внутри области видимости, чтобы объявление (и только объявление, а не предположения) было глобальным, то есть не вытолкнутым?

Answer 1

Да, в Z3 2.x все объявления были глобальными. Мы изменили это поведение в Z3 3.x, потому что стандарт SMT-LIB 2.0 гласит, что все объявления должны быть ограничены. Вы можете восстановить старое поведение, используя опцию :global-decls.

(set-option :global-decls true)
(push)
(declare-fun x () Int)
(pop)
(assert (= x x))