Procedural Attachment in Z3

Question

I am using z3py I have a predicate over two integers that needs to be evaluated using a custom algorithm. I have been trying to get it implemented, without much success. Apparently, what I need is a procedural attachment, which is now deprecated. Could anybody tell me how I might impelement this in z3py? I understand that it involves use of Tactics, but I am afraid I haven't managed to figure out how to use them. I wouldn't mind using the deprecated way either, as long as it works.

Answer 1

There is no procedural attachment tactic. All tactics are implemented inside of Z3; you can compose tactics from outside. Previous versions of Z3 exposed a way to register a "user theory". This was deprecated since (1) the source of Z3 is now available so users can compile with their custom theories directly, (2) the user-theory abstraction lacked proper support for model generation. You can of course try previous versions of Z3 that have the user theory extension, but it is not supported.