Commits · 55da06524c0386b56dff9b99b1413443e9d14e16 · LARA / inox

May 13, 2015
- Explicitly shutdown() solver factories when they are no longer used · 55da0652
  Etienne Kneuss authored 10 years ago
  55da0652
May 11, 2015
- No point in naming them Targets if they are Solvers. · 39403227
  Etienne Kneuss authored 10 years ago
  
  39403227
- Merge SMTLIBSolver with SMTLIBTarget · e3634bc8
  Manos Koukoutos authored 10 years ago
  
  e3634bc8
May 06, 2015
- Fallback to whatever is available, fatal otherwise. · 2ff6b9b5
  Etienne Kneuss authored 10 years ago
  
  2ff6b9b5
May 05, 2015
- Fallback to SMT solver in case native interface is unavailable · 86749646
  Etienne Kneuss authored 10 years ago
  
  86749646
- Unify and centralize use of solvers · 51e2f35c
  Etienne Kneuss authored 10 years ago
  
  51e2f35c
Apr 24, 2015
- typos · cac4e05a
  Manos Koukoutos authored 10 years ago
  
  cac4e05a
Apr 23, 2015
- Name all LeonOptionDefs opt* · b110b833
  Manos Koukoutos authored 10 years ago
  
  b110b833
- Multiline help, improvements · a04534f2
  Manos Koukoutos authored 10 years ago
  
  a04534f2
- Refactor how command line options are handled by Leon · 59b0b60a
  Manos Koukoutos authored 10 years ago
  59b0b60a
Apr 21, 2015
- Fix fullname, improve solver timeouts · 324beff9
  Etienne Kneuss authored 10 years ago
  
  324beff9
Apr 20, 2015
- Distinguish cvc4 solvers and options for proof and cex · 8c9d5ba5
  Etienne Kneuss authored 10 years ago
  8c9d5ba5
Apr 16, 2015
- Update copyright notices · 4c5796bc
  Manos Koukoutos authored 10 years ago
  
  4c5796bc
- Z3 solver with fundefs as quantified formulas · 8c208324
  Manos Koukoutos authored 10 years ago
  
  8c208324
- SMTLIB-CVC4 with define-funs-rec · e445f6d3
  Manos Koukoutos authored 10 years ago
  
  e445f6d3
Mar 18, 2015
- Fix a bunch of style/actual issues · 827a6535
  Manos Koukoutos authored 10 years ago
  
  827a6535
Feb 12, 2015
- Added higher-order function support to Leon · 2667b969
  Nicolas Voirol authored 10 years ago
  
  2667b969
Sep 16, 2014
- Implement and test everything for smt-z3 · 71d27ef2
  Etienne Kneuss authored 11 years ago
  71d27ef2
- Unify and simplify function templates and unrolling banks · 0a67f203
  Etienne Kneuss authored 11 years ago
  0a67f203
- Improve/Fix SMTLib solvers · 622d4d8b
  Etienne Kneuss authored 11 years ago
  622d4d8b
Mar 14, 2014
- Fix header (2013 -> 2014). Add script to do so. · 26ca0be2
  Etienne Kneuss authored 11 years ago
  
  26ca0be2
Oct 01, 2013
- Re-introduce type hierarchy for solvers, simplify factories · b86116f0
  Etienne Kneuss authored 11 years ago
  b86116f0
Sep 12, 2013
- Rename ReportingSection to DebugSection · 59e6fe6f
  Etienne Kneuss authored 11 years ago
  
  59e6fe6f
- Minor renamings. · 9f21f5f9
  Philippe Suter authored 11 years ago
  
  9f21f5f9
- Debug sections become implicit · ba4e4d30
  Etienne Kneuss authored 11 years ago
  
  ba4e4d30
- Drastic memory management for solvers during synthesis · be292ce0
  Etienne Kneuss authored 11 years ago
  be292ce0
- Refactor Solvers · f374e736
  Etienne Kneuss authored 11 years ago
  f374e736