diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala index ce34ab79cc7f40c5c8ea00ec3a24a153262616dc..3f9f54859ad19375aa024fbc58671529170404a2 100644 --- a/src/main/scala/leon/synthesis/Heuristics.scala +++ b/src/main/scala/leon/synthesis/Heuristics.scala @@ -273,11 +273,56 @@ class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 5 def closedFormula = And(f :: recTerms.keySet.map(id => Not(Variable(id))).toList) } - println("Formula is: "+p.phi) - val initF = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x))) // Set to expand on xs - println("unroll 1: "+initF.unroll.closedFormula) - println("unroll 2: "+initF.unroll.unroll.closedFormula) + var result: Option[RuleResult] = None - RuleInapplicable + var ass = p.as.toSet + + var lastF = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x))) + var currentF = lastF.unroll + var unrolings = 0 + do { + println("Was: "+lastF.closedFormula) + println("Now Trying : "+currentF.closedFormula) + + val tpe = TupleType(p.xs.map(_.getType)) + + var i = 0; + var maxTries = 10; + + var predicates: Seq[Expr] = Seq() + + while (result.isEmpty && i < maxTries) { + val phi = And(currentF.closedFormula +: predicates) + synth.solver.solveSAT(phi) match { + case (Some(true), satModel) => + val notAss = satModel.keySet.filterNot(ass) + val satXsModel = satModel.filterKeys(notAss) + + val newPhi = valuateWithModelIn(phi, notAss, satModel) + + synth.solver.solveSAT(Not(newPhi)) match { + case (Some(true), invalidModel) => + // Found as such as the xs break, refine predicates + predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates + + case (Some(false), _) => + result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe)))) + + case _ => + } + + case (Some(false), _) => + case _ => + } + + i += 1 + } + + lastF = currentF + currentF = lastF.unroll + unrolings += 1 + } while(unrolings < 5 && lastF != currentF && result.isEmpty) + + result.getOrElse(RuleInapplicable) } }