1
z3 (Microsoft Research) 웹 사이트에서 제공되는 MaxSAT/MaxSMT c 예제 (특히 maxsat.c)를 가지고 놀고 싶습니다. Visual Studio 2010을 사용하여 결국 z3 4.0을 새로 설치하여 컴파일 할 예제를 얻었습니다. 그러나, 나는 그것을 (SMT 2.0) 모델을 사용하여 실행할 수 없습니다. 또한, 나는 this에 게시 된 예제를 얻을 수 없습니다.z3 MaxSAT 예제 오류
첫 번째 경우 파일의 get_hard_constraints에 Z3_get_smtlib_num_formulas을 호출하려고하면 컴파일 된 프로그램이 충돌합니다. 이유를 모르겠다. 대신 표준 윈도우 7을 얻는다. "이 프로그램이 작동을 멈췄다"라는 팝업이 나타납니다.
두 번째 경우는 unsupported ;benchmark입니다.
내가이 작업을하는 데 도움이되도록 (a)이 코드를 컴파일 할 때 누구와도 비슷한 문제가 있었습니까? 그렇다면 어떻게 해결 했습니까? 또는 (b) 파일 컴파일을 디버깅하려면 어떻게해야합니까? 즉, 누군가이 컴파일러 옵션을 포함하도록 올바른 라이브러리 (및 라이브러리 버전 (예 : z3 4.0))를 열거 할 수 있습니까?
두 경우 모두에서보고 된 오류에 대한 정보도 알 수 있습니다. 정확히 무엇을 의미합니까? 키워드가 유효하지 않습니까? SMT 입력이 잘못된 버전입니까? 또는 다른 것?
감사합니다.
답변 해 주셔서 감사합니다. 예제도 작동하지 않았습니다. (이전에 언급 한 것을 잊었습니다.)하지만 (일부 환경 변수가 설정되지 않았습니다)이를 수정했습니다. 해당 함수 호출을 새로운 함수 호출로 대체 할 수 있는지 (그리고 이전 표준과 관련된 다른 함수 호출도 가능) SMTLIB 2.0에서 작동하게 할 수 있습니까? –
예, SMT2 용 함수도 있습니다. Z3_parse_smtlib2_file입니다. 이 예제에서는 가정과 일련의 수식이 아닌 단일 식만 반환하기 때문에이 예제에서는 추가 수정이 필요합니다. 따라서 SMT2에서 하드 및 소프트 제약을 구별하는 방법이 명확하지 않습니다 (주석을 통해 수행 할 수 있음). –