# I/O

There are some useful I/O classes for parsing/reading/writing formulas and other data structures.

## Parsers

Parsers are used to parse formula strings into LogicNG formulas. Throughout the documentation, we used the default parser on formula factories by calling `f.parse(...)`

, but we can also generate parsers by hand or - most important - implement own parsers for our applications.

Parsers in LogicNG are generated by the parser framework ANTRL (LogicNG's only external dependency). You only define a grammar file and ANTLR generates the Java classes for the parser at compile time. LogicNG's parser grammars lie here. There are two parsers:

- PropositionalParser for parsing propositional formulas without cardinality or pseudo-Boolean constraints. Its grammar can be found here
- PseudoBooleanParser for parsing formulas with cardinality or pseudo-Boolean constraints.

Application Insight

You can easily implement you own parsers for you propositional language by looking at these grammar files and implementing your own parser inheriting from FormulaParser. Then you only need to write minimal code.

## Readers

There are two formula readers implemented in LogicNG:

- DIMACS reader for reading CNF files as used in the SAT competition in the DIMACS CNF format.
- Formula reader for reading files in LogicNG syntax from a file.

The formula reader can read propositional formulas with or without pseudo-Boolean constraints. Multiple lines in a file are interpreted as a conjunction of the formulas in each line.

## Writers

There are three writers for formulas in the `org.logicng.io`

package:

- DIMACS writer for writing CNFs as DIMACS CNF files like described above.
- Formula writer for writing formulas in LogicNG syntax. The formula writer has the option
`splitAndMultiline`

which, if set to`true`

, writes the different operands of a top-level conjunction in single lines. This can often improve readability, and the corresponding`FormulaReader`

can read this format. - Formula dot file writer for writing a graphical representation of formulas as a DOT file. Such a file can be used to generate a graphical representation e.g. with Graphviz. E.g. the graphics in the chapter on formulas were generated this way. The parameter
`alignLiterals`

allows to align all literals of a formula at the same level, meaning all terminal nodes are at the same level.

Other data structures have also their own writers.

### BDDs

Graphs of a BDD can be written as DOT file with the BDD dot file writer. The graphics of BDDs in this documentation were generated this way.

### Graphs

For graphs, there are two writers:

- DIMACS writer for writing a DIMACS graph file of the graph.
- Graph dot file writer for writing a dot file of the graph. The graphics of graphs in this documentation were generated this way.