Toward Domain-Specific Solvers for Distributed Consistency (2012) [pdf]
users.soe.ucsc.edu
users.soe.ucsc.edu
> 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?
> 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. ;)