3

Z3 2.xには、シンボル宣言がポップされないという機能（おそらくバグ）がありました。たとえば、次のコードはZ32.xで受け入れられます。

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

Z3 3.xは、このコード（「不明な定数」）を受け入れなくなりました。

古い動作を復元する方法はありますか？または、宣言（および宣言のみ、仮定ではない）がグローバルになるように、つまりポップされないように、スコープ内でシンボルを宣言する方法はありますか？

4

1 に答える 1

0

はい、Z3 2.xでは、すべての宣言がグローバルでした。SMT-LIB 2.0標準では、すべての宣言をスコープする必要があると規定されているため、Z33.xでこの動作を変更しました。オプションを使用して、古い動作を復元できます:global-decls。

(set-option :global-decls true)
(push)
(declare-fun x () Int)
(pop)
(assert (= x x))
于 2011-09-07T17:23:04.363 に答える