--- a/thys2/blexer2.sc Fri Feb 11 17:28:41 2022 +0000
+++ b/thys2/blexer2.sc Wed Feb 16 17:20:40 2022 +0000
@@ -478,7 +478,7 @@
r match {
case ASEQ(bs, r1, r2) =>
val termsTruncated = allowableTerms.collect(rt => rt match {
- case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p
+ case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2))
})
val pruned : ARexp = pruneRexp(r1, termsTruncated)
pruned match {
@@ -489,7 +489,10 @@
case AALTS(bs, rs) =>
//allowableTerms.foreach(a => println(shortRexpOutput(a)))
- val rsp = rs.map(r => pruneRexp(r, allowableTerms)).filter(r => r != AZERO)
+ val rsp = rs.map(r =>
+ pruneRexp(r, allowableTerms)
+ )
+ .filter(r => r != AZERO)
rsp match {
case Nil => AZERO
case r1::Nil => fuse(bs, r1)
@@ -509,15 +512,17 @@
def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+
case Nil => Nil
case x :: xs =>
+ //assert(acc.distinct == acc)
val erased = erase(x)
if(acc.contains(erased))
distinctBy4(xs, acc)
else{
val addToAcc = breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
- val xp = pruneRexp(x, addToAcc)
- xp match {
+ //val xp = pruneRexp(x, addToAcc)
+ pruneRexp(x, addToAcc) match {
case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
}
@@ -827,40 +832,41 @@
//println(refSize)
println(pderSTAR.size)
- // val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%)
- // val B : Rexp = ((ONE).%)
- // val C : Rexp = ("d") ~ ((ONE).%)
- // val PRUNE_REG : Rexp = (A | B | C)
- // val APRUNE_REG = internalise(PRUNE_REG)
+ val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%)
+ val B : Rexp = ((ONE).%)
+ val C : Rexp = ("d") ~ ((ONE).%)
+ val PRUNE_REG : Rexp = (C | B | A)
+ val APRUNE_REG = internalise(PRUNE_REG)
// val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG))
// println("program executes and gives: as disired!")
// println(shortRexpOutput(erase(program_solution)))
-
- for(i <- List( 4, 8, 9, 17, 29) ){// 100, 400, 800, 840, 841, 900
+ val simpedPruneReg = strongBsimp(APRUNE_REG)
+ println(shortRexpOutput(erase(simpedPruneReg)))
+ for(i <- List(100, 900 ) ){// 100, 400, 800, 840, 841, 900
val prog0 = "a" * i
//println(s"test: $prog0")
println(s"testing with $i a's" )
- val bd = bdersSimp(prog0, STARREG)//DB
+ //val bd = bdersSimp(prog0, STARREG)//DB
val sbd = bdersSimpS(prog0, STARREG)//strongDB
starPrint(erase(sbd))
val subTerms = breakIntoTerms(erase(sbd))
- val subTermsLarge = breakIntoTerms(erase(bd))
+ //val subTermsLarge = breakIntoTerms(erase(bd))
- println(s"subterms of regex with strongDB: ${subTerms.length}, standard DB: ${subTermsLarge.length}")
+ println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}")
- println("the number of distinct subterms for bsimp with strongDB and standardDB")
+ println("the number of distinct subterms for bsimp with strongDB")
println(subTerms.distinct.size)
- println(subTermsLarge.distinct.size)
+ //println(subTermsLarge.distinct.size)
println("which coincides with the number of PDER terms")
// println(shortRexpOutput(erase(sbd)))
// println(shortRexpOutput(erase(bd)))
- println("pdersize, original, strongSimp, bsimp")
- println(refSize, size(STARREG), asize(sbd), asize(bd))
+ println("pdersize, original, strongSimp")
+ println(refSize, size(STARREG), asize(sbd))
val vres = strong_blexing_simp( STARREG, prog0)
println(vres)