-
- Downloads
Adding support for compressing VCs during checking
Showing
- src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala 2 additions, 1 deletion...in/scala/leon/invariant/engine/InferInvariantsPhase.scala
- src/main/scala/leon/invariant/engine/InferenceContext.scala 1 addition, 1 deletionsrc/main/scala/leon/invariant/engine/InferenceContext.scala
- src/main/scala/leon/invariant/engine/InferenceEngine.scala 40 additions, 46 deletionssrc/main/scala/leon/invariant/engine/InferenceEngine.scala
- src/main/scala/leon/invariant/engine/SpecInstantiator.scala 1 addition, 2 deletionssrc/main/scala/leon/invariant/engine/SpecInstantiator.scala
- src/main/scala/leon/invariant/factories/TemplateFactory.scala 1 addition, 0 deletions...main/scala/leon/invariant/factories/TemplateFactory.scala
- src/main/scala/leon/invariant/factories/TemplateInstantiator.scala 1 addition, 1 deletion...scala/leon/invariant/factories/TemplateInstantiator.scala
- src/main/scala/leon/invariant/structure/Constraint.scala 41 additions, 69 deletionssrc/main/scala/leon/invariant/structure/Constraint.scala
- src/main/scala/leon/invariant/structure/Formula.scala 148 additions, 37 deletionssrc/main/scala/leon/invariant/structure/Formula.scala
- src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala 11 additions, 39 deletions...in/scala/leon/invariant/templateSolvers/CegisSolver.scala
- src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala 7 additions, 6 deletions...la/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
- src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala 528 additions, 615 deletions...ala/leon/invariant/templateSolvers/NLTemplateSolver.scala
- src/main/scala/leon/invariant/templateSolvers/NLTemplateSolverWithMult.scala 6 additions, 6 deletions.../invariant/templateSolvers/NLTemplateSolverWithMult.scala
- src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala 24 additions, 30 deletions...scala/leon/invariant/templateSolvers/TemplateSolver.scala
- src/main/scala/leon/invariant/util/ExpressionTransformer.scala 40 additions, 50 deletions...ain/scala/leon/invariant/util/ExpressionTransformer.scala
- src/main/scala/leon/invariant/util/FlatToUnflatExpr.scala 0 additions, 60 deletionssrc/main/scala/leon/invariant/util/FlatToUnflatExpr.scala
- src/main/scala/leon/invariant/util/LinearRelationEvaluator.scala 82 additions, 0 deletions...n/scala/leon/invariant/util/LinearRelationEvaluator.scala
- src/main/scala/leon/invariant/util/Minimizer.scala 18 additions, 22 deletionssrc/main/scala/leon/invariant/util/Minimizer.scala
- src/main/scala/leon/invariant/util/SelectorToCons.scala 116 additions, 0 deletionssrc/main/scala/leon/invariant/util/SelectorToCons.scala
- src/main/scala/leon/invariant/util/SolverUtil.scala 1 addition, 1 deletionsrc/main/scala/leon/invariant/util/SolverUtil.scala
- src/main/scala/leon/invariant/util/Stats.scala 13 additions, 0 deletionssrc/main/scala/leon/invariant/util/Stats.scala
Loading
Please register or sign in to comment