Skip to content

Commit

Permalink
factored out parser code to its own module
Browse files Browse the repository at this point in the history
  • Loading branch information
@SHildebrandt
SHildebrandt committed Apr 24, 2024
1 parent 9fe3158 commit f69af01
Show file tree
Hide file tree
Showing 71 changed files with 1,505 additions and 1,161 deletions.
100 changes: 80 additions & 20 deletions core/pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,24 +46,6 @@
</resources>

<plugins>
<!-- ANTLR4 (Parser Generation) -->
<plugin>
<groupId>org.antlr</groupId>
<artifactId>antlr4-maven-plugin</artifactId>
<version>${version.antlr-plugin}</version>
<configuration>
<sourceDirectory>src/main/antlr</sourceDirectory>
<outputDirectory>target/generated-sources/antlr/org/logicng/io/parsers</outputDirectory>
</configuration>
<executions>
<execution>
<goals>
<goal>antlr4</goal>
</goals>
</execution>
</executions>
</plugin>

<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
Expand Down Expand Up @@ -197,18 +179,96 @@
<argLine>-Xmx2g</argLine>
</configuration>
</plugin>

<!-- ANTLR4 for Tests (Parser Generation) -->
<plugin>
<groupId>org.antlr</groupId>
<artifactId>antlr4-maven-plugin</artifactId>
<version>${version.antlr-plugin}</version>
<configuration>
<sourceDirectory>../parser/src/main/antlr</sourceDirectory>
<outputDirectory>target/generated-test-sources/antlr/org/logicng/io/parsers</outputDirectory>
</configuration>
<executions>
<execution>
<phase>generate-test-sources</phase>
<goals>
<goal>antlr4</goal>
</goals>
</execution>
</executions>
</plugin>

<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-resources-plugin</artifactId>
<version>${version.resources-plugin}</version>
<executions>
<execution>
<id>copy-parser-classes</id>
<phase>process-test-sources</phase>
<goals>
<goal>copy-resources</goal>
</goals>
<configuration>
<outputDirectory>target/generated-test-sources/antlr/org/logicng/io/parsers</outputDirectory>
<resources>
<resource>
<directory>../parser/src/main/java/org/logicng/io/parsers</directory>
<filtering>false</filtering>
</resource>
</resources>
</configuration>
</execution>
<execution>
<id>copy-reader-classes</id>
<phase>process-test-sources</phase>
<goals>
<goal>copy-resources</goal>
</goals>
<configuration>
<outputDirectory>target/generated-test-sources/antlr/org/logicng/io/readers</outputDirectory>
<resources>
<resource>
<directory>../parser/src/main/java/org/logicng/io/readers</directory>
<filtering>false</filtering>
</resource>
</resources>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.codehaus.mojo</groupId>
<artifactId>build-helper-maven-plugin</artifactId>
<version>${version.build-helper-plugin}</version>
<executions>
<execution>
<id>add-parser-sources</id>
<phase>generate-test-sources</phase>
<goals>
<goal>add-test-source</goal>
</goals>
<configuration>
<sources>
<source>target/generated-test-sources/antlr</source>
</sources>
</configuration>
</execution>
</executions>
</plugin>
</plugins>
</build>

<dependencies>
<!-- Parser -->
<!-- Testing -->
<dependency>
<groupId>org.antlr</groupId>
<artifactId>antlr4-runtime</artifactId>
<version>${version.antlr}</version>
<scope>test</scope>
</dependency>

<!-- Testing -->
<dependency>
<groupId>org.junit.jupiter</groupId>
<artifactId>junit-jupiter</artifactId>
Expand Down
14 changes: 0 additions & 14 deletions core/src/main/java/org/logicng/formulas/FormulaFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,6 @@
import org.logicng.formulas.cache.CacheEntry;
import org.logicng.formulas.printer.FormulaStringRepresentation;
import org.logicng.functions.SubNodeFunction;
import org.logicng.io.parsers.ParserException;
import org.logicng.io.parsers.PseudoBooleanParser;
import org.logicng.pseudobooleans.PBConfig;
import org.logicng.pseudobooleans.PBEncoder;
import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
Expand Down Expand Up @@ -103,7 +101,6 @@ public class FormulaFactory {
private final SubNodeFunction subformulaFunction;
private final PBEncoder pbEncoder;
private final CNFEncoder cnfEncoder;
private final PseudoBooleanParser parser;
Map<String, Variable> posLiterals;
Map<String, Literal> negLiterals;
Set<Variable> generatedVariables;
Expand Down Expand Up @@ -155,7 +152,6 @@ public FormulaFactory(final FormulaFactoryConfig config) {
this.cnfPrefix = CNF_PREFIX;
}
this.pbEncoder = new PBEncoder(this);
this.parser = new PseudoBooleanParser(this);
}

/**
Expand Down Expand Up @@ -1400,16 +1396,6 @@ public long numberOfNodes(final Formula formula) {
return formula.apply(this.subformulaFunction).size();
}

/**
* Parses a given string to a formula using a pseudo boolean parser.
* @param string a string representing the formula
* @return the formula
* @throws ParserException if the parser throws an exception
*/
public Formula parse(final String string) throws ParserException {
return this.parser.parse(string);
}

/**
* Adds a given formula to a list of operands. If the formula is the neutral element for the respective n-ary
* operation it will be skipped. If a complementary formula is already present in the list of operands or the
Expand Down
10 changes: 10 additions & 0 deletions core/src/test/java/org/logicng/TestWithExampleFormulas.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Literal;
import org.logicng.formulas.Variable;
import org.logicng.io.parsers.ParserException;
import org.logicng.io.parsers.PseudoBooleanParser;

public abstract class TestWithExampleFormulas {
protected final FormulaFactory f = new FormulaFactory();
Expand Down Expand Up @@ -89,4 +91,12 @@ public abstract class TestWithExampleFormulas {
protected final Formula PBC3 = this.f.pbc(CType.GE, 2, this.literals, this.coefficients);
protected final Formula PBC4 = this.f.pbc(CType.LT, 2, this.literals, this.coefficients);
protected final Formula PBC5 = this.f.pbc(CType.LE, 2, this.literals, this.coefficients);

public static Formula parse(final FormulaFactory f, final String formula) {
try {
return new PseudoBooleanParser(f).parse(formula);
} catch (final ParserException e) {
throw new RuntimeException(e);
}
}
}
8 changes: 4 additions & 4 deletions core/src/test/java/org/logicng/datastructures/AssignmentTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -207,22 +207,22 @@ public void testEquals() {
}

@Test
public void testBlockingClause() throws ParserException {
public void testBlockingClause() {
final Assignment ass = new Assignment();
ass.addLiteral(this.A);
ass.addLiteral(this.B);
ass.addLiteral(this.NX);
ass.addLiteral(this.NY);
final Formula bc01 = ass.blockingClause(this.f);
assertThat(bc01.containsVariable(this.C)).isFalse();
assertThat(bc01).isEqualTo(this.f.parse("~a | ~b | x | y"));
assertThat(bc01).isEqualTo(parse(this.f, "~a | ~b | x | y"));
final Formula bc02 = ass.blockingClause(this.f, null);
assertThat(bc02.containsVariable(this.C)).isFalse();
assertThat(bc02).isEqualTo(this.f.parse("~a | ~b | x | y"));
assertThat(bc02).isEqualTo(parse(this.f, "~a | ~b | x | y"));
final List<Literal> lits = Arrays.asList(this.A, this.X, this.C);
final Formula bcProjected = ass.blockingClause(this.f, lits);
assertThat(bcProjected.containsVariable(this.C)).isFalse();
assertThat(bcProjected).isEqualTo(this.f.parse("~a | x"));
assertThat(bcProjected).isEqualTo(parse(this.f, "~a | x"));
}

@Test
Expand Down
Loading

0 comments on commit f69af01

Please sign in to comment.