Designing Theory Solvers with Extensions

by Andrew Reynolds, Cesare Tinelli, Dejan Jovanović, Clark Barrett
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.
Reference:
Designing Theory Solvers with Extensions (Andrew Reynolds, Cesare Tinelli, Dejan Jovanović, Clark Barrett), In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS ’17) (Clare Dixon, Marcelo Finger, eds.), Springer, volume 10483, 2017. (Brasilia, Brazil)
Bibtex Entry:
@inproceedings{RTJ+17,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/RTJ+17.pdf",
  author    = "Andrew Reynolds and Cesare Tinelli and Dejan Jovanović and Clark Barrett",
  title     = "Designing Theory Solvers with Extensions",
  booktitle = "Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17)",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 10483,
  publisher = "Springer",
  editor    = "Clare Dixon and Marcelo Finger",
  pages     = "22--40",
  month     = sep,
  year      = 2017,
  note      = "Brasilia, Brazil",
  category  = "Conference Publications",
  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."
}

Fork me on GitHub