Modfied handling of quantifiablevariables

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java

@@ -106,7 +106,35 @@ public class MutableMatchings implements Matchings {
 
         for (String s1 : newMatch.keySet()) {
             if (h2.containsKey(s1)) {
-                if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable &&
+                if(h2.get(s1) instanceof  MatchPath.MPQuantifiableVariable){
+                    QuantifiableVariable qvH2 = (QuantifiableVariable) h2.get(s1).getUnit();
+                    QuantifiableVariable qvH1 = (QuantifiableVariable) ((Term) h1.get(s1).getUnit()).op();
+                    System.out.println("qvH1 = " + qvH1);
+                    System.out.println("qvH2 = " + qvH2);
+                    if(!qvH2.equals(qvH1)){
+                        return null;
+                    } else {
+                        h2.put(s1, h1.get(s1));
+
+                    }
+
+                }
+
+                if(h1.get(s1) instanceof  MatchPath.MPQuantifiableVariable){
+                    QuantifiableVariable qvH1 = (QuantifiableVariable) h1.get(s1).getUnit();
+                    QuantifiableVariable qvH2 = (QuantifiableVariable) ((Term) h2.get(s1).getUnit()).op();
+                    System.out.println("qvH1 = " + qvH1);
+                    System.out.println("qvH2 = " + qvH2);
+
+                    if(!qvH1.equals(qvH2)){
+                        return null;
+                    } else {
+                        h1.put(s1, h2.get(s1));
+
+                    }
+
+                }
+              /*  if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable &&
                         !((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) {
                     return null;
                 }
@@ -115,9 +143,10 @@ public class MutableMatchings implements Matchings {
                     return null;
                 }
 
-                if (!h2.get(s1).equals(h1.get(s1))) {
+               if (!h2.get(s1).equals(h1.get(s1))) {
+                    //h2.get(s1).unit.equals(((Term) h1.get(s1).unit).op())
                     return null;
-                }
+                }*/
             }
         }
         newMatch.putAll(h2);

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java

@@ -107,6 +107,8 @@ public class KeyMatcherFacadeTest {
 
     @Test
     public void testQuantMatch() throws Exception {
+       // shouldMatch("\\forall int x; fint2(1,x) ==>", "\\forall ?X; fint2(1,?X)", "[{?X=x}]");
+        shouldMatch("\\forall int x; fint2(1,x) ==>", "\\forall ?X; ?", "[{?X=x}]");
 
         shouldMatchT("fint2(1,i)", "fint2(1,i)", "[{}]");
 
@@ -117,7 +119,7 @@ public class KeyMatcherFacadeTest {
 
         shouldMatch("\\exists int j; fint2(j,i) ==>", "(\\exists int j; ?X)==>", "[{?X=fint2(j,i)}]");
 
-        shouldMatch("\\forall int i; \\exists int j; fint2(j,i) ==>", "(\\forall int i; (\\exists int j; fint2(i,j)))==>", "[{}]");
+        shouldMatch("\\forall int i; \\exists int j; fint2(j,i) ==>", "(\\forall int i; (\\exists int j; fint2(i,j)))==>", "{NOMATCH}");
 
     }