Lemmas on Demand for Lambdas

Mathias Preiner; Aina Niemetz; Armin Biere

Lemmas on Demand for Lambdas

Mathias Preiner, Aina Niemetz, Armin Biere

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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.

Original language	English
Title of host publication	Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems
Number of pages	10
Publication status	Published - Oct 2013

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{df625cba6cf5456e8f8760089d16f900,

title = "Lemmas on Demand for Lambdas",

abstract = "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.",

author = "Mathias Preiner and Aina Niemetz and Armin Biere",

year = "2013",

month = oct,

language = "English",

booktitle = "Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems",

}

TY - GEN

T1 - Lemmas on Demand for Lambdas

AU - Preiner, Mathias

AU - Niemetz, Aina

AU - Biere, Armin

PY - 2013/10

Y1 - 2013/10

N2 - 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.

AB - 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.

M3 - Conference proceedings

BT - Proc. 2nd Intl. Work. on Design and Implementation of Formal Tools and Systems

ER -