Implement parser for dimacs

src/main/java/me/paultristanwagner/satchecking/parse/DimacsLexer.java

@@ -0,0 +1,15 @@
+package me.paultristanwagner.satchecking.parse;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.IDENTIFIER;
+import static me.paultristanwagner.satchecking.parse.TokenType.INTEGER;
+
+public class DimacsLexer extends Lexer {
+
+  public DimacsLexer(String input) {
+    super(input);
+
+    registerTokenTypes(IDENTIFIER, INTEGER);
+
+    initialize(input);
+  }
+}

src/main/java/me/paultristanwagner/satchecking/parse/DimacsParser.java

@@ -0,0 +1,59 @@
+package me.paultristanwagner.satchecking.parse;
+
+import me.paultristanwagner.satchecking.sat.CNF;
+import me.paultristanwagner.satchecking.sat.Clause;
+import me.paultristanwagner.satchecking.sat.Literal;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import static me.paultristanwagner.satchecking.parse.TokenType.IDENTIFIER;
+import static me.paultristanwagner.satchecking.parse.TokenType.INTEGER;
+
+public class DimacsParser implements Parser<CNF> {
+
+  @Override
+  public ParseResult<CNF> parseWithRemaining(String string) {
+    Lexer lexer = new DimacsLexer(string);
+
+    lexer.consume(IDENTIFIER);
+
+    lexer.consume(IDENTIFIER);
+
+    lexer.require(INTEGER);
+    int variableCount = Integer.parseInt(lexer.getLookahead().getValue());
+    lexer.consume(INTEGER);
+
+    lexer.require(INTEGER);
+    int clauseCount = Integer.parseInt(lexer.getLookahead().getValue());
+    lexer.consume(INTEGER);
+
+    List<Clause> clauses = new ArrayList<>();
+    for (int i = 0; i < clauseCount; ++i) {
+      List<Literal> literals = new ArrayList<>();
+
+      while (lexer.hasNextToken()) {
+        lexer.require(INTEGER);
+        int literalId = Integer.parseInt(lexer.getLookahead().getValue());
+        lexer.consume(INTEGER);
+
+        if (literalId == 0) {
+          break;
+        }
+
+        Literal literal;
+        if (literalId >= 0) {
+          literal = new Literal("l" + literalId);
+        } else {
+          literal = new Literal("l" + -literalId, true);
+        }
+
+        literals.add(literal);
+      }
+
+      clauses.add(new Clause(literals));
+    }
+
+    return new ParseResult<>(new CNF(clauses), lexer.getCursor(), lexer.getRemaining().isEmpty());
+  }
+}