Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no constraint programming solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying only on integer variables. This conversion is obtained via rewrite rules, and does not require any extension of the existing FlatZinc specification. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems.
MiniZinc with strings / Amadini R.; Flener P.; Pearson J.; Scott J.D.; Stuckey P.J.; Tack G.. - ELETTRONICO. - 10184:(2017), pp. 59-75. (Intervento presentato al convegno 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016 tenutosi a gbr nel 2016) [10.1007/978-3-319-63139-4_4].
MiniZinc with strings
Amadini R.
;
2017
Abstract
Strings are extensively used in modern programming languages and constraints over strings of unknown length occur in a wide range of real-world applications such as software analysis and verification, testing, model checking, and web security. Nevertheless, practically no constraint programming solver natively supports string constraints. We introduce string variables and a suitable set of string constraints as builtin features of the MiniZinc modelling language. Furthermore, we define an interpreter for converting a MiniZinc model with strings into a FlatZinc instance relying only on integer variables. This conversion is obtained via rewrite rules, and does not require any extension of the existing FlatZinc specification. This provides a user-friendly interface for modelling combinatorial problems with strings, and enables both string and non-string solvers to actually solve such problems.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
