Commit b44624c5 authored by Sarah Grebing's avatar Sarah Grebing

Added new key jars with bugfix for matcher

parent e0deb8e1
Pipeline #20949 failed with stages
in 0 seconds
...@@ -60,6 +60,8 @@ public class KeyMatcherFacadeTest { ...@@ -60,6 +60,8 @@ public class KeyMatcherFacadeTest {
public void matchSeq() throws Exception { public void matchSeq() throws Exception {
//atm missing is catching the toplevel formula //atm missing is catching the toplevel formula
//shouldMatch("==> pred(a)", "==> pred(?)", "[]"); //shouldMatch("==> pred(a)", "==> pred(?)", "[]");
shouldMatch("p, q ==> !p, !q", "==> ?Z", "[{?Z=not(p)}, {?Z=not(q)}]");
shouldMatch("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]"); shouldMatch("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]");
...@@ -106,7 +108,7 @@ public class KeyMatcherFacadeTest { ...@@ -106,7 +108,7 @@ public class KeyMatcherFacadeTest {
@Test @Test
public void testQuantMatch() throws Exception { public void testQuantMatch() throws Exception {
shouldMatchT("fint2(1,i)", "fint2(1,i)"); shouldMatchT("fint2(1,i)", "fint2(1,i)", "[{}]");
shouldMatch("\\exists int i, int j; fint2(j,i) ==> ", "(\\exists ?Y, ?X; ?Term) ==> ", "[{?Term=fint2(j,i), ?X=j:int, ?Y=i:int}]"); shouldMatch("\\exists int i, int j; fint2(j,i) ==> ", "(\\exists ?Y, ?X; ?Term) ==> ", "[{?Term=fint2(j,i), ?X=j:int, ?Y=i:int}]");
......
...@@ -26,7 +26,7 @@ impRight; ...@@ -26,7 +26,7 @@ impRight;
impRight; impRight;
impLeft; impLeft;
cases{ cases{
case match `==> not(?Z), ?Z`: case match `==> !(?Z), ?Z`:
notRight; notRight;
default: default:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment