Drastic memory management for solvers during synthesis
- Free&Recreate solvers during synthesis. This avoids huge memory leaks due to Z3AST never being reclaimed thourough the entire synthesis process - Add safeguard to catch Z3Solvers for which memory management is incomplete
Showing
- .gitignore 3 additions, 0 deletions.gitignore
- project/Build.scala 1 addition, 1 deletionproject/Build.scala
- src/main/scala/leon/LeonContext.scala 2 additions, 1 deletionsrc/main/scala/leon/LeonContext.scala
- src/main/scala/leon/Main.scala 35 additions, 15 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/Reporter.scala 11 additions, 9 deletionssrc/main/scala/leon/Reporter.scala
- src/main/scala/leon/solvers/SimpleSolverAPI.scala 4 additions, 0 deletionssrc/main/scala/leon/solvers/SimpleSolverAPI.scala
- src/main/scala/leon/solvers/SolverFactory.scala 1 addition, 14 deletionssrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/TimeoutSolver.scala 4 additions, 0 deletionssrc/main/scala/leon/solvers/TimeoutSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 18 additions, 0 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala 0 additions, 30 deletionssrc/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
- src/main/scala/leon/synthesis/ParallelSearch.scala 1 addition, 7 deletionssrc/main/scala/leon/synthesis/ParallelSearch.scala
- src/main/scala/leon/synthesis/Rules.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/synthesis/SimpleSearch.scala 11 additions, 2 deletionssrc/main/scala/leon/synthesis/SimpleSearch.scala
- src/main/scala/leon/synthesis/SynthesisContext.scala 13 additions, 5 deletionssrc/main/scala/leon/synthesis/SynthesisContext.scala
- src/main/scala/leon/synthesis/Synthesizer.scala 7 additions, 3 deletionssrc/main/scala/leon/synthesis/Synthesizer.scala
- src/main/scala/leon/synthesis/heuristics/ADTInduction.scala 4 additions, 1 deletionsrc/main/scala/leon/synthesis/heuristics/ADTInduction.scala
- src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala 3 additions, 1 deletion...in/scala/leon/synthesis/heuristics/ADTLongInduction.scala
- src/main/scala/leon/synthesis/rules/ADTSplit.scala 3 additions, 1 deletionsrc/main/scala/leon/synthesis/rules/ADTSplit.scala
- src/main/scala/leon/synthesis/rules/Cegis.scala 244 additions, 239 deletionssrc/main/scala/leon/synthesis/rules/Cegis.scala
- src/main/scala/leon/synthesis/rules/EqualitySplit.scala 2 additions, 1 deletionsrc/main/scala/leon/synthesis/rules/EqualitySplit.scala
Loading
Please register or sign in to comment