Mathias Preiner, Aina Niemetz, Armin Biere,
"Lemmas on Demand for Lambdas"
: Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems, 10-2013
Original Titel:
Lemmas on Demand for Lambdas
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems
Original Kurzfassung:
We generalize the lemmas on demand de-
cision procedure for array logic as implemented in
Boolector to handle non-recursive and non-extensional
lambda terms. We focus on the implementation aspects
of our new approach and discuss the involved algorithms
and optimizations in more detail. Further, we show how
arrays, array operations and SMT-LIB v2 macros are
represented as lambda terms and lazily handled with
lemmas on demand. We provide experimental results that
demonstrate the effect of native lambda support within
an SMT solver and give an outlook on future work.