- Nov 30, 2016
-
-
Nicolas Voirol authored
-
- Aug 11, 2016
-
-
Nicolas Voirol authored
-
- Mar 20, 2016
-
-
Lars Hupel authored
Notable changes: * sbt-libisabelle plugin which takes care of Isabelle source management - no more submodules; Isabelle sources are now packaged in JAR files - no weird ROOTS file in the repository root * less isabelle: flags, everybody would want to use the defaults anyway * updating to Isabelle2016 becomes possible (future work)
-
- Sep 11, 2015
-
-
Lars Hupel authored
-
- Jun 22, 2015
-
-
Etienne Kneuss authored
Performance tests are invoked via "sbt perf:test". Currently testing performance of CEGIS on some random synthesis problems
-
- Jun 10, 2015
-
-
Manos Koukoutos authored
-
Manos Koukoutos authored
-
- Jun 03, 2015
-
-
Etienne Kneuss authored
-
- May 29, 2015
-
-
Manos Koukoutos authored
-
- Apr 23, 2015
-
-
Manos Koukoutos authored
-
- Apr 20, 2015
-
-
Etienne Kneuss authored
--solvers=smt-cvc4-cex --solvers=smt-cvc4-proof Update scala-smtlib with support for parsing special DefFunsRec
-
- Apr 16, 2015
-
-
Manos Koukoutos authored
-
- Mar 26, 2015
-
-
Manos Koukoutos authored
-
- Mar 10, 2015
-
-
Regis Blanc authored
-
- Mar 05, 2015
-
-
Regis Blanc authored
-
- Mar 04, 2015
-
-
Regis Blanc authored
-
- Feb 17, 2015
-
-
Regis Blanc authored
-
- Feb 16, 2015
-
-
Emmanouil (Manos) Koukoutos authored
-
- Feb 12, 2015
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Feb 06, 2015
-
-
Regis Blanc authored
Fixes a bug, where UnrollingSolver was interrupted but was not stopping its internal solver, leading to a timeout not being respected if the internal solver was stucked in a complicated check operation. UnrollingSolver now takes a Solver with Interruptible. In order to do that, Leon now relies on a more recent version of scala-smtlib, that provides a feature to kill the solver process in a relatively clean way. Update the SMTLIBSolver code to actually perform the kill operation on the interrupt.
-
- Oct 06, 2014
-
-
Etienne Kneuss authored
reactivate tests for CVC4, if available. Remove non-linear testcase that worked only on z3 (SumAndMax)
-
- Sep 26, 2014
-
-
Etienne Kneuss authored
-
- Sep 17, 2014
-
-
Etienne Kneuss authored
-
- Sep 16, 2014
-
-
Regis Blanc authored
Update the build to reference the most recent version of scala smt-lib and adapt the code to the new API. Replace some use of NonStandardCommand by built-in standard Commands of scala smt-lib.
-
Etienne Kneuss authored
- Partial support for CVC4
-
Etienne Kneuss authored
-
Etienne Kneuss authored
- 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
-
Régis Blanc authored
-
- Sep 03, 2014
-
-
Etienne Kneuss authored
-
Etienne Kneuss authored
-
- Aug 25, 2014
-
-
Etienne Kneuss authored
-
- Jul 29, 2014
-
-
Etienne Kneuss authored
-
- Apr 09, 2014
-
-
Etienne Kneuss authored
-
- Feb 28, 2014
-
-
Etienne Kneuss authored
- Implement the Leon Library in Leon-land rather than Scala-land. import leon.Utils._ becomes import leon.lang._ import leon.Annotations._ becomes import leon.annontation._ For now, the library defines generic Options and Lists. The library is automatically imported from the ./leon script, unless the --library=no option is passed. - Support parsing of multiple files and modules. - Introduce new annontations: @ignore: remove definition from Leon @verified: do not consider for verification unless explicitly specified
-
- Feb 20, 2014
-
-
Ivan Kuraj authored
-
- Sep 12, 2013
-
-
Etienne Kneuss authored
- Free&Recreate solvers during synthesis. This avoids huge memory leaks due to Z3AST never being reclaimed thourough the entire synthesis process - Add safeguard to catch Z3Solvers for which memory management is incomplete
-
- Aug 16, 2013
-
-
Etienne Kneuss authored
-
- Jul 11, 2013
-
-
Etienne Kneuss authored
- Refactor code extraction - Standardize extractors - Fix type identification by resolving type aliases - Redo reporter integration with Scalac - Fix relining to prevent bizarre compile-errors - Refactor Pretty-Printers - Extensible class interface - Not returning mutable string-buffers anymore - Fixes according to 2.10 - 100% false warnings in Tests - imports for postfix-ops or implicits - Upgrade ScalaZ3 to 2.10 - Upgrade Cafebabe to 2.10
-
- Dec 19, 2012
-
-
Etienne Kneuss authored
Improve performance of FairZ3 by lowering unrolling to the z3 level. Improve synthesis profiling script. Improve performance of FairZ3: Make function templates and unlocking/unrolling work directly at the z3 level for performance reasons. Implement push-pop at the unrolling-bank level. Works around a z3 bug. Z3 apparently side-effects during check-assumptions, causing a following check without assumptions to produce unreliable results. We work around this by backtracking to the state before the check-assumptions using push/pop. Improve synthesis profiling/benchmarking: Move benchrmarking suite away from tests. Synthesis Rule application benchmark can now use a --rule option specifying what rule to apply. Add Testcase to evaluate CEGIS unrolling of different depth. Benchmarking script is now generated via the 'bench' sbt task.
-