✅ Added missing tests

.github/workflows/classroom.yml

@@ -18,9 +18,6 @@ jobs:
         with:
           fetch-depth: 0
 
-      - name: Execute tests
-        run: curl -s https://gist.githubusercontent.com/soaibsafi/7aef43113171637395e8b4e900f5cc76/raw/4d5aa54850ab1145ebcc6afc5af02eb5b22e301f/smtsolving_tests.sh | bash -s
-
       - name: Set up Java 17
         uses: actions/setup-java@v3
         with:

src/test/java/de/buw/fm4se/smtsolving/tests/T1WhoKilledAgathaTest.java

@@ -0,0 +1,67 @@
+package de.buw.fm4se.smtsolving.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import org.junit.jupiter.api.Test;
+
+import de.buw.fm4se.smtsolving.Tasks;
+import de.buw.fm4se.smtsolving.utils.FmPlay;
+import de.buw.fm4se.smtsolving.utils.Z3Utils;
+
+public class T1WhoKilledAgathaTest {
+
+  String code = FmPlay.getCodeFromPermalink(Tasks.task_1);
+
+  @Test
+  void testCheckFormula1() {
+    String constraints = "(assert (not (exists ((x Person)) (killed x Agatha))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 1 is wrong");
+  }
+
+  @Test
+  void testCheckFormula2() {
+    String c1 = "(assert (not (forall ((x Person) (y Person))(=> (killed x y) (hates x y)))))";
+    String c2 = "(assert (not (forall ((x Person) (y Person))(=> (killed x y) (not (richer x y))))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, c1), "Encoding of formula 2 is wrong");
+    assertTrue(Z3Utils.isUnsatForConstraints(code, c2), "Encoding of formula 2 is wrong");
+  }
+
+  @Test
+  void testCheckFormula3() {
+    String c1 = "(assert (not (forall ((x Person))(=> (hates Agatha x) (not (hates Charles x))))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, c1), "Encoding of formula 3 is wrong");
+  }
+
+  @Test
+  void testCheckFormula4() {
+    String c1 = "(assert (not (hates Agatha Agatha)))";
+    String c2 = "(assert (not (hates Agatha Charles)))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, c1), "Encoding of formula 4 is wrong");
+    assertTrue(Z3Utils.isUnsatForConstraints(code, c2), "Encoding of formula 4 is wrong");
+  }
+
+  @Test
+  void testCheckFormula5() {
+    String constraints = "(assert (not (forall ((x Person))(=> (not (richer x Agatha)) (hates Butler x)))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 5 is wrong");
+  }
+
+  @Test
+  void testCheckFormula6() {
+    String constraints = "(assert (not (forall ((x Person))(=> (hates Agatha x) (hates Butler x)))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 6 is wrong");
+  }
+
+  @Test
+  void testCheckFormula7() {
+    String constraints = "(assert (not (forall ((x Person)) (exists ((y Person)) (not (hates x y))))))";
+    assertTrue(Z3Utils.isUnsatForConstraints(code, constraints), "Encoding of formula 7 is wrong");
+  }
+
+  @Test
+  void testCheckConclusion() {
+    String constraints = "(assert (killed Agatha Agatha))";
+    assertFalse(Z3Utils.isUnsatForConstraints(code, constraints), "Conclusion is wrong");
+  }
+
+}

src/test/java/de/buw/fm4se/smtsolving/tests/T2MathPuzzleTest.java

@@ -0,0 +1,61 @@
+package de.buw.fm4se.smtsolving.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import com.microsoft.z3.Z3Exception;
+
+import de.buw.fm4se.smtsolving.Tasks;
+import de.buw.fm4se.smtsolving.utils.FmPlay;
+import de.buw.fm4se.smtsolving.utils.PuzzleTest;
+import de.buw.fm4se.smtsolving.utils.Z3Utils;
+
+public class T2MathPuzzleTest {
+
+  String code = FmPlay.getCodeFromPermalink(Tasks.task_2);
+  String puzzle = PuzzleTest.readPuzzleFromMd();
+  List<String> mdPuzzle = PuzzleTest.convertEmoji(puzzle);
+  List<String> smt = PuzzleTest.generateSmtAssert(puzzle);
+
+  @Test
+  void testCheckFormula1() {
+    testCheckFormula(0);
+  }
+
+  @Test
+  void testCheckFormula2() {
+    testCheckFormula(1);
+  }
+
+  @Test
+  void testCheckFormula3() {
+    testCheckFormula(2);
+  }
+
+  @Test
+  void testCheckFormula4() {
+    testCheckFormula(3);
+  }
+
+  private void testCheckFormula(int i) {
+    String message = String.format("Encoding of formula %s is wrong", mdPuzzle.get(i));
+    try {
+      assertTrue(Z3Utils.isUnsatForConstraints(code, smt.get(i)), message);
+    } catch (Z3Exception e) {
+      fail(message);
+    }
+  }
+
+  @Test
+  void testCheckConclusion() {
+    try {
+      assertFalse(Z3Utils.isUnsatForConstraints(code, ""), "The puzzle has no solution");      
+    } catch (Z3Exception e) {
+      fail("The encoding of the puzzle likely contains a syntax error");
+    }
+  }
+
+}

src/test/java/de/buw/fm4se/smtsolving/tests/T3PcConfigurationTest.java

@@ -0,0 +1,77 @@
+package de.buw.fm4se.smtsolving.tests;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import org.junit.jupiter.api.Test;
+
+import de.buw.fm4se.smtsolving.Tasks;
+import de.buw.fm4se.smtsolving.utils.FmPlay;
+import de.buw.fm4se.smtsolving.utils.Z3Utils;
+
+public class T3PcConfigurationTest {
+  // Office: 283
+  // Server: 307
+  // Gaming: 1006
+  // Video: 318
+
+  String code = FmPlay.getCodeFromPermalink(Tasks.task_3);
+
+  @Test
+  void testPurposeOffice1(){
+    assertFalse(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose office))\n(assert (= budget 283))"),
+              "For office purpose, €283 is enough, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeOffice2(){
+    assertTrue(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose office))\n(assert (= budget 282))"),
+              "For office purpose, the budget should be at least €283, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeServer1(){
+    assertFalse(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose server))\n(assert (= budget 307))"),
+              "For server purpose, €307 is enough, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeServer2(){
+    assertTrue(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose server))\n(assert (= budget 306))"),
+              "For server purpose, the budget should be at least €307, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeGaming1(){
+    assertFalse(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose gaming))\n(assert (= budget 1006))"),
+              "For gaming purpose, €1006 is enough, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeGaming2(){
+    assertTrue(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose gaming))\n(assert (= budget 1005))"),
+              "For gaming purpose, the budget should be at least €1006, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeVideoEditing1(){
+    assertFalse(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose video))\n(assert (= budget 318))"),
+              "For video editing purpose, €318 is enough, Check `(get-value (budget))`");
+  }
+
+  @Test
+  void testPurposeVideoEditing2(){
+    assertTrue(Z3Utils.isUnsatForConstraints(code, 
+              "(assert (= purpose video))\n(assert (= budget 317))"),
+              "For video editing purpose, the budget should be at least €318, Check `(get-value (budget))`");
+  }
+
+
+
+}

src/test/java/de/buw/fm4se/smtsolving/utils/FmPlay.java

@@ -0,0 +1,55 @@
+package de.buw.fm4se.smtsolving.utils;
+import java.net.HttpURLConnection;
+import java.net.URL;
+import java.io.BufferedReader;
+import java.io.InputStreamReader;
+import org.json.JSONObject;
+
+public class FmPlay {
+    public static void main(String[] args) {
+        String plink = "https://play.formal-methods.net/?check=SMT&p=ex-3-task-3";
+        System.out.println(getCodeFromPermalink(plink));
+    }
+
+    /*
+     * Returns the code from a permalink of FM playground
+     * 
+     * @param plink permalink
+     * 
+     * @return code of if the permalink is valid, otherwise "error"
+     */
+    public static String getCodeFromPermalink(String plink) {
+      String[] parts = plink.split("\\?");
+      if (parts.length < 2) {
+        return "error";
+      }
+      String apiurl = parts[0]+"api/permalink/?"+parts[1];
+        try {
+            // Create URL object
+            URL url = new URL(apiurl);
+
+            // Open a connection
+            HttpURLConnection con = (HttpURLConnection) url.openConnection();
+
+            // Set the request method
+            con.setRequestMethod("GET");
+
+            // Read the response
+            BufferedReader in = new BufferedReader(new InputStreamReader(con.getInputStream()));
+            String inputLine;
+            StringBuilder content = new StringBuilder();
+            while ((inputLine = in.readLine()) != null) {
+                content.append(inputLine);
+            }
+            in.close();
+
+            JSONObject jsonResponse = new JSONObject(content.toString());
+            String codeContent = jsonResponse.getString("code");
+            return codeContent;
+
+        } catch (Exception e) {
+            e.printStackTrace();
+        }
+        return "error";
+    }
+}