TY - GEN

T1 - Variant Satisfiability of Parameterized Strings

AU - Meseguer, José

N1 - Funding Information:
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 - http://www.scopus.com/inward/record.url?scp=85099066853&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85099066853&partnerID=8YFLogxK

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 -