Skip to content

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:

  1. PropositionalParser for parsing propositional formulas without cardinality or pseudo-Boolean constraints. Its grammar can be found here
  2. 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:

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: