2

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.

M.Noe
  • 58
  • 4
  • [What topics can I ask about here?](https://stackoverflow.com/help/on-topic) – Rob Feb 24 '21 at 10:55
  • 3
    This is a perfectly good question to ask; and is seeking technical info. Should be re-open. – alias Feb 24 '21 at 18:39

1 Answers1

2

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!

alias
  • 28,120
  • 2
  • 23
  • 40