-
- Downloads
Implement a Z3-4.3-friendly API to Solver and consequently to Z3 Solvers
Solvers now supports: - pop(lvl) - push - check - assertCnstr (assert would collapse with the usual assert()) - checkAssumptions - getModel - getUnsatCore This API is supported naively by all non-z3 solvers
Showing
- src/main/scala/leon/solvers/Solver.scala 42 additions, 0 deletionssrc/main/scala/leon/solvers/Solver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 25 additions, 3 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 82 additions, 36 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
Loading
Please register or sign in to comment