diff --git a/src/main/scala/leon/aographs/Graph.scala b/src/main/scala/leon/aographs/Graph.scala
index 6519fe3b54e17bbb951fabe8c9256ac2390e501c..2ef04e2a79c2afd24db38c84a7cbec6210659bb7 100644
--- a/src/main/scala/leon/aographs/Graph.scala
+++ b/src/main/scala/leon/aographs/Graph.scala
@@ -112,7 +112,7 @@ class AndOrGraph[T <: AOTask[S], S <: AOSolution](val root: T) {
object RootNode extends AndLeaf(null, root) {
override def expandWith(succ: List[T]) {
val n = new AndNode(null, succ, task) {
- override def unsolvable(l: Tree) {}
+ override def unsolvable(l: Tree) { println("Root was unsolvable!") }
override def notifyParent(sol: S) {}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 928d7e31c7f1a117afe40172493d3a39e7511261..6787da103eb2ea5f23ee11dd56832439fb499c46 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -22,15 +22,15 @@ trait Heuristic {
}
object HeuristicStep {
- def verifyPre(synth: Synthesizer, problem: Problem)(s: Solution): (Solution, Boolean) = {
+ def verifyPre(synth: Synthesizer, problem: Problem)(s: Solution): Solution = {
synth.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
case (Some(true), model) =>
synth.reporter.warning("Heuristic failed to produce weakest precondition:")
synth.reporter.warning(" - problem: "+problem)
synth.reporter.warning(" - precondition: "+s.pre)
- (s, false)
+ s
case _ =>
- (s, true)
+ s
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 8602b74fbb3c583ee8c65b0da908a4075eb951d2..8fac72bce61e7598ff3a48f8ce74bcdf954a437d 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -30,18 +30,21 @@ case class RuleResult(alternatives: Traversable[RuleApplication])
object RuleInapplicable extends RuleResult(List())
abstract class RuleApplication(val subProblemsCount: Int,
- val onSuccess: List[Solution] => (Solution, Boolean)) {
+ val onSuccess: List[Solution] => Solution) {
def apply(): RuleApplicationResult
}
+abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
+
sealed abstract class RuleApplicationResult
case class RuleSuccess(solution: Solution) extends RuleApplicationResult
-case class RuleDecomposed(sub: List[Problem], onSuccess: List[Solution] => (Solution, Boolean)) extends RuleApplicationResult
+case class RuleDecomposed(sub: List[Problem], onSuccess: List[Solution] => Solution) extends RuleApplicationResult
+case object RuleApplicationImpossible extends RuleApplicationResult
object RuleFastApplication {
def apply(sub: List[Problem], onSuccess: List[Solution] => Solution) = {
- new RuleApplication(sub.size, ls => (onSuccess(ls), true)) {
+ new RuleApplication(sub.size, onSuccess) {
def apply() = RuleDecomposed(sub, onSuccess)
}
}
@@ -55,7 +58,7 @@ object RuleFastStep {
object RuleFastSuccess {
def apply(solution: Solution) = {
- RuleResult(List(new RuleApplication(0, ls => (solution, true)) {
+ RuleResult(List(new RuleApplication(0, ls => solution) {
def apply() = RuleSuccess(solution)
}))
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 8e2953edf6c6c2d42f2c0610010cae2c745ff3ac..efd82997a400e320ac8bba0affe1b6f37988eea9 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -29,15 +29,15 @@ class Synthesizer(val reporter: Reporter,
def synthesize(): Solution = {
- 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)
- }
- })
+ //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)
+ // }
+ //})
/*
if (generateDerivationTrees) {
@@ -64,10 +64,10 @@ class Synthesizer(val reporter: Reporter,
val subSols = (1 to app.subProblemsCount).map {i => Solution.simplest }.toList
val simpleSol = app.onSuccess(subSols)
- def cost = SolutionCost(simpleSol._1)
+ def cost = SolutionCost(simpleSol)
def composeSolution(sols: List[Solution]): Solution = {
- app.onSuccess(sols)._1
+ app.onSuccess(sols)
}
}
@@ -86,17 +86,18 @@ class Synthesizer(val reporter: Reporter,
val sub = rules.flatMap ( r => r.attemptToApplyOn(t.p).alternatives.map(TaskRunRule(t.p, r, _)) )
if (!sub.isEmpty) {
+ println("Was able to apply rules: "+sub.map(_.rule))
Expanded(sub.toList)
} else {
ExpandFailure
}
- case t: TaskRunRule=>
+ case t: TaskRunRule =>
val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
+ info(prefix+"Got: "+t.problem)
t.app.apply() match {
case RuleSuccess(sol) =>
- info(prefix+"Got: "+t.problem)
info(prefix+"Solved with: "+sol)
ExpandSuccess(sol)
@@ -108,6 +109,9 @@ class Synthesizer(val reporter: Reporter,
}
Expanded(sub.map(TaskTryRules(_)))
+
+ case RuleApplicationImpossible =>
+ ExpandFailure
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 80decb7fb90462d58d8cf9979201e29d9b367be9..50b9445322635c9f1bc171d8f96adaea163f648b 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -108,109 +108,115 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
def entireFormula = And(pathcond :: phi :: program :: bounds)
}
- var result: Option[RuleResult] = None
-
- var ass = p.as.toSet
- var xss = p.xs.toSet
-
- var lastF = TentativeFormula(p.c, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
- var currentF = lastF.unroll
- var unrolings = 0
- val maxUnrolings = 3
- var predicates: Seq[Expr] = Seq()
- do {
- //println("="*80)
- //println("Was: "+lastF.entireFormula)
- //println("Now Trying : "+currentF.entireFormula)
-
- val tpe = TupleType(p.xs.map(_.getType))
- val bss = currentF.bss
-
- var continue = true
-
- while (result.isEmpty && continue && synth.continue) {
- val basePhi = currentF.entireFormula
- val constrainedPhi = And(basePhi +: predicates)
- //println("-"*80)
- //println("To satisfy: "+constrainedPhi)
- synth.solver.solveSAT(constrainedPhi) match {
- case (Some(true), satModel) =>
- //println("Found candidate!: "+satModel.filterKeys(bss))
-
- //println("Corresponding program: "+simplifyTautologies(synth.solver)(valuateWithModelIn(currentF.program, bss, satModel)))
- val fixedBss = And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)
- //println("Phi with fixed sat bss: "+fixedBss)
-
- val counterPhi = And(Seq(currentF.pathcond, fixedBss, currentF.program, Not(currentF.phi)))
- //println("Formula to validate: "+counterPhi)
-
- synth.solver.solveSAT(counterPhi) match {
- case (Some(true), invalidModel) =>
- val fixedAss = And(ass.map(a => Equals(Variable(a), invalidModel(a))).toSeq)
-
- val mustBeUnsat = And(currentF.pathcond :: currentF.program :: fixedAss :: currentF.phi :: Nil)
-
- val bssAssumptions: Set[Expr] = bss.toSet.map { b: Identifier => satModel(b) match {
- case BooleanLiteral(true) => Variable(b)
- case BooleanLiteral(false) => Not(Variable(b))
- }}
-
- val unsatCore = synth.solver.solveSATWithCores(mustBeUnsat, bssAssumptions) match {
- case ((Some(false), _, core)) =>
- //println("Formula: "+mustBeUnsat)
- //println("Core: "+core)
- //println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq)))
- //println("maxcore: "+bssAssumptions)
- if (core.isEmpty) {
- synth.reporter.warning("Got empty core, must be unsat without assumptions!")
- Set()
+ val res = new RuleImmediateApplication {
+ def apply() = {
+ var result: Option[RuleApplicationResult] = None
+
+ var ass = p.as.toSet
+ var xss = p.xs.toSet
+
+ var lastF = TentativeFormula(p.c, p.phi, BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+ var currentF = lastF.unroll
+ var unrolings = 0
+ val maxUnrolings = 3
+ var predicates: Seq[Expr] = Seq()
+ do {
+ //println("="*80)
+ //println("Was: "+lastF.entireFormula)
+ //println("Now Trying : "+currentF.entireFormula)
+
+ val tpe = TupleType(p.xs.map(_.getType))
+ val bss = currentF.bss
+
+ var continue = true
+
+ while (result.isEmpty && continue && synth.continue) {
+ val basePhi = currentF.entireFormula
+ val constrainedPhi = And(basePhi +: predicates)
+ //println("-"*80)
+ //println("To satisfy: "+constrainedPhi)
+ synth.solver.solveSAT(constrainedPhi) match {
+ case (Some(true), satModel) =>
+ //println("Found candidate!: "+satModel.filterKeys(bss))
+
+ //println("Corresponding program: "+simplifyTautologies(synth.solver)(valuateWithModelIn(currentF.program, bss, satModel)))
+ val fixedBss = And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)
+ //println("Phi with fixed sat bss: "+fixedBss)
+
+ val counterPhi = And(Seq(currentF.pathcond, fixedBss, currentF.program, Not(currentF.phi)))
+ //println("Formula to validate: "+counterPhi)
+
+ synth.solver.solveSAT(counterPhi) match {
+ case (Some(true), invalidModel) =>
+ val fixedAss = And(ass.map(a => Equals(Variable(a), invalidModel(a))).toSeq)
+
+ val mustBeUnsat = And(currentF.pathcond :: currentF.program :: fixedAss :: currentF.phi :: Nil)
+
+ val bssAssumptions: Set[Expr] = bss.toSet.map { b: Identifier => satModel(b) match {
+ case BooleanLiteral(true) => Variable(b)
+ case BooleanLiteral(false) => Not(Variable(b))
+ }}
+
+ val unsatCore = synth.solver.solveSATWithCores(mustBeUnsat, bssAssumptions) match {
+ case ((Some(false), _, core)) =>
+ //println("Formula: "+mustBeUnsat)
+ //println("Core: "+core)
+ //println(synth.solver.solveSAT(And(mustBeUnsat +: bssAssumptions.toSeq)))
+ //println("maxcore: "+bssAssumptions)
+ if (core.isEmpty) {
+ synth.reporter.warning("Got empty core, must be unsat without assumptions!")
+ Set()
+ } else {
+ core
+ }
+ case _ =>
+ bssAssumptions
+ }
+
+ // Found as such as the xs break, refine predicates
+ //println("Found counter EX: "+invalidModel)
+ if (unsatCore.isEmpty) {
+ continue = false
} else {
- core
+ predicates = Not(And(unsatCore.toSeq)) +: predicates
}
- case _ =>
- bssAssumptions
- }
- // Found as such as the xs break, refine predicates
- //println("Found counter EX: "+invalidModel)
- if (unsatCore.isEmpty) {
- continue = false
- } else {
- predicates = Not(And(unsatCore.toSeq)) +: predicates
- }
+ case (Some(false), _) =>
+ //println("Sat model: "+satModel.toSeq.sortBy(_._1.toString).map{ case (id, v) => id+" -> "+v }.mkString(", "))
+ var mapping = currentF.mappings.filterKeys(satModel.mapValues(_ == BooleanLiteral(true))).values.toMap
- case (Some(false), _) =>
- //println("Sat model: "+satModel.toSeq.sortBy(_._1.toString).map{ case (id, v) => id+" -> "+v }.mkString(", "))
- var mapping = currentF.mappings.filterKeys(satModel.mapValues(_ == BooleanLiteral(true))).values.toMap
+ //println("Mapping: "+mapping)
- //println("Mapping: "+mapping)
+ // Resolve mapping
+ for ((c, e) <- mapping) {
+ mapping += c -> substAll(mapping, e)
+ }
- // Resolve mapping
- for ((c, e) <- mapping) {
- mapping += c -> substAll(mapping, e)
- }
+ result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
- result = Some(RuleFastSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
+ case _ =>
+ synth.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ continue = false
+ }
+ case (Some(false), _) =>
+ //println("%%%% UNSAT")
+ continue = false
case _ =>
- synth.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+ //println("%%%% WOOPS")
continue = false
}
+ }
- case (Some(false), _) =>
- //println("%%%% UNSAT")
- continue = false
- case _ =>
- //println("%%%% WOOPS")
- continue = false
- }
- }
+ lastF = currentF
+ currentF = currentF.unroll
+ unrolings += 1
+ } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
- lastF = currentF
- currentF = currentF.unroll
- unrolings += 1
- } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty && synth.continue)
+ result.getOrElse(RuleApplicationImpossible)
+ }
+ }
- result.getOrElse(RuleInapplicable)
+ RuleResult(List(res))
}
}