From 0351d6500d611b178d40db6485755bae553d5362 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 11:02:34 +0200
Subject: [PATCH] Fix Solution unapply, some cleanup
---
.../leon/solvers/string/StringSolver.scala | 30 ++++++++-----------
src/main/scala/leon/synthesis/Solution.scala | 6 ++--
.../scala/leon/synthesis/rules/Assert.scala | 3 +-
.../scala/leon/synthesis/rules/OnePoint.scala | 4 +--
.../rules/unused/IntegerEquation.scala | 15 +++++++---
.../rules/unused/IntegerInequalities.scala | 11 ++++---
6 files changed, 37 insertions(+), 32 deletions(-)
diff --git a/src/main/scala/leon/solvers/string/StringSolver.scala b/src/main/scala/leon/solvers/string/StringSolver.scala
index b717cccf5..baefc4fa7 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 571d42e21..bb0b047fd 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 d7dd317d7..61b356415 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 8665eaf33..1fb5ead14 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 a80963625..7c2d7b251 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 602a7e61b..8ef51a44d 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
}
--
GitLab