(: VAR 0) Z3 한정 기호의 몸에

Question

나는 Z3를 OCaml의 API의 한정사의 몸, 그 문자열

(exists ((u_1 Int)) (= u_1 x5)) 

가 Quantifier.get_body에 의해, 내가 표현을 얻기 예를 들어, 한정사를 얻을 때

(= (:var 0) x5) 

이 표현식에서 u_1이 새 변수로 바뀌었지만 다음 표현식의 종류 (: var 0)가 무엇인지 그리고 어떻게 다시 일치시키는 지 알지 못합니다. 우리가 몸체와 그것의 바운드 변수들로부터 Quantifier를 재구성하고자 할 때.

누구나 해결책을 제안 할 수 있습니까? 고맙습니다.

Answer 1

나는 해결책을 얻었다. 표현식 e

(:var 0) 

은 VAR_AST 표현식입니다. 당신은 인덱스로

Quantifier.get_index e 

에 의해, 예를 들어 인덱스, 0을 얻을 수 있습니다, 그리고

AST.is_var (Expr.ast_of_expr e) 

에 의해 확인하실 수 있습니다, 당신은 쉽게 바인드 변수에 식 전자를 일치시킬 수 있습니다. 한정 기호의 바운드 변수 목록은 다음과 같이 구할 수 있습니다.

Quantifier.get_bound_variable_names