public static void write ( final String fileName , Formula formula , boolean writeMapping ) throws IOException { File file = new File ( fileName . endsWith ( ".cnf" ) ? fileName : fileName + ".cnf" ) ; SortedMap < Variable , Long > var2id = new TreeMap <> ( ) ; long i = 1 ; for ( Variable var : new TreeSet <> ( formula . variables ( ) ) ) { var2id . put ( var , i ++ ) ; } if ( ! formula . holds ( CNF_PREDICATE ) ) { throw new IllegalArgumentException ( "Cannot write a non-CNF formula to dimacs. Convert to CNF first." ) ; } List < Formula > parts = new ArrayList <> ( ) ; if ( formula . type ( ) . equals ( FType . LITERAL ) ) { parts . add ( formula ) ; } else { for ( Formula part : formula ) { parts . add ( part ) ; } } StringBuilder sb = new StringBuilder ( "p cnf " ) ; int partsSize = formula . type ( ) . equals ( FType . FALSE ) ? 1 : parts . size ( ) ; sb . append ( var2id . size ( ) ) . append ( " " ) . append ( partsSize ) . append ( System . lineSeparator ( ) ) ; for ( Formula part : parts ) { for ( Literal lit : part . literals ( ) ) { sb . append ( lit . phase ( ) ? "" : "-" ) . append ( var2id . get ( lit . variable ( ) ) ) . append ( " " ) ; } sb . append ( String . format ( " 0%n" ) ) ; } if ( formula . type ( ) . equals ( FType . FALSE ) ) { sb . append ( String . format ( "0%n" ) ) ; } try ( BufferedWriter writer = new BufferedWriter ( new OutputStreamWriter ( new FileOutputStream ( file ) , StandardCharsets . UTF_8 ) ) ) { writer . append ( sb ) ; writer . flush ( ) ; } if ( writeMapping ) { String mappingFileName = ( fileName . endsWith ( ".cnf" ) ? fileName . substring ( 0 , fileName . length ( ) - 4 ) : fileName ) + ".map" ; writeMapping ( new File ( mappingFileName ) , var2id ) ; } }
Writes a given formula s internal data structure as a dimacs file . Must only be called with a formula which is in CNF .