Saída Z3 e DIMACS
Atualmente, o Z3 suporta o formato DIMACS para entrada. Existe alguma maneira de produzir o formato DIMACS para o problema antes da solução? Quero dizer, converter o problema para um sistema CNFs e imprimi-lo em um formato DIMACS. Se não, qualquer idéia nesse sentido seria mais que útil.