From fb3fccf8aa2e9d38b20d50c6b17f95aae3a5cf87 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <etienne.kneuss@epfl.ch> Date: Wed, 17 Dec 2014 17:53:12 +0100 Subject: [PATCH] I have trust issues --- src/main/scala/leon/repair/rules/GuidedDecomp.scala | 3 ++- .../scala/leon/synthesis/heuristics/ADTInduction.scala | 3 ++- .../leon/synthesis/heuristics/ADTLongInduction.scala | 3 ++- .../scala/leon/synthesis/heuristics/IntInduction.scala | 3 ++- src/main/scala/leon/synthesis/rules/ADTSplit.scala | 2 +- src/main/scala/leon/synthesis/rules/Assert.scala | 2 +- src/main/scala/leon/synthesis/rules/CaseSplit.scala | 2 +- src/main/scala/leon/synthesis/rules/DetupleInput.scala | 2 +- src/main/scala/leon/synthesis/rules/DetupleOutput.scala | 2 +- src/main/scala/leon/synthesis/rules/EqualitySplit.scala | 2 +- src/main/scala/leon/synthesis/rules/IfSplit.scala | 2 +- src/main/scala/leon/synthesis/rules/InequalitySplit.scala | 2 +- src/main/scala/leon/synthesis/rules/IntegerEquation.scala | 8 ++++---- .../scala/leon/synthesis/rules/IntegerInequalities.scala | 4 ++-- src/main/scala/leon/synthesis/rules/OnePoint.scala | 4 ++-- .../scala/leon/synthesis/rules/UnconstrainedOutput.scala | 2 +- 16 files changed, 25 insertions(+), 21 deletions(-) diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala index b07af84b9..6f8f44a45 100644 --- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala +++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala @@ -88,7 +88,8 @@ case object GuidedDecomp extends Rule("Guided Decomp") { orJoin(subs.map(_.pre)), subs.map(_.defs).foldLeft(Set[FunDef]())(_ ++ _), if (scrut0 != scrut) Let(scrut.id, scrut0, matchExpr(scrut, cases)) - else matchExpr(scrut, cases) + else matchExpr(scrut, cases), + subs.forall(_.isTrusted) )) } diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala index c55673a64..1e544d8e6 100644 --- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala +++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala @@ -108,7 +108,8 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic { Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet+newFun, - FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))) + FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))), + sols.forall(_.isTrusted) )) } } diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala index 145533122..36e642990 100644 --- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala +++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala @@ -157,7 +157,8 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic { Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet+newFun, - FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))) + FunctionInvocation(newFun.typed, Variable(origId) :: oas.map(Variable(_))), + sols.forall(_.isTrusted) )) } } diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala index a6f0d3179..8c593b54a 100644 --- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala +++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala @@ -61,7 +61,8 @@ case object IntInduction extends Rule("Int Induction") with Heuristic { ) - Some(Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun.typed, Seq(Variable(origId))))) + Some(Solution(preOut, base.defs++gt.defs++lt.defs+newFun, FunctionInvocation(newFun.typed, Seq(Variable(origId))), + Seq(base, gt, lt).forall(_.isTrusted))) } case _ => None diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala index 4453212ff..c4a259d76 100644 --- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala +++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala @@ -77,7 +77,7 @@ case object ADTSplit extends Rule("ADT Split.") { SimpleCase(pattern, sol.term) } - Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases))) + Some(Solution(orJoin(globalPre), sols.flatMap(_.defs).toSet, matchExpr(Variable(id), cases), sols.forall(_.isTrusted))) } Some(RuleInstantiation.immediateDecomp(p, this, subInfo.map(_._2).toList, onSuccess, "ADT Split on '"+id+"'")) diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala index 2e33a6dfe..eb290799e 100644 --- a/src/main/scala/leon/synthesis/rules/Assert.scala +++ b/src/main/scala/leon/synthesis/rules/Assert.scala @@ -24,7 +24,7 @@ case object Assert extends NormalizingRule("Assert") { val sub = p.copy(pc = andJoin(p.pc +: exprsA), phi = andJoin(others)) List(RuleInstantiation.immediateDecomp(p, this, List(sub), { - case Solution(pre, defs, term) :: Nil => Some(Solution(andJoin(exprsA :+ pre), defs, term)) + case (s @ Solution(pre, defs, term)) :: Nil => Some(Solution(andJoin(exprsA :+ pre), defs, term, s.isTrusted)) case _ => None }, "Assert "+andJoin(exprsA))) } diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala index 5967bc4e6..740ef8fd2 100644 --- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala +++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala @@ -31,7 +31,7 @@ case object CaseSplit extends Rule("Case-Split") { val term = prefix.foldRight(last.term) { (s, t) => IfExpr(s.pre, s.term, t) } - Some(Solution(pre, defs, term)) + Some(Solution(pre, defs, term, sols.forall(_.isTrusted))) case _ => None diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala index e2345ab76..aea676d18 100644 --- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala +++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala @@ -70,7 +70,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") { case List(sol) => val newPre = substAll(reverseMap, sol.pre) val newTerm = substAll(reverseMap, sol.term) - Some(Solution(newPre, sol.defs, newTerm)) + Some(Solution(newPre, sol.defs, newTerm, sol.isTrusted)) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala index 592853c84..5b5e7578e 100644 --- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala +++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala @@ -45,7 +45,7 @@ case object DetupleOutput extends Rule("Detuple Out") { val onSuccess: List[Solution] => Option[Solution] = { case List(sol) => - Some(Solution(sol.pre, sol.defs, letTuple(newOuts, sol.term, Tuple(outerOuts)))) + Some(Solution(sol.pre, sol.defs, letTuple(newOuts, sol.term, Tuple(outerOuts)), sol.isTrusted)) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala index 4740248cb..41a995da9 100644 --- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala +++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala @@ -49,7 +49,7 @@ case object EqualitySplit extends Rule("Eq. Split") { val onSuccess: List[Solution] => Option[Solution] = { case List(s1, s2) => - Some(Solution(or(s1.pre, s2.pre), s1.defs++s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term))) + Some(Solution(or(s1.pre, s2.pre), s1.defs++s2.defs, IfExpr(Equals(Variable(a1), Variable(a2)), s1.term, s2.term), s1.isTrusted && s2.isTrusted)) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala index c870f5fe8..e9e34b80d 100644 --- a/src/main/scala/leon/synthesis/rules/IfSplit.scala +++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala @@ -42,7 +42,7 @@ case object IfSplit extends Rule("If-Split") { val defs = ts.defs ++ es.defs val term = IfExpr(i.cond, ts.term, es.term) - Some(Solution(pre, defs, term)) + Some(Solution(pre, defs, term, sols.forall(_.isTrusted))) case _ => None diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala index a5ae2bf46..ac9bd86e8 100644 --- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala +++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala @@ -72,7 +72,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") { sEQ.term, sGT.term)) - Some(Solution(pre, defs, term)) + Some(Solution(pre, defs, term, sols.forall(_.isTrusted))) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala index cc9ca0e95..257a48247 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala @@ -60,8 +60,8 @@ case object IntegerEquation extends Rule("Integer Equation") { val newProblem = Problem(problem.as, problem.ws, and(eqPre, problem.pc), andJoin(allOthers), problem.xs) val onSuccess: List[Solution] => Option[Solution] = { - case List(Solution(pre, defs, term)) => - Some(Solution(and(eqPre, pre), defs, term)) + case List(s @ Solution(pre, defs, term)) => + Some(Solution(and(eqPre, pre), defs, term, s.isTrusted)) case _ => None } @@ -97,14 +97,14 @@ case object IntegerEquation extends Rule("Integer Equation") { val newProblem = Problem(problem.as ++ freshInputVariables, problem.ws, and(eqPre, problem.pc), freshFormula, subproblemxs) val onSuccess: List[Solution] => Option[Solution] = { - case List(Solution(pre, defs, term)) => { + case List(s @ Solution(pre, defs, term)) => { val freshPre = replace(equivalenceConstraints, pre) val freshTerm = replace(equivalenceConstraints, term) val freshsubxs = subproblemxs.map(id => FreshIdentifier(id.name).setType(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, Tuple(problem.xs.map(Variable(_))))))))) + Some(Solution(and(eqPre, freshPre), defs, simplifyArithmetic(simplifyLets(LetTuple(subproblemxs, freshTerm, replace(id2res, Tuple(problem.xs.map(Variable(_))))))), s.isTrusted)) } case _ => diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala index 6101bac28..3e56228e4 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala @@ -178,12 +178,12 @@ case object IntegerInequalities extends Rule("Integer Inequalities") { def onSuccess(sols: List[Solution]): Option[Solution] = sols match { - case List(Solution(pre, defs, term)) => { + case List(s @ Solution(pre, defs, term)) => { if(remainderIds.isEmpty) { Some(Solution(And(newPre, pre), defs, LetTuple(subProblemxs, term, Let(processedVar, witness, - Tuple(problem.xs.map(Variable(_))))))) + Tuple(problem.xs.map(Variable(_))))), isTrusted=s.isTrusted)) } else if(remainderIds.size > 1) { sys.error("TODO") } else { diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala index 6c0e81a3c..2d7c19cfe 100644 --- a/src/main/scala/leon/synthesis/rules/OnePoint.scala +++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala @@ -34,8 +34,8 @@ case object OnePoint extends NormalizingRule("One-point") { val newProblem = Problem(p.as, p.ws, p.pc, subst(x -> e, andJoin(others)), oxs) val onSuccess: List[Solution] => Option[Solution] = { - case List(Solution(pre, defs, term)) => - Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))))) + case List(s @ Solution(pre, defs, term)) => + Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_))))), s.isTrusted)) case _ => None } diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala index b349279c5..becf22f7a 100644 --- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala +++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala @@ -20,7 +20,7 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") { case List(s) => val term = letTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id)))) - Some(Solution(s.pre, s.defs, term)) + Some(Solution(s.pre, s.defs, term, s.isTrusted)) case _ => None } -- GitLab