On Simplification of Formulas with Unconstrained Variables and Quantifiers

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JONÁŠ Martin STREJČEK Jan

Rok publikování 2017
Druh Článek ve sborníku
Konference Theory and Applications of Satisfiability Testing – SAT 2017
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://link.springer.com/chapter/10.1007%2F978-3-319-66263-3_23
Doi http://dx.doi.org/10.1007/978-3-319-66263-3_23
Obor Informatika
Klíčová slova SMT solving; formula simplifications; bit-vectors
Popis Preprocessing of the input formula is an essential part of all modern smt solvers. An important preprocessing step is formula simplification. This paper elaborates on simplification of quantifier-free formulas containing unconstrained terms, i.e. terms that can have arbitrary values independently on the rest of the formula. We extend the idea in two directions. First, we introduce partially constrained terms and show some simplification rules employing this notion. Second, we show that unconstrained terms can be used also for simplification of formulas with quantifiers. Moreover, both these extensions can be merged in order to simplify partially constrained terms in formulas with quantifiers. We experimentally evaluate the proposed simplifications on formulas in the bit-vector theory.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.