범위 밖에서 유효한 기호를 선언하십시오.

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에서 모든 선언은 전역 적입니다. SMT-LIB 2.0 표준은 모든 선언의 유효 범위가 지정되어야하기 때문에 Z3 3.x에서이 동작을 변경했습니다. :global-decls 옵션을 사용하여 이전 동작을 복원 할 수 있습니다.

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