Commits · 9746ba52ce99f4eae2aad8f9922e38d2182512e7 · LARA / inox · GitLab

Snippets Groups Projects

Jan 14, 2013
- 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
- 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
- "Support" for `choose` in evaluators. · 57710fe2
  Philippe Suter authored 12 years ago
  57710fe2
- Fix Benchmarks · 222160e0
  Etienne Kneuss authored 12 years ago
  
  222160e0
- 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
- Allow onSuccess to fail. This is necessary to prevent soundness issues. · 965264c3
  Etienne Kneuss authored 12 years ago
  965264c3
- 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
Dec 20, 2012
- Displaying counter-examples. · a2479356
  Philippe Suter authored 12 years ago
  a2479356
- Bug fix in code generation. · 3c0a8231
  Philippe Suter authored 12 years ago
  3c0a8231
Dec 19, 2012
- Fix "minor" bug causing solvers to become autistic after the first search is over. · f2943cb1
  Etienne Kneuss authored 12 years ago
  
  f2943cb1
- Bugfix in Cegis. · 5945b726
  Philippe Suter authored 12 years ago
  5945b726
- Truncate fun. names to fit in AnalysisReport table. · eeb719e7
  Philippe Suter authored 12 years ago
  
  eeb719e7
- Improve performance of FairZ3 by lowering unrolling to the z3 level. Improve... · b9d98db8
  Etienne Kneuss authored 12 years ago
  b9d98db8
- Set contains e was wrongly printed as e contains Set · 51dd9459
  Etienne Kneuss authored 12 years ago
  
  51dd9459
Dec 17, 2012
- Generalization of Evaluators, and CodeGenEvaluator. · d1592f32
  Philippe Suter authored 12 years ago
  d1592f32
Dec 15, 2012
- Remove EmptySet, EmptyMap and SingletonMap · 65b1b6af
  Régis Blanc authored 12 years ago
  65b1b6af
- It might be that the counter example does not specify some input variables if... · 77a19904
  Etienne Kneuss authored 12 years ago
  77a19904
Dec 14, 2012
- Prevent double negations by construction. · 71ebadc5
  Philippe Suter authored 12 years ago
  71ebadc5
- Implement Literal Maps along with Tuple2 shorthands · 41576426
  Etienne Kneuss authored 12 years ago
  41576426