<div class="csl-bib-body">
<div class="csl-entry">Bjorner, N., Eisenhofer, C., & Kovács, L. (2022). User-Propagation for Custom Theories in SMT Solving. In D. Deharbe & A. Hyvärinen (Eds.), <i>Satisfiability Modulo Theories. 20th International Workshop. SMT 2022. Proceedings</i> (pp. 71–79). CEUR-WS.org. https://doi.org/10.34726/4104</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/177097
-
dc.identifier.uri
https://doi.org/10.34726/4104
-
dc.description.abstract
We present ongoing work on developing a user-propagator framework in SMT solving. We argue that the integration of user-propagators in SMT solving yields an efficient approach towards custom theory reasoning, without bringing fundamental changes in the underlining SMT architecture. We showcase our approach in the SMT solver Z3, provide practical evidence of our work, and also discuss potential venues for further improvements.
en
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
CEUR Workshop Proceedings
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
theory reasoning
en
dc.subject
lazy encoding
en
dc.subject
SMT callbacks
en
dc.title
User-Propagation for Custom Theories in SMT Solving
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34726/4104
-
dc.contributor.affiliation
Microsoft Research Lab, USA
-
dc.contributor.editoraffiliation
CLEARSY Systems Engineering; Universidade Federal do Rio Grande do Norte
