Don't care in SMT: Building flexible yet efficient abstraction/refinement solvers
This paper describes a method for combining "off-the-shelf" SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning don't care to as...[Show more]
|Collections||ANU Research Publications|
|Source:||International Journal on Software Tools for Technology Transfer|
|01_Bauer_Don't_care_in_SMT:_Building_2010.pdf||706.85 kB||Adobe PDF||Request a copy|
|02_Bauer_Don't_care_in_SMT:_Building_2010.pdf||183.49 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.