Some fixes and simplifications

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) {}
       }
 

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
     }
   }
 

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)
     }))
   }

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
           }
       }
     }

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))
   }
 }