Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1394152, author = {Jonáš, Martin and Strejček, Jan}, address = {Cham (Switzerland)}, booktitle = {Theory and Applications of Satisfiability Testing – SAT 2017}, doi = {http://dx.doi.org/10.1007/978-3-319-66263-3_23}, editor = {Serge Gaspers, Toby Walsh}, keywords = {SMT solving; formula simplifications; bit-vectors}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Cham (Switzerland)}, isbn = {978-3-319-66262-6}, pages = {364-379}, publisher = {Springer}, title = {On Simplification of Formulas with Unconstrained Variables and Quantifiers}, url = {https://link.springer.com/chapter/10.1007%2F978-3-319-66263-3_23}, year = {2017} }
TY - JOUR ID - 1394152 AU - Jonáš, Martin - Strejček, Jan PY - 2017 TI - On Simplification of Formulas with Unconstrained Variables and Quantifiers PB - Springer CY - Cham (Switzerland) SN - 9783319662626 KW - SMT solving KW - formula simplifications KW - bit-vectors UR - https://link.springer.com/chapter/10.1007%2F978-3-319-66263-3_23 N2 - 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. ER -
JONÁŠ, Martin and Jan STREJČEK. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In Serge Gaspers, Toby Walsh. \textit{Theory and Applications of Satisfiability Testing – SAT 2017}. Cham (Switzerland): Springer, 2017, p.~364-379. ISBN~978-3-319-66262-6. Available from: https://dx.doi.org/10.1007/978-3-319-66263-3\_{}23.
|