Commits · 8eef6f0c274d6ce902c03aa5a9f054b8e8ccf65d · LARA / inox

Oct 11, 2016
- Nicer abstract Symbol member overrides · 8eef6f0c
  Nicolas Voirol authored 8 years ago
  
  8eef6f0c
Oct 10, 2016
- Lots of refactoring to enable encoding solvers · bc7d332a
  Nicolas Voirol authored 8 years ago
  
  bc7d332a
Sep 28, 2016
- First-class function equality · 7734a377
  Nicolas Voirol authored 8 years ago
  
  7734a377
Sep 21, 2016
- Removed references to Leon in Inox source · 8d3f8d8b
  Nicolas Voirol authored 8 years ago
  
  8d3f8d8b
Aug 29, 2016
- Definition deconstruction for stainless VarDefs · 22e89278
  Nicolas Voirol authored 8 years ago
  
  22e89278
- More changes to support stainless · b86bbf89
  Nicolas Voirol authored 8 years ago
  
  b86bbf89
Aug 18, 2016
- Better names in inox ADT support · a3c19dd2
  Nicolas Voirol authored 8 years ago
  
  a3c19dd2
Aug 16, 2016
- All integration tests pass · 6f3c0e9c
  Nicolas Voirol authored 8 years ago
  
  6f3c0e9c
Aug 12, 2016
- Working on integration tests for solvers · 652e5b19
  Nicolas Voirol authored 8 years ago
  
  652e5b19
Aug 11, 2016
- All unit tests pass · b29c5b71
  Nicolas Voirol authored 8 years ago
  
  b29c5b71
Aug 10, 2016
- Operator follows same abstraction principle as NAryType · 5751f6c8
  Nicolas Voirol authored 8 years ago
  
  5751f6c8
- Start trans-tree traversals · db38c4e4
  Manos Koukoutos authored 8 years ago
  
  db38c4e4
Aug 08, 2016
- Fix == bugs/ run Intellij inspection · fb90ceb3
  Manos Koukoutos authored 8 years ago
  
  fb90ceb3
- Added Choose expression · b7493d67
  Nicolas Voirol authored 8 years ago
  
  b7493d67
Aug 04, 2016
- Working on Z3 solvers · 919c351b
  Nicolas Voirol authored 8 years ago
  
  919c351b
- A few new trees · d96c10a8
  Manos Koukoutos authored 8 years ago
  
  d96c10a8
Aug 03, 2016
- Finished up unrolling solver and theory encoders · 6bffff4f
  Nicolas Voirol authored 8 years ago
  
  6bffff4f
- Progress on unrolling solver · 0b8c4c38
  Nicolas Voirol authored 8 years ago
  
  0b8c4c38
Jul 27, 2016
- Pattern binders should be ordered · 2dd6b190
  Manos Koukoutos authored 8 years ago
  
  2dd6b190
Jul 20, 2016
- Compiles!! Wouhoouuuuu!! · d2303d96
  Nicolas Voirol authored 8 years ago
  
  d2303d96
Jul 16, 2016
- Progress on inox trees · 9574980d
  Nicolas Voirol authored 8 years ago
  
  9574980d
Jul 13, 2016
- Added datagen, continued working on trees · 282f172c
  Nicolas Voirol authored 8 years ago
  
  282f172c
Jul 12, 2016
- Started cleaning up Inox and rewrote Trees,Expressions,Types,Definitions · fc18ebd5
  Nicolas Voirol authored 8 years ago
  
  fc18ebd5
May 06, 2016
- adding bigSubstring and bigLength for strings. · 61c73029
  Mikaël Mayer authored 9 years ago
  
  61c73029
May 01, 2016
- test simple definition transformations · 4130daef
  Regis Blanc authored 9 years ago
  
  4130daef
- fix extractors for Arrays · 5c712143
  Regis Blanc authored 9 years ago
  
  5c712143
- Extractors do not perform simplifications · b6b685fd
  Regis Blanc authored 9 years ago
  
  b6b685fd
Apr 15, 2016
- test simple definition transformations · 9edf1840
  Regis Blanc authored 9 years ago
  
  9edf1840
- fix extractors for Arrays · 045a7274
  Regis Blanc authored 9 years ago
  
  045a7274
- Extractors do not perform simplifications · 87d6bd1f
  Regis Blanc authored 9 years ago
  
  87d6bd1f
Apr 12, 2016
- Refactor TreeOps a little · 54e486c3
  Manos Koukoutos authored 9 years ago
  
  54e486c3
Apr 07, 2016
- Bags in Leon · 29f8400c
  Nicolas Voirol authored 9 years ago
  
  29f8400c
Mar 28, 2016
- Added generic TheoryEncoders to Leon · 056f09f9
  Nicolas Voirol authored 9 years ago
  
  056f09f9
Mar 17, 2016
- Apply 2016 licence · 975bce69
  Manos Koukoutos authored 9 years ago
  
  975bce69
- Grammar transformers should propagate ProductionRule costs · 532bc4d7
  Manos Koukoutos authored 9 years ago
  532bc4d7
- fix some positions propagation in ops · 71db39f0
  Regis Blanc authored 9 years ago
  
  71db39f0
Feb 15, 2016
- Moar quantifier fixes · 63376f70
  Nicolas Voirol authored 9 years ago
  
  63376f70
- Constructing total models for quantifiers · b0227b0e
  Nicolas Voirol authored 9 years ago
  
  b0227b0e
Feb 05, 2016
- StringZ3 revisiter: Now the conversion is made BEFORE the solver is invoked. · e3e584ee
  Mikaël Mayer authored 9 years ago
  e3e584ee
Jan 08, 2016
- Moved ProgramSets to sub-package · 10ae6952
  Mikaël Mayer authored 9 years ago
  10ae6952