Commits · 8db71d9b8e9fa7dfbe98547f64307592f02f2198 · LARA / inox · GitLab

Snippets Groups Projects

Jan 14, 2013
- Makes unrolling tree a DAG. · 8db71d9b
  Philippe Suter authored 12 years ago
  8db71d9b
- Say goodbye to polarities. · 0588c15c
  Philippe Suter authored 12 years ago
  
  0588c15c
- Export userland flag to use unsat cores to drive the fairz3 unrolling · 2b09cd4c
  Etienne Kneuss authored 12 years ago
  
  2b09cd4c
- CEGIS: Implement enumerate&test given known valid inputs · 7687b797
  Etienne Kneuss authored 12 years ago
  7687b797
- OptimisticGround can take time, so we do the work on application rather than instantiation. · 25b5159f
  Etienne Kneuss authored 12 years ago
  
  25b5159f
- Implement InequalitySplit and improve EqualitySplit · 4fad2012
  Etienne Kneuss authored 12 years ago
  4fad2012
- Decompose out variables that match a single case-class · 9746ba52
  Etienne Kneuss authored 12 years ago
  9746ba52
- Simplify TupleSelect(Tuple(..), ..) and CaseClassSelect(CaseClass(..), ..) · db2fd782
  Etienne Kneuss authored 12 years ago
  db2fd782
Jan 12, 2013
- Termination checker. · 47f8001c
  Philippe Suter authored 12 years ago
  47f8001c
Jan 11, 2013
- Benchmark: Incremen Time, or Sequence of Times. Combine ADTs and Int · a3e44cf3
  Viktor Kuncak authored 12 years ago
  
  a3e44cf3
- Synthesis (and verification) benchmarks: · 31df5929
  Viktor Kuncak authored 12 years ago
  31df5929
- Fixed ClassLoader issue and type errors in evaluation. · 198a5489
  Philippe Suter authored 12 years ago
  198a5489
- --evalground makes FairZ3 evaluate ground applications · 1a0b9f93
  Philippe Suter authored 12 years ago
  1a0b9f93
- Propagate expected types to onSuccess · e4a278b4
  Etienne Kneuss authored 12 years ago
  e4a278b4
Jan 10, 2013
- Clarified assertion error. · e9bb6d75
  Philippe Suter authored 12 years ago
  
  e9bb6d75
- Fix a bug that affects case classes w/o parent. · 5e202817
  Philippe Suter authored 12 years ago
  5e202817
- Make ScalaPrinter support Iff and Implies. · 06fab159
  Philippe Suter authored 12 years ago
  
  06fab159
Jan 09, 2013
- Added MergeSort to (verification) regression suite. · e2654ec4
  Philippe Suter authored 12 years ago
  
  e2654ec4
- "Support" for `choose` in evaluators. · 57710fe2
  Philippe Suter authored 12 years ago
  57710fe2
- Fix Benchmarks · 222160e0
  Etienne Kneuss authored 12 years ago
  
  222160e0
- Add List-related benchmarks, with various invariants (none, isSorted,... · bea94705
  Etienne Kneuss authored 12 years ago
  bea94705
- Propagate the AtomicBoolean used by the SIGINT handler · 0e7bfc32
  Etienne Kneuss authored 12 years ago
  
  0e7bfc32
- Allow "&" along with "**" (Which is deprecated by Scala) · ab612ddc
  Etienne Kneuss authored 12 years ago
  
  ab612ddc
- Fix simplifyPath for Or() · 6308a2d3
  Etienne Kneuss authored 12 years ago
  
  6308a2d3
Jan 08, 2013
- Sorting testcases. · 2f5c6c88
  Philippe Suter authored 12 years ago
  2f5c6c88
- Allow onSuccess to fail. This is necessary to prevent soundness issues. · 965264c3
  Etienne Kneuss authored 12 years ago
  965264c3
- Add various benchmarks · abd6a94c
  Etienne Kneuss authored 12 years ago
  abd6a94c
- Accelerate CEGIS by disabling features we thought would help · 087889d5
  Etienne Kneuss authored 12 years ago
  087889d5
Jan 07, 2013
- Fix error preventing postConditions from being z3ified in FairZ3Solver · b0be7c0d
  Etienne Kneuss authored 12 years ago
  
  b0be7c0d
Jan 04, 2013
- Simplification of 1-uples and 0-uples. · ba41c6b2
  Philippe Suter authored 12 years ago
  ba41c6b2
- Define WeightedBranches as default cost model · 0ff0f3be
  Etienne Kneuss authored 12 years ago
  0ff0f3be
- Improve search by making it more deterministic · 8f620493
  Etienne Kneuss authored 12 years ago
  
  8f620493
- Simplify preconditions when possible · 94e82a7b
  Etienne Kneuss authored 12 years ago
  
  94e82a7b
- 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
- Implement --parallel[=N] to specify the number of workers to use. On success,... · a9f40660
  Etienne Kneuss authored 12 years ago
  a9f40660
- Remove obsolete concept of Rule priorities. This is now implicitly handled by the search. · ce6ef073
  Etienne Kneuss authored 12 years ago
  
  ce6ef073
- Implement WeightedBranches cost model · c3faef4e
  Etienne Kneuss authored 12 years ago
  c3faef4e
- Implement the inner case-split heuristic, extend case-split to Ors with more than two elements · 86573651
  Etienne Kneuss authored 12 years ago
  86573651
Dec 21, 2012
- Implement a new XlangAnalysisPhase · 32d53a55
  Régis Blanc authored 12 years ago
  32d53a55