Augment your SMT solver by learning to optimize its performance for your dataset of formulas.
Learn strategy that is fast at solving formulas in your dataset
Augment state-of-the-art SMT solver with the learned strategy
We learned strategies on five different benchmarks AProVE, lepzig, hycomp, core and Sage2. These contain formulas of varying complexity across 3 logics QF_NRA, QF_BV and QF_NIA. Below we provide runtime comparison of our learned strategies against the handcrafted strategy used by Z3 version 4.6.2. We provide more experiments in our paper.
Additional materials that describe the FastSMT tool in more detail
