CEGIS is now faster, and also actually correct.

src/main/scala/leon/synthesis/heuristics/IntInduction.scala

@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 import purescala.Definitions._
 
-class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 80) with Heuristic {
+class IntInduction(synth: Synthesizer) extends Rule("Int Induction", synth, 50) with Heuristic {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 

src/main/scala/leon/synthesis/rules/ADTSplit.scala

@@ -18,9 +18,9 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
 
         val optCases = for (dcd <- cd.knownDescendents) yield dcd match {
           case ccd : CaseClassDef =>
-            val toVal = Implies(p.c, CaseClassInstanceOf(ccd, Variable(id)))
+            val toSat = And(p.c, Not(CaseClassInstanceOf(ccd, Variable(id))))
 
-            val isImplied = synth.solver.solveSAT(Not(toVal)) match {
+            val isImplied = synth.solver.solveSAT(toSat) match {
               case (Some(false), _) => true
               case _ => false
             }
@@ -49,13 +49,11 @@ class ADTSplit(synth: Synthesizer) extends Rule("ADT Split.", synth, 70) {
         val oas = p.as.filter(_ != id)
 
         val subInfo = for(ccd <- cases) yield {
-           val subId  = FreshIdentifier(ccd.id.name, true).setType(CaseClassType(ccd))
            val args   = ccd.fieldsIds.map(id => FreshIdentifier(id.name, true).setType(id.getType)).toList
-           val subPre = Equals(CaseClass(ccd, args.map(Variable(_))), Variable(subId))
 
-           val subPhi = subst(id -> Variable(subId), p.phi)
-           val subProblem = Problem(subId :: args ::: oas, And(p.c, subPre), subPhi, p.xs)
-           val subPattern = CaseClassPattern(Some(subId), ccd, args.map(id => WildcardPattern(Some(id))))
+           val subPhi = subst(id -> CaseClass(ccd, args.map(Variable(_))), p.phi)
+           val subProblem = Problem(args ::: oas, p.c, subPhi, p.xs)
+           val subPattern = CaseClassPattern(None, ccd, args.map(id => WildcardPattern(Some(id))))
 
            (ccd, subProblem, subPattern)
         }

src/main/scala/leon/synthesis/rules/Cegis.scala

@@ -64,7 +64,8 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
       p.as.filter(a => isSubtypeOf(a.getType, t)).map(id => (Variable(id) : Expr, Set[Identifier]()))
     }
 
-    case class TentativeFormula(phi: Expr,
+    case class TentativeFormula(pathcond: Expr,
+                                phi: Expr,
                                 program: Expr,
                                 mappings: Map[Identifier, (Identifier, Expr)],
                                 recTerms: Map[Identifier, Set[Identifier]]) {
@@ -100,13 +101,13 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
           newProgram = newProgram ::: pre :: cases
         }
 
-        TentativeFormula(phi, And(program :: newProgram), mappings ++ newMappings, newRecTerms)
+        TentativeFormula(pathcond, phi, And(program :: newProgram), mappings ++ newMappings, newRecTerms)
       }
 
       def bounds = recTerms.keySet.map(id => Not(Variable(id))).toList
       def bss = mappings.keySet
 
-      def entireFormula = And(phi :: program :: bounds)
+      def entireFormula = And(pathcond :: phi :: program :: bounds)
     }
 
     var result: Option[RuleResult]   = None
@@ -114,11 +115,12 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
     var ass = p.as.toSet
     var xss = p.xs.toSet
 
-    var lastF     = TentativeFormula(Implies(p.c, p.phi), BooleanLiteral(true), Map(), Map() ++ p.xs.map(x => x -> Set(x)))
+    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 = 2
     do {
+      //println("="*80)
       //println("Was: "+lastF.entireFormula)
       //println("Now Trying : "+currentF.entireFormula)
 
@@ -141,15 +143,43 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
             val fixedBss = And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)
             //println("Phi with fixed sat bss: "+fixedBss)
 
-            val counterPhi = Implies(And(fixedBss, currentF.program), currentF.phi)
+            val counterPhi = And(Seq(currentF.pathcond, fixedBss, currentF.program, Not(currentF.phi)))
             //println("Formula to validate: "+counterPhi)
 
-            synth.solver.solveSAT(Not(counterPhi)) match {
+            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)
-                predicates = Not(And(bss.map(b => Equals(Variable(b), satModel(b))).toSeq)) +: predicates
-                //println("Let's avoid this case: "+bss.map(b => Equals(Variable(b), satModel(b))).mkString(" "))
+                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(", "))

src/main/scala/leon/synthesis/rules/IntegerEquation.scala

@@ -46,6 +46,9 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
       case None => RuleInapplicable
       case Some(normalizedEq0) => {
 
+        println(problem.phi)
+        println(normalizedEq0)
+
         val eqas = problem.as.toSet.intersect(vars)
 
         val (neqxs, normalizedEq1) = eqxs.zip(normalizedEq0.tail).filterNot{ case (_, IntLiteral(0)) => true case _ => false}.unzip