Z3 ast_to_string() 뺄셈이있는 API

Question

문제는 매우 간단합니다. C API 인터페이스를 사용하여 Z3에서 다음 명령문을 사용합니다.

(assert(>= (xA 1) (- (yB 0) period)))) 

가끔 어쩌면 어떤 종류의 어설 션과 결과가 SatSolver에 있는지 확인할 필요가 있습니다. ast_to_string() API를 사용하여 텍스트 파일을 생성하여이 작업을 수행합니다. 나는 토 찾기이 파일을 먹일 때 오류 나를 불평

(assert(>= (xA 1) (+ (yB 0) (* -1 period)))) 

- -

(error "ERROR: line 150 column 56: could not locate id -1.")

내가 수동으로 모든 -1 수정해야, 그럼으로이 API는 문 위의 저를 반환 코드를 작성하고 sat 솔버를 실행하십시오. 내가 이것을 피할 수있는 다른 방법이 있습니까?

Answer 1

설정 기억이 출력 공식 SMTLIB 2.0 형식을 준수하기 ast_to_string()를 사용하기 전에

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT); 

.