Learning to Instantiate Quantifiers
Armin Biere ( Johannes Kepler University Linz )
- 16:00 18th December 2017Room 278, Wolfson Building
In this talk we go over our recent result presented at TACAS'17 on using
grammar based model synthesis for quantifier instantiation to solve
quantified SMT problems, with a particular focus on the theory of fixed-size
bit-vectors. Our technique neither relies on quantifier specific
simplifications nor on other heuristic quantifier instantiation techniques.
It is implemented in our SMT solver Boolector and experiments show that it
is competitive with the state-of-the-art in solving quantified bit-vectors.
This is joint work with Mathias Preiner and Aina Niemetz.
Share this:
