diff -r dd9dde2d902b -r 80cc6dc4c98b thys2/blexer2.sc --- a/thys2/blexer2.sc Fri Dec 30 01:52:32 2022 +0000 +++ b/thys2/blexer2.sc Fri Dec 30 17:37:51 2022 +0000 @@ -1505,7 +1505,7 @@ } } - naive_matcher() + // naive_matcher() //single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))), // SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))) @@ -1638,13 +1638,14 @@ def bders_bderssimp() { - test(single(SEQ(ALTS(ONE,CHAR('c')), - SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 1) { (r: Rexp) => + + val r = //(SEQ(ALTS(ONE,CHAR('c')), + SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))) // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => - val ss = Set("aa")//stringsFromRexp(r) + val ss = Set("aa")//stringsFromRexp(r) val boolList = ss.map(s => { //val bdStrong = bdersStrong(s.toList, internalise(r)) - val bds = bsimp(bders(s.toList, internalise(r))) + val bds = (bders(s.toList, internalise(r))) val bdssimp = bsimp(bders_simp(s.toList, internalise(r))) //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r)) //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r)) @@ -1652,17 +1653,19 @@ //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size || //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size rprint(r) - println(bds) - println(bdssimp) + println(asize(bds)) + println(asize(bdssimp)) bds == bdssimp }) //!boolList.exists(b => b == false) !boolList.exists(b => b == false) } - } - // bders_bderssimp() + + + + bders_bderssimp() -println("hi!!!!!") -counterexample_check() \ No newline at end of file +// println("hi!!!!!") +// counterexample_check() \ No newline at end of file