Designing Theory Solvers with Extensions

“Designing Theory Solvers with Extensions” by Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, and Clark Barrett. In Proceedings of the 11^th International Symposium on Frontiers of Combining Systems (FroCoS '17), (Clare Dixon and Marcelo Finger, eds.), Sep. 2017, pp. 22-40. Brasilia, Brazil.

Abstract

Satisfiability Modulo Theories (SMT) solvers have been developed to natively support a wide range of theories, including linear arithmetic, bit-vectors, strings, algebraic datatypes and finite sets. They handle constraints in these theories using specialized theory solvers. In this paper, we overview the design of these solvers, specifically focusing on theories whose function symbols are partitioned into a base signature and an extended signature. We introduce generic techniques that can be used in solvers for extended theories, including a new context-dependent simplification technique and model-based refinement techniques. We provide case studies showing our techniques can be leveraged for reasoning in an extended theory of strings, for bit-vector approaches that rely on lazy bit-blasting and for new approaches to non-linear arithmetic.

BibTeX entry:

@inproceedings{RTJ+17,
   author = {Andrew Reynolds and Cesare Tinelli and Dejan Jovanovi{\'c}
	and Clark Barrett},
   editor = {Clare Dixon and Marcelo Finger},
   title = {Designing Theory Solvers with Extensions},
   booktitle = {Proceedings of the {\it 11^{th}} International Symposium
	on Frontiers of Combining Systems (FroCoS '17)},
   series = {Lecture Notes in Artificial Intelligence},
   volume = {10483},
   pages = {22--40},
   publisher = {Springer},
   month = sep,
   year = {2017},
   note = {Brasilia, Brazil},
   url = {http://theory.stanford.edu/~barrett/pubs/RTJ+17.pdf}
}

(This webpage was created with bibtex2web.)