Semantic Evaluation versus SMT Solving in the RISCAL Model Checker

In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room for improvements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.