Added BFS and SAT tests to MddCheckerTest

RipplB · Jul 12, 2024 · 3a80d94 · 3a80d94
1 parent 23cbb78
commit 3a80d94
Showing 1 changed file with 16 additions and 2 deletions.
diff --git a/...common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java b/...common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddCheckerTest.java
@@ -125,7 +125,21 @@ public static Collection<Object[]> data() {
     }
 
     @Test
-    public void test() throws Exception {
+    public void testBfs() throws Exception {
+        testWithIterationStrategy(MddChecker.IterationStrategy.BFS);
+    }
+
+    @Test
+    public void testSat() throws Exception {
+        testWithIterationStrategy(MddChecker.IterationStrategy.SAT);
+    }
+
+    @Test
+    public void testGsat() throws Exception {
+        testWithIterationStrategy(MddChecker.IterationStrategy.GSAT);
+    }
+
+    public void testWithIterationStrategy(MddChecker.IterationStrategy iterationStrategy) throws Exception {
 
         final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP);
 
@@ -141,7 +155,7 @@ public Expr<BoolType> toExpr() {
                 public VarIndexing nextIndexing() {
                     return VarIndexingFactory.indexing(1);
                 }
-            }, propExpr, solverPool, logger);
+            }, propExpr, solverPool, logger, iterationStrategy);
             status = checker.check(null);
         }