Towards a Modern Truth-Maintenance System and Inference Engine
This stub shows how to translate from the basics of the Truth-Maintenance System (TMS) as presented in the book Building Problem Solvers to an SMT solver. In particular, the tests show code very similar to the basic TMS examples.
Missing from this stub is incrementality of the encoded engine.