Re-introduce type hierarchy for solvers, simplify factories
Solvers wrap solvers or factories, depending on the needs. Factories no longer wrap factories, except for the special case of timeoutsolverfactories (it does it in a typesafe way though). Fix TupleRewrite with new posts, fix ScopeSimplified, Fix pretty printer
Showing
- src/main/scala/leon/purescala/ScalaPrinter.scala 18 additions, 18 deletionssrc/main/scala/leon/purescala/ScalaPrinter.scala
- src/main/scala/leon/purescala/TreeOps.scala 11 additions, 2 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 4 additions, 0 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/solvers/AssumptionSolver.scala 11 additions, 0 deletionssrc/main/scala/leon/solvers/AssumptionSolver.scala
- src/main/scala/leon/solvers/IncrementalSolver.scala 10 additions, 0 deletionssrc/main/scala/leon/solvers/IncrementalSolver.scala
- src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala 27 additions, 0 deletionssrc/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
- src/main/scala/leon/solvers/SimpleSolverAPI.scala 31 additions, 29 deletionssrc/main/scala/leon/solvers/SimpleSolverAPI.scala
- src/main/scala/leon/solvers/Solver.scala 13 additions, 7 deletionssrc/main/scala/leon/solvers/Solver.scala
- src/main/scala/leon/solvers/SolverFactory.scala 9 additions, 32 deletionssrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala 23 additions, 0 deletionssrc/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
- src/main/scala/leon/solvers/TimeoutSolver.scala 71 additions, 0 deletionssrc/main/scala/leon/solvers/TimeoutSolver.scala
- src/main/scala/leon/solvers/TimeoutSolverFactory.scala 13 additions, 0 deletionssrc/main/scala/leon/solvers/TimeoutSolverFactory.scala
- src/main/scala/leon/solvers/combinators/DNFSolver.scala 141 additions, 0 deletionssrc/main/scala/leon/solvers/combinators/DNFSolver.scala
- src/main/scala/leon/solvers/combinators/RewritingSolver.scala 36 additions, 0 deletions...main/scala/leon/solvers/combinators/RewritingSolver.scala
- src/main/scala/leon/solvers/combinators/RewritingSolverFactory.scala 0 additions, 81 deletions...ala/leon/solvers/combinators/RewritingSolverFactory.scala
- src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala 0 additions, 112 deletions...scala/leon/solvers/combinators/TimeoutSolverFactory.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolver.scala 155 additions, 0 deletions...main/scala/leon/solvers/combinators/UnrollingSolver.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolverFactory.scala 0 additions, 190 deletions...ala/leon/solvers/combinators/UnrollingSolverFactory.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 14 additions, 10 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 168 additions, 191 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
Loading
Please register or sign in to comment