Commits · 1e5b32d0af4bcdc7ae800af4d6be37c4359ca33c · LARA / inox · GitLab

Snippets Groups Projects

Nov 14, 2012
- ADT Induction · 1e5b32d0
  Etienne Kneuss authored 12 years ago
  
  1e5b32d0
- Starting ADTInduction · 46fabd14
  Etienne Kneuss authored 12 years ago
  
  46fabd14
- .. I guess this time should be good · d8fc644e
  Régis Blanc authored 12 years ago
  
  d8fc644e
- really no crash this time · 39185b06
  Régis Blanc authored 12 years ago
  
  39185b06
- Implement EqualitySplit We should check whether we do not always split on same variables · 0b2eb621
  Etienne Kneuss authored 12 years ago
  
  0b2eb621
- integrate equation synthesis as a rule · f751527f
  Régis Blanc authored 12 years ago
  
  f751527f
Nov 13, 2012
- Verify preconditions for heuristics · 50b03820
  Etienne Kneuss authored 12 years ago
  
  50b03820
- Fundefs separated in solutions · 2c92e5a7
  Etienne Kneuss authored 12 years ago
  
  2c92e5a7
- Move cegis and optimistic ground to rules · c9f0f7de
  Etienne Kneuss authored 12 years ago
  
  c9f0f7de
Nov 12, 2012
- Re-implement Assert using C · 71ad4bf8
  Etienne Kneuss authored 12 years ago
  
  71ad4bf8
- Tentative implementation of multi-steps rules · 8c22a926
  Etienne Kneuss authored 12 years ago
  
  8c22a926
Nov 10, 2012
- Add path condition into problems, unused for now · 48f9fd72
  Etienne Kneuss authored 12 years ago
  
  48f9fd72
Nov 09, 2012
- By convention, we reserve priorities 1-99 to heuristics · fa25dd45
  Etienne Kneuss authored 12 years ago
  
  fa25dd45
- Add heuristic exploiting an optimistic assumption about injective nature of functions. · 6fde235e
  Etienne Kneuss authored 12 years ago
  6fde235e
Nov 03, 2012
- Kill Assert as we know it for now. Keep the trivial base case. · 76e4a4a5
  Etienne Kneuss authored 12 years ago
  76e4a4a5
- Remove concept of rule cost, this is not needed now · e810f63d
  Etienne Kneuss authored 12 years ago
  
  e810f63d
Nov 02, 2012
- Reporter should be silent, as it fails on under-constrained expressions using... · e5649f3d
  Etienne Kneuss authored 12 years ago
  e5649f3d
- Implement timeouts, trim search horizon based on solution so far · 244f18b6
  Etienne Kneuss authored 12 years ago
  
  244f18b6
- This tends to guarantee termination, better handling of giveups · 862613e1
  Etienne Kneuss authored 12 years ago
  
  862613e1
- Simplify generic transform, silence reporters · 039486a1
  Etienne Kneuss authored 12 years ago
  
  039486a1
- Rework complexities a bit · f34ab79b
  Etienne Kneuss authored 12 years ago
  
  f34ab79b
Nov 01, 2012
- Complexity needs to be carefully extracted/computed · 206fe471
  Etienne Kneuss authored 12 years ago
  
  206fe471
- Some organization · 40ed136d
  Etienne Kneuss authored 12 years ago
  
  40ed136d
- Reduce number of tries · d91e3a1b
  Etienne Kneuss authored 12 years ago
  
  d91e3a1b
- Return an expression, not a formula · 5f18731b
  Etienne Kneuss authored 12 years ago
  
  5f18731b
- Optimistic Ground Rule with CE guided refinement · e16ab22c
  Etienne Kneuss authored 12 years ago
  
  e16ab22c
- Store sufficient information to track resolution from rootTask · d5815659
  Etienne Kneuss authored 12 years ago
  
  d5815659
- Score solution programatically, not by hand. Allow arbitrary scrutinees (to check) · 70f68bc7
  Etienne Kneuss authored 12 years ago
  
  70f68bc7
Oct 31, 2012
- Decomposing task is a task itself · ecaff254
  Etienne Kneuss authored 12 years ago
  
  ecaff254
Oct 26, 2012
- Oups · be75f07f
  Etienne Kneuss authored 12 years ago
  
  be75f07f
Oct 24, 2012
- Some lumberjack work · f221d11a
  Etienne Kneuss authored 12 years ago
  
  f221d11a
- Make sure model is complete, simplify rule · 857317fc
  Etienne Kneuss authored 12 years ago
  
  857317fc
Oct 23, 2012
- Simplify Lets, fix types · ba235ac1
  Etienne Kneuss authored 12 years ago
  
  ba235ac1
- Fix assert, Add example, add more debug output for last rule · 6adbc583
  Etienne Kneuss authored 12 years ago
  
  6adbc583
- Keep precondition inside formula, print precondition · 54d6ebe2
  Etienne Kneuss authored 12 years ago
  
  54d6ebe2
- ADTDual · 1a6a2be3
  Etienne Kneuss authored 12 years ago
  
  1a6a2be3
- Add unification rules (Trivial, Symbol Clash, Decomposition, Occurs Check) · e0dd0a63
  Etienne Kneuss authored 12 years ago
  
  e0dd0a63
- Call z3 to get model satisfying no conditions · 147d699d
  Etienne Kneuss authored 12 years ago
  
  147d699d
- Implement Unconstraint Output · 0bebfffe
  Etienne Kneuss authored 12 years ago
  
  0bebfffe
- Simplify task decomposition by going via task methods · 921978f7
  Etienne Kneuss authored 12 years ago
  
  921978f7