-
- Downloads
Improve/Fix SMTLib solvers
- Implement smt and smt-z3/smt-cvc4 as options for --solvers - Uses a main solver sources for verification/CLP, taking into account --solvers - Implement Z3-SMT sets - Add tests for Z3-SMT
Showing
- project/Build.scala 1 addition, 1 deletionproject/Build.scala
- project/plugins.sbt 0 additions, 0 deletionsproject/plugins.sbt
- src/main/scala/leon/Main.scala 11 additions, 4 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/Reporter.scala 10 additions, 0 deletionssrc/main/scala/leon/Reporter.scala
- src/main/scala/leon/Settings.scala 3 additions, 1 deletionsrc/main/scala/leon/Settings.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 5 additions, 4 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/purescala/Common.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/Common.scala
- src/main/scala/leon/purescala/Trees.scala 2 additions, 1 deletionsrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/purescala/TypeTrees.scala 0 additions, 43 deletionssrc/main/scala/leon/purescala/TypeTrees.scala
- src/main/scala/leon/smtlib/ExprToSExpr.scala 0 additions, 107 deletionssrc/main/scala/leon/smtlib/ExprToSExpr.scala
- src/main/scala/leon/smtlib/PrettyPrinter.scala 0 additions, 46 deletionssrc/main/scala/leon/smtlib/PrettyPrinter.scala
- src/main/scala/leon/smtlib/SExprToExpr.scala 0 additions, 48 deletionssrc/main/scala/leon/smtlib/SExprToExpr.scala
- src/main/scala/leon/smtlib/SMTLIBSolver.scala 0 additions, 147 deletionssrc/main/scala/leon/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/smtlib/package.scala 0 additions, 30 deletionssrc/main/scala/leon/smtlib/package.scala
- src/main/scala/leon/solvers/SolverFactory.scala 41 additions, 1 deletionsrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/combinators/FunctionTemplate.scala 11 additions, 38 deletions...ain/scala/leon/solvers/combinators/FunctionTemplate.scala
- src/main/scala/leon/solvers/combinators/PortfolioSolver.scala 16 additions, 12 deletions...main/scala/leon/solvers/combinators/PortfolioSolver.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolver.scala 21 additions, 22 deletions...main/scala/leon/solvers/combinators/UnrollingSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala 51 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 68 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
Loading
Please register or sign in to comment