Decouple ADT-dependencies from solvers
- ADTManager is responsible for computing dependencies between ADTs so that definitions can be grouped. - Simplify and generalize solver handling of RawArrays. - Remove dead-code in fair-z3 to parse non-ground models. - OptionManager was mostly useless, moved *Type to Library - MapGet can be implemented as (Some-value (Select m k)), as the solver will treat Some-value as uninterpreted if Select yields a None
Showing
- src/main/scala/leon/solvers/ADTManager.scala 106 additions, 0 deletionssrc/main/scala/leon/solvers/ADTManager.scala
- src/main/scala/leon/solvers/RawArray.scala 13 additions, 0 deletionssrc/main/scala/leon/solvers/RawArray.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala 0 additions, 32 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 57 additions, 234 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala 4 additions, 23 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 238 additions, 361 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/utils/Library.scala 5 additions, 0 deletionssrc/main/scala/leon/utils/Library.scala
Loading
Please register or sign in to comment