diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala index b717cccf513babcd76b38ec0973b1e19330777ff..baefc4fa77202304a9b8eb2fc76bc86c73e9e8a0 100644 --- a/src/main/scala/leon/solvers/string/StringSolver.scala +++ b/src/main/scala/leon/solvers/string/StringSolver.scala @@ -3,13 +3,7 @@ package leon.solvers.string import leon.purescala.Common._ -import leon.purescala.Definitions._ -import leon.purescala.Expressions._ -import leon.solvers.Solver -import leon.utils.Interruptible -import leon.LeonContext import scala.collection.mutable.ListBuffer -import vanuatoo.Pattern import scala.annotation.tailrec /** @@ -287,7 +281,7 @@ object StringSolver { (constants match { case Some(_) => None case None => // Ok now let's assign all variables to empty string. - val newMap = (ids.collect{ case Right(id) => id -> ""}) + val newMap = ids.collect { case Right(id) => id -> "" } val newAssignments = (Option(assignments) /: newMap) { case (None, (id, rhs)) => None case (Some(a), (id, rhs)) => @@ -310,7 +304,7 @@ object StringSolver { } // Check if constants form a partition in the string, i.e. getting the .indexOf() the first time is the only way to split the string. - if(constants.length > 0) { + if(constants.nonEmpty) { var pos = -2 var lastPos = -2 @@ -327,7 +321,7 @@ object StringSolver { if(invalid) None else { val i = rhs.indexOfSlice(lastConst, lastPos + 1) if(i == -1) { // OK it's the smallest position possible, hence we can split at the last position. - val (before, constant, after) = splitAtLastConstant(ids) + val (before, _, after) = splitAtLastConstant(ids) val firstConst = rhs.substring(0, lastPos) val secondConst = rhs.substring(lastPos + lastConst.length) constantPropagate((before, firstConst)::(after, secondConst)::q, assignments, newProblem) @@ -415,12 +409,12 @@ object StringSolver { case List(x) => Stream(Map(x -> rhs)) case x :: ys => - val (bestVar, bestScore, worstScore) = (((None:Option[(Identifier, Int, Int)]) /: ids) { + val (bestVar, bestScore, worstScore) = ((None: Option[(Identifier, Int, Int)]) /: ids) { case (None, x) => val sx = statistics(x) Some((x, sx, sx)) case (s@Some((x, i, ws)), y) => val yi = statistics(y) - if(i >= yi) Some((x, i, Math.min(yi, ws))) else Some((y, yi, ws)) - }).get + if (i >= yi) Some((x, i, Math.min(yi, ws))) else Some((y, yi, ws)) + }.get val pos = prioritizedPositions(rhs) val numBestVars = ids.count { x => x == bestVar } @@ -462,11 +456,11 @@ object StringSolver { } //println("Best variable:" + bestVar + " going to test " + strings.toList) - (for(str <- strings.distinct + for (str <- strings.distinct if java.util.regex.Pattern.quote(str).r.findAllMatchIn(rhs).length >= numBestVars ) yield { Map(bestVar -> str) - }) + } } } } @@ -496,7 +490,7 @@ object StringSolver { for((lhs, rhs) <- p) { val constants = lhs.collect{ case Left(constant) => constant } val identifiers_grouped = ListBuffer[List[Identifier]]() - var current_buffer = ListBuffer[Identifier]() + val current_buffer = ListBuffer[Identifier]() for(e <- lhs) e match { case Left(constant) => // At this point, there is only one constant here. identifiers_grouped.append(current_buffer.toList) @@ -523,7 +517,7 @@ object StringSolver { minIdentifiersGrouped = identifiers_grouped.toList } } - val (lhs, rhs) = minStatement + val (_, rhs) = minStatement val constants = minConstants val identifiers_grouped = minIdentifiersGrouped val statistics = stats(p) @@ -585,7 +579,7 @@ object StringSolver { /** Supposes that all variables are transitively bounded by length*/ type GeneralProblem = List[GeneralEquation] - def variablesStringForm(sf: StringForm): Set[Identifier] = (sf.collect{ case Right(id) => id }).toSet + def variablesStringForm(sf: StringForm): Set[Identifier] = sf.collect { case Right(id) => id }.toSet def variables(gf: GeneralEquation): Set[Identifier] = variablesStringForm(gf._1) ++ variablesStringForm(gf._2) /** Returns true if the problem is transitively bounded */ @@ -593,7 +587,7 @@ object StringSolver { def isBounded(sf: GeneralEquation) = { variablesStringForm(sf._1).forall(transitivelyBounded) || variablesStringForm(sf._2).forall(transitivelyBounded) } - val (bounded, notbounded) = b.partition(isBounded _) + val (bounded, notbounded) = b.partition(isBounded) if(notbounded == Nil) true else if(notbounded == b) false diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala index 571d42e21b89b09c8f1fa7d955acc73b15668c48..bb0b047fd72cc7a46ddefebd0fe35cd173721425 100644 --- a/src/main/scala/leon/synthesis/Solution.scala +++ b/src/main/scala/leon/synthesis/Solution.scala @@ -70,14 +70,14 @@ object Solution { new Solution(BooleanLiteral(true), Set(), simplify(term), isTrusted) } - def unapply(s: Solution): Option[(Expr, Set[FunDef], Expr)] = if (s eq null) None else Some((s.pre, s.defs, s.term)) + def unapply(s: Solution): Option[(Expr, Set[FunDef], Expr, Boolean)] = if (s eq null) None else Some((s.pre, s.defs, s.term, s.isTrusted)) def choose(p: Problem): Solution = { - new Solution(BooleanLiteral(true), Set(), Choose(Lambda(p.xs.map(ValDef(_)), p.phi))) + new Solution(BooleanLiteral(true), Set(), Choose(Lambda(p.xs.map(ValDef), p.phi))) } def chooseComplete(p: Problem): Solution = { - new Solution(BooleanLiteral(true), Set(), Choose(Lambda(p.xs.map(ValDef(_)), p.pc and p.phi))) + new Solution(BooleanLiteral(true), Set(), Choose(Lambda(p.xs.map(ValDef), p.pc and p.phi))) } // Generate the simplest, wrongest solution, used for complexity lowerbound diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala index d7dd317d73992a68b7446e205ece0b31d592ceea..61b356415f833f493bfc9d7ebf2bbf9c17676a9a 100644 --- a/src/main/scala/leon/synthesis/rules/Assert.scala +++ b/src/main/scala/leon/synthesis/rules/Assert.scala @@ -32,7 +32,8 @@ case object Assert extends NormalizingRule("Assert") { val sub = p.copy(pc = p.pc withConds exprsA, phi = andJoin(others), eb = p.qeb.filterIns(andJoin(exprsA))) Some(decomp(List(sub), { - case (s @ Solution(pre, defs, term)) :: Nil => Some(Solution(pre=andJoin(exprsA :+ pre), defs, term, s.isTrusted)) + case List(s @ Solution(pre, defs, term, isTrusted)) => + Some(Solution(andJoin(exprsA :+ pre), defs, term, isTrusted)) case _ => None }, "Assert "+andJoin(exprsA).asString)) } diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala index 8665eaf3320757d8a4d295cc7953899d01d8f55d..1fb5ead1472a33eb1b7554e092dda512e8b13a4a 100644 --- a/src/main/scala/leon/synthesis/rules/OnePoint.scala +++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala @@ -35,8 +35,8 @@ case object OnePoint extends NormalizingRule("One-point") { val newProblem = Problem(p.as, p.ws, p.pc, subst(x -> e, andJoin(others)), oxs, p.qeb.removeOuts(Set(x))) val onSuccess: List[Solution] => Option[Solution] = { - case List(s @ Solution(pre, defs, term)) => - Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, tupleWrap(p.xs.map(Variable)))), s.isTrusted)) + case List(s @ Solution(pre, defs, term, isTrusted)) => + Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, tupleWrap(p.xs.map(Variable)))), isTrusted)) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala index a80963625fe040d041863ecf3e32d2918a680513..7c2d7b251a02c0cdd431298fab67e4419b747a8d 100644 --- a/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala +++ b/src/main/scala/leon/synthesis/rules/unused/IntegerEquation.scala @@ -59,8 +59,8 @@ case object IntegerEquation extends Rule("Integer Equation") { val newProblem = Problem(problem.as, problem.ws, problem.pc withCond eqPre, andJoin(allOthers), problem.xs) val onSuccess: List[Solution] => Option[Solution] = { - case List(s @ Solution(pre, defs, term)) => - Some(Solution(and(eqPre, pre), defs, term, s.isTrusted)) + case List(s @ Solution(pre, defs, term, isTrusted)) => + Some(Solution(and(eqPre, pre), defs, term, isTrusted)) case _ => None } @@ -96,14 +96,21 @@ case object IntegerEquation extends Rule("Integer Equation") { val newProblem = Problem(problem.as ++ freshInputVariables, problem.ws, problem.pc withCond eqPre, freshFormula, subproblemxs) val onSuccess: List[Solution] => Option[Solution] = { - case List(s @ Solution(pre, defs, term)) => { + case List(s @ Solution(pre, defs, term, isTrusted)) => { val freshPre = replace(equivalenceConstraints, pre) val freshTerm = replace(equivalenceConstraints, term) val freshsubxs = subproblemxs.map(id => FreshIdentifier(id.name, id.getType)) val id2res: Map[Expr, Expr] = freshsubxs.zip(subproblemxs).map{case (id1, id2) => (Variable(id1), Variable(id2))}.toMap ++ neqxs.map(id => (Variable(id), eqSubstMap(Variable(id)))).toMap - Some(Solution(and(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(letTuple(subproblemxs, freshTerm, replace(id2res, tupleWrap(problem.xs.map(Variable)))))), s.isTrusted)) + Some(Solution( + and(eqPre, freshPre), + defs, + simplifyArithmetic(simplifyLets( + letTuple(subproblemxs, freshTerm, replace(id2res, tupleWrap(problem.xs.map(Variable)))) + )), + isTrusted + )) } case _ => diff --git a/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala index 602a7e61ba1e94c174f44cc71c04790feeb636f6..8ef51a44db038af0990f0a35e8bac5f154713a15 100644 --- a/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala +++ b/src/main/scala/leon/synthesis/rules/unused/IntegerInequalities.scala @@ -175,12 +175,16 @@ case object IntegerInequalities extends Rule("Integer Inequalities") { def onSuccess(sols: List[Solution]): Option[Solution] = sols match { - case List(s @ Solution(pre, defs, term)) => { + case List(s @ Solution(pre, defs, term, isTrusted)) => if(remainderIds.isEmpty) { - Some(Solution(And(newPre, pre), defs, + Some(Solution( + And(newPre, pre), + defs, letTuple(subProblemxs, term, Let(processedVar, witness, - tupleWrap(problem.xs.map(Variable)))), isTrusted=s.isTrusted)) + tupleWrap(problem.xs.map(Variable)))), + isTrusted + )) } else if(remainderIds.size > 1) { sys.error("TODO") } else { @@ -207,7 +211,6 @@ case object IntegerInequalities extends Rule("Integer Inequalities") { Some(Solution(And(newPre, pre), defs + funDef, FunctionInvocation(funDef.typed, Seq(IntLiteral(L-1))))) } - } case _ => None }