Skip to content
Snippets Groups Projects
  1. Jan 25, 2016
  2. Jan 08, 2016
  3. Oct 20, 2015
  4. Oct 08, 2015
  5. Sep 28, 2015
  6. Sep 14, 2015
  7. Aug 31, 2015
  8. Jun 24, 2015
  9. Jun 23, 2015
  10. May 05, 2015
  11. Apr 28, 2015
  12. Apr 23, 2015
  13. Apr 16, 2015
  14. Mar 04, 2015
  15. Feb 12, 2015
  16. Aug 20, 2014
  17. Sep 12, 2013
  18. Aug 31, 2013
  19. Dec 19, 2012
    • Etienne Kneuss's avatar
      Improve performance of FairZ3 by lowering unrolling to the z3 level. Improve... · b9d98db8
      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.
      b9d98db8
  20. Nov 01, 2012
  21. Oct 26, 2012
  22. Oct 25, 2012
  23. Apr 17, 2012
  24. Mar 21, 2012
  25. Mar 05, 2012
  26. Feb 29, 2012
Loading