Commits · 3b9c89c3efe0fb487ab095a7d98aecd4c9d49252 · LARA / inox · GitLab

Snippets Groups Projects

Feb 12, 2015
- Refactor rules, remove Heuristics/Rules · 01062258
  Etienne Kneuss authored 10 years ago
  
  01062258
- I have trust issues · fb3fccf8
  Etienne Kneuss authored 10 years ago
  
  fb3fccf8
- Split witnesses and path condition. · 2b7d480c
  Etienne Kneuss authored 10 years ago
  
  2b7d480c
- Separate trees from tree constructors,use them more,simplifications · 2872b0e8
  Etienne Kneuss authored 10 years ago
  
  2872b0e8
Aug 20, 2014
- Field Extraction & handling · 0889f2f7
  Emmanouil (Manos) Koukoutos authored 10 years ago
  
  0889f2f7
Apr 11, 2014
- All-seeing synthesis with Oracles, library reorganisation · 8f2438cc
  Etienne Kneuss authored 11 years ago
  8f2438cc
Mar 14, 2014
- Fix header (2013 -> 2014). Add script to do so. · 26ca0be2
  Etienne Kneuss authored 11 years ago
  
  26ca0be2
Feb 17, 2014
- Introduce support for methods and multiple objects/fields · 9c7e02b5
  Etienne Kneuss authored 11 years ago
  9c7e02b5
Feb 04, 2014
- Implement generics for functions and ADTs · 1708d239
  Etienne Kneuss authored 11 years ago
  1708d239
Oct 01, 2013
- Re-introduce type hierarchy for solvers, simplify factories · b86116f0
  Etienne Kneuss authored 11 years ago
  b86116f0
Sep 12, 2013
- 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
Aug 27, 2013
- Remove ResultVariable, postcondition are explicitly bound · f24aafcc
  Etienne Kneuss authored 11 years ago
  
  f24aafcc
Jun 03, 2013
- Apply BSD 2 clauses license · 3cb6d843
  Etienne Kneuss authored 12 years ago
  
  3cb6d843
Apr 12, 2013
- Check whether pc to ADTInduction is inductive before propagating it · fa9db943
  Etienne Kneuss authored 12 years ago
  
  fa9db943
Feb 13, 2013
- Various improvements necessary for the web-interface · f48ff213
  Etienne Kneuss authored 12 years ago
  f48ff213
Jan 08, 2013
- Allow onSuccess to fail. This is necessary to prevent soundness issues. · 965264c3
  Etienne Kneuss authored 12 years ago
  965264c3
Jan 04, 2013
- Improve search by making it more deterministic · 8f620493
  Etienne Kneuss authored 12 years ago
  
  8f620493
- Simplifications for LetTuple. · c6ed682f
  Philippe Suter authored 12 years ago
  c6ed682f
Jan 03, 2013
- Handle problem of costs=0 in case of missing SolutionBuilder, requires passing... · b986717b
  Etienne Kneuss authored 12 years ago
  b986717b
- Remove obsolete concept of Rule priorities. This is now implicitly handled by the search. · ce6ef073
  Etienne Kneuss authored 12 years ago
  
  ce6ef073
Dec 12, 2012
- Fix bug in ADT Induction · 1dae9568
  Etienne Kneuss authored 12 years ago
  
  1dae9568
Dec 06, 2012
- Rework the semantics of rules, their applications/instantiation, results · 7378ba6f
  Etienne Kneuss authored 12 years ago
  
  7378ba6f
Nov 23, 2012
- Prepare ground for parallel search · 5ccb8ebe
  Etienne Kneuss authored 12 years ago
  
  5ccb8ebe
Nov 21, 2012
- Gah, that bug was hard to track down. onSuccess should never alter global... · 67b81315
  Etienne Kneuss authored 12 years ago
  67b81315
Nov 19, 2012
- Some re-work based on and-or graphs · e69cbc14
  Etienne Kneuss authored 12 years ago
  
  e69cbc14
- Make ADTInduction mutli-alternatives · ea78ac3f
  Etienne Kneuss authored 12 years ago
  
  ea78ac3f
- Make RuleInapplicable a RuleAlternatives with no alternative · 9a05ae05
  Etienne Kneuss authored 12 years ago
  
  9a05ae05
- Rules can (and should) have multiple application alternatives · 9c8b6e54
  Etienne Kneuss authored 12 years ago
  
  9c8b6e54
Nov 15, 2012
- Mooooaaaar files · 8c3708b0
  Etienne Kneuss authored 12 years ago
  
  8c3708b0