# $Id: README,v 1.33 2008-06-16 01:23:54 babic Exp $ Copyright (C) 2007. Domagoj Babic. All rights reserved. This document is considered Spear documentation, and can be used under the same terms as the theorem prover itself. To see the license, please run Spear with --license. This is is the change log of the Spear theorem prover. Currently, Spear supports the following input formats: - Dimacs CNF - Spear modular arithmetic format v 1.0 - SMT format (use smft2sf tool) spear-2-6 [Mon Jun 16 01:17:16 UTC 2008] - Fixed bug in constant folding of sign extension, discovered and reported by Trevor Alexander Hansen (Thx!). Added Luby sequence restarts and phase saving. Both features are disabled by default (see --hidden if you want to play with them). The next version of Spear will offer a new set of parameters with tuned Luby restarts. spear-2-5 [Thu Apr 3 02:12:54 UTC 2008] - New fh_1_4 set of parameters. This release competed at SAT Race 2008. spear-2-4 [Tue Mar 11 17:51:04 UTC 2008] - Minor code cleanup, added several new targets to the Makefile. Changed the default parameter configuration for CNF input from fh_1_0 to fh_1_3. If Spear runs slower now on your instances, use --spset-autotuned-fh_1_0. spear-2-3 [Thu Mar 6 18:10:45 UTC 2008] - Added 3 new sets of parameters (fh_1_3, quasigroup, graph coloring) found by ParamILS. Fixed a performance bug in common subexpression elimination, reported by Greg Bronevetsky (currently at Lawrence Livermore National Lab). Thx Greg for reporting it! This release is a good candidate for SAT Race 2008 competition. spear-2-2 [Mon Feb 18 19:17:49 UTC 2008] - Code cleanup. spear-2-1-revert [Sat Feb 16 05:26:12 UTC 2008] - Reverted back to 2.1. spear-subsumption [Sat Feb 16 05:04:01 UTC 2008] - Experimental implementation of subsumption, but doesn't seem to be very effective. Next release will be a revert. spear-2-1 [Sat Feb 16 04:54:32 UTC 2008] - Removed fine-grained structural abstraction and don't-care analysis. Coarse-grained abstraction is much more effective and don't-care analysis is not worth the effort. Added -Wextra to Makefile. Added new clause sorting heuristics. Improved clause deletion. A couple of fixes in SpearTools. Eliminated cluster solving mode (ineffective). spear-2-0 [Wed Oct 17 21:39:09 UTC 2007] - Complete rewrite of the front-end (parser) and common subexpression elimination. Wrote expression-level simplifier, and wrote the first part of dynamic gating analysis. Added fine-grained structural abstraction, but more work is needed on that, so it's disabled by default (use --laziness to experiment with it). spear-1-9 [Tue Jun 26 02:46:01 UTC 2007] - Added switch for SMT-COMP compatible output, added a new set of parameters fh_1_2. spear-1-8 - Fixed an overflow bug in multiplication with 2^32. Improved memory handling, fixed incomplete cleanup (important only if the solver is called a large number of times - related to Calysto). Added one boolean parameter. Cleaned up the code a bit. Cleaned and improved SF parser. Fixed a bug in signed division with some constants. spear-1-7 - Fixed a bug in the modular arithmetic interface reported by Ashutosh Kumar Gupta (Thx!). Fixed a bug in unsigned division by a constant - under some fairly rare circumstances, the solver could have segfaulted (interestingly extensive testing of div did not reveal this bug before). Renamed model-stdout switch to just model. spear-1-6 - Fixed a minor performance bug (in some rare cases, simplify would never run, even on hard benchmarks). Fixed a recently introduced performance bug in the restart mechanism (restarts became rare). Fixed a performance bug in variable elimination - recently pure literal rule was moved into variable elimination, and there were some undesirable interactions between the two. Solver passes 20 million random test cases. spear-1-5 - Removed fh_1_2 set, as it was ineffective. Added/removed a couple of parameters. Fixed a bug that under very rare circumstances could lead to an inconsistent state of the decision queue. Fixed bug in variable elimination which might cause UNKNOWN solution being reported. Added code for avoiding memory thrashing. Added new parameter set ibm-bmc, found by Frank Hutter, optimized for IBM BMC instances. Made clause deletion more aggressive. Decision heap is now always in the proper order, which means that heuristics are more aggressive, and there should be a more pronounced difference among different heuristics. Added some comments to the help message which point out that some heuristics are not appropriate for a variable decision heuristic. spear-1-4 - Added -ffloat-store to the Makefile to avoid additional 80-bit precision. That additional precision can cause non-determinism due to rounding errors between different FPUs even when the decision procedure is completely deterministic. This was observed on Alloy handshake.als.3.cnf instance, where on the same AMD machine 32-bit version ran in 0.33 sec, while the 64-bit version timed out after 3000 sec. I tracked the problem down to the divergence in the rounding errors. Quite a fascinating case! Fixed a bug in parsing of SF files - sle was read as slt. Fixed a bug in modular arithmetic expression simplifier. Fixed bug in cyclic constraints - in some cases variables in cyclic constraints would not be properly declared. Added a small model heuristic for modular arithmetic. spear-1-3 - This is the first release that supports Spear modular arithmetic format v 1.0. Note that although the core of the solver has been heavily tested, the parser and this new interface hasn't. Since I don't use it in my work (Calysto static checker calls Spear routines directly), there might be some bugs. If you get an unexpected answer, or Spear segfaults, please file a bug report (babic >AT< cs ubc ca). Other modifications: fixed a performance bug in the simplifier, fixed clock() overflow on 32-bit machines reported by Frank Hutter (thx Frank!), significantly optimized handling of the modular arithmetic constraints, and cleaned code a bit. Wrote a simple random test case generator that tests complex operations. Spear passes tens of thousands of random test vectors for each allowed bit-width for all complex operations (div/mul/rem). Hopefully, simple ops are simple enough, that there are no bugs :-). The SAT solver has been extensively tested for an extremely large number of parameter combinations on a 50 machine cluster (thx to Frank). Note that for verification reasons, this release still has solution checking enabled. spear-1-2 - Changed default parameters to fh-1-0 with additional sorting of original clauses. Old defaults are accessible through spset-old-default. Cleaned up parameter handling code, added clause-inversion parameter, and split clause-sort-heur into separate heuristics for sorting learned (learned-clause-sort-heur) and original (orig-clause-sort-heur) heuristics. Cleaned up parsing and solver instance creation. Added a hidden parameter for seed setup. Fixed performance bug - all versions from 1.0 to 1.1 (including the one sent to SAT 07' competition) had clause deletion disabled. This bug was introduced in the last cycle of optimizations for the competition :-(. Added additional heuristic for finding the second watched literal. Optimized timeout checking code to avoid divisions. spear-1-1 - Returned default sw verification parameters to the old, manually found defaults. Fixed several minor bugs: command line variable decision heuristic was not handled properly (ended up being NOP), fixed timeout bug (some parameters sets would incorrectly overwrite timeout limit), fixed memory leak that appeared in the incremental mode during the last round of optimizations. Added bit-vector specific decision heuristic (more works needs to be done on nailing that one down). This is the first public release of Spear. Modular arithmetic interface is still disabled. spear-1-0 - Fixed bug in resolution reported by Frank Hutter, optimized pure literal rule a bit. Added several assertions. This version was submitted to SAT competition 2007. spear-0-9 - Almost complete rewrite of resolution. Fixed some other minor things, like ANSI compatibility, and LLVM build process compatibility. Default sw verification parameters is now fh_1_0 set. spear-0-8 - Minor performance improvements, wrote first implementation of resolution, removed the old clumsy binary resolution. More work needs to be done on getting resolution to work really well. spear-0-7 - Significant performance improvements, exposed all search params to the command line. spear-0-6 - Performance improvements. spear-0-5 - Fixed bug in conflict analysis. Performance is much worse now. Added a number of heuristics, split the tool code into separate files (Solver.*). rel-0-4 - Improved performance, removed equivalence processing, but left some comments how to do it. New heuristic might make equivalence processing ineffective anyways. Still some work left to be done on clause removal. rel-0-3 - Improved performance, added equivalence processing, clause removal. rel-0-2 - Improved performance, added timeout feature. rel-0-1 - Solver passes 3M random tests with 10 variables (compared to zChaff for unsat instances). Still more work to be done on the performance side.