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?

Improve this question
$\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$
    – purple_lolakos
    Commented Feb 15, 2021 at 10:53

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
0
$\begingroup$

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

Improve this answer
$\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
    Commented Feb 28, 2021 at 3:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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