CODEWITHSUNDEEP
z3
Ton-Chanh Le
Ton-Chanh Le

Reputation: 313

(:var 0) in z3 Quantifier's body

When I get the body of a Quantifier of the Z3 OCaml API, for example a Quantifier whose string is

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

by Quantifier.get_body, I obtain the expression

(= (:var 0) x5)

I guess (:var 0) in this expression is the renaming of u_1 to a fresh variable, but I do not know what is the kind of the expression (:var 0) and how to match it back to u_1 when we want to reconstruct the Quantifier from its body and its bound variables.

Could anyone suggest a solution? Thank you very much.

Upvotes: 3

Views: 146

Answers (1)

Ton-Chanh Le
Ton-Chanh Le

Reputation: 313

I got the solution. The expression e

(:var 0)

is an expression of VAR_AST. You can check by

AST.is_var (Expr.ast_of_expr e)

Then, you can get its index, e.g., 0, by 

Quantifier.get_index e

With the index, you can easily match the expression e to its bound variable. Note that the list of bound variables of a quantifier can be obtained by

Quantifier.get_bound_variable_names

Upvotes: 2

Related Questions