Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
a745eb0d
Commit
a745eb0d
authored
Aug 22, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fixed test cases for matcher
parent
d8831558
Pipeline
#13014
failed with stage
in 3 minutes and 27 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
85 additions
and
88 deletions
+85
-88
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
...n/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
+61
-63
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
...ain/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
+13
-14
src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
...va/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
+11
-11
No files found.
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
View file @
a745eb0d
...
...
@@ -10,10 +10,7 @@ import org.antlr.v4.runtime.CharStreams;
import
org.antlr.v4.runtime.CommonTokenStream
;
import
org.key_project.util.collection.ImmutableList
;
import
java.util.ArrayList
;
import
java.util.Collections
;
import
java.util.HashMap
;
import
java.util.List
;
import
java.util.*
;
import
java.util.stream.Collectors
;
import
static
edu
.
kit
.
formal
.
psdb
.
termmatcher
.
MatchPatternParser
.
SequentPatternContext
;
...
...
@@ -64,64 +61,6 @@ public class MatcherFacade {
}
public
static
Matchings
matches
(
SemiSeqPatternContext
pattern
,
Semisequent
semiSeq
)
{
MatcherImpl
matcher
=
new
MatcherImpl
();
ImmutableList
<
SequentFormula
>
allSequentFormulas
=
semiSeq
.
asList
();
List
<
TermPatternContext
>
termPatternContexts
=
pattern
.
termPattern
();
List
<
List
<
MatcherImpl
.
MatchInfo
>>
allMatches
=
new
ArrayList
<>();
for
(
TermPatternContext
termPatternContext
:
termPatternContexts
)
{
List
<
MatchInfo
>
m
=
new
ArrayList
<>();
for
(
SequentFormula
form
:
allSequentFormulas
)
{
Matchings
temp
=
matcher
.
accept
(
termPatternContext
,
form
.
formula
());
for
(
HashMap
<
String
,
Term
>
match
:
temp
)
{
m
.
add
(
new
MatchInfo
(
match
,
Collections
.
singleton
(
form
)));
}
}
allMatches
.
add
(
m
);
}
List
<
MatchInfo
>
res
=
reduceCompatibleMatches
(
allMatches
);
if
(
res
==
null
)
return
NO_MATCH
;
List
<
HashMap
<
String
,
Term
>>
resMap
=
res
.
stream
().
map
(
el
->
el
.
matching
).
collect
(
Collectors
.
toList
());
Matchings
resMatchings
=
new
Matchings
();
resMatchings
.
addAll
(
resMap
);
return
resMatchings
;
}
//BiMap<Pair<SequentFormula, MatchPatternParser.TermPatternContext>, Matchings> formulaToMatchingInfo,
/**
* Reduce all matches to only compatible matchings
* @param allMatches
* @return
*/
private
static
List
<
MatchInfo
>
reduceCompatibleMatches
(
List
<
List
<
MatchInfo
>>
allMatches
)
{
if
(
allMatches
.
size
()
==
1
)
{
return
allMatches
.
get
(
0
);
}
if
(
allMatches
.
size
()
==
2
)
{
return
MatcherImpl
.
reduceConform
(
allMatches
.
get
(
0
),
allMatches
.
get
(
1
));
}
else
{
List
<
MatchInfo
>
tmp
=
MatcherImpl
.
reduceConform
(
allMatches
.
get
(
0
),
allMatches
.
get
(
1
));
List
<
List
<
MatchInfo
>>
list
=
new
ArrayList
<>();
list
.
add
(
tmp
);
list
.
addAll
(
allMatches
.
subList
(
2
,
allMatches
.
size
()));
return
reduceCompatibleMatches
(
list
);
}
}
/**
* Match a sequent pattern against a concrete sequent
*
...
...
@@ -146,7 +85,7 @@ public class MatcherFacade {
SemiSeqPatternContext
patternCtx
=
ctx
.
anywhere
;
if
(
antec
.
isEmpty
()
&
succ
.
isEmpty
())
{
//Sonderbehandlung, falls beide EmptyMatch-> kein
t
hema aber ansonsten bevorzugung von Varzuweisungen
//Sonderbehandlung, falls beide EmptyMatch-> kein
T
hema aber ansonsten bevorzugung von Varzuweisungen
Matchings
antecMatches
=
matches
(
patternCtx
,
antec
);
Matchings
succMatches
=
matches
(
patternCtx
,
succ
);
Matchings
ret
=
compareMatchings
(
antecMatches
,
succMatches
);
...
...
@@ -172,6 +111,65 @@ public class MatcherFacade {
return
newMatching
;
}
//BiMap<Pair<SequentFormula, MatchPatternParser.TermPatternContext>, Matchings> formulaToMatchingInfo,
/**
* Reduce all matches to only compatible matchings
*
* @param allMatches
* @return
*/
private
static
List
<
MatchInfo
>
reduceCompatibleMatches
(
List
<
List
<
MatchInfo
>>
allMatches
)
{
if
(
allMatches
.
size
()
==
1
)
{
return
allMatches
.
get
(
0
);
}
if
(
allMatches
.
size
()
==
2
)
{
return
MatcherImpl
.
reduceConform
(
allMatches
.
get
(
0
),
allMatches
.
get
(
1
));
}
else
{
List
<
MatchInfo
>
tmp
=
MatcherImpl
.
reduceConform
(
allMatches
.
get
(
0
),
allMatches
.
get
(
1
));
List
<
List
<
MatchInfo
>>
list
=
new
ArrayList
<>();
list
.
add
(
tmp
);
list
.
addAll
(
allMatches
.
subList
(
2
,
allMatches
.
size
()));
return
reduceCompatibleMatches
(
list
);
}
}
public
static
Matchings
matches
(
SemiSeqPatternContext
pattern
,
Semisequent
semiSeq
)
{
MatcherImpl
matcher
=
new
MatcherImpl
();
ImmutableList
<
SequentFormula
>
allSequentFormulas
=
semiSeq
.
asList
();
List
<
TermPatternContext
>
termPatternContexts
=
pattern
.
termPattern
();
List
<
List
<
MatcherImpl
.
MatchInfo
>>
allMatches
=
new
ArrayList
<>();
for
(
TermPatternContext
termPatternContext
:
termPatternContexts
)
{
List
<
MatchInfo
>
m
=
new
ArrayList
<>();
for
(
SequentFormula
form
:
allSequentFormulas
)
{
Matchings
temp
=
matcher
.
accept
(
termPatternContext
,
form
.
formula
());
for
(
HashMap
<
String
,
Term
>
match
:
temp
)
{
m
.
add
(
new
MatchInfo
(
match
,
Collections
.
singleton
(
form
)));
}
}
allMatches
.
add
(
m
);
}
List
<
MatchInfo
>
res
=
reduceCompatibleMatches
(
allMatches
);
if
(
res
==
null
)
return
NO_MATCH
;
Set
<
HashMap
<
String
,
Term
>>
resMap
=
res
.
stream
().
map
(
el
->
el
.
matching
).
collect
(
Collectors
.
toSet
());
//remove dups?
Matchings
resMatchings
=
new
Matchings
();
resMatchings
.
addAll
(
resMap
);
return
resMatchings
;
}
private
static
Matchings
compareMatchings
(
Matchings
antecMatches
,
Matchings
succMatches
)
{
if
(
antecMatches
.
equals
(
EMPTY_MATCH
)
&&
succMatches
.
equals
(
EMPTY_MATCH
))
{
return
MatcherImpl
.
EMPTY_MATCH
;
...
...
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
View file @
a745eb0d
...
...
@@ -22,6 +22,13 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
private
Stack
<
Term
>
termStack
=
new
Stack
<>();
/**
* Reduce two matchinfos
*
* @param m1
* @param m2
* @return
*/
protected
static
List
<
MatchInfo
>
reduceConform
(
List
<
MatchInfo
>
m1
,
List
<
MatchInfo
>
m2
)
{
if
(
m1
==
null
||
m2
==
null
)
return
null
;
//"null" is equivalent to NO_MATCH
...
...
@@ -33,7 +40,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
Set
<
SequentFormula
>
intersection
=
new
HashSet
<>(
minfo1
.
matchedForms
);
intersection
.
retainAll
(
minfo2
.
matchedForms
);
if
(!
intersection
.
isEmpty
())
continue
;
HashMap
<
String
,
Term
>
h3
=
reduceConform
(
minfo1
.
matching
,
minfo2
.
matching
);
if
(
h3
!=
null
)
{
...
...
@@ -48,28 +54,20 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
private
static
HashMap
<
String
,
Term
>
reduceConform
(
HashMap
<
String
,
Term
>
h1
,
HashMap
<
String
,
Term
>
h2
)
{
HashMap
<
String
,
Term
>
h3
=
new
HashMap
<>(
h1
);
for
(
String
s1
:
h3
.
keySet
())
{
if
(!
s1
.
equals
(
"EMPTY_MATCH"
)
&&
(
h2
.
containsKey
(
s1
)
&&
!
h2
.
get
(
s1
).
equals
(
h1
.
get
(
s1
))))
{
return
null
;
}
}
}
h3
.
putAll
(
h2
);
return
h3
;
}
/*@Override
protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
if (peek != null) {
return EMPTY_MATCH;
} else {
return NO_MATCH;
}
}*/
/**
* Reduce the matchings by eliminating non-compatible matchings.
* For example:
...
...
@@ -91,7 +89,8 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
for
(
HashMap
<
String
,
Term
>
h2
:
m2
)
{
HashMap
<
String
,
Term
>
h3
=
reduceConform
(
h1
,
h2
);
if
(
h3
!=
null
)
{
m3
.
add
(
h3
);
//m3.add(h3);
if
(!
m3
.
contains
(
h3
))
m3
.
add
(
h3
);
oneMatch
=
true
;
}
}
...
...
@@ -182,7 +181,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
/**
* Trasnform a term t
a
ht represent a number to int
* Trasnform a term th
a
t represent a number to int
*
* @param sub
* @return
...
...
src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
View file @
a745eb0d
...
...
@@ -154,23 +154,23 @@ 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=f(a), ?Z=b}, {?X=b, ?Z=f(a)}]"
);
shouldMatchSeq
(
"pred(f(a)), pred(b) ==> pred(b)"
,
"pred(...?X...) ==>"
,
"[{?X=f(a)}, {?X=a}, {?X=b}]"
);
shouldMatchSeq
(
"==> pred(a)"
,
"==>"
,
"[{EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> "
,
"==>"
,
"[{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(f(a)), pred(b) ==> pred(b)"
,
"pred(...?X...) ==>"
,
"[{?X=a}, {?X=f(a)}, {?X=b}]"
);
//these two need to be checked I think
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
"_ ==> _"
,
"[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]"
);
shouldMatchSeq
(
"pred(a) ==> pred(a), pred(b)"
,
" ==> _"
,
"[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]"
);
// shouldMatchSeq("fint2(1,2), fint2(2,3), !p ==> pred(a), p", "fint2(1, ?X), fint2(?X, ?Y) ==> p" , "[{?X=2, ?Y=3}]");
shouldMatchSeq
(
"fint2(1,2), fint2(2,3), !p ==> pred(a), p"
,
"fint2(1, ?X), fint2(?X, ?Y) ==> p"
);
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(#))}]"
);
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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