-
- Downloads
"matlab/TCV_IMAS/ids_empty/ids_empty_runaway_electrons.m" did not exist on "007d7b5d2b196685a7fd2c0432ad06da1f10128e"
Flatten & Simplify Solver API
Solvers are no longer distinguished in 20 traits depending on what they implement. It turns out that most leon solvers already implemented everything: 1) Being interrupted 2) Push / Pop 3) checkAssertions/getUnsatCore (a naive implementation of these can be added by mixing NaiveAssumptionSolver in)
Showing
- src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala 2 additions, 1 deletion...cala/leon/integration/solvers/ModelEnumerationSuite.scala
- src/integration/scala/leon/integration/solvers/TimeoutSolverSuite.scala 4 additions, 1 deletion...n/scala/leon/integration/solvers/TimeoutSolverSuite.scala
- src/main/scala/leon/solvers/AssumptionSolver.scala 0 additions, 11 deletionssrc/main/scala/leon/solvers/AssumptionSolver.scala
- src/main/scala/leon/solvers/EnumerationSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/EnumerationSolver.scala
- src/main/scala/leon/solvers/GroundSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/GroundSolver.scala
- src/main/scala/leon/solvers/IncrementalSolver.scala 0 additions, 10 deletionssrc/main/scala/leon/solvers/IncrementalSolver.scala
- src/main/scala/leon/solvers/NaiveAssumptionSolver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/NaiveAssumptionSolver.scala
- src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala 0 additions, 27 deletionssrc/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
- src/main/scala/leon/solvers/SimpleSolverAPI.scala 17 additions, 6 deletionssrc/main/scala/leon/solvers/SimpleSolverAPI.scala
- src/main/scala/leon/solvers/Solver.scala 8 additions, 2 deletionssrc/main/scala/leon/solvers/Solver.scala
- src/main/scala/leon/solvers/SolverFactory.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala 0 additions, 21 deletionssrc/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
- src/main/scala/leon/solvers/TimeoutSolver.scala 13 additions, 1 deletionsrc/main/scala/leon/solvers/TimeoutSolver.scala
- src/main/scala/leon/solvers/combinators/DNFSolver.scala 0 additions, 138 deletionssrc/main/scala/leon/solvers/combinators/DNFSolver.scala
- src/main/scala/leon/solvers/combinators/PortfolioSolver.scala 11 additions, 3 deletions...main/scala/leon/solvers/combinators/PortfolioSolver.scala
- src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala 1 addition, 1 deletion...ala/leon/solvers/combinators/PortfolioSolverFactory.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolver.scala 1 addition, 1 deletion...main/scala/leon/solvers/combinators/UnrollingSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 3 additions, 7 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 1 addition, 5 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/utils/ModelEnumerator.scala 27 additions, 26 deletionssrc/main/scala/leon/utils/ModelEnumerator.scala
Loading
Please register or sign in to comment