diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala index 91999a0143ca394f3047a48201fda2c0eb9498bb..37939efa033bd85ca39e6b02ea14643aba328e7b 100644 --- a/src/main/scala/leon/purescala/TreeOps.scala +++ b/src/main/scala/leon/purescala/TreeOps.scala @@ -1210,37 +1210,46 @@ object TreeOps { def simplifyTautologies(solver : Solver)(expr : Expr) : Expr = { def pre(e : Expr) = e match { - case IfExpr(cond, then, elze) => solver.solve(cond) match { - case Some(true) => then - case Some(false) => solver.solve(Not(cond)) match { - case Some(true) => elze - case _ => e + + case IfExpr(cond, then, elze) => + try { + solver.solve(cond) match { + case Some(true) => then + case Some(false) => solver.solve(Not(cond)) match { + case Some(true) => elze + case _ => e + } + case None => e + } + } catch { + // let's give up when the solver crashes + case _ : Exception => e } - case None => e - } + case _ => e } simplePreTransform(pre)(expr) } - // NOTE : this is currently untested, use at your own risk ! - // (or better yet, write tests for it) - // TODO : test and remove this header. - // PS + // This function could be made ridiculously faster by using push/pop... def simplifyPaths(solver : Solver)(expr : Expr) : Expr = { - def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = { + def impliedBy(e : Expr, path : Seq[Expr]) : Boolean = try { solver.solve(Implies(And(path), e)) match { case Some(true) => true case _ => false } + } catch { + case _ : Exception => false } - def contradictedBy(e : Expr, path : Seq[Expr]) : Boolean = { + def contradictedBy(e : Expr, path : Seq[Expr]) : Boolean = try { solver.solve(Implies(And(path), Not(e))) match { case Some(true) => true case _ => false } + } catch { + case _ : Exception => false } def rec(e : Expr, path : Seq[Expr]): Expr = e match { diff --git a/src/main/scala/leon/synthesis/ArithmeticNormalization.scala b/src/main/scala/leon/synthesis/ArithmeticNormalization.scala index f1b3bd269723dcadcf6bef44c4d7936383b8bf7d..1ec71f0fe7d65be64b2ace4aa6208288034eb472 100644 --- a/src/main/scala/leon/synthesis/ArithmeticNormalization.scala +++ b/src/main/scala/leon/synthesis/ArithmeticNormalization.scala @@ -111,6 +111,8 @@ object ArithmeticNormalization { case Times(IntLiteral(i1), Times(t, IntLiteral(i2))) => Times(IntLiteral(i1*i2), t) case Times(IntLiteral(i), UMinus(e)) => Times(IntLiteral(-i), e) case Times(UMinus(e), IntLiteral(i)) => Times(e, IntLiteral(-i)) + case Times(IntLiteral(i1), Division(e, IntLiteral(i2))) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), e) + case Times(IntLiteral(i1), Plus(Division(e1, IntLiteral(i2)), e2)) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), Plus(e1, e2)) case Division(IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 / i2) case Division(e, IntLiteral(1)) => e diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 63db3ca0a70d718ae6aacd84b7c449d29efa866b..f33ffe5c9f6edcdad631e70cbcf0f6f45a0c4cae 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -6,6 +6,7 @@ import purescala.Definitions.{Program, FunDef} import purescala.TreeOps._ import purescala.Trees.{Expr, Not} import purescala.ScalaPrinter +import sun.misc.{Signal, SignalHandler} import solvers.Solver import java.io.File @@ -36,7 +37,10 @@ class Synthesizer(val reporter: Reporter, val worstSolution = Solution.choose(problem) + var continue = true + def synthesize(): Solution = { + continue = true workList.clear() workList += rootTask @@ -51,7 +55,17 @@ class Synthesizer(val reporter: Reporter, } } - while (!workList.isEmpty) { + val sigINT = new Signal("INT") + var oldHandler: SignalHandler = null + oldHandler = Signal.handle(sigINT, new SignalHandler { + def handle(sig: Signal) { + reporter.info("Aborting...") + continue = false; + Signal.handle(sigINT, oldHandler) + } + }) + + while (!workList.isEmpty && continue) { val task = workList.dequeue() val prefix = "[%-20s] ".format(Option(task.rule).map(_.toString).getOrElse("root")) @@ -78,7 +92,19 @@ class Synthesizer(val reporter: Reporter, if (timeoutExpired()) { warning("Timeout reached") - workList.clear() + continue = false + } + } + + if (!workList.isEmpty) { + // We flush the worklist by solving everything with chooses, that should + // rebuild a partial solution + while (!workList.isEmpty) { + val t = workList.dequeue() + + if (t.parent ne null) { + t.parent.partlySolvedBy(t, Solution.choose(t.problem)) + } } } diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala index 0f16842edb1b18c8db65dbd359e6d7b17fcc04f9..307840d69bd3589781bb1dbd168a056f8e27e26a 100644 --- a/src/main/scala/leon/synthesis/rules/Cegis.scala +++ b/src/main/scala/leon/synthesis/rules/Cegis.scala @@ -130,7 +130,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) { var continue = true - while (result.isEmpty && continue) { + while (result.isEmpty && continue && synth.continue) { val basePhi = currentF.entireFormula val constrainedPhi = And(basePhi +: predicates) //println("-"*80) @@ -211,7 +211,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) { lastF = currentF currentF = currentF.unroll unrolings += 1 - } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty) + } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue) result.getOrElse(RuleInapplicable) } diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala index 2bc884b4217bc29fd95e4ea15db10f93181c12a1..4ea9e93f579588cae5911f49ae6e0ccf2ef505a9 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala @@ -72,20 +72,35 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth } val eqSubstMap: Map[Expr, Expr] = neqxs.zip(eqWitness).map{case (id, e) => (Variable(id), simplify(e))}.toMap - val freshFormula = simplify(replace(eqSubstMap, And(allOthers))) + val freshFormula0 = simplify(replace(eqSubstMap, And(allOthers))) + + var freshInputVariables: List[Identifier] = Nil + var equivalenceConstraints: Map[Expr, Expr] = Map() + val freshFormula = simplePreTransform({ + case d@Division(_, _) => { + assert(variablesOf(d).intersect(problem.xs.toSet).isEmpty) + val newVar = FreshIdentifier("d", true).setType(Int32Type) + freshInputVariables ::= newVar + equivalenceConstraints += (Variable(newVar) -> d) + Variable(newVar) + } + case e => e + })(freshFormula0) val ys: List[Identifier] = problem.xs.filterNot(neqxs.contains(_)) val subproblemxs: List[Identifier] = freshxs ++ ys - val newProblem = Problem(problem.as, And(eqPre, problem.c), freshFormula, subproblemxs) + val newProblem = Problem(problem.as ++ freshInputVariables, And(eqPre, problem.c), freshFormula, subproblemxs) val onSuccess: List[Solution] => Solution = { case List(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 - Solution(And(eqPre, pre), defs, simplify(simplifyLets(LetTuple(subproblemxs, term, replace(id2res, Tuple(problem.xs.map(Variable(_)))))))) + Solution(And(eqPre, freshPre), defs, simplify(simplifyLets(LetTuple(subproblemxs, freshTerm, replace(id2res, Tuple(problem.xs.map(Variable(_)))))))) } case _ => Solution.none } diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequality.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala similarity index 93% rename from src/main/scala/leon/synthesis/rules/IntegerInequality.scala rename to src/main/scala/leon/synthesis/rules/IntegerInequalities.scala index fe9b6f14a243bd50dc3e7b0ac585944157e00eb4..e15291969b04171a1776856bd60889f28bde9b5b 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerInequality.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala @@ -11,7 +11,7 @@ import purescala.Definitions._ import LinearEquations.elimVariable import ArithmeticNormalization.simplify -class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", synth, 300) { +class IntegerInequalities(synth: Synthesizer) extends Rule("Integer Inequalities", synth, 300) { def applyOn(task: Task): RuleResult = { val problem = task.problem val TopLevelAnds(exprs) = problem.phi @@ -96,7 +96,7 @@ class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", s val pre = And( for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds) yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))) - RuleSuccess(Solution(BooleanLiteral(true), Set(), IfExpr(pre, witness, Error("precondition violation")))) + RuleSuccess(Solution(pre, Set(), witness)) } else { val L = GCD.lcm((upperBounds ::: lowerBounds).map(_._2)) val newUpperBounds: List[Expr] = upperBounds.map{case (bound, coef) => Times(IntLiteral(L/coef), bound)} @@ -122,12 +122,10 @@ class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", s val newPre = And( for((ub, uc) <- upperBounds; (lb, lc) <- lowerBounds) yield LessEquals(ceilingDiv(lb, IntLiteral(lc)), floorDiv(ub, IntLiteral(uc)))) - Solution(pre, defs, - IfExpr(newPre, - LetTuple(subProblemxs, term, - Let(processedVar, witness, - Tuple(problem.xs.map(Variable(_))))), - Error("Precondition violation"))) + Solution(And(newPre, pre), defs, + LetTuple(subProblemxs, term, + Let(processedVar, witness, + Tuple(problem.xs.map(Variable(_)))))) } else if(upperBounds.isEmpty || lowerBounds.isEmpty) { Solution(pre, defs, LetTuple(otherVars++quotientIds, term, @@ -138,7 +136,7 @@ class IntegerInequality(synth: Synthesizer) extends Rule("Integer Inequality", s } else { val k = remainderIds.head - val loopCounter = Variable(FreshIdentifier("i").setType(Int32Type)) + val loopCounter = Variable(FreshIdentifier("i", true).setType(Int32Type)) val concretePre = replace(Map(Variable(k) -> loopCounter), pre) val concreteTerm = replace(Map(Variable(k) -> loopCounter), term) val returnType = TupleType(problem.xs.map(_.getType)) diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala index 6b015b9afc8fac4a8fbe51828680920b555a2a40..1ae79ce1d04505eabfe7c49c57463864d9735c6d 100644 --- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala +++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala @@ -45,6 +45,10 @@ class UninterpretedZ3SolverTests extends FunSuite { private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil) fDef.body = Some(Plus(Variable(fx), IntLiteral(1))) + // g is a function that is not in the program (on purpose) + private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Int32Type, VarDecl(fx, Int32Type) :: Nil) + gDef.body = Some(Plus(Variable(fx), IntLiteral(1))) + private val minimalProgram = Program( FreshIdentifier("Minimal"), ObjectDef(FreshIdentifier("Minimal"), Seq( @@ -55,6 +59,7 @@ class UninterpretedZ3SolverTests extends FunSuite { private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type)) private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type)) private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil) + private def g(e : Expr) : Expr = FunctionInvocation(gDef, e :: Nil) private val solver = new UninterpretedZ3Solver(silentReporter) solver.setProgram(minimalProgram) @@ -82,4 +87,10 @@ class UninterpretedZ3SolverTests extends FunSuite { // This is true, but that solver shouldn't know it. private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1))) assertUnknown(solver, unknown1) + + test("Expected crash on undefined functions.") { + intercept[Exception] { + solver.solve(Equals(g(x), g(x))) + } + } } diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala index f84c3d3b8934d141ef1a397438b93394d9e5486b..d356e0448e7e5cba3d1414937a8a8059bde3a559 100644 --- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala +++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala @@ -208,6 +208,10 @@ class LinearEquationsSuite extends FunSuite { val c4 = List(IntLiteral(2), IntLiteral(4)) val (pre4, wit4, f4) = elimVariable(Set(aId), t4::c4) + val t5 = Minus(a, b) + val c5 = List(IntLiteral(-60), IntLiteral(-3600)) + val (pre5, wit5, f5) = elimVariable(Set(aId, bId), t5::c5) + } }