Skip to content
Snippets Groups Projects
  1. Aug 31, 2015
  2. Aug 27, 2015
  3. Aug 24, 2015
  4. Aug 20, 2015
  5. Aug 18, 2015
    • Etienne Kneuss's avatar
      Flatten & Simplify Solver API · a6724892
      Etienne Kneuss authored
      Solvers are no longer distinguished in 20 traits depending on what they
      implement. It turns out that most leon solvers already implemented
      everything:
      
      1) Being interrupted
      2) Push / Pop
      3) checkAssertions/getUnsatCore (a naive implementation of these
         can be added by mixing NaiveAssumptionSolver in)
      a6724892
    • Etienne Kneuss's avatar
      ble · fc3b9930
      Etienne Kneuss authored
      fc3b9930
    • Manos Koukoutos's avatar
      Update to latest scala-smtlib · d920a174
      Manos Koukoutos authored
      d920a174
  6. Aug 17, 2015
  7. Aug 13, 2015
    • Etienne Kneuss's avatar
      Introduce model minimization/maximization · 184b4790
      Etienne Kneuss authored
      - Measure is provided by an user-defined expression of BigInt type
        (e.g. List.size)
      
      - Search for min/max lazily enumerates intermediate models. Users of the
        enumerator may wish to skip them using `.last`, and/or bound the
        search using `.take(N)`.
      
      - Discovery of upper&lower bounds is done with pseudo-exponential
        progression from initial model. Bisection method is then used to
        zero-in on the min/max.
      184b4790
    • Etienne Kneuss's avatar
      Solver-based enumeration of models · 8346494c
      Etienne Kneuss authored
      - enumSimple allows to enumerate distinct models (models will typically
        only slightly differ , e.g. only w.r.t one integer)
      
      - enumVarying allows to specify a caracteristic (i.e. `size`) and
        enumerate `N` models of each size.
      8346494c
  8. Aug 12, 2015
  9. Aug 11, 2015
  10. Aug 06, 2015
  11. Jul 22, 2015
  12. Jul 21, 2015
  13. Jul 17, 2015
  14. Jul 14, 2015
    • Manos Koukoutos's avatar
      Introducing UnapplyPattern, plus improvements · 74aba11f
      Manos Koukoutos authored
      - Custom pattern matching through unapply functions.
      - TypeParameter now has private constructor, can only be created
        with TypeParameter.fresh or _.freshen
      - Stricter type checking for expressions. Correct various type errors.
      - Remove some redundant code.
      74aba11f
  15. Jul 09, 2015
  16. Jul 06, 2015
  17. Jul 02, 2015
  18. Jun 30, 2015
  19. Jun 29, 2015
  20. Jun 25, 2015
  21. Jun 24, 2015
  22. Jun 23, 2015
  23. Jun 22, 2015
  24. Jun 19, 2015
  25. Jun 17, 2015
Loading