I'm using the MONOSAT SMT solver for graphs which only accepts .gnf files (an extension of DIMACS CNF with a way to specify graph nodes/edges) or input through its Python API. However, the input files I want to test for satisfiability are written in the SMT-LIB format. Are there tools to convert between the two formats?
For instance, it is my understanding that the Z3 solver supports input from both SMT-LIB and DIMACS and has respective parsers in the source code for these formats. Is there anything else that would work on its own to convert an SMT problem?