diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index 1c045aabb35882606b408df6a294ede5699f098e..b2792da85cbc65a4f7cc9fdd1a53519c7434c352 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -256,24 +256,17 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) { val TopLevelAnds(exprs) = p.phi - val (toRemove, toAdd, toPre) = exprs.collect { + val (toRemove, toAdd) = exprs.collect { case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty => - (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) ) + (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } ) case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty => - (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) ) - }.unzip3 + (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } ) + }.unzip if (!toRemove.isEmpty) { val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq)) - val onSuccess: List[Solution] => Solution = { - case List(s) => - Solution(And(s.pre +: toPre), s.term) - case _ => - Solution.none - } - - List(task.decompose(this, List(sub), onSuccess, 80)) + List(task.decompose(this, List(sub), forward, 80)) } else { Nil } diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 2b927cad09ac10ae4134fcf4cdea0526c86a99c7..9361e2c92de1645ba8040177270e1a8a686e43b1 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -95,7 +95,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) { val sol = synthesize(Problem(as, phi, xs), rules) info("Scala code:") - info(ScalaPrinter(sol.term)) + info(ScalaPrinter(IfExpr(sol.pre, sol.term, Error("Precondition failed").setType(sol.term.getType)))) a case _ =>