S3: An Efficient String Solver and Model Counter

- S3N is the newest version of S3. It is built as a native solver of Z3. Its performance is boosted up with the help of inter-theory dependency analysis. It is introduced in the OOPSLA-20 [Paper]

- S3# is the next version of S3. It also supports model counting. It is introduced in the CAV-17 [Paper][Slide]

- S3P is the next version of S3. S3P stands for Progressive S3, and is introduced in the CAV-16 [Paper][Slide]

- S3 stands for Symbolic String Solver and is introduced in the CCS-14 [Paper][Slide]

- Version [26-Nov-2020]: Tested on Ubuntu 14.04

- Version [03-Jan-2018]: Fixed bugs.

- Version [08-Nov-2017]: Removed Minimize function.

- Version [28-Sep-2017]: Fixed bugs reported by ABC group.

- Version [20-Jul-2017]: Contains binaries, benchmarks, etc.

- Version [09-Aug-2017]: Fixed bugs reported by Hung-En and Petr Janku.

- Version [22-Jun-2017]: Fixed bugs.

- Version [10-Mar-2017]: Implemented some heuristics.

- Initial Version: Supported progressive reasoning.

- Version [17-Sep-2015]: Fixed bugs with Kaluza benchmarks (reported by Z3-str group and Norn group).

- Version [25-Aug-2015]: Fixed bugs reported by Yongbo Li.

- Version [16-Aug-2015]: Fixed bugs reported by Steve Kratzer, and Yongbo Li.

- Version [06-Jan-2015]: Changed the input format. Supported SMT-LIB2 format. Fixed bugs reported by Xiaofei Xie.

- Initial Version: Supported Kaluza input format (in order to test with Kaluza benchmark test suite).

- The source code of S3 solver is available here.

- To build S3 from source codes, you also need to download the modified version of Z3 below.

- S3 is built on top of Z3-str. In addition to what Z3-str supports, S3 supports (see our CCS'14 paper):
+ Regular expressions
+ Membership predicates
+ High-level string operations that work on regular expressions such as replaceAll

- The source code of the modified Z3 is available here.
+ We modify Z3 to have the interaction between String theory and Arithmetic theory.
+ These newly-added API methods allows us to query the length of a string variable, and relationship between the length of different string variables, as shown in our CCS'14 paper.

- Our modified version of Z3 is also used by Z3-str GROUP for integer/string theory integration.