SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver

摘要

Existing Separation Logic (a.k.a Difference Logic, DL) solvers can be broadly classified as eager or lazy, each with its own merits and de-merits. We propose a novel Separation Logic Solver SDSAT that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver SDSAT works in two phases: allocation and solve. In the allocation phase, it allocates non-uniform adequate ranges for variables appearing in separation predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm Nu-SMOD with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the Separation Logic formula is not transformed into an equi-satisfiable Boolean formula in one step, but rather done lazily in the following phase. In the solve phase, SDSAT uses a lazy refinement approach to search for a satisfying model within the allocated ranges. Thus, any partially DL-theory consistent model can be discarded if it can not be satisfied within the allocated ranges. Note the crucial difference: in eager approaches, such a partially consistent model is not allowed in the first place, while in lazy approaches such a model is never discarded. Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers.