Norn: an SMT solver for string constraints. We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Diep, Bui Phi; Holík, Lukáš; Janků, Petr: Chain-free string constraints (2019)
- Day, Joel D.; Ganesh, Vijay; He, Paul; Manea, Florin; Nowotka, Dirk: The satisfiability of word equations: decidable and undecidable theories (2018)
- Amadini, Roberto; Flener, Pierre; Pearson, Justin; Scott, Joseph D.; Stuckey, Peter J.; Tack, Guido: Minizinc with strings (2017)
- Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A String Solver with Theory-aware Branching (2017) arXiv
- Scott, Joseph D.; Flener, Pierre; Pearson, Justin; Schulte, Christian: Design and implementation of bounded-length sequence variables (2017)