diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala index 03ee8d6db6f3bec7250b3358c114277b4f12545c..2bf690f8c7af7ba8efb6a5fe8987aa890433f307 100644 --- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala +++ b/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 diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala index 74dadefe73ed2634e0f1c4b14f0713a7fcb6bd47..f4a90086aba4f603215dbc2448e35794559a08e5 100644 --- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala +++ b/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) } diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala index 6894a035344d5904137e7cc540d342f769e7fe8e..52691946d482c6518553de92d6edf35bae1df35d 100644 --- a/src/main/scala/leon/synthesis/rules/Cegis.scala +++ b/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(", ")) diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala index a3f5f9e6ff408647087a0a3005696cc31d890f0c..08151050351fb9bfb90a4bd1580c0230f629f100 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala +++ b/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