Commits · 45963f7c266eeed146a3caa1df6560007f527611 · LARA / inox · GitLab

Snippets Groups Projects

Dec 13, 2012
- Fix buggy stop() on non-parallel synthesis searches · 45963f7c
  Etienne Kneuss authored 12 years ago
  
  45963f7c
- One way of handling integer command line options. · 1288fc0b
  Philippe Suter authored 12 years ago
  
  1288fc0b
Dec 12, 2012
- Fix bug in ADT Induction · 1dae9568
  Etienne Kneuss authored 12 years ago
  
  1dae9568
Dec 11, 2012
- move LetDef to xlang and ScalaPrinter do not use xlang · 00c00c92
  Régis Blanc authored 12 years ago
  
  00c00c92
- Introducing : LeonComponent · 42c314f5
  Philippe Suter authored 12 years ago
  
  42c314f5
Dec 06, 2012
- Fix number of '-'s · 4cdebe4d
  Etienne Kneuss authored 12 years ago
  
  4cdebe4d
- Reintroduce luckytests fix two problems arising from parallelism of task dispatching · 6a5b1b67
  Etienne Kneuss authored 12 years ago
  
  6a5b1b67
- More reliable shutdown · 45985e1b
  Etienne Kneuss authored 12 years ago
  
  45985e1b
- Provide reliable way to shutdown long-lasting rules · c5e13beb
  Etienne Kneuss authored 12 years ago
  
  c5e13beb
- Rework the semantics of rules, their applications/instantiation, results · 7378ba6f
  Etienne Kneuss authored 12 years ago
  
  7378ba6f
- Fix parallel search with FairZ3Solver · ebd264dc
  Etienne Kneuss authored 12 years ago
  
  ebd264dc
Dec 05, 2012
- Improve search for leaves to target unsolved branches, fix one issue regarding parallelism · c76506d3
  Etienne Kneuss authored 12 years ago
  
  c76506d3
Dec 04, 2012
- Further improve speed of Cegis · bed47535
  Etienne Kneuss authored 12 years ago
  
  bed47535
- This CEGIS appears to work fine, with two solvers and inter-unrollings state preservation · 4e71a8af
  Etienne Kneuss authored 12 years ago
  
  4e71a8af
- Implement tests for synthesis · 04ed391b
  Etienne Kneuss authored 12 years ago
  
  04ed391b
- Selectable cost-model using the --costmodel option, yet to define multiple cost models · a48811ca
  Etienne Kneuss authored 12 years ago
  
  a48811ca
- Prepare ground for multiple cost models · ed115bf5
  Etienne Kneuss authored 12 years ago
  
  ed115bf5
- Add cost models, make things a tad bit nicer, synthesizer options · 242ae4cd
  Etienne Kneuss authored 12 years ago
  
  242ae4cd
Dec 03, 2012
- Generate multiple derivation graphs, output more info · edfc397d
  Etienne Kneuss authored 12 years ago
  
  edfc397d
Nov 30, 2012
- Do not report error in case of invalid model · 864bdc4a
  Etienne Kneuss authored 12 years ago
  
  864bdc4a
- Confidence is now over 9000 · aaed71ab
  Etienne Kneuss authored 12 years ago
  
  aaed71ab
Nov 29, 2012
- Implement partial solution reconstruction · ae93c204
  Etienne Kneuss authored 12 years ago
  
  ae93c204
- Partial push/pop implementation in CEGIS, it is currently not preserved between unrollings · 9dd29fb9
  Etienne Kneuss authored 12 years ago
  
  9dd29fb9
- apply simplification using the new expand and group simplification · 1126592b
  Régis Blanc authored 12 years ago
  
  1126592b
- No longer report warnings for empty unsat cores, as they represent a valid... · ff1c8857
  Etienne Kneuss authored 12 years ago
  ff1c8857
Nov 27, 2012
- Remove unused cleanups when restarting, fix reporter to solver · 2f5199f4
  Etienne Kneuss authored 12 years ago
  
  2f5199f4
Nov 26, 2012
- Proper passing of `LeonContext`s in synthesis. · 29c3acd4
  Philippe Suter authored 12 years ago
  
  29c3acd4
- The full `LeonContext` is now passed to `Solver`s. · deca849d
  Philippe Suter authored 12 years ago
  
  deca849d
- Cosmetics · 46b7b643
  Etienne Kneuss authored 12 years ago
  
  46b7b643
- Implement --firstonly for new dotconverter · 7f9a3874
  Etienne Kneuss authored 12 years ago
  
  7f9a3874
Nov 23, 2012
- Better organization and handling for Ctrl^C · c4dbcb7e
  Etienne Kneuss authored 12 years ago
  
  c4dbcb7e
- Works fine with a trivialsolver, now back to problematic case · 5d082e8c
  Etienne Kneuss authored 12 years ago
  
  5d082e8c
- Graceful init and termination of the search in parallel · 6475e73d
  Etienne Kneuss authored 12 years ago
  
  6475e73d
- Add --parallel option, default=false since it crashes like crazy · a81068b3
  Etienne Kneuss authored 12 years ago
  
  a81068b3
- How many cores do you have? · a1d180ea
  Etienne Kneuss authored 12 years ago
  
  a1d180ea
- Simple Refactoring for parallel search · 4236152b
  Etienne Kneuss authored 12 years ago
  
  4236152b
- Decouple Synthesizer from Search · 99a20e07
  Etienne Kneuss authored 12 years ago
  
  99a20e07
- Prepare ground for parallel search · 5ccb8ebe
  Etienne Kneuss authored 12 years ago
  
  5ccb8ebe
Nov 22, 2012
- optimization that does not introduce variables when the modulo is smaller than B - A · dc0a2865
  Régis Blanc authored 12 years ago
  
  dc0a2865
- heuristic to remove variable in inequality with lower lcm · acd77b90
  Régis Blanc authored 12 years ago
  
  acd77b90