Possible to use native C API along with dotnet API?

[thisiscam]

I currently have a use case where I would like to write C code and use the C API to create some Z3 object, and then pass it back to dotnet.

As far as I can tell, all the Z3 object's constructors are marked as internal, but I'm having the hope that maybe someone can point out a function in the dotnet API where I can use my own Intptr as the underlying object? I was wondering this because the Native.Z3xxxx are all marked as public, so I can literally call those method and get an Intptr.

I don't want to extend Z3 since otherwise I will have to ship a custom Z3.dll I suppose.

[wintersteiger]

I've never considered that partciluar use case, but if you can call the native functions that should be just fine as long as you make sure all terms are correctly reference-counted. The object constructors are marked internal as users should never need to construct any such objects directly (all that is done via Mk... functions), but for legacy reasons we have Context.WrapAST and Context.UnwrapAST, which were used for a similar purpose in the past, and Context.WrapAST does exactly what you want: it calls (the internal) AST.Create(this, nativeObject).

[thisiscam]

Thanks! I think I have figured out the (Un)WrapAST functions, but is there a way to also unwrap other kinds of native objects? e.g. Context? I need the Context to call the C API function I assume?

Currently I looked into the internal sources and used reflection to get the Context, but I found it strange because without a Context, how should one use the Native.Z3xxx apis normally?

[NikolajBjorner]

You could add a pull request with additional public methods to accomplish what you want.

[wintersteiger]

Indeed, you'd have to know the context. Currently there are no public facilities for constructing other objects, because we've never needed them. The reason all the constructors are internal/private is that newbie users would intuitively start out with ... = new Solver(); when they should use ... = ctx.MkSolver(), but we might just as well make the current constructor public and add Solver(Context ctx) etc.

Regarding context objects: the current interface does not provide a way to get the context (pointer) off of an object that you only hold an IntPtr for (e.g., a solver) and it may not be so easy to add that, so for now I think we'll just have to know them.