I am trying to build a string theory solver and one of the ideas that came up was to write the code inside the z3 prover but that requires understanding the whole z3 code, I am wondering if there is a tutorial on how to do that? I have checked thoroughly but I don't seem to find anything.
1 Answers
You can't really integrate a custom theory with z3 without getting more or less intimately familiar with the internals, and unfortunately this process isn't all that well documented. This is hardly surprising: Z3 is a big and a research(-y) project and there are many moving parts.
Having said that, see the stack-overflow question on prior advice from Nikolaj, who is the main author of z3: SMT solver with custom theories?
This resource is a nice write-up about how to understand theory solvers are architected: http://theory.stanford.edu/~nikolaj/z3navigate.html
No matter which path you go, you'll have a lot of questions. The best place to ask them would be the "discussions" forum of the z3 GitHub site: https://github.com/Z3Prover/z3/discussions
Best of luck!
Related