Declare characters that remain valid outside their scope

Question

Declare characters that remain valid outside their scope

Z3 2.x had a function (well, most likely an error) that declarations of the symbol were not deleted, for example. The following code is adopted by Z3 2.x:

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

Z3 3.x no longer accepts this code ("unknown constant").

Is there a way to restore old behavior? Or in another way, how you can declare characters inside areas so that the declaration (and only the declaration, not the assumptions) is global, i.e. Didn’t jump out?

+3

scope symbols declaration z3

Malte schwerhoff Sep 7 '11 at 17:07

source share

1 answer

Leonardo de Moura · Accepted Answer · 2011-09-07T17:23:04+0000

, 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))

Declare characters that remain valid outside their scope

More articles: