3 ms·
> There ought to be some representation for theorem resolvers that is good for general purpose programming. It's just that nobody found it yet. There are some
by tom_mellior 9y ago
> There ought to be some representation for theorem resolvers that is good for general purpose programming. It's just that nobody found it yet.
There are some nice examples of search-based programming in Z3 (using the Python API) in https://yurichev.com/writings/SAT_SMT_draft-EN.pdf https://yurichev.com/writings/SAT_SMT_draft-EN.pdf , if that is along the lines of what you meant.
- marcosdumay 9y agoThat's cool. Although the syntax is very specialized, I never though about approaching general purpose search from a SAT solver.