ABC - Automata-Based model Counter for string constraints
The Automata Based Counter (ABC) is a string constriant solver and model counter. ABC provides solutions to systems of string constraints in the form of a deterministic finite automaton. In addition ABC produces symbolic representation of the number of strings within a length bound, k, that satisfy a set of constraints. ABC can also output the number of satisfying solutions for a specific provided bound.
ABC source code is available on GitHub
String, integer, and mixed constraint data
CAV'15 Experimental DataWe validated ABC on several sets of benchmarks. The counting results and input files are available for download.
Java Benchmarks (Original Data Source)
Satisfiability Checking (Original Data Source)