diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index b07af84b9d889543bfcbbb67bb5686f6cb97b860..6f8f44a45b22fcbd648d9df2d77e5bc42fb9ae07 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 c55673a64766e17c347e862f80b84fc3c34f3031..1e544d8e6fc4e2339f695ed60d799c8c00055705 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 1455331223860b0f0c6204be91d10358ce6d4cd7..36e642990364e8972b14549003ad623f842c62d9 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 a6f0d31794046b4d775c7841380035145ac5abd3..8c593b54ae20aff5f951f4938e20f8149e83cfb9 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 4453212ffbfcc4c2bea70c6630b975cc38f577d5..c4a259d766862ed502b7da7ed9e66aaaa7c90b5c 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 2e33a6dfe7bb07907ea60175f6984c61e7ba3659..eb290799e9fc1a2d643793062b52644afbc6834b 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 5967bc4e6c859d0fb259fa59770428c73d085104..740ef8fd2fc5414aa452cf20a04954e04acb003b 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 e2345ab76b0fa1a348af7a9aad784f6e1ab9be8f..aea676d187c674f627f0efce2678e9dfde39f17c 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 592853c846f26342f12169634f08e576a8229d79..5b5e7578e4049e1132e8c1458e9a94aac373e7a5 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 4740248cb90329164bca07026d0414f4f37cb698..41a995da9a25b4c4ee785aced2cfa3b2cb4571c8 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 c870f5fe8f3c05ad19f93d252ac55396a45ef3ad..e9e34b80d8d7121e736a4f2f0742c065ba4e57db 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 a5ae2bf46d85f3f1f1e1073928153a8adf148b3f..ac9bd86e8f8fa226f800137f935160357ea5e47c 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 cc9ca0e95891371c8d6db3b7f7d28e035dc6b04e..257a48247b5e7d831cc3857c58e1b9feacf94500 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 6101bac28d303ad0af3857724f89f587abbef609..3e56228e488b53e8731ec3caf2be0b0550df8d5e 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 6c0e81a3c3dfc0d2951903f11f53d2b038af1023..2d7c19cfecc50670cebb4ac9bdc47e8f2c49ef3b 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 b349279c5b31a8ab9172ed67314c6bf6c11a9279..becf22f7ae0aa1fa05e2926cfdee61cfa2741b4d 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
}