Z3_parse_smtlib2_file을 사용하여 Z3에 제공된 예제 파일을 구문 분석 할 때 구문 분석 오류가 발생했습니다.

Question

Z3 4.1을 사용하고 있으며 프로그램에서 smt lib2 형식 입력을 구문 분석하려고합니다.

그래서 먼저 Z3_parse_smtlib2_file을 사용하여 Z3 (Z3-4.1/examples/smtlib 폴더 아래에 있음)에 제공된 예제를 구문 분석하십시오. 그러나 많은 구문 분석 오류를 발견하고 즉시 내 프로그램이 종료됩니다. 입력 형식이 맞아야한다고 생각합니다. 다음

(set-option :auto-config true) 
(set-option :produce-models true) 

(declare-const a Int) 
(declare-fun f (Int Bool) Int) 
(assert (> a 10)) 
(assert (< (f a true) 100)) 
(check-sat) 

결과 :

smt2parser_example 
(error "line 1 column 26: error setting ':auto-config', option value cannot be modified after initialization") 
Error code: 4 
BUG: incorrect use of Z3. 

이 API는 다음과 같이 호출 :

fs = Z3_parse_smtlib2_file(ctx, fname, 0, 0, 0, 0, 0, 0); 

어디에서 다음 코드를 사용하여 Z3.2.smt2을 구문 분석하려고 문제는 무엇입니까? 입력 파일은 OK 여야합니다. Z3_parse_smtlib2_file의 인수에 문제가 있습니까?

Answer 1

오류 메시지에서 알 수 있듯이 Z3 컨텍스트가 초기화되면 자동 구성 옵션을 수정할 수 없습니다. 몇 가지 옵션 만 변경 가능하며 컨텍스트가 만들어지고 auto-config가 그 중 하나가 아닌 경우 변경할 수 있습니다. 광고

(set-option :auto-config true) 

가 입력 파일에서 제거하면 는 올바르게 파싱한다. 애플리케이션에 옵션을 설정해야하는 경우에는 config (C++) 또는 Z3_config (C) 객체를 전달하여 문맥 생성자에 직접 전달하는 것이 가장 좋습니다.