International Conference on integrated Formal Methods (iFM)
In the SMT(LRA) learning problem, the goal is to learn SMT(LRA) constraints from real-world data. To improve the scalability of SMT(LRA) learning, we present a novel approach called SHREC which uses hierarchical clustering to guide the search, thus reducing runtime. A designer can choose between higher quality (SHREC1 ) and lower runtime (SHREC2 ) according to their needs. Our experiments show a significant scalability improvement and only a negligible loss of accuracy compared to the current state-of-the-art.