Mathias Preiner, Aina Niemetz, Armin Biere,
"Better Lemmas with Lambda Extraction"
, in FMCAD Inc. 2015: Proc. 15th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15),, Seite(n) 128-135, 2015
Better Lemmas with Lambda Extraction
Sprache des Titels:
Proc. 15th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'15),
In Satisfiability Modulo Theories (SMT), the theory
of arrays provides operations to access and modify an array at
a given index, e.g., read and write. However, common operations
to modify multiple indices at once, e.g., memset or memcpy of the
standard C library, are not supported. We describe algorithms to
identify and extract array patterns representing such operations,
including memset and memcpy.We represent these patterns in our
SMT solver Boolector by means of compact and succinct lambda
terms, which yields better lemmas and increases overall performance.
We describe how extraction and merging of lambda terms
affects lemma generation, and provide an extensive experimental
evaluation of the presented techniques. It shows a considerable
improvement in terms of solver performance, particularly on
instances from symbolic execution.