src/HOL/Tools/sat_solver.ML
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)
less more (0) -50 -30 tip