3
- All source files moved to FreeBSD licence.
5
- Proof search is no longer entered if time limit or loops are 0.
7
- If the Sorts flag is set, Flotter prints clauses with set sort constraints.
9
- Default for Sorts is now correctly set to 1, reflecting documentation.
14
- Moved distribution to the FreeBSD licence.
16
- Joined the flags -PCRW und -PREW into the latter, renamed -QuantExch into -CNFQuantExch.
18
- For Linux binaries SPASS now always respects a given time limit.
21
- Moved to a fair and eager splitting heuristic. The new flag -SplitMinInst, sets the minimal
22
average number of instances of all split atoms of a split in order to perfrom the split and is
23
increased after each subsequent split and reset after performance of a different inference.
24
Propositional non-Horn clauses are always split.
25
Removed the flag -SplitHeuristic.
27
- Reimplemented the conjunctive normal form algorithm of FLOTTER.
29
- Added printing of the number of performed splits to the output.
31
- Added improved split backtracking where also the split information of a left branch refutation
32
is stored and then compared to the split information of the corresponding right branch, potentially
33
leading to a more aggressive branch condensing. See the papers on Splitting by Fietzke and Weidenbach.
35
- Added subterm contextual rewriting with fault caching. See the man page and the corresponding
36
papers by Weidenbach & Wischnewski.
38
- Added support for XOR, NAND, NOR and special symbol for NOT EQUAL to DFG syntax.
40
- Added new translator tptp2dfg from TPTP syntax to DFG syntax. See the man page.
42
- Added include directives to the SPASS DFG input syntax. For more information see the syntax description.
44
- Removed a bunch of compile time constants hindering handling of large files.
46
- Added native TPTP syntax support, controlled by the -TPTP flag.
48
- Moved from a sort theory module considering residues to a purely declaration based sort theory.
50
- New self written command line parser.
52
- Added the flags -CNFSub, -CNFCon, -CNFRedTimeLimit to FLOTTER that control
53
the use of subsumption, condensing and the overall time for reduction during
54
cnf transformation. See the man pages for further details.
56
- Added rewriting with unoriented equations to forward and
57
backward rewriting. Until Version 3.0 only for unit equations
58
both directions were implemented.
60
- Fixed all known bugs.
66
- Build the extended modal logic translation technology coming from
67
MSPASS into SPASS. This also results in a number of new flags. The
68
modal formulae are handled by translation to FOL, build into FLOTTER.
69
See the handbook and man page.
71
- Added two more formula renaming strategies for complex as
72
well as quantified formulae.
74
- Added additional selection strategies via the Select flag and
75
the input file option "set_Selection". See the man page.
77
- Added extended SPASS model format for saturated clause sets. The new clause
78
format is close to the format at run time and enables marking of selected
81
- Implemented the new settings command set_ClauseFormulaRelation that
82
allows to give the clause formula relation in the input file.
83
If FLOTTER is called or the flag DOCPROOF for SPASS is set,
84
this relation is computed.
86
- In full reduction mode, the reduction potential of unit clauses for splitting
87
is now considered with respect to the usable and worked-off clauses. In lazy
88
reduction mode, only worked off clauses are considered, as it was before for
89
both modes. This has an effect on the selection of clauses for splitting.
91
- During clause generation at parse time, the literal true, not(false) is no
92
longer deleted (the clause was not generated before) but handled
93
later on during input reduction.
94
This prevents strange error messages like "No Clauses found"
95
in case the clause set contains a single clause " -> true".
97
- Added the alarm module (alarm.[ch]) that stops SPASS after
98
reaching the set time limit via a signal mechanism in order
99
to prevent the mainloop time polling for taking too long to stop.
100
The alarm is set wirh respect to the value of the TimeLimit flag.
102
- Changed the static constant in the subsumption module that determined the max.
103
length of a clause to a flexible run time parameter. Prevents some ugly crashes.
104
Now the clause literal marking vectors are dynamically allocated and adjusted.
105
We will apply this transformation to all static constants in the next releases.
107
- Changed error reporting in dfgparser.y to verbose.
110
- Fixed the following bugs:
111
the flag flag_CNFFEQREDUCTIONS was forgotten to transfer to FLOTTER
112
if DocProof is set now the clause axiom relation is still printed
113
supressed printing of predefined symbols in case of model output
114
fixed missing label enumeration of sort declarations
115
fixed compiler warnings of gcc 3.3 and gcc 4.1.
116
fixed the symbol order to the input order when FLOTTER prints the CNF
122
- Fixed a bug in the sort module where an inference was missing.
124
- Some small changes to extend output in CHECK mode.
126
- Fixed a bug in fol_ReplaceVariable where an "else" branch was missing.
128
- Added another splitting heuristic where input conjecture ground clauses are always split.
129
The splitting heuristics can be controlled by the new flag "SplitHeuristic".
131
- Extended the documentation of DOCSPLIT, if set to 2, it now also prints the backtracked clauses.
133
- Changed makefile option names (now prefixed SPASS).
135
- The timing module is now based on gettimeofday to be compatible with the MAC infrastructure.
137
- Some minor code changes due to get rid of new gcc compiler warnings.
139
- Moved some misc.h, string.h inline functions to misc.c, string.c respectively to
140
get rid of compiler warnings
142
- added new flag SPLITHEURISTIC, enabling additional selection of any ground input
143
conjecture clauses for splitting.
145
- added Signal support, with makefile optioon SPASSIGNALS, the standard signals are catched
147
- fixed a bug in ana_CalculateFunctionPrecedence that could cause a segmentation fault
152
- Fixed a bug in the definition module. Formulae were not normalized before
153
application of the procedure, leading to wrong matchings of variables.
155
- Fixed a bug in the flag module. The subproof flagstore settings were not
156
complete: ordering flag and the weight flags were missing.
158
- Fixed a bug in dfgparser.y, where a missing semicolon with
159
bison version 1.75 now caused an error.
161
- Fixed a bug in cnf.c where the formula "equiv(false,false)" was
162
not properly treated in function cnf_RemoveTrivialAtoms.
164
- Fixed a bug in symbol_LowerSignature where capital 'A's and 'Z's were not
165
prefixed by a lowercase 'ss' due to their exclusion in the condition. This
166
caused problems in the result of dfg2tptp applied to dfg input files with
167
uppercase symbols starting with an 'A' or 'Z'.
169
- Now dfg2otter negates conjecture formulae of the SPASS input file
170
before printing the Otter usable list.
172
- Added man pages for dfg2ascii, dfg2otter and dfg2tptp.
177
- Corrections to spellings, documentation.
179
- Added handbooks for SPASS and dfg2dfg.
181
- Added contextual rewriting.
183
- Added semantic tautology check.
185
- Fixed bugs in CNF translation: Renaming, Equation elimination rules.
187
- Improved splitting clause selection on the basis of reduction potential.
189
- Improved robustness of initial clause list ordering.
191
- Added the terminator module.
193
- Extended formula definition detection/expansion to so called guarded definitions.
195
- Improved determination of initial precedence such that as many as possible
196
equations in the input clause list can be oriented.
198
- Added mainloop without complete interreduction.
200
- Developed PROOFSEARCH data type enabling a modularization of the SPASS
201
source code on search engine level, such that several proof attempts can
202
now be run completely independantly at the same time within SPASS.
204
- Moved GUI to Qt 3.0. The GUI now also includes dfg2dfg and new even more
205
user friendly layout. The GUI runs on any platform where SPASS and Qt are
212
- Improved SPASS man pages: In particular, we added further detailed
213
explanations of inference rule flags and soft typing flags.
215
- Significantly improved modularity of the code by making the flagstore
216
object part of the proof search object; so there is no global flagstore
217
around anymore. These changes touched nearly all modules.
219
- Changed certain clause generation procedures such that now applying SPASS
220
directly to a formula or subsequent application of FLOTTER and SPASS produce
221
exactly the same ordering of a clause set (literlas). Since the behaviour of
222
SPASS is not independant from initial clause/literal orderings the changes
223
make SPASS results a little more robust/more predictable.
224
As all code was touched, we also included a code style review (comments,
227
- Flag values given to SPASS are now checked and rejected if out of range.
232
- Changed some clause generation functions such that sequentially
233
applying FLOTTER, SPASS and just applying SPASS result in the
234
very same clause sets.
236
- Added the new tool dfg2dfg that supports transformations into
237
monadic clause classes and their further approximations.
242
- Sharpend renaming; it now potentially produces fewer clauses.
247
- Fixed inconsistencies between the DFG proof format description in
248
dfgsyntax.ps and the actual implementation. Proof checking is more
249
more liberal, because the empty clause needs not to have the highest
255
- Fixed a bug in the atom definition support where it could happen
256
that variable dependencies between the atom definition and formulae
257
outside the definition are discarded.
259
- Fixed a bug in the renaming module, where in some cases a renaming
260
with non-zero benefit was not performed.
added
removed
VERSIONHISTORY
