-
- Downloads
(a) Unflattenning VCs while checking
(b) Preserving if-then-elze in the VCs (c) Optimizing elimnation and UFADT reduction
Showing
- library/annotation/package.scala 3 additions, 1 deletionlibrary/annotation/package.scala
- src/main/scala/leon/invariant/datastructure/Graph.scala 21 additions, 25 deletionssrc/main/scala/leon/invariant/datastructure/Graph.scala
- src/main/scala/leon/invariant/engine/CompositionalTimeBoundSolver.scala 22 additions, 31 deletions.../leon/invariant/engine/CompositionalTimeBoundSolver.scala
- src/main/scala/leon/invariant/engine/ConstraintTracker.scala 27 additions, 2 deletionssrc/main/scala/leon/invariant/engine/ConstraintTracker.scala
- src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala 1 addition, 2 deletions...in/scala/leon/invariant/engine/InferInvariantsPhase.scala
- src/main/scala/leon/invariant/engine/InferenceContext.scala 5 additions, 3 deletionssrc/main/scala/leon/invariant/engine/InferenceContext.scala
- src/main/scala/leon/invariant/engine/InferenceEngine.scala 37 additions, 35 deletionssrc/main/scala/leon/invariant/engine/InferenceEngine.scala
- src/main/scala/leon/invariant/engine/RefinementEngine.scala 33 additions, 44 deletionssrc/main/scala/leon/invariant/engine/RefinementEngine.scala
- src/main/scala/leon/invariant/engine/SpecInstantiator.scala 15 additions, 16 deletionssrc/main/scala/leon/invariant/engine/SpecInstantiator.scala
- src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala 35 additions, 103 deletions...scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
- src/main/scala/leon/invariant/factories/TemplateInstantiator.scala 19 additions, 14 deletions...scala/leon/invariant/factories/TemplateInstantiator.scala
- src/main/scala/leon/invariant/structure/Constraint.scala 177 additions, 96 deletionssrc/main/scala/leon/invariant/structure/Constraint.scala
- src/main/scala/leon/invariant/structure/Formula.scala 197 additions, 115 deletionssrc/main/scala/leon/invariant/structure/Formula.scala
- src/main/scala/leon/invariant/structure/FunctionUtils.scala 19 additions, 9 deletionssrc/main/scala/leon/invariant/structure/FunctionUtils.scala
- src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala 198 additions, 280 deletions...scala/leon/invariant/structure/LinearConstraintUtil.scala
- src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala 2 additions, 1 deletion...in/scala/leon/invariant/templateSolvers/CegisSolver.scala
- src/main/scala/leon/invariant/templateSolvers/DisjunctChooser.scala 213 additions, 0 deletions...cala/leon/invariant/templateSolvers/DisjunctChooser.scala
- src/main/scala/leon/invariant/templateSolvers/ExistentialQuantificationSolver.scala 93 additions, 0 deletions...ant/templateSolvers/ExistentialQuantificationSolver.scala
- src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala 1 addition, 1 deletion...la/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
- src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala 11 additions, 610 deletions...ala/leon/invariant/templateSolvers/NLTemplateSolver.scala
Loading
Please register or sign in to comment