Moved test files

.gitignore

@@ -14,15 +14,15 @@ target/
 .sonar/
 
 # test logs
-core/src/test/resources/maxsat/log.txt
-core/src/test/resources/partialmaxsat/log.txt
-core/src/test/resources/partialweightedmaxsat/log.txt
+test_files/maxsat/log.txt
+test_files/partialmaxsat/log.txt
+test_files/partialweightedmaxsat/log.txt
 
 # test temporary files
-core/src/test/resources/writers/temp/*.dot
-core/src/test/resources/writers/temp/*.txt
-core/src/test/resources/writers/temp/*.cnf
-core/src/test/resources/writers/temp/*.map
+test_files/writers/temp/*.dot
+test_files/writers/temp/*.txt
+test_files/writers/temp/*.cnf
+test_files/writers/temp/*.map
 
 # LSP
 .settings

core/pom.xml

@@ -207,4 +207,25 @@
       <scope>test</scope>
     </dependency>
   </dependencies>
+
+  <profiles>
+    <profile>
+      <id>parallel-tests</id>
+      <build>
+        <plugins>
+          <plugin>
+            <groupId>org.apache.maven.plugins</groupId>
+            <artifactId>maven-surefire-plugin</artifactId>
+            <configuration>
+              <argLine>-Xmx16g</argLine>
+              <systemPropertyVariables>
+                <junit.jupiter.execution.parallel.enabled>true</junit.jupiter.execution.parallel.enabled>
+                <junit.jupiter.execution.parallel.mode.default>concurrent</junit.jupiter.execution.parallel.mode.default>
+              </systemPropertyVariables>
+            </configuration>
+          </plugin>
+        </plugins>
+      </build>
+    </profile>
+  </profiles>
 </project>

core/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java

@@ -22,7 +22,6 @@
 import com.booleworks.logicng.solvers.SolverState;
 import com.booleworks.logicng.solvers.functions.BackboneFunction;
 import com.booleworks.logicng.util.FormulaHelper;
-import org.assertj.core.api.Assertions;
 import org.junit.jupiter.api.Test;
 
 import java.io.IOException;
@@ -114,78 +113,78 @@ public void testSimpleBackbones() {
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x);
         solver.loadState(before);
 
         formula = f.and(x, y);
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x, y);
         solver.loadState(before);
 
         formula = f.or(x, y);
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .isEmpty();
         solver.loadState(before);
 
         formula = x.negate(f);
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x.negate(f));
         solver.loadState(before);
 
         formula = f.or(f.and(x, y, z), f.and(x, y, u), f.and(x, u, z));
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x);
         solver.loadState(before);
 
         formula = f.and(f.or(x, y, z), f.or(x, y, u), f.or(x, u, z));
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .isEmpty();
         solver.loadState(before);
 
         formula = f.and(f.or(x.negate(f), y), x);
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x, y);
         solver.loadState(before);
 
         formula = f.and(f.or(x, y), f.or(x.negate(f), y));
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(y);
         solver.loadState(before);
 
         formula = f.and(f.and(f.or(x.negate(f), y), x.negate(f)), f.and(z, f.or(x, y)));
         before = solver.saveState();
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(x.negate(f), y, z);
         solver.loadState(before);
 
         formula = f.and(f.or(x, y), f.or(u, v), z);
         solver.add(formula);
         assertThat(
-                        solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
+                solver.execute(BackboneFunction.builder().variables(variables).build()).getCompleteBackbone(f))
                 .containsExactly(z);
     }
 
@@ -194,7 +193,7 @@ public void testSimpleBackbones() {
     public void testSmallFormulas() throws IOException, ParserException {
         final FormulaFactory f = FormulaFactory.caching();
         final Formula formula =
-                FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt");
+                FormulaReader.readFormula(f, "../test_files/formulas/small_formulas.txt");
         final SATSolver solver = SATSolver.newSolver(f);
         solver.add(formula);
         final Backbone backbone = solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build());
@@ -205,7 +204,7 @@ public void testSmallFormulas() throws IOException, ParserException {
     public void testLargeFormula() throws IOException, ParserException {
         final FormulaFactory f = FormulaFactory.caching();
         final Formula formula =
-                FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt");
+                FormulaReader.readFormula(f, "../test_files/formulas/large_formula.txt");
         final SATSolver solver = SATSolver.newSolver(f);
         solver.add(formula);
         final Backbone backbone = solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build());
@@ -321,7 +320,7 @@ public void testBackboneType() {
 
     @Test
     public void testCancellationPoints() throws IOException {
-        final List<Formula> formulas = DimacsReader.readCNF(f, "src/test/resources/sat/term1_gr_rcs_w4.shuffled.cnf");
+        final List<Formula> formulas = DimacsReader.readCNF(f, "../test_files/sat/term1_gr_rcs_w4.shuffled.cnf");
         for (int numStarts = 0; numStarts < 10; numStarts++) {
             final ComputationHandler handler = new BoundedSatHandler(numStarts);
             final LNGResult<Backbone> result = BackboneGeneration.compute(f, formulas, FormulaHelper.variables(f, formulas),

core/src/test/java/com/booleworks/logicng/explanations/drup/DRUPTest.java

@@ -21,7 +21,6 @@
 import com.booleworks.logicng.solvers.SolverState;
 import com.booleworks.logicng.solvers.sat.SATCall;
 import com.booleworks.logicng.solvers.sat.SATSolverConfig;
-import org.assertj.core.api.Assertions;
 import org.assertj.core.api.SoftAssertions;
 import org.junit.jupiter.api.Test;
 
@@ -42,9 +41,9 @@ public class DRUPTest implements LogicNGTest {
     @LongRunningTag
     public void testUnsatCoresFromDimacs() throws IOException {
         final List<List<Formula>> cnfs = new ArrayList<>(3);
-        cnfs.add(DimacsReader.readCNF(f, "src/test/resources/drup/simple_input.cnf"));
-        cnfs.add(DimacsReader.readCNF(f, "src/test/resources/drup/pg4_input.cnf"));
-        cnfs.add(DimacsReader.readCNF(f, "src/test/resources/drup/avg_input.cnf", "var"));
+        cnfs.add(DimacsReader.readCNF(f, "../test_files/drup/simple_input.cnf"));
+        cnfs.add(DimacsReader.readCNF(f, "../test_files/drup/pg4_input.cnf"));
+        cnfs.add(DimacsReader.readCNF(f, "../test_files/drup/avg_input.cnf", "var"));
 
         for (final List<Formula> cnf : cnfs) {
             final SATSolver solver = solverSupplier.get();
@@ -58,7 +57,7 @@ public void testUnsatCoresFromDimacs() throws IOException {
     @Test
     @LongRunningTag
     public void testUnsatCoresFromLargeTestset() throws IOException {
-        final File testFolder = new File("src/test/resources/sat");
+        final File testFolder = new File("../test_files/sat");
         final File[] files = testFolder.listFiles();
         assert files != null;
         int count = 0;
@@ -80,7 +79,7 @@ public void testUnsatCoresFromLargeTestset() throws IOException {
 
     @Test
     public void testUnsatCoresAimTestset() throws IOException {
-        final File testFolder = new File("src/test/resources/sat/unsat");
+        final File testFolder = new File("../test_files/sat/unsat");
         final File[] files = testFolder.listFiles();
         assert files != null;
         int count = 0;

core/src/test/java/com/booleworks/logicng/explanations/mus/MUSGenerationTest.java

@@ -51,10 +51,10 @@ public MUSGenerationTest() throws IOException {
         pg5 = generatePGPropositions(5);
         pg6 = generatePGPropositions(6);
         pg7 = generatePGPropositions(7);
-        file1 = readDimacs("src/test/resources/sat/3col40_5_10.shuffled.cnf");
-        file2 = readDimacs("src/test/resources/sat/x1_16.shuffled.cnf");
-        file3 = readDimacs("src/test/resources/sat/grid_10_20.shuffled.cnf");
-        file4 = readDimacs("src/test/resources/sat/ca032.shuffled.cnf");
+        file1 = readDimacs("../test_files/sat/3col40_5_10.shuffled.cnf");
+        file2 = readDimacs("../test_files/sat/x1_16.shuffled.cnf");
+        file3 = readDimacs("../test_files/sat/grid_10_20.shuffled.cnf");
+        file4 = readDimacs("../test_files/sat/ca032.shuffled.cnf");
     }
 
     @Test
@@ -126,7 +126,7 @@ public void testPlainInsertionBasedMUS() {
     public void testDeletionBasedCancellationPoints() throws IOException {
         final MUSGeneration mus = new MUSGeneration();
         final List<StandardProposition> propositions =
-                DimacsReader.readCNF(f, "src/test/resources/sat/too_large_gr_rcs_w5.shuffled.cnf").stream()
+                DimacsReader.readCNF(f, "../test_files/sat/too_large_gr_rcs_w5.shuffled.cnf").stream()
                         .map(StandardProposition::new)
                         .collect(Collectors.toList());
         for (int numStarts = 0; numStarts < 20; numStarts++) {
@@ -141,7 +141,7 @@ public void testDeletionBasedCancellationPoints() throws IOException {
     public void testCancellationPoints() throws IOException {
         final MUSGeneration mus = new MUSGeneration();
         final List<StandardProposition> propositions =
-                DimacsReader.readCNF(f, "src/test/resources/sat/unsat/bf0432-007.cnf").stream()
+                DimacsReader.readCNF(f, "../test_files/sat/unsat/bf0432-007.cnf").stream()
                         .map(StandardProposition::new)
                         .collect(Collectors.toList());
         final List<MUSConfig.Algorithm> algorithms =

core/src/test/java/com/booleworks/logicng/explanations/smus/SmusComputationTest.java

@@ -230,7 +230,7 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException {
                 new TimeoutHandler(System.currentTimeMillis() + 1L, FIXED_END)
         );
         final Formula formula =
-                FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt");
+                FormulaReader.readFormula(f, "../test_files/formulas/large_formula.txt");
         final List<Formula> formulas = formula.stream().collect(Collectors.toList());
         for (final TimeoutHandler handler : handlers) {
             testHandler(handler, formulas, true);
@@ -240,7 +240,7 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException {
     @Test
     @LongRunningTag
     public void testCancellationPoints() throws IOException {
-        final List<Formula> formulas = DimacsReader.readCNF(f, "src/test/resources/sat/unsat/bf0432-007.cnf");
+        final List<Formula> formulas = DimacsReader.readCNF(f, "../test_files/sat/unsat/bf0432-007.cnf");
         for (int numOptimizationStarts = 1; numOptimizationStarts < 5; numOptimizationStarts++) {
             for (int numSatHandlerStarts = 1; numSatHandlerStarts < 10; numSatHandlerStarts++) {
                 final ComputationHandler handler =

core/src/test/java/com/booleworks/logicng/functions/MinimumPrimeImplicantTest.java

@@ -83,15 +83,16 @@ public void testSmallExamples() throws ParserException {
         isPrimeImplicant(formula, pi);
 
         formula = f.parse(
-                "v173 + v174 + v451 + v258 + v317 + v259 + v452 + v453 + v175 + v176 + v177 + v178 + v179 + v180 + v181 + v182 + v183 + v102 + v103 + v104 + v105 = 1");
+                "v173 + v174 + v451 + v258 + v317 + v259 + v452 + v453 + v175 + v176 + v177 + v178 + v179 + v180 + v181 + v182 + v183 + v102 + v103 + v104 + " +
+                        "v105 = 1");
         pi = formula.apply(new MinimumPrimeImplicantFunction(f));
         assertThat(pi).hasSize(21);
         isPrimeImplicant(formula, pi);
     }
 
     @Test
     public void testMiddleExamples() throws IOException, ParserException {
-        final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt");
+        final Formula parsed = FormulaReader.readFormula(f, "../test_files/formulas/formula1.txt");
         for (final Formula formula : parsed) {
             isPrimeImplicant(formula, formula.apply(new MinimumPrimeImplicantFunction(f)));
         }
@@ -100,7 +101,7 @@ public void testMiddleExamples() throws IOException, ParserException {
     @Test
     public void testLargeExamples() throws IOException, ParserException {
         final Formula parsed =
-                FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt");
+                FormulaReader.readFormula(f, "../test_files/formulas/small_formulas.txt");
         for (final Formula formula : parsed) {
             isPrimeImplicant(formula, formula.apply(new MinimumPrimeImplicantFunction(f)));
         }

core/src/test/java/com/booleworks/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java

@@ -100,7 +100,7 @@ public void graph50Test() throws IOException {
     public void testFormulaSplit() throws IOException, ParserException {
         final FormulaFactory f = FormulaFactory.caching();
         f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build());
-        final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt");
+        final Formula parsed = FormulaReader.readFormula(f, "../test_files/formulas/formula1.txt");
         final List<Formula> formulas = new ArrayList<>();
         final List<Formula> originalFormulas = new ArrayList<>();
         for (final Formula formula : parsed) {

core/src/test/java/com/booleworks/logicng/graphs/datastructures/GraphTest.java

@@ -22,7 +22,7 @@ public static Graph<Long> getLongGraph(final String id) throws IOException {
         final Graph<Long> g = new Graph<>(id + "-Long");
 
         final BufferedReader reader =
-                new BufferedReader(new FileReader("src/test/resources/graphs/graph" + id + ".txt"));
+                new BufferedReader(new FileReader("../test_files/graphs/graph" + id + ".txt"));
 
         while (reader.ready()) {
             final String line = reader.readLine().trim();

core/src/test/java/com/booleworks/logicng/graphs/generators/ConstraintGraphGeneratorTest.java

@@ -86,18 +86,18 @@ public void testCnf() throws ParserException {
         expected.connect(d, a);
         expected.connect(d, e);
         assertThat(ConstraintGraphGenerator.generateFromFormulas(f,
-                        p.parse("a | ~b | c"),
-                        p.parse("d | ~a"),
-                        p.parse("d + e = 1"),
-                        p.parse("g")).toString())
+                p.parse("a | ~b | c"),
+                p.parse("d | ~a"),
+                p.parse("d + e = 1"),
+                p.parse("g")).toString())
                 .isEqualTo(expected.toString());
     }
 
     @Test
     public void testRealExample() throws IOException, ParserException {
         final FormulaFactory f = FormulaFactory.caching();
         f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build());
-        final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt");
+        final Formula parsed = FormulaReader.readFormula(f, "../test_files/formulas/formula1.txt");
         final List<Formula> formulas = new ArrayList<>();
         for (final Formula formula : parsed) {
             if (formula instanceof PBConstraint) {

core/src/test/java/com/booleworks/logicng/graphs/io/GraphDimacsFileWriterTest.java

@@ -48,14 +48,14 @@ public void test50p1() throws IOException {
     }
 
     private <T> void testFiles(final String fileName, final Graph<T> g) throws IOException {
-        GraphDimacsFileWriter.write("src/test/resources/graphs/io/temp/" + fileName + "_t.col", g, true);
-        GraphDimacsFileWriter.write("src/test/resources/graphs/io/temp/" + fileName + "_f", g, false);
-        final File expectedT = new File("src/test/resources/graphs/io/graphs-dimacs/" + fileName + "_t.col");
-        final File expectedF = new File("src/test/resources/graphs/io/graphs-dimacs/" + fileName + "_f.col");
-        final File tempT = new File("src/test/resources/graphs/io/temp/" + fileName + "_t.col");
-        final File tempF = new File("src/test/resources/graphs/io/temp/" + fileName + "_f.col");
-        final File expectedMap = new File("src/test/resources/graphs/io/graphs-dimacs/" + fileName + "_t.map");
-        final File tempMap = new File("src/test/resources/graphs/io/temp/" + fileName + "_t.map");
+        GraphDimacsFileWriter.write("../test_files/graphs/io/temp/" + fileName + "_t.col", g, true);
+        GraphDimacsFileWriter.write("../test_files/graphs/io/temp/" + fileName + "_f", g, false);
+        final File expectedT = new File("../test_files/graphs/io/graphs-dimacs/" + fileName + "_t.col");
+        final File expectedF = new File("../test_files/graphs/io/graphs-dimacs/" + fileName + "_f.col");
+        final File tempT = new File("../test_files/graphs/io/temp/" + fileName + "_t.col");
+        final File tempF = new File("../test_files/graphs/io/temp/" + fileName + "_f.col");
+        final File expectedMap = new File("../test_files/graphs/io/graphs-dimacs/" + fileName + "_t.map");
+        final File tempMap = new File("../test_files/graphs/io/temp/" + fileName + "_t.map");
         assertFilesEqual(expectedT, tempT);
         assertFilesEqual(expectedF, tempF);
         assertMapFilesEqual(expectedMap, tempMap);

core/src/test/java/com/booleworks/logicng/handlers/TimeoutMaxSATHandlerTest.java

@@ -91,7 +91,7 @@ public void testThatMethodsAreCalled() throws ParserException {
     @Test
     public void testTimeoutHandlerSingleTimeout() throws IOException {
         final List<Formula> formulas =
-                DimacsReader.readCNF(f, "src/test/resources/sat/too_large_gr_rcs_w5.shuffled.cnf");
+                DimacsReader.readCNF(f, "../test_files/sat/too_large_gr_rcs_w5.shuffled.cnf");
         for (final MaxSATSolver solver : solvers) {
             final int weight = solver.isWeighted() ? 2 : 1;
             formulas.forEach(c -> solver.addSoftFormula(c, weight));