This history list describes the major differences between versions of the E equational theorem prover. Version 0.3 --> 0.31 Jungpana + Added TPTP format parser and output routines. + Did some more hacks for evaluation. + Restructured EXAMPLE_PROBLEMS subdirectory (now has the non-obfuscated TPTP and LOP versions of the CASC-15 problems). + Ripped out AVL trees and plugged in Splay trees in clb_ptrees.c. Should save significant amounts of memory, definitly speeds things up. Also reduces code size seriously. I will probably replace some more AVL trees with Splay trees. + Did that: Term Trees and Evaluation Trees now also use Splay trees. The remaning AVL's should be cleaned up sometimes, but are definitly uncritical. + Made $true-term special, it will now no longer carry ext-ref information. Not nice, but saves time and lot's of memory (3 words + Overhead per non-equational literal). + Added options for intermediate filtering of unprocessed clauses, including deletion of (possibly) non-redundant clauses to keep memory consumption in check. The prover no works quite well with whatever memory is offered (but 10 MB is about a rational minimum for non-trivial problems, with 128 MB suggested). + Made all boolean options NoArg options (instead of options with optional argument). + Following a hint by Roberto Nieuwenhuis, implemented real PosUnit-Strategy. I'll have to learn to read sometime... + Added soft cpu limit. + Debugged filtering of unprocessed clauses...first time I ever had to deal with a long overflow (due to my stupidity, no doubt). + Fixed bugs with long option handling and auto-mode (introduced by the changes necessary to support multiple paramod-strategies) + Added filtering for clause copies. + Added removing of clauses in cases of tight memory + Added new weight functions (Sigweight, Proofweight) + Removed entry-index in term banks + Changed rewrite machinery to stop replaced term from being reinserted as super-terms + Brought depanalyze up to working state (it currently prints a dependency graph for clauses, including demodulators). As a side effect, the -l3 option should now work and really print a complete protocol. + Fixed a bug in Equality factoring (it allowed unification between variable and predicate term). + Improved Auto-Mode for heuristic selection, now optimized for standard term ordering (no need for -tAuto anymore). Version 0.24 --> 0.3 Castleton + Tested signal handling under HPUX - works fine. + Added a simple auto-mode, changed WFCB interface and added WFCB-Administration for new heuristics-management. + BIG ONE: The command line semantics of the prover changed. Previously, "eprover p1 p2 p3" was equivalent to "eprover p1; eprover p2; eprover p3", but that did not make to much sense and complicated quite some things. Now it is equivalent to "cat p1 p2 p3| eprover". This allows you to modularize your specifications to a certain degree. + Added HCB-Administration and interface, rewrote heuristics-code. Does now need user-level documentation badly! + Wrote some of this documentation ;-) See CLIB/DOC/eprover.tex + Added proof output (machine friendly only, will need tools to post-process). + Hacked a lot of scripts for test runs and evaluation. + Fixed an extremely stupid bug (4 times over) in precedence generation, fixed a lot of bugs in weight generation that were masked by this one. Removed TOGenerateDefaultWeights(), as it was redundant anyways. Moved TOGenerateDefaultPrecedence() to che_to_precgen.[ch], were it belongs. + Fixed incompleteness caused by too strong subsumption. + Added auto-mode for heuristic selection and ordering selection. Version 0.23 --> 0.24 "Yunnan" + Fixed one more bug (subsumption of negative literals without recomputation of maximal literals) + Added simple signal handler to make --cpu-limit work on more platforms (should now work on all versions of Linux and Solaris, untested on other platforms). + Restructured part of the code, moved ProofState object deeper to allow clean coding of an auto-mode. + Variables do not have external references anymore -> saves time and space, and fixes half a bug. + Did some testing. "eprover -x Standard --memory-limit=192 --cpu-limit=300" on a SUN Ultra-10 Workstation should be able to solve about 1312 problems from the TPTP version 2.1.0. Version 0.22 --> 0.23 "StopGap" + Fixed bugs in LiteralCompare() (main reason for new release) + Added paramodulation with maximal variable sides (makes the prover more complete ;-) + Wrote some simple precedence generation schemes for the orderings + Added unit-paramodulation strategy for Horn Clauses form [Der91]. Very strong except for the TPTP PLA domain. Version 0.21 --> 0.22 "Risheehat" + Removed rewrite cruft (see last version change) + Unified term banks for processed and unprocessed clauses, optimized rewriting + Optimized unification + More verbose and more correct statistics + Removed a long-standing (but basically user-invisible) memory allocation bug from cto_ocb.c. Yes this is important (to me...)! + Optimized rewriting (again) with better use of normal form dates. Helps some, but not as much as I would have expected - perhaps a lingering bug? + Removed some more cruft, cleaned up term type + Simplified clause type. + Simplified equation type, replaced boolean properties with bit properties after profiling showed that shared terms are so efficient that clause and equation cells contribute significantly to memory consumption. + Implemented simple non-unit-subsumption. Prover now works in some fashion on non-unit problems (i.e. would not come in as last in CASC-15). + Did some more profiling on KBO and found out that new implementation does help -> it is now the default. + Implemented weight-generation schemes for KBO + Took variables out of the term trees in the term bank. + Implemented pre-hashing for term bank terms. Works great! + Changed default weight for terms and variables -> usually better performance. Currently, use -i1 -i1 for old default behaviour. + Decided to give cool names to releases. + Optimized rewriting once more...marginal improvements. Version 0.2 --> 0.21 + Rewrote rewrite machinery (still some cruft to remove) and simplified proof procedure + Added --version option for GNU's sake + Fixed still more serious (if seldom occuring) bugs + Added --memory-limit option (works only on systems with rational setrlimit()) + Added second implementation of KBO (no improvement *sigh*) + Some cleanup Version 0.1 --> 0.2 + Improved indexing + Stronger unit-subsumption + Fixed lots of serious bugs + Improved KBO efficiency