-
- Downloads
remove the need for innerXXX methods
Refactor the TimeoutSolver and TimeoutAssumptionSolver so that they no longer use innerCheck methods. We now only create solver as subclassing Solver or IncrementalSolver and implementing the interuptible trait, and we can turn them into TimeoutSolver at instantiation time with a mixin.
Showing
- src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala 2 additions, 1 deletionsrc/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 3 additions, 1 deletionsrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala 3 additions, 5 deletionssrc/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
- src/main/scala/leon/solvers/TimeoutSolver.scala 3 additions, 5 deletionssrc/main/scala/leon/solvers/TimeoutSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
- src/main/scala/leon/synthesis/SynthesisContext.scala 2 additions, 2 deletionssrc/main/scala/leon/synthesis/SynthesisContext.scala
- src/main/scala/leon/synthesis/Synthesizer.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/Synthesizer.scala
- src/main/scala/leon/termination/Processor.scala 1 addition, 1 deletionsrc/main/scala/leon/termination/Processor.scala
- src/main/scala/leon/testgen/TestGeneration.scala 2 additions, 2 deletionssrc/main/scala/leon/testgen/TestGeneration.scala
- src/main/scala/leon/verification/AnalysisPhase.scala 1 addition, 1 deletionsrc/main/scala/leon/verification/AnalysisPhase.scala
- src/test/scala/leon/test/solvers/TimeoutSolverTests.scala 4 additions, 3 deletionssrc/test/scala/leon/test/solvers/TimeoutSolverTests.scala
Loading
Please register or sign in to comment