Updated raytracer test. Added SPASS test.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 135 insertions, 0 deletions

diff --git a/test/spass/VERSIONHISTORY b/test/spass/VERSIONHISTORY
new file mode 100644
index 0000000..448870c
--- /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.
+
+
+
+
+
+
+
+
+
+
+
+