-
- Downloads
Accelerate CEGIS by disabling features we thought would help
CEGIS now support internal flags that can enable/disable its features: 1) Injecting Counter-Examples on top of the unsat core to drive the search to interesting areas. Does not help => disabled 2) Computing Unsat-Cores to strenghten the search of programs. Help in some cases, doesn't hurt much => enabled 3) Checking whether the formula is unsat without blockers, to unrolling when there is no chance of finding a solution. Does not help => disable 4) Add support for function calls in CEGIS generators. This is disabled by default and can be enabled using --cegis:gencalls. It seems that doing additional checks in 1) and 3) triggers FairZ3 to unroll more, tempering with the performance of the solver. Also, this implements some improvements in the resulting programs by simplifying further expressions.
Showing
- src/main/scala/leon/purescala/TreeOps.scala 31 additions, 1 deletionsrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 7 additions, 2 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/purescala/TypeTrees.scala 9 additions, 0 deletionssrc/main/scala/leon/purescala/TypeTrees.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 3 additions, 1 deletionsrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FunctionTemplate.scala 2 additions, 0 deletionssrc/main/scala/leon/solvers/z3/FunctionTemplate.scala
- src/main/scala/leon/synthesis/ParallelSearch.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/ParallelSearch.scala
- src/main/scala/leon/synthesis/SynthesisContext.scala 15 additions, 1 deletionsrc/main/scala/leon/synthesis/SynthesisContext.scala
- src/main/scala/leon/synthesis/SynthesisPhase.scala 17 additions, 9 deletionssrc/main/scala/leon/synthesis/SynthesisPhase.scala
- src/main/scala/leon/synthesis/Synthesizer.scala 1 addition, 0 deletionssrc/main/scala/leon/synthesis/Synthesizer.scala
- src/main/scala/leon/synthesis/SynthesizerOptions.scala 2 additions, 1 deletionsrc/main/scala/leon/synthesis/SynthesizerOptions.scala
- src/main/scala/leon/synthesis/rules/ADTSplit.scala 0 additions, 1 deletionsrc/main/scala/leon/synthesis/rules/ADTSplit.scala
- src/main/scala/leon/synthesis/rules/Cegis.scala 82 additions, 46 deletionssrc/main/scala/leon/synthesis/rules/Cegis.scala
- src/main/scala/leon/synthesis/utils/Benchmarks.scala 11 additions, 3 deletionssrc/main/scala/leon/synthesis/utils/Benchmarks.scala
- src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala 3 additions, 8 deletions...eon/synthesis/utils/SynthesisProblemExtractionPhase.scala
- src/test/scala/leon/test/synthesis/SynthesisSuite.scala 10 additions, 9 deletionssrc/test/scala/leon/test/synthesis/SynthesisSuite.scala
- testcases/synthesis/CegisFunctions.scala 30 additions, 0 deletionstestcases/synthesis/CegisFunctions.scala
Loading
Please register or sign in to comment