Added test for Modulo Translation

Author: BookWood7th

key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTMod.java

@@ -0,0 +1,79 @@
+package de.uka.ilkd.key.smt;
+
+import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.smt.solvertypes.SolverType;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+import org.junit.Test;
+import org.key_project.util.helper.FindResources;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.io.File;
+
+/**
+ * This class is for testing the translation of modulo from KeY to SMT
+ * @author Nils Buchholz, 2024
+ */
+public class TestSMTMod {
+
+    private static final Logger LOGGER = LoggerFactory.getLogger(TestSMTMod.class);
+
+    private static final File testCaseDirectory = FindResources.getTestCasesDirectory();
+
+    private static final SolverType Z3_SOLVER = SolverTypes.getSolverTypes().stream()
+            .filter(it -> it.getClass().equals(SolverTypeImplementation.class)
+                    && it.getName().equals("Z3"))
+            .findFirst().orElse(null);
+
+    private static final SolverType CVC4_SOLVER = SolverTypes.getSolverTypes().stream()
+            .filter(it -> it.getClass().equals(SolverTypeImplementation.class)
+                    && it.getName().equals("CVC4"))
+            .findFirst().orElse(null);
+
+    /**
+     * This tests if x mod y is non-negative and x mod y < |y| for y != 0
+     * thus satisfying the definition of euclidean modulo
+     * @throws ProblemLoaderException Occured Exception during load of problem file
+     */
+    @Test
+    public void testModSpec() throws ProblemLoaderException {
+        KeYEnvironment<DefaultUserInterfaceControl> env =
+                KeYEnvironment.load(new File(testCaseDirectory, "smt/modSpec.key"));
+        try {
+            Proof proof = env.getLoadedProof();
+            assertNotNull(proof);
+            assertEquals(1, proof.openGoals().size());
+            Goal g = proof.openGoals().iterator().next();
+            SMTSolverResult result;
+            if (Z3_SOLVER.isInstalled(true)) {
+                result = checkGoal(g, Z3_SOLVER);
+                assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid());
+            } else {
+                LOGGER.warn("Warning:Z3 solver not installed, tests skipped.");
+            }
+            if (CVC4_SOLVER.isInstalled(true)) {
+                result = checkGoal(g, CVC4_SOLVER);
+                assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid());
+            } else {
+                LOGGER.warn("Warning:CVC4 solver not installed, tests skipped.");
+            }
+        } finally {
+            env.dispose();
+        }
+    }
+
+    private SMTSolverResult checkGoal(Goal g, SolverType solverType) {
+        SolverLauncher launcher = new SolverLauncher(new SMTTestSettings());
+        SMTProblem problem = new SMTProblem(g);
+        launcher.launch(problem, g.proof().getServices(), solverType);
+        return problem.getFinalResult();
+    }
+}

key.core/src/test/resources/testcase/smt/modSpec.key

@@ -0,0 +1,9 @@
+\functions {
+    int y;
+    int x;
+}
+
+\problem {
+    ((y>0) -> x % y >= 0 & x % y < y) & ((y<0) -> x%y >= 0 & x % y < -y)
+}
+