Commits · 92dd9a78d6c40f80ca3b9b37e8c8184261060ea3 · Why3 / why3

09 Oct, 2015 1 commit
- Add local rewrite rules for compute · 1c896e89
  MARCHE Claude authored Oct 09, 2015
  
  1c896e89
27 Aug, 2015 2 commits
- prover can now parse TPTP files (but still cannot run on them...) · ce8468c6
  MARCHE Claude authored Aug 27, 2015
  
  ce8468c6
- TPTP parsing: added a load function that expands the includes · de7a7a6e
  MARCHE Claude authored Aug 27, 2015
  
  de7a7a6e
26 Aug, 2015 1 commit
- Petit test de parsing des fichiers TPTP · d36beb56
  MARCHE Claude authored Aug 26, 2015
  
  d36beb56
20 Aug, 2015 1 commit
- Cleaning, add a few tests in the repository · 26dc2b1c
  MARCHE Claude authored Aug 02, 2015
  
  26dc2b1c
21 Jul, 2015 2 commits
- meta "rewrite_def" is transformed into meta "rewrite" by eliminate_definition · 0a79a618
  MARCHE Claude authored Jul 21, 2015
  
  0a79a618
- Extraction: replace debug message with appropriate warning · 6049c2ea
  MARCHE Claude authored Jul 21, 2015
  
  6049c2ea
20 Jul, 2015 2 commits
- SMTv2 printer: do not print declarations of algebraic datatypes when they are... · c5f1bb89
  MARCHE Claude authored Jul 20, 2015
```
SMTv2 printer: do not print declarations of algebraic datatypes when they are given in the syntax map
```
  c5f1bb89
- Driver for Zenon Modulo: no encoding needed · 4eed53de
  MARCHE Claude authored Jul 20, 2015
  
  4eed53de
18 Jul, 2015 1 commit
- Discriminate preserves the meta "rewrite" · d00b4a8b
  MARCHE Claude authored Jul 18, 2015
  
  d00b4a8b
17 Jul, 2015 2 commits
- a bit of cleaning · d9fe3880
  MARCHE Claude authored Jul 17, 2015
  
  d9fe3880
- printer smtv2: add missing cases in special handling of pattern-matching on Bool · 80fcc07d
  MARCHE Claude authored Jul 17, 2015
```
incidentally, removed also the "dirty hack"
```
  80fcc07d
16 Jul, 2015 1 commit
- tptp printers: produce an annotation for axioms declared as rewrite rules · 12edf166
  MARCHE Claude authored Jul 16, 2015
  
  12edf166
08 Jul, 2015 1 commit
- ignore map polymorphism in CVC4 1.4 · 5bb881e8
  MARCHE Claude authored Jul 08, 2015
  
  5bb881e8
11 May, 2015 1 commit
- new tests from bugs reported in the BTS. Bug 16972 fixed · 78d24b14
  MARCHE Claude authored May 11, 2015
  
  78d24b14
07 Apr, 2015 1 commit
- transformation detect_polymorphism: meta to ignore some polymorphic symbols · 31af7785
  MARCHE Claude authored Apr 07, 2015
  
  31af7785
03 Mar, 2015 3 commits
- test poly with defined projections · 6be4bcf6
  MARCHE Claude authored Feb 27, 2015
  
  6be4bcf6
- printing of match expressions in smtv2 · 80b5b265
  MARCHE Claude authored Mar 03, 2015
  
  80b5b265
- Tests de Michael · a07e74f4
  MARCHE Claude authored Mar 03, 2015
  
  a07e74f4
02 Mar, 2015 1 commit
- test for compile match · 9c60096e
  MARCHE Claude authored Mar 02, 2015
  
  9c60096e
25 Feb, 2015 1 commit
- Syntax converter for theories · 7487f2a1
  Clément Fumex authored Feb 25, 2015
  
  7487f2a1
17 Feb, 2015 3 commits
- Attempt to print algebraic data types in SMTv2 syntax · e1b4522b
  MARCHE Claude authored Feb 17, 2015
  
  e1b4522b
- New transformation eliminate_definition_if_poly, seems to work so far · 1d343bdb
  MARCHE Claude authored Feb 17, 2015
  
  1d343bdb
- Transformation detect_polymorphism seems to work, although · b3443c82
  MARCHE Claude authored Feb 17, 2015
```
probably not efficient because not memoized (Claude needs help for that)
```
  b3443c82
16 Feb, 2015 1 commit
- test detect poly · 95902ecd
  MARCHE Claude authored Feb 16, 2015
  
  95902ecd
11 Feb, 2015 1 commit
- test on booleans · 519e823c
  MARCHE Claude authored Feb 11, 2015
  
  519e823c
25 Oct, 2014 2 commits
- nightly bench: show in the subject of the mail if there are diffs or not · 1a1bcbab
  MARCHE Claude authored Oct 25, 2014
  
  1a1bcbab
- do not issue a warning on axioms derived from lemma functions · cf308ded
  MARCHE Claude authored Oct 25, 2014
  
  cf308ded
24 Oct, 2014 1 commit
- emit warning when axiom does not contains any local abstract symbol · d2c5647b
  MARCHE Claude authored Oct 24, 2014
  
  d2c5647b
19 Sep, 2014 1 commit
- Fixed small bug due to previous cleaning. Better cleaning in fact! · 208b5f5a
  MARCHE Claude authored Sep 19, 2014
  
  208b5f5a
18 Sep, 2014 1 commit
- removed usage of phantom type "notask" in sessions. Added detached old goals. · 45df78c8
  MARCHE Claude authored Sep 18, 2014
```
(no yet displayed in IDE)
```
  45df78c8
12 Sep, 2014 1 commit
- [compute] a simple additional test · cde46567
  MARCHE Claude authored Sep 12, 2014
  
  cde46567
09 Sep, 2014 2 commits
- [compute] maximal number of steps can be given with meta compute_max_steps · 6a3b6896
  MARCHE Claude authored Sep 09, 2014
  
  6a3b6896
- allow rewrite rules with a builtin symbol or a defined symbol, or a constructor · fad54f38
  MARCHE Claude authored Sep 09, 2014
```
as root of the left-hand side
```
  fad54f38
08 Sep, 2014 1 commit
- [compute] support for lambda-expressions · 5e54ace2
  MARCHE Claude authored Sep 08, 2014
  
  5e54ace2
07 Sep, 2014 1 commit
- compute: preserve labels as much as possible · 90bf8fb3
  MARCHE Claude authored Sep 07, 2014
```
side effect: also preserve asymmetric && and ||
```
  90bf8fb3
05 Sep, 2014 2 commits
- compute: more built-in simplifications · 8e850a73
  MARCHE Claude authored Sep 05, 2014
  
  8e850a73
- compute: attempt to rewrite undetermined equalities · 0f48a6f6
  MARCHE Claude authored Sep 05, 2014
  
  0f48a6f6
04 Sep, 2014 2 commits
- rename "split_goal" to "split_goal_wp" in session files · 310c51d0
  Andrei Paskevich authored Sep 04, 2014
  
  310c51d0
- fix #17181 · fb9ff35a
  MARCHE Claude authored Sep 04, 2014
  
  fb9ff35a