SyMT: Symmetry Detection for SMT

Description

This is a preliminary page to host SyMT, a command-line tool to detect symmetries in SMT formulas. SyMT detects symmetries by building a colored graph from the given SMT formula, and applying graph automorphism detection with the third party tool Saucy3.
A description of SyMT is available in this tool paper submitted to CADE-24.

Download and installation

The code source of SyMT is distributed in this file, under the BSD license. To install, apply the following instructions:

  tar zxvf SyMT.tar.gz
  cd SyMT
  make

and type

  ./SyMT -h

for help usage. For instance, type

  ./SyMT ~/SMT-LIB2/QF_UF/NEQ/NEQ004_size4.smt2

to get the set of generators for the symmetries of the formula in file QF_UF/NEQ/NEQ004_size4.smt2.

Feedback

To submit a bug report, please fill this form. Thanks for helping us improving SyMT.