diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 12:34:43 +0000 |
commit | 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 (patch) | |
tree | 4e1422ea2a810520d0d9b0fbb78c0014ba9f8443 /test/spass/VERSIONHISTORY | |
parent | 93d89c2b5e8497365be152fb53cb6cd4c5764d34 (diff) | |
download | compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.tar.gz compcert-6c196ec8a41d6ed506c133c8b33dba9684f9a7a6.zip |
Updated raytracer test. Added SPASS test.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'test/spass/VERSIONHISTORY')
-rw-r--r-- | test/spass/VERSIONHISTORY | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/test/spass/VERSIONHISTORY b/test/spass/VERSIONHISTORY new file mode 100644 index 00000000..448870cc --- /dev/null +++ b/test/spass/VERSIONHISTORY @@ -0,0 +1,135 @@ +Version: 1.0.1 + + - Fixed a bug in the atom definition support where it could happen + that variable dependencies between the atom definition and formulae + outside the definition are discarded. + + - Fixed a bug in the renaming module, where in some cases a renaming + with non-zero benefit was not performed. + +Version: 1.0.2 + + - Fixed inconsistencies between the DFG proof format description in + dfgsyntax.ps and the actual implementation. Proof checking is more + more liberal, because the empty clause needs not to have the highest + clause number. + +Version: 1.0.3 + + - Sharpend renaming; it now potentially produces fewer clauses. + +Version: 1.0.4 + + - Changed some clause generation functions such that sequentially + applying FLOTTER, SPASS and just applying SPASS result in the + very same clause sets. + + - Added the new tool dfg2dfg that supports transformations into + monadic clause classes and their further approximations. + +Version: 1.0.5 + + - Improved SPASS man pages: In particular, we added further detailed + explanations of inference rule flags and soft typing flags. + + - Significantly improved modularity of the code by making the flagstore + object part of the proof search object; so there is no global flagstore + around anymore. These changes touched nearly all modules. + + - Changed certain clause generation procedures such that now applying SPASS + directly to a formula or subsequent application of FLOTTER and SPASS produce + exactly the same ordering of a clause set (literlas). Since the behaviour of + SPASS is not independant from initial clause/literal orderings the changes + make SPASS results a little more robust/more predictable. + As all code was touched, we also included a code style review (comments, + prototypes, ...). + + - Flag values given to SPASS are now checked and rejected if out of range. + +Version: 1.0.6 + + - Strengthened prototyping of functions in particular in the case of function + arguments. This resulted in specialized extra functions. + + - Improved printing efficiency by replacing (f)printf calls with (f)puts calls + whenever possible. + + - Removed the modul global precedence variable of the symbol modul and replaced + it by argument passing. The precedence is now stored in the proofsearch structure. + This affected huge parts of the SPASS code. + + - Adjusted comments and code layout. + + - Strengthened warnings for the gcc compiler. + + - Increased usage of the string module. + + +Version: 2.0.0 + + - Corrections to spellings, documentation. + + - Added handbooks for SPASS and dfg2dfg. + + - Added contextual rewriting. + + - Added semantic tautology check. + + - Fixed bugs in CNF translation: Renaming, Equation elimination rules. + + - Improved splitting clause selection on the basis of reduction potential. + + - Improved robustness of initial clause list ordering. + + - Added the terminator module. + + - Extended formula definition detection/expansion to so called guarded definitions. + + - Improved determination of initial precedence such that as many as possible + equations in the input clause list can be oriented. + + - Added mainloop without complete interreduction. + + - Developed PROOFSEARCH data type enabling a modularization of the SPASS + source code on search engine level, such that several proof attempts can + now be run completely independantly at the same time within SPASS. + + - Moved GUI to Qt 3.0. The GUI now also includes dfg2dfg and new even more + user friendly layout. The GUI runs on any platform where SPASS and Qt are + available. + +Version: 2.1 + + - Fixed a bug in the definition module. Formulae were not normalized before + application of the procedure, leading to wrong matchings of variables. + + - Fixed a bug in the flag module. The subproof flagstore settings were not + complete: ordering flag and the weight flags were missing. + + - Fixed a bug in dfgparser.y, where a missing semicolon with + bison version 1.75 now caused an error. + + - Fixed a bug in cnf.c where the formula "equiv(false,false)" was + not properly treated in function cnf_RemoveTrivialAtoms. + + - Fixed a bug in symbol_LowerSignature where capital 'A's and 'Z's were not + prefixed by a lowercase 'ss' due to their exclusion in the condition. This + caused problems in the result of dfg2tptp applied to dfg input files with + uppercase symbols starting with an 'A' or 'Z'. + + - Now dfg2otter negates conjecture formulae of the SPASS input file + before printing the Otter usable list. + + - Added man pages for dfg2ascii, dfg2otter and dfg2tptp. + + + + + + + + + + + + |