94
T. Okudono and A. King
of contrast, Backeman et al. [2] propose a calculus over a core language, which
supports interpolation and is rich enough to describe BV formulae, even making
use of Groebner bases to express polynomial equality relationships. Since interpolation is performed within their core language, they do not aim to derive a
BV interpolant, and therefore their work is orthogonal to ours. Yet if Backeman’s procedure returns an interpolant in their core language and it could be
interpreted as an LIA formula, which would seem likely for many cases, then our
work could convert the LIA formula back to BV.
Further afield, polynomial algorithms for interpolation have developed for
systems of linear congruence equations [19, section 4], conjunctions of linear
Diophantine equations and disequations [19, section 6], and systems of mixed
integer linear equations [19, section 7]. This comprehensive study stops short of
using LIA to interpolate BV formula, mentioning the problem as future work.
Abstract domains have been proposed for tracking linear modulo relationships where the module is a power of 2 [13, 22, 28]. These domains, which are essentially specialist solvers, express more than linear equalities [21], while enabling
the domain operations to be realised using machine arithmetic. Surprisingly, systems of linear inequalities can be reinterpreted to model machine arithmetic by
just changing the concretisation function [32] and the handling of guards [32].
6 Concluding Discussion
To repurpose efficient LIA interpolation engines to BV, we have shown how to
systematically construct a BV formula so its solutions are exactly those of an
LIA interpolant. Since an LIA interpolant summarises the reason for a conflict
between two LIA formula, we seek to retain its compact structure by introducing no more than simple boxes around the LIA solutions which block extraneous
BV solutions. When this encoding tactic, called boxing, is not applicable, gapping is used to decompose an LIA inequality into two or more inequalities which
are amenable to boxing. We show how the size of the resulting BV interpolants
are smaller than BV interpolants constructed by merely partitioning the LIA
solutions into columns, and demonstrate how boxing and gapping improves the
runtime of an interpolation-based model-checker. We instantiate a model-checker
with LIA and BV to compare their performance, and conclude that with this
encoding BV interpolation is feasible. Because of wrap-around, BV is substantially more complicated than LIA for interpolation, yet BV is no more than
twice as slow as LIA for over half the benchmarks. Furthermore, the resulting
BV interpolants can be validated, independent of LIA, just using a BV solver.
Acknowledgments We thank anonymous reviewers for their comments which helped us
improve the paper. We thank Alberto Griggio for his help with MathSAT5 and looking
into the intellectual property restrictions on sharing his extension to Kratos [8], a
model checker based on lazy predicate abstraction. We also thank Chris Coppins with
his help with IMPACT and Peter Backeman for tirelessly answering our e-mails. This
work was funded, in part, by EPSRC EP/N020243/1 and by JST ERATO HASUO
Metamathematics for Systems Design Project JPMJER1603.
T. Okudono and A. King
of contrast, Backeman et al. [2] propose a calculus over a core language, which
supports interpolation and is rich enough to describe BV formulae, even making
use of Groebner bases to express polynomial equality relationships. Since interpolation is performed within their core language, they do not aim to derive a
BV interpolant, and therefore their work is orthogonal to ours. Yet if Backeman’s procedure returns an interpolant in their core language and it could be
interpreted as an LIA formula, which would seem likely for many cases, then our
work could convert the LIA formula back to BV.
Further afield, polynomial algorithms for interpolation have developed for
systems of linear congruence equations [19, section 4], conjunctions of linear
Diophantine equations and disequations [19, section 6], and systems of mixed
integer linear equations [19, section 7]. This comprehensive study stops short of
using LIA to interpolate BV formula, mentioning the problem as future work.
Abstract domains have been proposed for tracking linear modulo relationships where the module is a power of 2 [13, 22, 28]. These domains, which are essentially specialist solvers, express more than linear equalities [21], while enabling
the domain operations to be realised using machine arithmetic. Surprisingly, systems of linear inequalities can be reinterpreted to model machine arithmetic by
just changing the concretisation function [32] and the handling of guards [32].
6 Concluding Discussion
To repurpose efficient LIA interpolation engines to BV, we have shown how to
systematically construct a BV formula so its solutions are exactly those of an
LIA interpolant. Since an LIA interpolant summarises the reason for a conflict
between two LIA formula, we seek to retain its compact structure by introducing no more than simple boxes around the LIA solutions which block extraneous
BV solutions. When this encoding tactic, called boxing, is not applicable, gapping is used to decompose an LIA inequality into two or more inequalities which
are amenable to boxing. We show how the size of the resulting BV interpolants
are smaller than BV interpolants constructed by merely partitioning the LIA
solutions into columns, and demonstrate how boxing and gapping improves the
runtime of an interpolation-based model-checker. We instantiate a model-checker
with LIA and BV to compare their performance, and conclude that with this
encoding BV interpolation is feasible. Because of wrap-around, BV is substantially more complicated than LIA for interpolation, yet BV is no more than
twice as slow as LIA for over half the benchmarks. Furthermore, the resulting
BV interpolants can be validated, independent of LIA, just using a BV solver.
Acknowledgments We thank anonymous reviewers for their comments which helped us
improve the paper. We thank Alberto Griggio for his help with MathSAT5 and looking
into the intellectual property restrictions on sharing his extension to Kratos [8], a
model checker based on lazy predicate abstraction. We also thank Chris Coppins with
his help with IMPACT and Peter Backeman for tirelessly answering our e-mails. This
work was funded, in part, by EPSRC EP/N020243/1 and by JST ERATO HASUO
Metamathematics for Systems Design Project JPMJER1603.