Overview
rxn-balancer reads an unbalanced chemical equation typed at the command line and prints the balanced version. It parses each chemical formula into element counts, then uses the Z3 theorem prover to find integer stoichiometric coefficients that conserve every element between reactants and products.
Features
- Parses chemical formulas (including multi-letter elements and subscripts) into element/count pairs
- Supports equations with any number of reactants and products
- Builds one conservation constraint per distinct element across the whole equation
- Constrains all coefficients to be positive integers
- Reports when no balanced solution exists
- Runs as an interactive loop, accepting new equations repeatedly