diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 1c4f19bf6cd2bee75ba514b6620e0f838e2f1e82..ea5318e4b96c21bbf2645afd1b791f95a22f9551 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -1486,7 +1486,6 @@ trait CodeExtraction extends ASTExtractors { Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos) case c @ ExCall(rec, sym, tps, args) => - println("Parsing call:" + c) val rrec = rec match { case t if (defsToDefs contains sym) && !isMethod(sym) => null diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala index abe8dbe1a27c730f8d9ccefd05522bc8a0d9120f..0a6971eb3715aa8e87facf39296c3d73b73630b7 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -27,6 +27,10 @@ object Extractors { Some((Seq(t), (es: Seq[Expr]) => RealUMinus(es.head))) case BVNot(t) => Some((Seq(t), (es: Seq[Expr]) => BVNot(es.head))) + case StringLength(t) => + Some((Seq(t), (es: Seq[Expr]) => StringLength(es.head))) + case ToString(t) => + Some((Seq(t), (es: Seq[Expr]) => ToString(es.head))) case SetCardinality(t) => Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head))) case CaseClassSelector(cd, e, sel) => @@ -120,6 +124,8 @@ object Extractors { Some(Seq(t1, t2), (es: Seq[Expr]) => times(es(0), es(1))) case RealDivision(t1, t2) => Some(Seq(t1, t2), (es: Seq[Expr]) => RealDivision(es(0), es(1))) + case StringConcat(t1, t2) => + Some(Seq(t1, t2), (es: Seq[Expr]) => StringConcat(es(0), es(1))) case ElementOfSet(t1, t2) => Some(Seq(t1, t2), (es: Seq[Expr]) => ElementOfSet(es(0), es(1))) case SubsetOf(t1, t2) => @@ -156,6 +162,7 @@ object Extractors { case CaseClass(cd, args) => Some((args, CaseClass(cd, _))) case And(args) => Some((args, and)) case Or(args) => Some((args, or)) + case SubString(t1, a, b) => Some((t1::a::b::Nil, es => SubString(es(0), es(1), es(2)))) case FiniteSet(els, base) => Some((els.toSeq, els => FiniteSet(els.toSet, base))) case FiniteMap(args, f, t) => { diff --git a/testcases/stringrender/runTests.sh b/testcases/stringrender/runTests.sh index ec84397547290bf33b08b790f7d42812edbaada3..92ab18023d4c1fc74a9391b3bd9ecfa863d22472 100644 --- a/testcases/stringrender/runTests.sh +++ b/testcases/stringrender/runTests.sh @@ -15,12 +15,12 @@ echo "################################" >> $summaryLog echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog #All benchmarks: -./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog +./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnwrapped testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog -./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog +./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnwrapped testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog ./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog