mister-walter
commented
3 years ago We also tried using Z3_solver_to_string and Z3_solver_from_string, but as far as I can remember, this did not include all of the information known by Z3 at the point where the custom theory was invoked.
We are working on integrating our string solver SeqSolve written in ACL2s and Lisp with Z3. SeqSolve solves both string and length constraints using another instance of Z3 as a backend (Linear Integer Arithmetic) LIA solver.
The integration works by loading a modified version of Z3 containing a custom theory that we developed. This theory invokes SeqSolve and passes constraints as a SMTLIB string using a function pointer. SeqSolve then uses Z3_eval_smtlib2_string to parse the SMT2LIB string it received and solves it. We have attached a diagram showing the SeqSolve stack below.
Our issue stems from the fact that we would like the C API Z3_solver that the Lisp function will end up using to have access to the constraints that exist in the original problem or have been added by other theories. One way we considered getting these constraints is by using the C API inside of the Lisp function. However, SeqSolve’s invocation of Z3_eval_smtlib2_string creates its own C++ solver instance, and it's not clear that it is possible to access all of the information needed to make a C Z3_solver_ref struct that refers to the "same" solver. We also tried using smt_context::get_assertions inside of our custom theory, but that simply dumps all the assertions seen in the input smt2 file. If there is any way to get a reference to the Z3_Solver from within a theory inside Z3, such that it can be passed on to the lisp function in an ffi call? The goal here is to copy the current Z3_solver being used inside a theory of Z3, and send the copy's reference for use by the lisp procedure so it can use it independently.
Thanks.