TY - GEN
T1 - Variant Satisfiability of Parameterized Strings
AU - Meseguer, José
N1 - Acknowledgements. I cordially thank the referees for their very helpful suggestions to improve the paper. This work has been partially supported by NRL under contract N00173-17-1-G002.
PY - 2020
Y1 - 2020
N2 - Two “knowingly incomplete,” yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of “parametric” here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a “knowingly incomplete,” yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.
AB - Two “knowingly incomplete,” yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of “parametric” here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a “knowingly incomplete,” yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.
UR - https://www.scopus.com/pages/publications/85099066853
UR - https://www.scopus.com/pages/publications/85099066853#tab=citedBy
U2 - 10.1007/978-3-030-63595-4_6
DO - 10.1007/978-3-030-63595-4_6
M3 - Conference contribution
AN - SCOPUS:85099066853
SN - 9783030635947
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 96
EP - 113
BT - Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
A2 - Escobar, Santiago
A2 - Martí-Oliet, Narciso
PB - Springer
T2 - 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
Y2 - 20 October 2020 through 22 October 2020
ER -