CODEWITHSUNDEEP
z3
Manjeet Dahiya
Manjeet Dahiya

Reputation: 505

Z3: moving expressions from OCaml to C/C++

I have two modules in my program, one is written on OCaml and other in C. Both use Z3. OCaml one is used to build expressions and these expressions have to be moved to the C module. I will then perform more operations on these expressions in C and then I will call final assert in C module.

  1. Is it possible to hack the OCaml wrapper to get the C objects (of context and expressions)?
  2. Is it possible to convert the expressions into string and then parse it back into to Z3 context in C module?

Please guide if there is any other way to go about.

Upvotes: 0

Views: 122

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The Z3 Ocaml API does in fact translate everything to C/native land and then back again. So yes, it is possible to extend that. This is true for both, the old ML API and the new one (in the ml-ng branch). I'm using the terminology of the latter: ASTs have functions called wrap and unwrap which translates any AST (or 'derived' object like Expr, FuncDecl, anything that has an ast_of_* function) Unwrapping produces an Z3native.ptr and, as the name implies, this is just a C native pointer. All Z3 objects also 'derive' from the z3_native_object type, which has a field called m_n_obj which is also just a pointer (this also exists for objects other than ast/expr/funcdecl).

Once you have a C pointer to a Z3 object and you want to translate it back, you can use one of the *_from_ptr functions to create a proper Ocaml object again (these functions are not exported in z3.mli, you'd have to unhide them.

Of course, if it's just a little bit of code, you can add it directly in z3native_stubs.c.

It's very likely that you'd be using different contexts in Ocaml and in C land. Note that any objects created from one context can not be used in another context, to do that, objects must be translated by the according translate function.

Upvotes: 1

Related Questions