Encoding Files and Problem Generators for Diagrammatic Equivalence in TPTP and SMT-LIB

This material is complementary to the paper Challenging Benchmarks for Diagrammatic Equivalence in TPTP and SMT-LIB by Julie Cailler, Noé Delorme, and Sophie Tourret.This archive provides encoding files and benchmark generators for circuit equivalence problems (CE, PCE, SPCE). It includes TPTP and SMT-LIB first-order logic encodings of the corresponding coherence equations. Scripts are provided to automatically generate benchmark instances for each problem variant in TPTP and SMT-LIB formats.