-
- Downloads
Improve Identifier API, and "undefined" errors
Identifier fields which can be private are now private. Identifier now inherits Ordered. Define Undefined error, and its subclass SolverUndefinedError. Use it mainly in solvers.
Showing
- src/main/scala/leon/LeonExceptions.scala 5 additions, 0 deletionssrc/main/scala/leon/LeonExceptions.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 7 additions, 4 deletionssrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/datagen/VanuatooDataGen.scala 1 addition, 1 deletionsrc/main/scala/leon/datagen/VanuatooDataGen.scala
- src/main/scala/leon/evaluators/CodeGenEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/CodeGenEvaluator.scala
- src/main/scala/leon/purescala/Common.scala 21 additions, 14 deletionssrc/main/scala/leon/purescala/Common.scala
- src/main/scala/leon/solvers/ADTManager.scala 5 additions, 3 deletionssrc/main/scala/leon/solvers/ADTManager.scala
- src/main/scala/leon/solvers/Solver.scala 12 additions, 1 deletionsrc/main/scala/leon/solvers/Solver.scala
- src/main/scala/leon/solvers/SolverUnsupportedError.scala 15 additions, 0 deletionssrc/main/scala/leon/solvers/SolverUnsupportedError.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala 2 additions, 1 deletion...ain/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala 4 additions, 3 deletions...cala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 15 additions, 21 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala 2 additions, 1 deletion.../scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala 3 additions, 3 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 22 additions, 33 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/synthesis/rules/CEGISLike.scala 3 additions, 2 deletionssrc/main/scala/leon/synthesis/rules/CEGISLike.scala
- src/test/scala/leon/test/helpers/WithLikelyEq.scala 1 addition, 1 deletionsrc/test/scala/leon/test/helpers/WithLikelyEq.scala
Loading
Please register or sign in to comment