0
나는 z3_logdir 및 z3_loglevel 환경 변수를 사용하여 * .z3 파일 형식의 Pex 로그 경로 조건을 기록합니다. pex가 SMT 2 형식으로 경로 조건을 내보내도록 할 수 있습니까? 또는 .Z3 파일 형식을 SMT 2로 변환 하시겠습니까?Pex에서 SMT 2 형식의 경로 조건을 얻을 수 있습니까?
A
답변
1
Pex는 Z3 용 DLL 인 Microsoft.Z3.dll과 함께 제공됩니다. 이것은 Z3 버전 2.5에 해당합니다 (http://research.microsoft.com/en-us/um/redmond/projects/z3/old/older_z3.html에서 다운로드 가능). Z3 v 2.5의 API에는 내부 형식으로 Z3 파일 용 구문 분석 지원 이 있으며 SMT-LIB (1)에 덤프하는 API 함수가 있습니다. SMT-LIB1 벤치 마크를 SMT-LIB2로 변환하기위한 최신 버전의 Z3 및 기타 도구가 있습니다.
관련 문제
- 1. 인코딩이있는 형식의 크기를 어떻게 얻을 수 있습니까?
- 2. SMT-LIB 수식 추출
- 3. NEST 2를 사용하여 InnerHits에서 강력한 형식의 조회수를 얻을 수 있습니까?
- 4. Z3/SMT : 초기화하려면 푸시/팝을 언제 선택해야합니까?
- 5. GNU make의 두 번째 전제 조건을 얻을 수 있습니까?
- 6. wp 커스텀 헤더 이미지의 조건을 어떻게 얻을 수 있습니까?
- 7. nil 조건을 무시하도록 ActiveRecord 쿼리를 어떻게 얻을 수 있습니까?
- 8. Worklight JSON Store, 경쟁 조건을 얻을 수 있습니까?
- 9. WPF/XAML에서 강력한 형식의 바인딩을 얻을 수 있습니까?
- 10. 강력한 형식의 경로 검사
- 11. SMT 솔버에서 제약 강화의 효율성
- 12. 어떻게이 형식으로 2 차원 배열을 얻을 수 있습니까?
- 13. Symfony 2 : 형식의 Doctrine 제약
- 14. PaintCode 2 - 제약 조건을 수정할 수 없습니까?
- 15. 1 if 문 내에서 2 개의 조건을 가질 수 있습니까?
- 16. 스칼라 : 경로 종속 형식의 동일성
- 17. 안드로이드에서 준비된 경로에 대한 경로 데모를 얻을 수 있습니까?
- 18. 경로로 Google지도를 얻을 수 있습니까 경로 유형을 지정 하시겠습니까?
- 19. 문자열에서 PTypeInfo를 얻을 수 있습니까?
- 20. Z3과 SMT-LIB를 사용하여 최대 2 개의 값을 얻으십시오.
- 21. 부분 뷰에서 MVC 2 강력한 형식의 도우미를 사용할 수 있습니까?
- 22. LINQ는 익명 형식의 컬렉션을 얻을
- 23. 익명 형식의 문자열 멤버에서 강력한 형식의 컨트롤러 작업으로 암시 적 형식 변환을 어떻게 얻을 수 있습니까?
- 24. 강력한 형식의 GetVirtualPath 메서드를 사용할 수 있습니까?
- 25. 은 SMT/Z3 optimazation
- 26. SMT 솔버의 한계
- 27. '설치'에서만 유효화 될 WiX 조건을 얻을 수 없습니다.
- 28. 두 개 이상의 조건을 확인할 수 있습니까?
- 29. html 형식의 파일 경로 첨부하기
- 30. 리퍼러를 얻을 수 있습니까?