[llvm-commits] CVS: llvm-test/MultiSource/Applications/SPASS/AUTHORS COPYING LICENSE.TXT README VERSIONHISTORY
Duraid Madina
duraid at octopus.com.au
Sun Apr 24 21:13:27 PDT 2005
Changes in directory llvm-test/MultiSource/Applications/SPASS:
AUTHORS added (r1.1)
COPYING added (r1.1)
LICENSE.TXT added (r1.1)
README added (r1.1)
VERSIONHISTORY added (r1.1)
---
Log message:
add some docs
- for more, see the SPASS homepage: http://spass.mpi-sb.mpg.de/
---
Diffs of the changes: (+595 -0)
AUTHORS | 23 +++
COPYING | 340 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
LICENSE.TXT | 1
README | 96 ++++++++++++++++
VERSIONHISTORY | 135 ++++++++++++++++++++++
5 files changed, 595 insertions(+)
Index: llvm-test/MultiSource/Applications/SPASS/AUTHORS
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/AUTHORS:1.1
*** /dev/null Sun Apr 24 23:13:26 2005
--- llvm-test/MultiSource/Applications/SPASS/AUTHORS Sun Apr 24 23:13:16 2005
***************
*** 0 ****
--- 1,23 ----
+ Current:
+ ========
+
+ Christoph Weidenbach <weidenb at mpi-sb.mpg.de>
+ Uwe Brahm <brahm at mpi-sb.mpg.de>
+ Thomas Hillenbrand <hillen at mpi-sb.mpg.de>
+ Dalibor Topic <topic at mpi-sb.mpg.de>
+
+
+ Former:
+ =======
+
+ Bijan Afshordel <afshorde at mpi-sb.mpg.de>
+ Christof Brinker <chbr at mpi-sb.mpg.de>
+ Christian Cohrs <cohrs at mpi-sb.mpg.de>
+ Thorsten Engel <engel at mpi-sb.mpg.de>
+ Bernd Gaede <gaede at mpi-sb.mpg.de>
+ Peter Graf <graf at mpi-sb.mpg.de>
+ Georg Jung <gjung at mpi-sb.mpg.de>
+ Christoph Meyer <meyer at mpi-sb.mpg.de>
+ Georg Rock <rock at mpi-sb.mpg.de>
+ Christian Theobalt <theobalt at mpi-sb.mpg.de>
+
Index: llvm-test/MultiSource/Applications/SPASS/COPYING
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/COPYING:1.1
*** /dev/null Sun Apr 24 23:13:27 2005
--- llvm-test/MultiSource/Applications/SPASS/COPYING Sun Apr 24 23:13:16 2005
***************
*** 0 ****
--- 1,340 ----
+ GNU GENERAL PUBLIC LICENSE
+ Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.
+ 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+ freedom to share and change it. By contrast, the GNU General Public
+ License is intended to guarantee your freedom to share and change free
+ software--to make sure the software is free for all its users. This
+ General Public License applies to most of the Free Software
+ Foundation's software and to any other program whose authors commit to
+ using it. (Some other Free Software Foundation software is covered by
+ the GNU Library General Public License instead.) You can apply it to
+ your programs, too.
+
+ When we speak of free software, we are referring to freedom, not
+ price. Our General Public Licenses are designed to make sure that you
+ have the freedom to distribute copies of free software (and charge for
+ this service if you wish), that you receive source code or can get it
+ if you want it, that you can change the software or use pieces of it
+ in new free programs; and that you know you can do these things.
+
+ To protect your rights, we need to make restrictions that forbid
+ anyone to deny you these rights or to ask you to surrender the rights.
+ These restrictions translate to certain responsibilities for you if you
+ distribute copies of the software, or if you modify it.
+
+ For example, if you distribute copies of such a program, whether
+ gratis or for a fee, you must give the recipients all the rights that
+ you have. You must make sure that they, too, receive or can get the
+ source code. And you must show them these terms so they know their
+ rights.
+
+ We protect your rights with two steps: (1) copyright the software, and
+ (2) offer you this license which gives you legal permission to copy,
+ distribute and/or modify the software.
+
+ Also, for each author's protection and ours, we want to make certain
+ that everyone understands that there is no warranty for this free
+ software. If the software is modified by someone else and passed on, we
+ want its recipients to know that what they have is not the original, so
+ that any problems introduced by others will not reflect on the original
+ authors' reputations.
+
+ Finally, any free program is threatened constantly by software
+ patents. We wish to avoid the danger that redistributors of a free
+ program will individually obtain patent licenses, in effect making the
+ program proprietary. To prevent this, we have made it clear that any
+ patent must be licensed for everyone's free use or not licensed at all.
+
+ The precise terms and conditions for copying, distribution and
+ modification follow.
+
+ GNU GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License applies to any program or other work which contains
+ a notice placed by the copyright holder saying it may be distributed
+ under the terms of this General Public License. The "Program", below,
+ refers to any such program or work, and a "work based on the Program"
+ means either the Program or any derivative work under copyright law:
+ that is to say, a work containing the Program or a portion of it,
+ either verbatim or with modifications and/or translated into another
+ language. (Hereinafter, translation is included without limitation in
+ the term "modification".) Each licensee is addressed as "you".
+
+ Activities other than copying, distribution and modification are not
+ covered by this License; they are outside its scope. The act of
+ running the Program is not restricted, and the output from the Program
+ is covered only if its contents constitute a work based on the
+ Program (independent of having been made by running the Program).
+ Whether that is true depends on what the Program does.
+
+ 1. You may copy and distribute verbatim copies of the Program's
+ source code as you receive it, in any medium, provided that you
+ conspicuously and appropriately publish on each copy an appropriate
+ copyright notice and disclaimer of warranty; keep intact all the
+ notices that refer to this License and to the absence of any warranty;
+ and give any other recipients of the Program a copy of this License
+ along with the Program.
+
+ You may charge a fee for the physical act of transferring a copy, and
+ you may at your option offer warranty protection in exchange for a fee.
+
+ 2. You may modify your copy or copies of the Program or any portion
+ of it, thus forming a work based on the Program, and copy and
+ distribute such modifications or work under the terms of Section 1
+ above, provided that you also meet all of these conditions:
+
+ a) You must cause the modified files to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ b) You must cause any work that you distribute or publish, that in
+ whole or in part contains or is derived from the Program or any
+ part thereof, to be licensed as a whole at no charge to all third
+ parties under the terms of this License.
+
+ c) If the modified program normally reads commands interactively
+ when run, you must cause it, when started running for such
+ interactive use in the most ordinary way, to print or display an
+ announcement including an appropriate copyright notice and a
+ notice that there is no warranty (or else, saying that you provide
+ a warranty) and that users may redistribute the program under
+ these conditions, and telling the user how to view a copy of this
+ License. (Exception: if the Program itself is interactive but
+ does not normally print such an announcement, your work based on
+ the Program is not required to print an announcement.)
+
+ These requirements apply to the modified work as a whole. If
+ identifiable sections of that work are not derived from the Program,
+ and can be reasonably considered independent and separate works in
+ themselves, then this License, and its terms, do not apply to those
+ sections when you distribute them as separate works. But when you
+ distribute the same sections as part of a whole which is a work based
+ on the Program, the distribution of the whole must be on the terms of
+ this License, whose permissions for other licensees extend to the
+ entire whole, and thus to each and every part regardless of who wrote it.
+
+ Thus, it is not the intent of this section to claim rights or contest
+ your rights to work written entirely by you; rather, the intent is to
+ exercise the right to control the distribution of derivative or
+ collective works based on the Program.
+
+ In addition, mere aggregation of another work not based on the Program
+ with the Program (or with a work based on the Program) on a volume of
+ a storage or distribution medium does not bring the other work under
+ the scope of this License.
+
+ 3. You may copy and distribute the Program (or a work based on it,
+ under Section 2) in object code or executable form under the terms of
+ Sections 1 and 2 above provided that you also do one of the following:
+
+ a) Accompany it with the complete corresponding machine-readable
+ source code, which must be distributed under the terms of Sections
+ 1 and 2 above on a medium customarily used for software interchange; or,
+
+ b) Accompany it with a written offer, valid for at least three
+ years, to give any third party, for a charge no more than your
+ cost of physically performing source distribution, a complete
+ machine-readable copy of the corresponding source code, to be
+ distributed under the terms of Sections 1 and 2 above on a medium
+ customarily used for software interchange; or,
+
+ c) Accompany it with the information you received as to the offer
+ to distribute corresponding source code. (This alternative is
+ allowed only for noncommercial distribution and only if you
+ received the program in object code or executable form with such
+ an offer, in accord with Subsection b above.)
+
+ The source code for a work means the preferred form of the work for
+ making modifications to it. For an executable work, complete source
+ code means all the source code for all modules it contains, plus any
+ associated interface definition files, plus the scripts used to
+ control compilation and installation of the executable. However, as a
+ special exception, the source code distributed need not include
+ anything that is normally distributed (in either source or binary
+ form) with the major components (compiler, kernel, and so on) of the
+ operating system on which the executable runs, unless that component
+ itself accompanies the executable.
+
+ If distribution of executable or object code is made by offering
+ access to copy from a designated place, then offering equivalent
+ access to copy the source code from the same place counts as
+ distribution of the source code, even though third parties are not
+ compelled to copy the source along with the object code.
+
+ 4. You may not copy, modify, sublicense, or distribute the Program
+ except as expressly provided under this License. Any attempt
+ otherwise to copy, modify, sublicense or distribute the Program is
+ void, and will automatically terminate your rights under this License.
+ However, parties who have received copies, or rights, from you under
+ this License will not have their licenses terminated so long as such
+ parties remain in full compliance.
+
+ 5. You are not required to accept this License, since you have not
+ signed it. However, nothing else grants you permission to modify or
+ distribute the Program or its derivative works. These actions are
+ prohibited by law if you do not accept this License. Therefore, by
+ modifying or distributing the Program (or any work based on the
+ Program), you indicate your acceptance of this License to do so, and
+ all its terms and conditions for copying, distributing or modifying
+ the Program or works based on it.
+
+ 6. Each time you redistribute the Program (or any work based on the
+ Program), the recipient automatically receives a license from the
+ original licensor to copy, distribute or modify the Program subject to
+ these terms and conditions. You may not impose any further
+ restrictions on the recipients' exercise of the rights granted herein.
+ You are not responsible for enforcing compliance by third parties to
+ this License.
+
+ 7. If, as a consequence of a court judgment or allegation of patent
+ infringement or for any other reason (not limited to patent issues),
+ conditions are imposed on you (whether by court order, agreement or
+ otherwise) that contradict the conditions of this License, they do not
+ excuse you from the conditions of this License. If you cannot
+ distribute so as to satisfy simultaneously your obligations under this
+ License and any other pertinent obligations, then as a consequence you
+ may not distribute the Program at all. For example, if a patent
+ license would not permit royalty-free redistribution of the Program by
+ all those who receive copies directly or indirectly through you, then
+ the only way you could satisfy both it and this License would be to
+ refrain entirely from distribution of the Program.
+
+ If any portion of this section is held invalid or unenforceable under
+ any particular circumstance, the balance of the section is intended to
+ apply and the section as a whole is intended to apply in other
+ circumstances.
+
+ It is not the purpose of this section to induce you to infringe any
+ patents or other property right claims or to contest validity of any
+ such claims; this section has the sole purpose of protecting the
+ integrity of the free software distribution system, which is
+ implemented by public license practices. Many people have made
+ generous contributions to the wide range of software distributed
+ through that system in reliance on consistent application of that
+ system; it is up to the author/donor to decide if he or she is willing
+ to distribute software through any other system and a licensee cannot
+ impose that choice.
+
+ This section is intended to make thoroughly clear what is believed to
+ be a consequence of the rest of this License.
+
+ 8. If the distribution and/or use of the Program is restricted in
+ certain countries either by patents or by copyrighted interfaces, the
+ original copyright holder who places the Program under this License
+ may add an explicit geographical distribution limitation excluding
+ those countries, so that distribution is permitted only in or among
+ countries not thus excluded. In such case, this License incorporates
+ the limitation as if written in the body of this License.
+
+ 9. The Free Software Foundation may publish revised and/or new versions
+ of the General Public License from time to time. Such new versions will
+ be similar in spirit to the present version, but may differ in detail to
+ address new problems or concerns.
+
+ Each version is given a distinguishing version number. If the Program
+ specifies a version number of this License which applies to it and "any
+ later version", you have the option of following the terms and conditions
+ either of that version or of any later version published by the Free
+ Software Foundation. If the Program does not specify a version number of
+ this License, you may choose any version ever published by the Free Software
+ Foundation.
+
+ 10. If you wish to incorporate parts of the Program into other free
+ programs whose distribution conditions are different, write to the author
+ to ask for permission. For software which is copyrighted by the Free
+ Software Foundation, write to the Free Software Foundation; we sometimes
+ make exceptions for this. Our decision will be guided by the two goals
+ of preserving the free status of all derivatives of our free software and
+ of promoting the sharing and reuse of software generally.
+
+ NO WARRANTY
+
+ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+ FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN
+ OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+ PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+ OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+ MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS
+ TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE
+ PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+ REPAIR OR CORRECTION.
+
+ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+ WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+ REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+ INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+ OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+ TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+ YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+ PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+ POSSIBILITY OF SUCH DAMAGES.
+
+ END OF TERMS AND CONDITIONS
+
+ How to Apply These Terms to Your New Programs
+
+ If you develop a new program, and you want it to be of the greatest
+ possible use to the public, the best way to achieve this is to make it
+ free software which everyone can redistribute and change under these terms.
+
+ To do so, attach the following notices to the program. It is safest
+ to attach them to the start of each source file to most effectively
+ convey the exclusion of warranty; and each file should have at least
+ the "copyright" line and a pointer to where the full notice is found.
+
+ <one line to give the program's name and a brief idea of what it does.>
+ Copyright (C) 19yy <name of author>
+
+ This program is free software; you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation; either version 2 of the License, or
+ (at your option) any later version.
+
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with this program; if not, write to the Free Software
+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+
+
+ Also add information on how to contact you by electronic and paper mail.
+
+ If the program is interactive, make it output a short notice like this
+ when it starts in an interactive mode:
+
+ Gnomovision version 69, Copyright (C) 19yy name of author
+ Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+ This is free software, and you are welcome to redistribute it
+ under certain conditions; type `show c' for details.
+
+ The hypothetical commands `show w' and `show c' should show the appropriate
+ parts of the General Public License. Of course, the commands you use may
+ be called something other than `show w' and `show c'; they could even be
+ mouse-clicks or menu items--whatever suits your program.
+
+ You should also get your employer (if you work as a programmer) or your
+ school, if any, to sign a "copyright disclaimer" for the program, if
+ necessary. Here is a sample; alter the names:
+
+ Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+ `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+ <signature of Ty Coon>, 1 April 1989
+ Ty Coon, President of Vice
+
+ This General Public License does not permit incorporating your program into
+ proprietary programs. If your program is a subroutine library, you may
+ consider it more useful to permit linking proprietary applications with the
+ library. If this is what you want to do, use the GNU Library General
+ Public License instead of this License.
Index: llvm-test/MultiSource/Applications/SPASS/LICENSE.TXT
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/LICENSE.TXT:1.1
*** /dev/null Sun Apr 24 23:13:27 2005
--- llvm-test/MultiSource/Applications/SPASS/LICENSE.TXT Sun Apr 24 23:13:16 2005
***************
*** 0 ****
--- 1 ----
+ see the file "COPYING"
Index: llvm-test/MultiSource/Applications/SPASS/README
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/README:1.1
*** /dev/null Sun Apr 24 23:13:27 2005
--- llvm-test/MultiSource/Applications/SPASS/README Sun Apr 24 23:13:16 2005
***************
*** 0 ****
--- 1,96 ----
+ Welcome to SPASS!
+ =================
+
+ This is the generic README file for all SPASS distributions, so your downloaded
+ package may only contain a subset of what is described here.
+
+
+ Important Files
+ ===============
+
+ AUTHORS all authors that contributed to SPASS
+
+ INSTALLATION for a guide to install the prover, man pages,
+ tools etc.; by default binaries are installed
+ in /usr/local/bin and man-pages in /usr/local/man;
+ use the prefix option of make install for a different
+ path
+
+ COPYING for the licence agreement that you certify by
+ installation, its the GNU GENERAL PUBLIC LICENSE, Version 2
+
+ VERSIONHISTORY changes starting from version 1.0.0
+
+ README is this file
+
+
+
+
+ Programs
+ ========
+
+ The distribution contains the following programs. Most
+ of them give you a brief description if they are called
+ without arguments. Most of the programs come with man-pages.
+
+ SPASS is our prover for first-order logic with equality.
+
+ FLOTTER translates first-order formulae into clauses; its
+ incorporated in SPASS and hence now only a link to
+ SPASS.
+
+ pcs is our proof checker. NOTE that in its default settings
+ pcs needs an installation of otter for proof checking.
+ You can also employ SPASS itself for this purpose by the
+ -o option.
+
+ pgen generates out of a SPASS proof file all subtasks needed
+ to guarantee the correctness of the proof.
+
+ dfg2otter translates DFG-syntax input files into otter input files,
+ without any settings commands.
+
+ dfg2otter.pl has the same functionality than dfg2otter but adds specific
+ settings that are useful if otter is employd as a proof checker
+ for SPASS.
+
+ dfg2tptp translates DFG-syntax input files into TPTP input files.
+
+
+ dfg2ascii provides an ASCII pretty print of DFG-syntax input files
+
+
+ Documentation
+ =============
+
+ Besides the man pages, in the directory doc you'll find a description
+ of our input syntax (spass-input-syntax.pdf), a small tutorial (tutorial.pdf)
+ that is just a print out of our tutorial web page and the complete
+ theory of SPASS (handbook-spass.pdf). Furthermore, there is a FAQ
+ database (faq.txt).
+
+
+ Examples
+ ========
+
+ In the examples directory you'll find some small examples. Further
+ example collections can be downloaded from the SPASS homepage. By
+ convention, files ending in ".dfg" are formula files and files ending
+ in ".cnf" are files containing clauses.
+
+
+ WWW
+ ===
+
+ Consider the SPASS homepage at
+
+ http://spass.mpi-sb.mpg.de/
+
+ for recent developments, downloads etc.
+
+
+
+
+
+ have SPASS
+ Christoph Weidenbach
\ No newline at end of file
Index: llvm-test/MultiSource/Applications/SPASS/VERSIONHISTORY
diff -c /dev/null llvm-test/MultiSource/Applications/SPASS/VERSIONHISTORY:1.1
*** /dev/null Sun Apr 24 23:13:27 2005
--- llvm-test/MultiSource/Applications/SPASS/VERSIONHISTORY Sun Apr 24 23:13:16 2005
***************
*** 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.
+
+
+
+
+
+
+
+
+
+
+
+
More information about the llvm-commits
mailing list