다음 코드에서 으로 선언 될 때까지 Z3은 줄 1의 nil을 인식하지 않습니다. 어떻게 해결할 수 있을까요? Z3/SMT-LIB2에 import/include 구조가 있습니까?Z3이 삽입을 인식하지 못하고 문자가없는 경우
(assert (= nil nil)) ; (error "line 1 column 12: unknown constant nil")
(declare-const xs (List Int))
(assert (= nil nil)) ; OK after declare-const List Int
파일에서 테스트하거나 z3 -in을 사용하면 오류가 표시됩니다.
이것은 불행히도 SMT-Lib 표준의 일반적인 단점입니다. 범위를 나타내는 심볼을 가져 오는 유일한 방법은 set-logic 선언을 사용하는 것이며 이러한 논리 목록은 고정되어 있습니다. 개별 솔버 (예 : z3)가 새로운 의사 결정 절차를 구현할 때 기호를 임시로 가져와야합니다. 을 선언 할 때 z3은 nil 기호를 범위로 가져옵니다. 오류가 발생하기 쉽습니다.
다양한 논의가있었습니다. 구체적인 제안을하고 모든 세부 작업을 수행하기에 충분한 동기 부여가있는 사람은 없습니다. 예를 들어 여기를 참조하십시오 : http://www.cs.nyu.edu/pipermail/smt-lib/2015/000862.html, 고정 논리 선언에서 더 많은 숫자로 import 스타일 사양으로 이동하라는 제안이있었습니다.
따라서 현재 상황을 고려할 때 List이 처음으로 나타나는 것으로 나타났습니다. 바라건대, SMTLib는 앞으로 더욱 유연한 방식으로 새로운 기능을 지원할 수있는 방법으로 발전 할 것입니다.