Integrating a decision procedure written in ACL2s and lisp with Z3

[ankitku]

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.

[mister-walter]

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.

[NikolajBjorner]

The solver interface is a general interface that can cover different backends with each their characteritics.
To force using just the SMT core solver you should initialize a Z3_mk_simple_solver.
You can then run a query with the solver (say with a bounded number of conflicts by setting smt.max_conflicts).
To tease out the current set of base assertions and lemmas with low glue level you can copy that solver into a fresh solver.
The function Z3_solver_translate supports copy routines between different or the same contexts. You can use the same context for your use.
Then the copied solver is initialized with assertions that are the result of solving.
The original solver may only expose assertions that are added from outside.

You can for example try:

from z3 import *

set_option(verbose=10)
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y, Or(x > y, x > z))
s.add(Or(x == y, x == z))
s.check()
s1 = s.translate(Context())
print(s1)
print(s)

You will then see some unusual state printed for both s and s1.
On the other hand, if you use just the standard "Solver" instead of "SimpleSolver", the internal state gets hidden and is then opaque.

[mister-walter]

Thanks for the reply!

Part of our issue is that we want to use Z3 with our custom tactic on SMTLIB2 files just like "vanilla" Z3, and so we are using Z3_eval_smtlib2_string on the contents of the relevant files after performing some setup. It does not seem as though it is possible to provide a Solver to this function for use when parsing the file, which makes sense as in the general case Z3 may need to make multiple Solvers depending on the commands inside of a SMTLIB2 file. We tried creating a custom SolverFactory that takes in a Solver and returns it every time it is asked for a new Solver, but that did not work properly.

We are currently using Z3_solver_translate, but as you noted the only assertions that are copied over are those that were added using an external interface (as opposed to those added by other theories etc). Is there no way to, given a Solver a, create a Solver b such that b contains all external assertions plus things like theory axioms and additional mid-solve information?

For example, assume that the file we're evaluating contains the assertion (or P Q), where both P and Q are clauses that are relevant to our tactic. Assume that P is UNSAT and Q is SAT. Imagine then that Z3 "decides" to investigate the satisfiability of P first, and then Q. Other theories may assert some theory axioms based on the contents of P. Our theory may add some theory axioms and theory variables. Then, Z3 calls new_eq_eh for our theory. Let the Solver that is performing the current check_sat be S (assume that we're using a SimpleSolver as you suggest above). At this point, we would like to call out to our Lisp function, which ideally would use all of the information known to be true by S at this point.

The problem lies in the fact that S is currently in the middle of a check_sat, and it seems that Z3 does not allow us to directly use S with the C API when it is in the middle of a check_sat. (I'm eliding some details here regarding the difference between solver and Z3_solver, and how we might e.g. prevent infinite looping with our theory calling check_sat which calls our theory...) So it seems like we need to create a new Solver. This Solver should contain all information that Z3 knows about P, including any theory axioms we added (note that we need to add theory axioms since it's not legal to call smt::context::assert_expr inside a theory call). For our theory axioms we could get around this issue by keeping track of which theory axioms we add, and sending them over to be added to the Z3_solver on the Lisp side. However, I'm concerned about other information that Z3 may have (e.g. that P is not true).

Hopefully this makes sense. It's possible that Z3 is simply not designed to allow the kind of interaction we're looking for here, so apologies if that is the case.

[NikolajBjorner]

I am not sure what "new_eq_eh for our theory" means.

The code I can find online https://github.com/ankitku/SeqSolve/tree/master/model-analyses/lisp-z3/src/z3 only references external APIs.
new_eq_eh is internal.
The external API supports a specialized instance of user callbacks, but I don't see those mentioned in your lisp bindings.
The user callbacks are defined here:

z3/src/api/z3_api.h

Line 6541 in aa05298

/**

They can be used to pick up variable assignments to Boolean and Bit-vectors and allow callbacks.
The Python bindings go through the hoops of registering callback functions.
An application of this newer API is sketched here: http://theory.stanford.edu/~nikolaj/supercharging.html
It is generally suitable for supporting ad-hoc global propagators.

[mister-walter]

Apologies for any confusion!
The code in the seqsolve repo is old - we're working in https://github.com/ankitku/z3/tree/paper (note the paper branch)

We have a subclass of smt::theory that we have added (https://github.com/ankitku/z3/blob/paper/src/smt/theory_transeq.cpp) and Z3 calls its new_eq_eh method. Just to be clear, we have added two things here:

1. A theory subclass that uses the internal theory APIs to e.g. add theory axioms and variables. We want this to call out to the Lisp code, described below, and use the response of the Lisp code.
2. Some Lisp code that uses the (external) Z3 C API, which is in a private repo

Thanks again for your responses!

[NikolajBjorner]

If you are somehow losing axioms you have asserted it could be because they get removed during a pop.
context::pop_scope_core removes auxiliary clauses on the stack.
Using the external API for such extensions is generally preferred for several reasons:

1. The legacy core is really difficult to debug.
2. I would like to sunset it in favor of a more extensible and cleaner core (it will still take several months before this is solid, though).
   The user propagator abstraction is supported for both legacy and new core.

The big catch in your case is that I don't support user propagators for string sorts because there is no notion of when a string variable gets assigned a constant string. It could however track equalities without tracking assignments.

As you have your tentacles deep inside the solver already you do have access to the internal state of assertions. This state is accessed by the "copy" method and you can determine which parts should be relevant for you.

[NikolajBjorner]

@mister-walter: maybe consider what it would take to expose enough callbacks for your functionality, similar to user_propagator callbacks. Then you don't ffi link z3 code with yours and you have interface boundaries better defined. This is more up-front overhead than the code you pointed to, but you can use user_propagator as boiler plate to replicate and you will not have to hack your way around what is an external representation of AST objects vs internal. Your LISP code would just see external.

[ankitku]

@NikolajBjorner thanks for suggesting user_propagator. It seems like a very clean way to integrate our decision procedure, and doesn't require ffi linking. I have some questions about the user_propagator class.
I have uploaded a sample file here : https://github.com/ankitku/z3/blob/master/examples/ex.py
It solves the string equation xcyczvycya = yacwazvbu (x,y,z,u,v,w are variables). The function my_eq is not called with the ids assigned for the lhs and rhs. Or it may be that I do not have the correct ids? In which case, is it possible to get the correct ids?
Also, is it possible to extend user_propagator such that one can track integer variables as well?
Thanks

[NikolajBjorner]

user_propagator only works for bit-vectors and Boolean. I mention this above. The solver doesn't assign values to integers or strings during search. It only has to establish that there is a satisfying assignment and the temporary values to integers can change even without backtracking. You would have to either augment user_propagator or create your own version that takes care of the FFI portions you are using.

[NikolajBjorner]

To say it in a different way: the only theories where it suffices to rely on fixed_eh are bit-vectors and booleans. For integers you may be able to propagate based on watching equalities and disequalities but something in addition may be needed. Instead of exposing a general purpose API across theories, user_propagator is focused on the types where I can assume some value assignment.

[ankitku]

Thanks, this is helpful. I will look into augmenting user_propagator with int and string types.