src/HOL/Tools/sat_solver.ML
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
Thu, 17 Jun 2004 22:01:23 +0200 webertj new SAT solver interface
Wed, 26 May 2004 17:42:46 +0200 webertj solver "auto" now issues a warning when it uses solver "enumerate"
Mon, 17 May 2004 14:05:06 +0200 webertj Comments fixed
Tue, 04 May 2004 18:04:28 +0200 webertj redundant clause removed
Fri, 02 Apr 2004 17:28:16 +0200 webertj fixed dpll solver (now uses NNF)
Fri, 26 Mar 2004 19:58:43 +0100 webertj satsolver=dpll
Fri, 26 Mar 2004 12:21:50 +0100 webertj Installed solvers now determined at call time (as opposed to compile time)
Thu, 11 Mar 2004 00:15:24 +0100 webertj SML/NJ compatibility fixes
Wed, 10 Mar 2004 20:28:18 +0100 webertj Internal and external SAT solvers
less more (0) tip