방금 seq 및 regexp 정렬 (z3-4.3.2 사용)에 대한 벤치 마크를 다운로드했습니다. "membership_1.smt2"를 실행 한 후 결과가 알려지지 않을 때의 문제점은 무엇입니까?z3 SMT solver : QF_BVRE 벤치 마크 실행 후 알 수없는 결과
추가 명령 줄 옵션을 지정하지 않았습니다. 벤치 마크 결과에 따르면 결과는 sat이지만 알 수없는 것은 모델없이 인쇄됩니다.
감사합니다편집 :
내가 "다시 시작"인식되지 않도록, 더 나타났습니다. z3 버전과 관련이 있습니까? 아니면 그냥 명령 줄 옵션을 잊어 버렸습니까?
첫째, OP 또는 주석 작성자가 "membership_1.smt2"예제 입력을 찾은 곳을 알 수 없습니다. SMT-LIB benchmarks과 Z3, S3 및 Z3-str의 소스를 확인했지만 찾을 수 없습니다.
문제는 OP가 S3 또는 Z3-str으로 작성되고 수정되지 않은 버전의 Z3에 대해 실행되는 벤치 마크를 테스트하고 있다는 것이 었습니다. S3 및 Z3-str은 이러한 확장을 처리하기 위해 Z3의 수정 된 버전이 필요합니다. 이것은 S3 웹 사이트에 설명되어 있습니다 [S3 : 8월 4일 액세스 웹 보안 분석, http://www.comp.nus.edu.sg/~trinhmt/S3/, 2016 년에 대한 기호 문자열 찾기] :
수정 된 Z3은 here입니다.
이러한 새로 추가 된 API 메서드를 사용하면 문자열 변수의 길이와 문자열 변수의 길이 간의 관계를 쿼리 할 수 있습니다 (our CCS'14 paper).
수정 된 버전 Z3은 Z3-str GROUP에 의해 integer/string theory integration으로 사용됩니다. (unmodified) Z3 source을 Grepping
는 "재 CONCAT를", "다시 시작"나에 대한 일치를 보여줍니다. 수정 된 버전을 그려 보면 lib/seq_decl_plugin.cpp에 정의 된 토큰이 z3-source-060115.zip 인 것으로 나타납니다.
맞습니다. 명령 "re-begin"이 인식되지 않고 "re-concat"명령도 인식되지 않습니다. –