Commits · 74aba11fbb8e7b09a5d0c636efb80334132e3c12 · LARA / inox · GitLab

Snippets Groups Projects

Jul 14, 2015
- Introducing UnapplyPattern, plus improvements · 74aba11f
  Manos Koukoutos authored 9 years ago
  74aba11f
Jul 09, 2015
- Correct typo · 101707b6
  Manos Koukoutos authored 9 years ago
  
  101707b6
- Improve/fix/use consistently features related to deep type hierarchies · e45a3e18
  Manos Koukoutos authored 9 years ago
  
  e45a3e18
- More support for inheritance · d02ded7e
  Manos Koukoutos authored 9 years ago
  d02ded7e
- Unify XOperators. Eliminate dead trees · baa5b60b
  Manos Koukoutos authored 9 years ago
  
  baa5b60b
- Copyright notices · b5a913dc
  Manos Koukoutos authored 9 years ago
  
  b5a913dc
Jul 06, 2015
- Fix handling of holes, and multiple-variables chooses · 8ca74bdc
  Etienne Kneuss authored 9 years ago
  
  8ca74bdc
Jul 02, 2015
- Indentation · eb451d8e
  Manos Koukoutos authored 9 years ago
  
  eb451d8e
- Refactor quantified solvers. smt-z3-q is now sound · 011c63af
  Manos Koukoutos authored 9 years ago
  
  011c63af
Jun 30, 2015
- Remove Choose having mutable, optional implementation · e89165c6
  Etienne Kneuss authored 9 years ago
  
  e89165c6
Jun 29, 2015
- Fix Asserts in VCs in fairz3 · c0b4ac13
  Etienne Kneuss authored 9 years ago
  
  c0b4ac13
Jun 25, 2015
- Enrich TypedFunDef/Lambda API a little · 97d98a80
  Manos Koukoutos authored 9 years ago
  
  97d98a80
- Introduce FunctionFlags. Remove all other mutability from FunDef (except body). · 6b897a99
  Manos Koukoutos authored 9 years ago
  
  6b897a99
Jun 24, 2015
- Simlify check/getModel in ProofSolver · d395bae9
  Manos Koukoutos authored 9 years ago
  d395bae9
Jun 23, 2015
- Filter model variables with function parameters in new Solvers · 8f426de9
  Manos Koukoutos authored 9 years ago
  
  8f426de9
Jun 22, 2015
- No forall in cvc4-cex · 9806d230
  Manos Koukoutos authored 9 years ago
  
  9806d230
Jun 19, 2015
- Report timeouts as timeouts, not unknown · e69595de
  Etienne Kneuss authored 9 years ago
  
  e69595de
Jun 17, 2015
- Simplify/clean up extractors · a8cdb84c
  Manos Koukoutos authored 9 years ago
  
  a8cdb84c
- Some simplifications · a9c3f4c2
  Manos Koukoutos authored 9 years ago
  
  a9c3f4c2
Jun 10, 2015
- Include GroundSolver in docs · 0118c357
  Manos Koukoutos authored 9 years ago
  
  0118c357
- Introducing GroundSolver · 8d899398
  Manos Koukoutos authored 9 years ago
  
  8d899398
- Assume ind. hypothesis for all VCKind's · ff0c03d0
  Manos Koukoutos authored 9 years ago
  
  ff0c03d0
- More cleanup · 64c49949
  Manos Koukoutos authored 9 years ago
  
  64c49949
- Assume contracts of inductive calls · 58c16119
  Manos Koukoutos authored 9 years ago
  
  58c16119
- Display id instead of globalID for SMT identifiers · 024778d8
  Manos Koukoutos authored 9 years ago
  
  024778d8
- Choose GroupedTactic even if subsolver of Portfolio needs it · d5536f7c
  Manos Koukoutos authored 10 years ago
  
  d5536f7c
Jun 03, 2015
- Add --assumpre option to assume the precondition when unfolding · 85505865
  Etienne Kneuss authored 10 years ago
  85505865
Jun 02, 2015
- Prevent user in case of an invalid usage of ADTs · 1949076d
  Etienne Kneuss authored 10 years ago
  1949076d
- Handle conversion errors gracefully in fair-z3, detect bad ADTs · edf7a574
  Etienne Kneuss authored 10 years ago
  
  edf7a574
- Decouple ADT-dependencies from solvers · 4128ce89
  Etienne Kneuss authored 10 years ago
  4128ce89
Jun 01, 2015
- Introduce Modulo as mod operator on BigInt · 08113e8d
  Regis Blanc authored 10 years ago
  08113e8d
- Move Option to lang.Option, add Map.get/getOrElse/+ · 1b3e61b0
  Etienne Kneuss authored 10 years ago
  
  1b3e61b0
May 29, 2015
- Improve model reconstruction by providing target type · 3ef201af
  Etienne Kneuss authored 10 years ago
  3ef201af
- Implement char comparison (<,<=,>,>=) · e8e1b598
  Etienne Kneuss authored 10 years ago
  
  e8e1b598
- Translate if-then-else back to leon · 4eabdc60
  Manos Koukoutos authored 10 years ago
  
  4eabdc60
May 27, 2015
- Maps/Sets have explicit types, remove Empty/NonemptySet/Map · 73ca139b
  Etienne Kneuss authored 10 years ago
  
  73ca139b
May 26, 2015
- Improvements in smtlib solvers · 0666b058
  Manos Koukoutos authored 10 years ago
  
  0666b058
- Portfolio should implement assertVC · 73ce19e6
  Manos Koukoutos authored 10 years ago
  
  73ce19e6
- Give 0 rather than -0 to solver · fcac8a89
  Manos Koukoutos authored 10 years ago
  
  fcac8a89
- Fix soundness bug for smt-cvc4-cex/proof · 47a16427
  Manos Koukoutos authored 10 years ago
  
  47a16427