On Incremental Pre-processing for SMT

Bjorner, N; Fazekas, K

Bjorner, N (通讯作者),Microsoft Res, Redmond, WA 98052 USA.

AUTOMATED DEDUCTION, CADE 29, 2023; 14132 (): 41

Abstract

We introduce a calculus for incremental pre-processing for SMT and instantiate it in the context of z3. It identifies when powerful formula simplifica......

Full Text Link