-
- Downloads
Introduce Hints in synthesis
Rules that decompose variables (e.g. ADTSplit) introduce the previous recomposed expression as a Hint. These Hints are used by the default grammar when they are of a specific size upwards (currently 4).
Showing
- src/main/scala/leon/grammars/Grammars.scala 7 additions, 2 deletionssrc/main/scala/leon/grammars/Grammars.scala
- src/main/scala/leon/synthesis/Problem.scala 5 additions, 0 deletionssrc/main/scala/leon/synthesis/Problem.scala
- src/main/scala/leon/synthesis/Witnesses.scala 8 additions, 0 deletionssrc/main/scala/leon/synthesis/Witnesses.scala
- src/main/scala/leon/synthesis/rules/ADTSplit.scala 19 additions, 16 deletionssrc/main/scala/leon/synthesis/rules/ADTSplit.scala
- src/main/scala/leon/synthesis/rules/DetupleInput.scala 4 additions, 1 deletionsrc/main/scala/leon/synthesis/rules/DetupleInput.scala
Loading
Please register or sign in to comment