-
- Downloads
Merge pull request #166 from MikaelMayer/stringz3
Translation from String to List[Char] for Z3 on demand.
No related branches found
No related tags found
Showing
- library/lang/string/String.scala 0 additions, 28 deletionslibrary/lang/string/String.scala
- library/lang/string/package.scala 0 additions, 24 deletionslibrary/lang/string/package.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 3 additions, 0 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/datagen/VanuatooDataGen.scala 2 additions, 1 deletionsrc/main/scala/leon/datagen/VanuatooDataGen.scala
- src/main/scala/leon/purescala/Definitions.scala 4 additions, 0 deletionssrc/main/scala/leon/purescala/Definitions.scala
- src/main/scala/leon/purescala/Expressions.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/purescala/SelfPrettyPrinter.scala 0 additions, 1 deletionsrc/main/scala/leon/purescala/SelfPrettyPrinter.scala
- src/main/scala/leon/solvers/SolverFactory.scala 2 additions, 0 deletionssrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala 35 additions, 2 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala 0 additions, 35 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala 2 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala 22 additions, 7 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 307 additions, 290 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/Z3StringConversion.scala 94 additions, 0 deletionssrc/main/scala/leon/solvers/z3/Z3StringConversion.scala
- src/main/scala/leon/utils/Library.scala 0 additions, 1 deletionsrc/main/scala/leon/utils/Library.scala
- src/test/scala/leon/integration/solvers/SolversSuite.scala 3 additions, 3 deletionssrc/test/scala/leon/integration/solvers/SolversSuite.scala
- src/test/scala/leon/integration/solvers/StringSolverSuite.scala 0 additions, 2 deletions...st/scala/leon/integration/solvers/StringSolverSuite.scala
- src/test/scala/leon/regression/termination/TerminationSuite.scala 1 addition, 1 deletion.../scala/leon/regression/termination/TerminationSuite.scala
- src/test/scala/leon/test/LeonRegressionSuite.scala 1 addition, 1 deletionsrc/test/scala/leon/test/LeonRegressionSuite.scala
- testcases/verification/case-studies/LambdaSound.scala 0 additions, 1 deletiontestcases/verification/case-studies/LambdaSound.scala
Loading
Please register or sign in to comment