Stingx — String Constraint Solver

Stingx is a string constraint solver backend for invariant generation. It is vendored in third-party/stingx_toolchain/ and used by experimental invariant-generation scripts in this repository.

Location: third-party/stingx_toolchain/ (vendored, local use)

Overview

Stingx solves systems of linear constraints over string variables and generates loop invariants expressed as linear arithmetic constraints. It parses constraint descriptions from .in files and produces invariant candidates.

The toolchain includes:

• A lexer/parser (LinTS.l / LinTS.y) for the constraint input format.

• Core constraint-solving engine with expression stores, matrix solvers, and polynomial stores.

• A standalone driver (main.cpp) that reads .in files and runs the invariant-generation pipeline.

Directory Structure

third-party/stingx_toolchain/
├── main.cpp              # Standalone driver
├── CMakeLists.txt        # Local build entry
├── Dockerfile            # Container build environment
└── stingx/               # Vendored backend
    ├── Expression.*      # Expression representation
    ├── LinTS.*           # Linear constraint system
    ├── Elimination.*     # Variable elimination
    ├── MatrixStore.*     # Matrix storage
    ├── PolyStore.*       # Polynomial store
    └── ...

Build and Run

cd third-party/stingx_toolchain
cmake -S . -B build
cmake --build build -j$(nproc)
./build/bin/stingx_file_runner <input.in>