Commit 9869029d authored by Sarah Grebing's avatar Sarah Grebing

Added auantifiablevariable handling

parent a3e2a780
Pipeline #20403 failed with stages
in 1 minute and 54 seconds
......@@ -130,63 +130,17 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
if (!toMatch.op().equals(pattern.op())) {
return NoMatch.INSTANCE;
}
// Decision: Order of bounded vars
if (toMatch.boundVars().size() != pattern.boundVars().size()) {
return NoMatch.INSTANCE;
}
Matchings mm = new MutableMatchings();
Matchings match = MutableMatchings.emptySingleton();
/* for (int i = 0; i < pattern.boundVars().size(); i++) {
QuantifiableVariable qfPattern = pattern.boundVars().get(i);
QuantifiableVariable qv = toMatch.boundVars().get(i);
if (qfPattern.getType() == MatchPatternLexer.DONTCARE) {
//match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i)));
match = reduceConform(match, EmptyMatch.INSTANCE);
continue;
}
if (qfPattern.getType() == MatchPatternLexer.SID) {
TermFactory tf = new TermFactory(new HashMap<>());
TermBuilder tb = new TermBuilder(tf, services);
Term termQVariable = tb.var(qv);
match = reduceConform(match, Matchings.singleton(qfPattern.getText(),
new MatchPath.MPTerm(peek, termQVariable, -i)));
} else {
if (!qv.name().toString().equals(qfPattern.getText())) {
return NoMatch.INSTANCE;
}
match = reduceConform(match, EmptyMatch.INSTANCE);
}
}
Matchings fromTerm = accept(ctx.skope, create(peek, 0));
Matchings retM = reduceConform(fromTerm, match);
retM.forEach(stringMatchPathMap -> {
stringMatchPathMap.forEach((s, matchPath) -> {
if (matchPath instanceof MatchPath.MPQuantifiableVariable) {
//create term from variablename and put instead into map
}
}
);
});
return handleBindClause(ctx.bindClause(), peek, retM);
/* // Decision: Order of bounded vars
Matchings mm = new MutableMatching();
if (term.getUnit().boundVars().size() != pattern.boundVars().size()) {
return NoMatch.INSTANCE;
}
Map<String, MatchPath> mPaths = new HashMap<>();
Match mPaths = new Match();
mm.add(mPaths);
for (int i = 0; i < term.getUnit().boundVars().size(); i++) {
QuantifiableVariable bv = term.getUnit().boundVars().get(i);
for (int i = 0; i < toMatch.boundVars().size(); i++) {
QuantifiableVariable bv = toMatch.boundVars().get(i);
QuantifiableVariable pv = pattern.boundVars().get(i);
if (pv instanceof MatchIdentifierOp) {
......@@ -195,16 +149,21 @@ public class KeyTermMatcher extends KeyTermBaseVisitor<Matchings, MatchPath> {
if (pv.name().toString().equalsIgnoreCase("?")) {
name = getRandomName();
} else {
name = getBindingName(pv.name());
name = pv.name().toString();
}
mPaths.put(name, term);
} else if (!pv.equals(bv)) {
MatchPath mp = new MatchPath.MPQuantifiableVariable(subject, bv, -i);
mPaths.put(name, mp);
// mPaths.put(name, subject);
} else if (!pv.name().equals(bv.name())) {
return NoMatch.INSTANCE;
}
}
return mm;*/
return null;
Term scope = toMatch.sub(0);
Matchings m = visit(pattern.sub(0), MatchPathFacade.create(subject, 0));
mm = m.reduceConform(mm);
return mm;
// return null;
}
......
......@@ -29,7 +29,12 @@ public class MutableMatchings implements Matchings {
@Override
public boolean isEmpty() {
return false;
if(!inner.isEmpty()){
return false;
} else {
return true;
}
// return false;
}
@Override
......
......@@ -89,7 +89,7 @@ public class KeyMatcherFacadeTest {
//how to deal with trying to match top-level, w.o. adding the type of the variable
shouldMatch("f(a)=0 ==> ", "(f(a)=0) : ?Y:Formula ==>", "[{?Y=equals(f(a),Z(0(#)))}]");
//shouldMatch("f(g(a))", "_ \\as ?Y", "[{?Y=f(g(a))}]");
//shouldMatch("i+i+j", "(?X + ?Y) : ?Z", "[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]");
shouldMatchT("i+i+j", "(?X + ?Y) : ?Z", "[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]");
shouldMatch("==>f(g(a))= 0", "==> f((...a...):?G) = 0", "[{?G=g(a)}]");
......@@ -99,13 +99,25 @@ public class KeyMatcherFacadeTest {
shouldMatch("pred(f(a)) ==>", "pred((...a...):?Q) ==>","[{?Q=f(a)}]");
shouldMatch("p ==>", "(p):?X:Formula ==>", "[{?X=p}]");
shouldMatch("pred(a) ==>", "(pred(?)):?X:Formula ==>");
shouldMatch("==>f(f(g(a)))= 0", "==> (f((...g((...a...):?Q)...):?G)):?Y = 0", "[{?G=f(g(a)), ?Q=a, ?Y=f(f(g(a)))}]");
shouldMatch("==>f(f(g(a)))= 0", "==> ((f((...g((...a...):?Q)...):?G)):?R):?Y = 0", "[{?G=f(g(a)), ?Q=a, ?R=f(f(g(a))), ?Y=f(f(g(a)))}]");
// shouldMatch("f(f(g(a)))= 0 ==>", "f( (... g( (...a...):?Q ) ...) : ?R) : ?Y = 0 ==>",
// "[{EMPTY_MATCH=null, ?Q=a, ?Y=f(f(g(a))), ?R=f(g(a))}]");
}
@Test
public void testQuantMatch() throws Exception {
// 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}]");
// shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X _)");
// shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X (fint2(1,?X)))");
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)))==>", "[{}]");
}
@Test
public void hasToplevelComma() throws Exception {
......
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