2013-03-16 7 views
1

사이트에있는 Windows 용 Z3 4.3.0 (64 비트) 파일을 다운로드했습니다 : http://z3.codeplex.com/releases.Windows에 Z3 설치

bin 폴더에있는 z3.exe 파일을 실행하려고하면 어떻게됩니까? 프롬프트가 나타나고 즉시 사라집니다. z3.exe 파일을 통해 z3로 작성된 파일을 실행하는 방법을 알아야했습니다.

어떻게하면됩니까? 또는 Java를 통해 z3을 실행하는 가장 좋은 옵션은 무엇입니까?

답변

4

z3.exe은 명령 줄 도구입니다. file.smt2이라는 SMT-LIB 2.0 파일을 실행하려면 명령 프롬프트에서 다음 명령을 실행해야합니다. z3.exe를 포함하는 디렉토리가 PATH 환경 변수에없는 경우

z3 file.smt2 

, 당신은 위의 명령에 디렉토리를 포함해야합니다.

BTW, Z3에는 그래픽 사용자 인터페이스 또는 환경이 없습니다. 그것은 본질적으로 자동화 된 추론을위한 라이브러리입니다. z3.exe은이 라이브러리를 사용하여 빌드 된 간단한 실행 파일로, 파일에 저장된 명령을 실행할 수 있습니다.

rise4fun에서 제공되는 웹 인터페이스를 사용하여 Z3으로 재생할 수도 있습니다. rise4fun에서는 SMT-LIB 프런트 엔드와 Python을 기반으로합니다. 둘 다 대화 형 자습서가 있습니다.

Z3에는 C, C++, .Net, Python 및 OCaml과 같은 프로그래밍 언어에 대한 API가 있습니다. 다음 릴리스에서는 Java에 대한 지원도 제공 할 예정입니다. 야간 빌드 중 하나를 사용하여 Java로 이미 게임을 즐길 수 있습니다. Z3 야간 빌드에 대한 자세한 내용은 here으로 이동하십시오. 야간 빌드에는 Z3 API를 사용하는 Java 예제 애플리케이션이 포함되어 있습니다.

+0

그래서 지금 자바에서는 사용할 수 없습니다. – Robert

+0

가능한 일이지만 야간 빌드를 사용해야합니다. 공식 릴리스는 아니지만 미리보기입니다. 위에 포함 된 링크에서 설명합니다. 이미 Java API와 야간 빌드를 사용하는 사람들이 여러 명 있습니다. –