Z3 from string

[Pat-Lafon]

I am interested in pushing through #194.

The changes I made are:

• Loosening the input type to be Into<Vec<u8>> which is the most general type CString expects. This allows one to pass a &str to this function as shown in the tests. (Comment in Expose Z3_solver_from_string and Z3_optimize_from_string #194 (comment))
• The inner unsafe code is reworked to the current style used in the library with Self::wrap for construction.
• Renamed the function argument in Z3_solver_from_string to be c_str which matches the cpp api https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/api_solver.cpp#L358-L369 and makes more sense to me

[Pat-Lafon]

I have two additional comments which came up while I was attempting this. First, I was wondering if instead of creating a solver object, the api here should be mutating an already existing solver object with some smtlib2 string-based assertions? Second, I noticed some of the surrounding unsafe code does explicit null checks on the pointers it gets from the ffi. Should some of the Z3 pointers instead be wrapped in https://doc.rust-lang.org/std/ptr/struct.NonNull.html ?

[waywardmonkeys]

For the first question, I would look to see what the other language bindings for Z3 do.

for the second, I am not very familiar with that, so I haven’t thought about it before. Want to Kay out some arguments in favor in a separate issue?

[Pat-Lafon]

Basically all the official bindings take string based assertions and augment an existing solver.

CPP: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/c%2B%2B/z3%2B%2B.h#L2751
Dotnet: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/dotnet/Solver.cs#L282-L288
Java: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/java/Solver.java#L195-L201
Js: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/js/src/high-level/high-level.ts#L1324-L1327
Julia: Just re-exports the cpp version https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/julia/z3jl.cpp#L387
Ocaml: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/ml/z3.mli#L3466-L3469 for the optimizer but seemingly no implementation for the Solver.
Python: https://github.com/Z3Prover/z3/blob/a0f3727e90c4446ba2c1fa7e4392637587ad9632/src/api/python/z3/z3.py#L7208-L7210

[waywardmonkeys]

Can you rebase this into fewer commits? Some of the changes modify the earlier commits in the sequence, but shouldn't be needed in the history...