Can Z3 call an externally defined function?

Question

I am using Z3opt. The majority of my model can be expressed in standard SMTLIB but part of it needs to be implemented in a general purpose programming language with constructs like string processing, associative arrays etc.

Is it possible to use an externally defined function in a Z3 model? I know this would kill solver performance but it would only be a small part of the model.

-- edit for clarification --

I wish to supply the implementation of a constraint (as a function pointer or equivalent) in order to support functions not supported by Z3 (e.g. trig functions). I would accept the tradeoff that Z3 cannot apply any heuristics when using a blackbox constraint like this.

Answer 1

You can load SMTLIB assertions from the binary interfaces that Z3 exposes, and then use Z3 from python, Java, .NET, C++, Ocaml to perform other operations before calling into the code that checks feasibility or optimizes objectives. The z3opt tutorial on http://rise4fun.com/z3opt contains pointers to Phan's F# code that exemplifies using the binary API (in this case from F#/.NET). The examples directory in the source code contains examples of using the various APIs. If you need something fancier that isn't exposed, then the default fallback is based on Z3 being open source so you can add any special feature you desire. If you feel there is a useful feature of general interest it would be useful to track an issue on https://github.com/z3prover/z3.git, and if you have it implemented you can add a pull request.