diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 56249605f64c06323bd402917978b61226aae52f..46c7bab49c6e38c25281406eee5f25dc2291f292 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -2083,16 +2083,6 @@ object TreeOps {
None
}
- // Remove terminating/guiding witnesses that bother solvers
- def removeWitnesses(prog: Program)(e: Expr): Expr = {
- val witnesses = Set() ++ prog.library.guide ++ prog.library.terminating
-
- postMap {
- case FunctionInvocation(TypedFunDef(fd, _), _) if witnesses contains fd => Some(BooleanLiteral(true))
- case _ => None
- }(e)
- }
-
/**
* Deprecated API
* ========
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index 37bf364613d2c08d9bcb267d1b6da367fb196aa4..de119dbc2edc11b9ae17ee2b6ff3a752a405c25f 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -73,14 +73,13 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
passes
)
- val pc = and(
- pre,
+ val ws = and(
guide,
terminating
)
// Synthesis from the ground up
- val p = Problem(fd.params.map(_.id).toList, pc, spec, List(out))
+ val p = Problem(fd.params.map(_.id).toList, ws, pre, spec, List(out))
val ch = Choose(List(out), spec)
// do we really want to do that?
fd.body = Some(ch)
@@ -96,7 +95,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
)) diff Seq(ADTInduction)
);
- ChooseInfo(ctx, program, fd, pc, gexpr, ch, soptions)
+ ChooseInfo(ctx, program, fd, pre, gexpr, ch, soptions)
}
def repair(): Unit = {
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 36e1e3ff2f2f1c1ba5fab5b968976ffddf96dde1..b3959f35c6c7034124a5db1a3f6b8d3b5505a3ce 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -10,10 +10,9 @@ import leon.purescala.Common._
import leon.purescala.Constructors._
// Defines a synthesis triple of the form:
-// ⟦ as ⟨ C | phi ⟩ xs ⟧
-case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
- override def toString =
- "⟦ "+as.mkString(";")+", " + (if (pc != BooleanLiteral(true)) pc+" ≺ " else "") + " ⟨ "+phi+" ⟩ " + xs.mkString(";") + " ⟧ "
+// ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
+case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier]) {
+ override def toString = "⟦ "+as.mkString(";")+", "+(if (ws != BooleanLiteral(true)) ws+" - " else "")+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
def getTests(sctx: SynthesisContext): Seq[Example] = {
import purescala.Extractors._
@@ -23,14 +22,12 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
val ev = new DefaultEvaluator(sctx.context, sctx.program)
- val safePc = removeWitnesses(sctx.program)(pc)
-
def isValidExample(ex: Example): Boolean = {
val (mapping, cond) = ex match {
case io: InOutExample =>
- (Map((as zip io.ins) ++ (xs zip io.outs): _*), And(safePc, phi))
+ (Map((as zip io.ins) ++ (xs zip io.outs): _*), And(pc, phi))
case i =>
- ((as zip i.ins).toMap, safePc)
+ ((as zip i.ins).toMap, pc)
}
ev.eval(cond, mapping) match {
@@ -212,6 +209,6 @@ object Problem {
val phi = simplifyLets(ch.pred)
val as = (variablesOf(And(pc, phi))--xs).toList
- Problem(as, pc, phi, xs)
+ Problem(as, BooleanLiteral(true), pc, phi, xs)
}
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index be9d37584100c5bd9ac2dca599d25e4c652a3494..c55673a64766e17c347e862f80b84fc3c34f3031 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -43,6 +43,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
val innerPhi = substAll(substMap, p.phi)
val innerPC = substAll(substMap, p.pc)
+ val innerWS = substAll(substMap, p.ws)
val subProblemsInfo = for (cct <- ct.knownCCDescendents) yield {
var recCalls = Map[List[Identifier], List[Expr]]()
@@ -66,10 +67,11 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
val subPhi = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerPhi)
val subPC = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerPC)
+ val subWS = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable(_)))), innerWS)
val subPre = CaseClassInstanceOf(cct, Variable(origId))
- val subProblem = Problem(inputs ::: residualArgs, andJoin(subPC :: postFs), subPhi, p.xs)
+ val subProblem = Problem(inputs ::: residualArgs, subWS, andJoin(subPC :: postFs), subPhi, p.xs)
(subProblem, subPre, cct, newIds, recCalls)
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index 033dfd592e398380dafa3e6a2bf8aace2acdefe1..1455331223860b0f0c6204be91d10358ce6d4cd7 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -95,6 +95,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
val innerPhi = substAll(substMap, p.phi)
val innerPC = substAll(substMap, p.pc)
+ val innerWS = substAll(substMap, p.ws)
val subProblemsInfo = for (c <- cases) yield {
val InductCase(ids, calls, pat, pc, trMap) = c
@@ -104,6 +105,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
var recCalls = Map[List[Identifier], List[Expr]]()
val subPC = substAll(trMap, innerPC)
+ val subWS = substAll(trMap, innerWS)
val subPhi = substAll(trMap, innerPhi)
var postXss = List[Identifier]()
@@ -118,7 +120,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
recCalls += postXs -> (Variable(cid) +: residualArgs.map(id => Variable(id)))
}
- val subProblem = Problem(c.ids ::: postXss, andJoin(subPC :: postFs), subPhi, p.xs)
+ val subProblem = Problem(c.ids ::: postXss, subWS, andJoin(subPC :: postFs), subPhi, p.xs)
//println(subProblem)
//println(recCalls)
(subProblem, pat, recCalls, pc)
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 71a2f3e9526641c4d9e909d5eb15e710f95b6bcf..a6f0d31794046b4d775c7841380035145ac5abd3 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -26,12 +26,13 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
val newPhi = subst(origId -> Variable(inductOn), p.phi)
val newPc = subst(origId -> Variable(inductOn), p.pc)
+ val newWs = subst(origId -> Variable(inductOn), p.ws)
val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi)
val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
- val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.pc), subst(origId -> IntLiteral(0), p.phi), p.xs)
- val subGT = Problem(inductOn :: postXs, and(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, newPc), newPhi, p.xs)
- val subLT = Problem(inductOn :: postXs, and(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, newPc), newPhi, p.xs)
+ val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.ws), subst(origId -> IntLiteral(0), p.pc), subst(origId -> IntLiteral(0), p.phi), p.xs)
+ val subGT = Problem(inductOn :: postXs, newWs, and(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, newPc), newPhi, p.xs)
+ val subLT = Problem(inductOn :: postXs, newWs, and(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, newPc), newPhi, p.xs)
val onSuccess: List[Solution] => Option[Solution] = {
case List(base, gt, lt) =>
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 16ca8f15f325de5a0caab01e2cce5539ddf4fb6f..4453212ffbfcc4c2bea70c6630b975cc38f577d5 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -23,7 +23,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val optCases = for (dcd <- cd.knownDescendents.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
val cct = CaseClassType(ccd, tpes)
- val toSat = and(removeWitnesses(sctx.program)(p.pc), CaseClassInstanceOf(cct, Variable(id)))
+ val toSat = and(p.pc, CaseClassInstanceOf(cct, Variable(id)))
val isImplied = solver.solveSAT(toSat) match {
case (Some(false), _) => true
@@ -59,7 +59,8 @@ case object ADTSplit extends Rule("ADT Split.") {
val subPhi = subst(id -> CaseClass(cct, args.map(Variable(_))), p.phi)
val subPC = subst(id -> CaseClass(cct, args.map(Variable(_))), p.pc)
- val subProblem = Problem(args ::: oas, subPC, subPhi, p.xs)
+ val subWS = subst(id -> CaseClass(cct, args.map(Variable(_))), p.ws)
+ val subProblem = Problem(args ::: oas, subWS, subPC, subPhi, p.xs)
val subPattern = CaseClassPattern(None, cct, args.map(id => WildcardPattern(Some(id))))
(cct, subProblem, subPattern)
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 5ec5e3b0f75262f933ceaa518c4443552626ccef..5967bc4e6c859d0fb259fa59770428c73d085104 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -20,7 +20,7 @@ case object CaseSplit extends Rule("Case-Split") {
}
def split(alts: Seq[Expr], p: Problem, description: String): RuleInstantiation = {
- val subs = alts.map(a => Problem(p.as, p.pc, a, p.xs)).toList
+ val subs = alts.map(a => Problem(p.as, p.ws, p.pc, a, p.xs)).toList
val onSuccess: List[Solution] => Option[Solution] = {
case sols if sols.size == subs.size =>
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 5470b1769f0557f935098e9763eaa011e7289f85..a458f51f1c7b7fd2ebdf6706b4aba6617e1c65f1 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -182,7 +182,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// Map each x generated by the program to fresh xs passed as argument
val newXs = p.xs.map(x => x -> FreshIdentifier(x.name, true).setType(x.getType))
- val baseExpr = removeWitnesses(sctx.program)(p.phi)
+ val baseExpr = p.phi
bssOrdered = bss.toSeq.sortBy(_.id)
@@ -429,14 +429,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
baseExampleInputs ++= p.getTests(sctx).map(_.ins).toSet
- val safePc = removeWitnesses(sctx.program)(p.pc)
+ val pc = p.pc
- if (safePc == BooleanLiteral(true)) {
+ if (pc == BooleanLiteral(true)) {
baseExampleInputs += p.as.map(a => simplestValue(a.getType))
} else {
val solver = sctx.newSolver.setTimeout(exSolverTo)
- solver.assertCnstr(safePc)
+ solver.assertCnstr(pc)
try {
solver.check match {
@@ -467,9 +467,9 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
* We generate tests for discarding potential programs
*/
val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
- new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, safePc, 20, 3000)
+ new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, pc, 20, 3000)
} else {
- new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, safePc, 20, 1000)
+ new NaiveDataGen(sctx.context, sctx.program, evaluator).generateFor(p.as, pc, 20, 1000)
}
val cachedInputIterator = new Iterator[Seq[Expr]] {
@@ -501,7 +501,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val res = Equals(Tuple(p.xs.map(Variable(_))), expr)
val solver3 = sctx.newSolver.setTimeout(cexSolverTo)
- solver3.assertCnstr(and(safePc, res, not(p.phi)))
+ solver3.assertCnstr(and(pc, res, not(p.phi)))
try {
solver3.check match {
@@ -523,8 +523,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
// Keep track of collected cores to filter programs to test
var collectedCores = Set[Set[Identifier]]()
- val initExClause = and(safePc, p.phi, Variable(initGuard))
- val initCExClause = and(safePc, not(p.phi), Variable(initGuard))
+ val initExClause = and(pc, p.phi, Variable(initGuard))
+ val initCExClause = and(pc, not(p.phi), Variable(initGuard))
// solver1 is used for the initial SAT queries
var solver1 = sctx.newSolver.setTimeout(exSolverTo)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index ecf0774d66313d5592a8c3300eaa50c587f56fd0..e2345ab76b0fa1a348af7a9aad784f6e1ab9be8f 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -41,6 +41,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
if (p.as.exists(isDecomposable)) {
var subProblem = p.phi
var subPc = p.pc
+ var subWs = p.ws
var reverseMap = Map[Identifier, Expr]()
@@ -50,6 +51,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
subProblem = subst(a -> expr, subProblem)
subPc = subst(a -> expr, subPc)
+ subWs = subst(a -> expr, subWs)
reverseMap ++= map
@@ -62,7 +64,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
val newAs = subAs.flatten
//sctx.reporter.warning("newOuts: " + newOuts.toString)
- val sub = Problem(newAs, subPc, subProblem, p.xs)
+ val sub = Problem(newAs, subWs, subPc, subProblem, p.xs)
val onSuccess: List[Solution] => Option[Solution] = {
case List(sol) =>
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index f64f3f31bc12861696911a3cb4787f55868fec66..592853c846f26342f12169634f08e576a8229d79 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -41,7 +41,7 @@ case object DetupleOutput extends Rule("Detuple Out") {
val newOuts = subOuts.flatten
- val sub = Problem(p.as, p.pc, subProblem, newOuts)
+ val sub = Problem(p.as, p.ws, p.pc, subProblem, newOuts)
val onSuccess: List[Solution] => Option[Solution] = {
case List(sol) =>
diff --git a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala b/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
index 45599ec7c29e2286191b1232171e881cb51c0520..0cc03942c364ec52da59e20cc0d1a9342bf59491 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedCloser.scala
@@ -17,7 +17,7 @@ import solvers._
case object GuidedCloser extends NormalizingRule("Guided Closer") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val TopLevelAnds(clauses) = p.pc
+ val TopLevelAnds(clauses) = p.ws
val guide = sctx.program.library.guide.get
diff --git a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
index af2ad3b6d5e5d84ad4eaf037c300a77bd01c6a98..a5a7418c218a87fa9e08acccedee547ebf5f4d9a 100644
--- a/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/synthesis/rules/GuidedDecomp.scala
@@ -18,7 +18,7 @@ import solvers._
case object GuidedDecomp extends Rule("Guided Decomp") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- val TopLevelAnds(clauses) = p.pc
+ val TopLevelAnds(clauses) = p.ws
val guide = sctx.program.library.guide.get
@@ -26,9 +26,7 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
}
- def simplify(e: Expr): Expr = {
- Simplifiers.forPathConditions(sctx.context, sctx.program)(e)
- }
+ val simplify = Simplifiers.bestEffort(sctx.context, sctx.program)_
def doSubstitute(substs: Seq[(Expr, Expr)], e: Expr): Expr = {
var res = e
@@ -40,8 +38,8 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val alts = guides.collect {
case g @ IfExpr(c, thn, els) =>
- val sub1 = p.copy(pc = and(c, replace(Map(g -> thn), p.pc)))
- val sub2 = p.copy(pc = and(Not(c), replace(Map(g -> els), p.pc)))
+ val sub1 = p.copy(ws = replace(Map(g -> thn), p.ws), pc = and(c, replace(Map(g -> thn), p.pc)))
+ val sub2 = p.copy(ws = replace(Map(g -> els), p.ws), pc = and(Not(c), replace(Map(g -> els), p.pc)))
val onSuccess: List[Solution] => Option[Solution] = {
case List(s1, s2) =>
@@ -53,7 +51,7 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
Some(RuleInstantiation.immediateDecomp(p, this, List(sub1, sub2), onSuccess, "Guided If-Split on '"+c+"'"))
case m @ MatchExpr(scrut0, cs) =>
-
+
val scrut = scrut0 match {
case v : Variable => v
case _ => Variable(FreshIdentifier("scrut", true).setType(scrut0.getType))
@@ -68,14 +66,15 @@ case object GuidedDecomp extends Rule("Guided Decomp") {
val pc = simplify(and(
scrutCond,
- replace(Map(scrut0 -> scrut),doSubstitute(substs,scrutConstraint)),
+ replace(Map(scrut0 -> scrut), doSubstitute(substs,scrutConstraint)),
replace(Map(scrut0 -> scrut), replace(Map(m -> c.rhs), andJoin(cond)))
))
- val phi = doSubstitute(substs, p.phi)
+ val ws = replace(Map(m -> c.rhs), p.ws)
+ val phi = doSubstitute(substs, p.phi)
val free = variablesOf(and(pc, phi)) -- p.xs
val asPrefix = p.as.filter(free)
- Problem(asPrefix ++ (free -- asPrefix), pc, phi, p.xs)
+ Problem(asPrefix ++ (free -- asPrefix), ws, pc, phi, p.xs)
}
val onSuccess: List[Solution] => Option[Solution] = { subs =>
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index 600e7f1c2ecfacbfa301c2d706096788db30321b..c870f5fe8f3c05ad19f93d252ac55396a45ef3ad 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -30,8 +30,8 @@ case object IfSplit extends Rule("If-Split") {
def split(i: IfExpr, p: Problem, description: String): RuleInstantiation = {
val subs = List(
- Problem(p.as, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs),
- Problem(p.as, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs)
+ Problem(p.as, p.ws, and(p.pc, i.cond), replace(Map(i -> i.thenn), p.phi), p.xs),
+ Problem(p.as, p.ws, and(p.pc, not(i.cond)), replace(Map(i -> i.elze), p.phi), p.xs)
)
val onSuccess: List[Solution] => Option[Solution] = {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index ec7e2ae55ee6140f3559d4cdaf3ccc1099e1dd66..cc9ca0e95891371c8d6db3b7f7d28e035dc6b04e 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -57,7 +57,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
if(normalizedEq.size == 1) {
val eqPre = Equals(normalizedEq.head, IntLiteral(0))
- val newProblem = Problem(problem.as, and(eqPre, problem.pc), andJoin(allOthers), problem.xs)
+ 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)) =>
@@ -94,7 +94,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
val ys: List[Identifier] = problem.xs.filterNot(neqxs.contains(_))
val subproblemxs: List[Identifier] = freshxs ++ ys
- val newProblem = Problem(problem.as ++ freshInputVariables, and(eqPre, problem.pc), freshFormula, subproblemxs)
+ 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)) => {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 0b69b8fd22135be7ebe8c5321f1ebe5efd242735..6101bac28d303ad0af3857724f89f587abbef609 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -174,7 +174,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
newLowerBounds.map(lbound => LessEquals(Variable(k), Minus(b, lbound)))
} ++ exprNotUsed))
val subProblemxs: List[Identifier] = quotientIds ++ otherVars
- val subProblem = Problem(problem.as ++ remainderIds, problem.pc, subProblemFormula, subProblemxs)
+ val subProblem = Problem(problem.as ++ remainderIds, problem.ws, problem.pc, subProblemFormula, subProblemxs)
def onSuccess(sols: List[Solution]): Option[Solution] = sols match {
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 5628e3404a1c7c545cde14224863252c27d7eff2..6c0e81a3c3dfc0d2951903f11f53d2b038af1023 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -31,7 +31,7 @@ case object OnePoint extends NormalizingRule("One-point") {
val others = exprs.filter(_ != eq)
val oxs = p.xs.filter(_ != x)
- val newProblem = Problem(p.as, p.pc, subst(x -> e, andJoin(others)), oxs)
+ 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)) =>
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index e9953f65a17af5b4f1e2eefa3a296c52aa41d376..58eb0f5827450cde0038f9567cc02e3b9cf27fad 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -333,9 +333,9 @@ object ExpressionGrammars {
}
}
- case class SafeRecCalls(prog: Program, pc: Expr) extends ExpressionGrammar[TypeTree] {
+ case class SafeRecCalls(prog: Program, ws: Expr, pc: Expr) extends ExpressionGrammar[TypeTree] {
def computeProductions(t: TypeTree): Seq[Gen] = {
- val calls = terminatingCalls(prog, t, pc)
+ val calls = terminatingCalls(prog, t, ws, pc)
calls.map {
case (e, free) =>
@@ -347,14 +347,14 @@ object ExpressionGrammars {
}
}
- def default(prog: Program, inputs: Seq[Expr], currentFunction: FunDef, pc: Expr): ExpressionGrammar[TypeTree] = {
+ def default(prog: Program, inputs: Seq[Expr], currentFunction: FunDef, ws: Expr, pc: Expr): ExpressionGrammar[TypeTree] = {
BaseGrammar ||
OneOf(inputs) ||
FunctionCalls(prog, currentFunction, inputs.map(_.getType)) ||
- SafeRecCalls(prog, pc)
+ SafeRecCalls(prog, ws, pc)
}
def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
- default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, p.pc)
+ default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, p.ws, p.pc)
}
}
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 98d946485dadb5356f6c5d78367065161896859a..5567c9d7a757d67b2253b80911bf1b89a716eb0b 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -34,10 +34,11 @@ object Helpers {
}
}
- def terminatingCalls(prog: Program, tpe: TypeTree, e: Expr): List[(Expr, Set[Identifier])] = {
+ def terminatingCalls(prog: Program, tpe: TypeTree, ws: Expr, pc: Expr): List[(Expr, Set[Identifier])] = {
+ // TODO: Also allow calls to f(y) when: terminating(f(x)) && y == x.f
val terminating = prog.library.terminating.get
- val TopLevelAnds(clauses) = e
+ val TopLevelAnds(clauses) = ws
val gs: List[FunctionInvocation] = clauses.toList.collect {
case FunctionInvocation(TypedFunDef(`terminating`, _), Seq(fi: FunctionInvocation)) => fi
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index cb57f3fd18f7d70e2b72fb41995509552f22d235..c0ccde86d850bae5cfb7a6e748b9da54c49ced67 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -14,7 +14,6 @@ object Simplifiers {
val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
val simplifiers = List[Expr => Expr](
- removeWitnesses(p) _,
simplifyTautologies(uninterpretedZ3)(_),
simplifyLets _,
simplifyPaths(uninterpretedZ3)(_),
@@ -36,27 +35,6 @@ object Simplifiers {
(new ScopeSimplifier).transform(s)
}
- // Besteffort, but keep witnesses
- def forPathConditions(ctx: LeonContext, p: Program)(e: Expr): Expr = {
- val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))
-
- val simplifiers = List[Expr => Expr](
- simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
- simplifyPaths(uninterpretedZ3)(_),
- rewriteTuples _//,
- //normalizeExpression _
- )
-
- val simple = { expr: Expr =>
- simplifiers.foldLeft(expr){ case (x, sim) =>
- sim(x)
- }
- }
-
- fixpoint(simple, 5)(e)
- }
-
def namePreservingBestEffort(ctx: LeonContext, p: Program)(e: Expr): Expr = {
val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, p))