0
$\begingroup$

I've built a rudimentary SAT Solver from scratch, and wanted to do the same with SMT solvers as well.

While I've found two toy SMT Solver implementations in Haskell and Ocaml, but no tutorials or examples, which is a stark contrast from all SAT Solver tutorials out there.

Is there a resource for building a toy SMT Solver from scratch?

$\endgroup$
1
  • $\begingroup$ That's quite an interesting point. I personally would follow the SAT ones and then "modify" it towards an SMT. There are plenty of examples with that. $\endgroup$ Feb 15 at 10:53
0
$\begingroup$

Have a look at the material on Leonardo de Moura's website. For starters, I can recommend the talk he gave at the Aalto SAT/SMT Summer School in 2013 titled Internals of SMT solvers.

$\endgroup$
0
$\begingroup$

I think these slides give a foundation of building a SMT solver, somewhat

$\endgroup$
1
  • 1
    $\begingroup$ Thank you for your answer! 1) Unfortunately, your link doesn't work. 2) If it's applicable here, can you please also summarize the main points of the link? Link-only answers can be broken someday and have other issues 3) The general meeting of an "accepted answer" is that it solves the problem. As I understand, you currently don't know whether the slides will actually help you to build a SMT solver, so I'm not sure that the answer should be accepted. $\endgroup$
    – user114966
    Feb 28 at 3:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.