Commits · e6f9e4b490129dde96265db72dadb038c1a58b2c · LARA / inox · GitLab

Snippets Groups Projects

Mar 28, 2016
- ADT Invariants in program transformations · e6f9e4b4
  Nicolas Voirol authored 9 years ago
  
  e6f9e4b4
- Added generic TheoryEncoders to Leon · 056f09f9
  Nicolas Voirol authored 9 years ago
  
  056f09f9
- Quantifier improvements + invariant preservation in program transforms · e0734347
  Nicolas Voirol authored 9 years ago
  
  e0734347
Mar 17, 2016
- Apply 2016 licence · 975bce69
  Manos Koukoutos authored 9 years ago
  
  975bce69
- New rule to introduce safe recursive call as a variable · a269985e
  Manos Koukoutos authored 9 years ago
  a269985e
Feb 15, 2016
- Renamed Henkin to Partial (makes more sense) · 4ddead34
  Nicolas Voirol authored 9 years ago
  
  4ddead34
- Moar quantifier fixes · 63376f70
  Nicolas Voirol authored 9 years ago
  
  63376f70
- Fixed forall evaluation · 0b73b9d4
  Nicolas Voirol authored 9 years ago
  
  0b73b9d4
- Small fix to DualEvaluator · 3f1a23c0
  Nicolas Voirol authored 9 years ago
  
  3f1a23c0
- Added generics to codegen evaluator · 827d8f01
  Nicolas Voirol authored 9 years ago
  
  827d8f01
- Finishing up optimized quantification · 1ae235ce
  Nicolas Voirol authored 9 years ago
  
  1ae235ce
- Constructing total models for quantifiers · b0227b0e
  Nicolas Voirol authored 9 years ago
  
  b0227b0e
- Remove pre-processing phase during evaluation (what?) · edbd3e5f
  Etienne Kneuss authored 9 years ago
  
  edbd3e5f
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 27, 2016
- Homomorphic to work on lambdas + tests. · 7366462b
  Mikaël Mayer authored 9 years ago
  7366462b
Jan 26, 2016
- Added passing Abstract test to render a double list of dummies to string. · 634d9478
  Mikaël Mayer authored 9 years ago
  634d9478
Jan 20, 2016
- Corrected abstract evaluator to partially evaluate the scrutinee. · ce61a86d
  Mikaël Mayer authored 9 years ago
  ce61a86d
Jan 19, 2016
- Simplified StringTracingEvaluator.scala, · d1d1114d
  Mikaël Mayer authored 9 years ago
  d1d1114d
Jan 11, 2016
- Hot fix: EvalError instead of FatalError · 936ce9ba
  Mikaël Mayer authored 9 years ago
  
  936ce9ba
Jan 08, 2016
- Moved ProgramSets to sub-package · 10ae6952
  Mikaël Mayer authored 9 years ago
  10ae6952
Jan 06, 2016
- Added string escape · dcc22b09
  Mikaël Mayer authored 9 years ago
  
  dcc22b09
Dec 10, 2015
- Fix bugs in Evaluators, add tests · 950381a5
  Manos Koukoutos authored 9 years ago
  
  950381a5
Nov 25, 2015
- Use StreamEvaluator in repair · fd33cc09
  Manos Koukoutos authored 9 years ago
  fd33cc09
- Refactor Evaluators. Introduce NDEvaluator trait and StreamEvaluator · ac306f8f
  Manos Koukoutos authored 9 years ago
  ac306f8f
Nov 23, 2015
- Fixed many bugs in the evaluator. · d9b937d6
  Mikaël Mayer authored 9 years ago
  d9b937d6
- Efficient procedure for transitive dependencies in quantifiers · 6285db89
  Nicolas Voirol authored 9 years ago
  
  6285db89
- Transitive quantifiers and lambda axioms · 3a11a76d
  Nicolas Voirol authored 9 years ago
  
  3a11a76d
- First working version of string synthesis, works on simple data types. · fc58e80a
  Mikaël Mayer authored 9 years ago
  
  fc58e80a
Nov 20, 2015
- String Tracing evaluator (invomplete!) · 79eb9ef7
  Manos Koukoutos authored 9 years ago
  
  79eb9ef7
Nov 17, 2015
- Refactor Evaluators. Introduce NDEvaluator · 27d034eb
  Manos Koukoutos authored 9 years ago
  27d034eb
Nov 06, 2015
- Set cardinality is a bigint, and we map it to CVC4's card · 7b4600e5
  Etienne Kneuss authored 9 years ago
  
  7b4600e5
Nov 04, 2015
- Refactor ChooseInfo to account for all types of synthesis problems · 76cd5058
  Manos Koukoutos authored 9 years ago
  76cd5058
Oct 22, 2015
- Adding Evaluation and code generation for strings. · 84e8cc8f
  Mikaël Mayer authored 9 years ago
  
  84e8cc8f
Oct 19, 2015
- convertHoles -> convert · e8e87ca8
  Manos Koukoutos authored 9 years ago
  
  e8e87ca8
Oct 16, 2015
- Squash synthesis conversion phases · 346748f5
  Manos Koukoutos authored 9 years ago
  
  346748f5
Oct 15, 2015
- Catch exceptions thrown in assertCnstr · d39332d2
  Etienne Kneuss authored 9 years ago
  
  d39332d2
Oct 09, 2015
- Support for calling @extern functions · f12376b2
  Etienne Kneuss authored 9 years ago
  
  f12376b2
- FiniteMap is implemented with a Map · f997139f
  Manos Koukoutos authored 9 years ago
  
  f997139f
Sep 29, 2015
- (a) Adding support for inferring invariants in Leon. · 9d37d6ad
  Ravi Madhavan authored 10 years ago
  9d37d6ad
Sep 18, 2015
- Fixes and rebase for quantifiers · 352a48f8
  Nicolas Voirol authored 9 years ago
  
  352a48f8