Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
1891b430
Commit
1891b430
authored
Jan 16, 2018
by
Sarah Grebing
Browse files
Fixed a bug in quantifier matching
parent
54462912
Pipeline
#16925
failed with stages
in 116 minutes and 58 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
matcher/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
View file @
1891b430
...
...
@@ -22,7 +22,7 @@ sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
semiSeqPattern : termPattern (',' termPattern)*;
termPattern :
'(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+ skope=termPattern ')' #quantForm
'(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+ skope=termPattern ')'
bindClause?
#quantForm
| termPattern MUL termPattern #mult
| <assoc=right> termPattern op=(DIV|MOD) termPattern #divMod
| termPattern op=(PLUS|MINUS) termPattern #plusMinus
...
...
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java
View file @
1891b430
...
...
@@ -464,7 +464,9 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
Matchings
fromTerm
=
accept
(
ctx
.
skope
,
create
(
peek
,
0
));
return
reduceConformQuant
(
fromTerm
,
match
);
//return handleBindClause(ctx.bindClause(), path, m);
Matchings
retM
=
reduceConformQuant
(
fromTerm
,
match
);
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
retM
);
}
@Override
...
...
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
View file @
1891b430
...
...
@@ -211,37 +211,40 @@ public class MatcherFacadeTest {
@Test
public
void
seqTest
()
throws
Exception
{
//testcases for empty matches
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
" ==> _"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
"==>"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
"_ ==> "
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
"_ ==> _"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"==> pred(a)"
,
"==>"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> "
,
"==>"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==> pred(?Y)"
,
"[{?X=a, ?Y=b, ?Z=b}, {?X=b, ?Y=b, ?Z=a}]"
);
shouldMatchSeq
(
"pred(a), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==> pred(?X)"
,
"[{?X=b, ?Z=a}]"
);
shouldMatchSeq
(
"pred(a), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==>"
,
"[{?X=a, ?Z=b}, {?X=b, ?Z=a}]"
);
shouldMatchSeq
(
"pred(f(a)), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==>"
,
"[{?X=b, ?Z=f(a)}, {?X=f(a), ?Z=b}]"
);
shouldMatchSeq
(
"pred(f(a)), pred(b) ==> pred(b)"
,
"pred(...?X...) ==>"
,
"[{?X=a}, {?X=b}, {?X=f(a)}]"
);
shouldMatchSeq
(
"fint2(1,2), fint2(2,3), !p ==> pred(a), p"
,
"fint2(1, ?X), fint2(?X, ?Y) ==> p"
,
"[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]"
);
shouldMatchSeq
(
"2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p"
,
"?X=0 ==>"
,
"[{?X=h2(Z(2(#)),Z(3(#)))}]"
);
shouldMatchSeq
(
"pred(a) <-> pred(b), pred(a), pred(b) ==> p"
,
"?X <-> ?Y ==> "
,
"[{?X=pred(a), ?Y=pred(b)}]"
);
// shouldMatchSeq("i <= 10 ==>", "i <= ?X ==>");
shouldMatchSeq
(
"==> (\\forall int i; \\exists int j; fint2(j,i)) , pred(a)"
,
"==> (\\forall i (\\exists j _))"
);
// //testcases for empty matches
// shouldMatchSeq("pred(a) ==> pred(a), pred(b)", " ==> _", "[{EMPTY_MATCH=null}]");
//
// shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "==>", "[{EMPTY_MATCH=null}]");
// shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> ", "[{EMPTY_MATCH=null}]");
// shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> _", "[{EMPTY_MATCH=null}]");
// shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
// shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
//
//
// shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?Y)", "[{?X=a, ?Y=b, ?Z=b}, {?X=b, ?Y=b, ?Z=a}]");
// shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?X)", "[{?X=b, ?Z=a}]");
// shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]");
//
// shouldMatchSeq(
// "pred(f(a)), pred(b) ==> pred(b)",
// "pred(?X), pred(?Z) ==>",
// "[{?X=b, ?Z=f(a)}, {?X=f(a), ?Z=b}]");
//
// shouldMatchSeq(
// "pred(f(a)), pred(b) ==> pred(b)",
// "pred(...?X...) ==>",
// "[{?X=a}, {?X=b}, {?X=f(a)}]");
//
// shouldMatchSeq(
// "fint2(1,2), fint2(2,3), !p ==> pred(a), p",
// "fint2(1, ?X), fint2(?X, ?Y) ==> p",
// "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
// shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]");
//
// shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p", "?X <-> ?Y ==> ", "[{?X=pred(a), ?Y=pred(b)}]");
}
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
,
String
exp
)
throws
ParserException
{
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment