1

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.

daw
  • 1,959
  • 1
  • 20
  • 25

1 Answers1

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.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • I think you are suggesting a pre-processing step before calling Z3 but that won't be enough. What I'm looking for is a way to write a custom assertion that is called by the solver when testing permutations. – daw Jul 09 '16 at 17:31
  • I think you should look at the API mentioned by Nikolaj. – Heyji Jul 10 '16 at 22:38
  • I am not asking about building a z3 SMTLIB expression piecemeal using the API. 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 think the actual answer is that it can't be done. – daw Jul 11 '16 at 09:37
  • You might be able to achieve what you want by writing a custom theory extension (similar to a plugin) for Z3. Lacking personal experience in this direction, I can unfortunately not give you any further pointers, though. – Malte Schwerhoff Jul 11 '16 at 13:19
  • Thanks Malte - that sounds promising but I haven't found any documentation, examples or API calls related to custom theories. The only mention is in other stack overflow questions that indicate they may have been deprecated. – daw Jul 11 '16 at 14:06