SONOLAR, the Solver for non-linear Arithmetic, is an SMT-Solver that solves quantifier-free fixed-size bit-vector logic formulas. The solver supports the SMT-LIB format including the following logics: Bit vectors (QF_BV). Bit vectors with arrays (QF_ABV). IEEE 754 floating point operations including all rounding modes with arbitrary range and precision: The solver supports the symbols described in the SMT-LIB theory for floting point numbers. Since SMT-LIB logic names are yet to be defined for this theory, the logics QF_BV and QF_ABV have been extended by these symbols. SONOLAR uses bit-blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide the satisfiability. For handling the extensional theory of arrays, the lemmas on demand approach described in  has been adopted. To this end a series of word-level simplification rules are applied to the input formula which is then converted to an And-Inverter Graph. After performing bit-level simplifications a Boolean CNF formula is generated and fed to a SAT solver. MiniSat 2.2.0 and Glucose 3.0 are used as SAT solvers [4, 1]. SONOLAR is currently used for automatic test data generation in the field of model-based testing and C/C++-unit testing
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Zeljić, Aleksandar; Backeman, Peter; Wintersteiger, Christoph M.; Rümmer, Philipp: Exploring approximations for floating-point arithmetic using uppsat (2018)
- Brain, Martin; D’Silva, Vijay; Griggio, Alberto; Haller, Leopold; Kroening, Daniel: Deciding floating-point logic with abstract conflict driven clause learning (2014)