Implement the inner case-split heuristic, extend case-split to Ors with more than two elements
1) Implement inner-case-split heuristic, that distribute And(..,Or(),..) in a case-split. It also pushes Not() inside the formula, so Not(And(a,b)) becomes Or(Not(a), Not(b)) which is then handled by inner-case-split. 2) Extend regular case-split to work with n-way ors. Or(a, .., m,n) gets decomposed into a N-alternatives case-split. Given solutions (Sa, .., Sm, Sn), it recomposes into: If(Sa.pre, Sa.term, If(.., If(Sm.pre, Sm.term, Sn.term)))
Showing
- src/main/scala/leon/purescala/TreeOps.scala 1 addition, 14 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/synthesis/Heuristics.scala 1 addition, 0 deletionssrc/main/scala/leon/synthesis/Heuristics.scala
- src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala 51 additions, 0 deletions...main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
- src/main/scala/leon/synthesis/rules/CaseSplit.scala 22 additions, 9 deletionssrc/main/scala/leon/synthesis/rules/CaseSplit.scala
- testcases/synthesis/InnerSplit.scala 5 additions, 0 deletionstestcases/synthesis/InnerSplit.scala
Loading
Please register or sign in to comment