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
1e21327d
Commit
1e21327d
authored
Aug 20, 2017
by
Sarah Grebing
Browse files
Fixed a bug in semiseq matching, added testcases
parent
e7bb515b
Pipeline
#12960
failed with stage
in 2 minutes and 21 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
View file @
1e21327d
...
...
@@ -87,7 +87,6 @@ public class MatcherFacade {
}
List
<
MatchInfo
>
res
=
reduceCompatibleMatches
(
allMatches
);
System
.
out
.
println
(
"res = "
+
res
);
if
(
res
==
null
)
return
NO_MATCH
;
...
...
@@ -141,13 +140,11 @@ public class MatcherFacade {
SemiSeqPatternContext
antecPattern
=
ctx
.
antec
;
SemiSeqPatternContext
succPattern
=
ctx
.
succ
;
System
.
out
.
println
(
"SuccPattern "
+
succPattern
);
Matchings
mAntec
=
matches
(
antecPattern
,
antec
);
Matchings
mSucc
=
matches
(
succPattern
,
succ
);
Matchings
mAntec
=
antecPattern
==
null
?
MatcherImpl
.
EMPTY_MATCH
:
matches
(
antecPattern
,
antec
);
Matchings
mSucc
=
succPattern
==
null
?
MatcherImpl
.
EMPTY_MATCH
:
matches
(
succPattern
,
succ
);
Matchings
newMatching
=
MatcherImpl
.
reduceConform
(
mAntec
,
mSucc
);
//return MatcherImpl.NO_MATCH;
return
newMatching
;
}
...
...
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
View file @
1e21327d
...
...
@@ -62,7 +62,10 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
* @return
*/
protected
static
Matchings
reduceConform
(
Matchings
m1
,
Matchings
m2
)
{
//shortcuts
if
(
m1
==
NO_MATCH
||
m2
==
NO_MATCH
)
return
NO_MATCH
;
if
(
m1
==
EMPTY_MATCH
)
return
m2
;
if
(
m2
==
EMPTY_MATCH
)
return
m1
;
Matchings
m3
=
new
Matchings
();
boolean
oneMatch
=
false
;
...
...
@@ -163,13 +166,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
*/
@Override
protected
Matchings
visitSemiSeqPattern
(
MatchPatternParser
.
SemiSeqPatternContext
ctx
,
Term
peek
)
{
/*Matchings m = new Matchings();
List<MatchPatternParser.TermPatternContext> termPatterns = ctx.termPattern();
for (MatchPatternParser.TermPatternContext termPattern : termPatterns) {
System.out.println("Searching for "+termPattern.getText()+" and "+peek.toString());
Matchings m1 = accept(termPattern,peek);
}*/
return
null
;
}
...
...
src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
View file @
1e21327d
...
...
@@ -43,17 +43,6 @@ public class MatcherFacadeTest {
shouldMatchForm
(
"pred(a)"
,
"_"
);
shouldMatchForm
(
"pred(a)"
,
"pred(?X)"
,
"[{?X=a}]"
);
shouldMatchSeq
(
"pred(a), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==> pred(?Y)"
);
shouldMatchSeq
(
"pred(a), pred(b) ==> pred(b)"
,
"pred(?X), pred(?Z) ==> pred(?X)"
);
shouldMatchSemiSeq
(
"pred(a), pred(b) ==>"
,
"pred(?X), pred(?Y)"
,
"[{?X=a, ?Y=b}, {?X=b, ?Y=a}]"
);
// shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[]");
// shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]");
// shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]");
// shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)");
//shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(?X), pred(?Y)", "[{?X=a}, {?Y:=b}]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
...
...
@@ -91,19 +80,6 @@ public class MatcherFacadeTest {
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
System
.
out
.
println
(
m
);
}
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
,
String
exp
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
public
Term
parseKeyTerm
(
String
term
)
throws
ParserException
{
Reader
in
=
new
StringReader
(
term
);
Sort
sort
=
Sort
.
ANY
;
...
...
@@ -135,9 +111,24 @@ public class MatcherFacadeTest {
return
dtp
.
parse
(
in
,
sort
,
services
,
namespace
,
abbrev
);
}
private
Sequent
parseSeq
(
String
s
)
throws
ParserException
{
Reader
in
=
new
StringReader
(
s
);
return
dtp
.
parseSeq
(
in
,
services
,
namespace
,
abbrev
);
@Test
public
void
semiSeqTest
()
throws
Exception
{
shouldMatchSemiSeq
(
"pred(a), pred(b) ==>"
,
"pred(?X), pred(?Y)"
,
"[{?X=a, ?Y=b}, {?X=b, ?Y=a}]"
);
shouldMatchSemiSeq
(
"pred(a), pred(b) ==>"
,
"pred(?X), pred(?X)"
,
"[]"
);
shouldMatchSemiSeq
(
"pred(a), pred(f(a)) ==>"
,
"pred(?X), pred(f(?X))"
,
"[{?X=a}]"
);
shouldMatchSemiSeq
(
"pred(b), pred(f(a)) ==>"
,
"pred(?X), pred(f(?X))"
,
"[]"
);
shouldMatchSemiSeq
(
"pred(a), pred(b) ==> qpred(a,b)"
,
"pred(a), pred(b)"
);
shouldMatchSemiSeq
(
"pred(a), pred(b) ==> qpred(a,b)"
,
"pred(?X), pred(?Y)"
,
"[{?X=a, ?Y=b}, {?X=b, ?Y=a}]"
);
}
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
,
String
exp
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
)
throws
ParserException
{
...
...
@@ -145,4 +136,33 @@ public class MatcherFacadeTest {
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
System
.
out
.
println
(
m
);
}
private
Sequent
parseSeq
(
String
s
)
throws
ParserException
{
Reader
in
=
new
StringReader
(
s
);
return
dtp
.
parseSeq
(
in
,
services
,
namespace
,
abbrev
);
}
@Test
public
void
seqTest
()
throws
Exception
{
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)}]"
);
}
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
,
String
exp
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
System
.
out
.
println
(
m
);
}
}
\ No newline at end of file
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