3 ms·
Toward Domain-Specific Solvers for Distributed Consistency (2012) [pdf]
- Arathorn 8y agoaccording to https://users.soe.ucsc.edu/~lkuper/ https://users.soe.ucsc.edu/~lkuper/ this paper is Feb 2019, not 2012 vintage?
- etrain 8y agoYes, this is correct: http://composition.al/lindsey_kuper_cv.pdf http://composition.al/lindsey_kuper_cv.pdf
- fulafel 8y agoThis got me thinking: > Existing general-purpose SMT solvers lack native supportfor reasoning efficiently about such [..] What is the usual level of reuse and building 3rd party abstractions, when applying solvers? Is there a good web site to look if I want to find some domain specific solver libraries?
- sa1 8y agoThe paper goes on to say that > Unfortunately, in practice it would seem that SMT solvers are monolithic, and SMT internals expertise is required for implementing new theory solvers. and > We argue that programmers should not have to be SMT internals experts in order to implement theory solvers for their domain of interest. We propose to evaluate that claim by developing a framework for implementing custom, efficient domain-specific solvers. In doing so, we hope to democratize theory solver development and make it accessible to programmers who are not SMT internals experts, in the same way that Delite aimed to democratize DSL implementation and make it accessible to programmers who are not compiler experts. The title should give a hint. ;)