src/HOL/Tools/sat_solver.ML
Mon, 31 May 2010 18:49:32 +0200 blanchet move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it;
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Sat, 06 Feb 2010 15:51:22 +0100 wenzelm proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
Tue, 01 Dec 2009 22:29:46 +0000 webertj read_dimacs_cnf_file can now read DIMACS files that contain successive
Thu, 29 Oct 2009 23:08:51 +0100 blanchet merged
Thu, 29 Oct 2009 15:23:25 +0100 blanchet make "auto" SAT solver less verbose
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Tue, 27 Oct 2009 16:03:06 +0100 wenzelm more thread-safe access to global refs;
Wed, 21 Oct 2009 12:12:21 +0200 haftmann merged
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Wed, 21 Oct 2009 00:36:12 +0200 wenzelm standardized basic operations on type option;
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 21 May 2009 15:23:32 +0100 webertj write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first
Thu, 05 Mar 2009 10:19:51 +0100 blanchet Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Tue, 24 Feb 2009 16:12:27 +0100 blanchet Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
Tue, 10 Feb 2009 18:57:02 +0100 blanchet Added serial_string to SAT solver input and output files, to prevent multithreading chaos.
Tue, 03 Apr 2007 19:24:11 +0200 wenzelm removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
Wed, 31 Jan 2007 16:05:13 +0100 haftmann dropped Output.update_warn
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Thu, 09 Nov 2006 18:58:52 +0100 webertj timing/tracing code removed
Thu, 09 Nov 2006 18:48:45 +0100 webertj interpreters for fst and snd added
Sat, 02 Sep 2006 01:10:10 +0200 webertj zchaff_with_proofs: proof is a reference now
Thu, 31 Aug 2006 02:22:05 +0200 webertj read_dimacs_cnf_file ignores more comment lines
Wed, 19 Jul 2006 02:35:22 +0200 webertj MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
Mon, 17 Jul 2006 15:16:17 +0200 webertj butlast removed (use fst o split_last instead)
Mon, 17 Jul 2006 00:37:06 +0200 webertj support for MiniSat proof traces added
Fri, 07 Jul 2006 02:12:52 +0200 webertj added support for MiniSat 1.14
Sun, 05 Mar 2006 18:49:13 +0100 webertj fixed a typo in a comment
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Sat, 24 Sep 2005 07:10:57 +0200 webertj bugfix in "zchaff_with_proofs"
Sat, 24 Sep 2005 02:53:08 +0200 webertj parse_std_result_file renamed to read_std_result_file
Thu, 22 Sep 2005 13:52:55 +0200 webertj solver "auto" does not reverse the list of solvers anymore
Wed, 21 Sep 2005 22:01:09 +0200 webertj zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
Wed, 21 Sep 2005 10:33:59 +0200 haftmann introduced AList module
Tue, 20 Sep 2005 19:38:35 +0200 webertj bugfix in "zchaff_with_proofs"
Tue, 20 Sep 2005 00:16:29 +0200 webertj using curried Inttab.update_new function now
Mon, 19 Sep 2005 23:45:59 +0200 webertj SAT solver interface modified to support proofs of unsatisfiability
Tue, 26 Jul 2005 15:29:37 +0200 webertj write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
Tue, 26 Jul 2005 14:31:42 +0200 webertj replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
Tue, 26 Jul 2005 12:40:52 +0200 webertj write_dimacs_sat_file writes outer parentheses again
Tue, 26 Jul 2005 12:23:10 +0200 webertj replaced calls to PropLogic.defcnf by PropLogic.auxcnf
Thu, 21 Jul 2005 18:52:17 +0200 webertj write_dimacs_sat_file now generates slightly smaller files
Sun, 05 Jun 2005 11:57:14 +0200 wenzelm replaced File.sysify_path by Path.pack;
Fri, 11 Mar 2005 16:56:48 +0100 webertj minor Library.option related modifications
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Thu, 25 Nov 2004 14:44:52 +0100 webertj added ZCHAFF_VERSION
Wed, 24 Nov 2004 19:51:33 +0100 webertj Removed a "Matches are not exhaustive" warning
Tue, 23 Nov 2004 15:36:39 +0100 webertj external solvers may now overwrite existing temporary files
Fri, 19 Nov 2004 15:05:10 +0100 webertj solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
Sat, 14 Aug 2004 16:27:56 +0200 webertj bugfix in read_dimacs_cnf_file
Mon, 12 Jul 2004 19:56:58 +0200 webertj read_dimacs_cnf_file added
Tue, 22 Jun 2004 14:14:08 +0200 webertj faster conversion into DIMACS CNF and DIMACS SAT format
less more (0) -60 tip