4 ms·

For anyone wondering how you could write a solver in 1500 lines of C, the answer is here: https://github.com/DennisYurichev/ToySMT/blob/master/ToySMT.c#L1189 ht

by munin 9y ago

For anyone wondering how you could write a solver in 1500 lines of C, the answer is here: https://github.com/DennisYurichev/ToySMT/blob/master/ToySMT.c#L1189 https://github.com/DennisYurichev/ToySMT/blob/master/ToySMT.... (i.e., use 'system' to shell out to an already existing solver, which is at least documented in the readme).

hardmath123 9y ago
(To be clear, it shells out to an existing SAT solver. If I understand correctly, the 1500 lines of C implement the "modulo theory" part of "satisfiable modulo theory" — that is, they "compile" things like bitvector addition into pure boolean circuits.)