src/HOL/Tools/sat_solver.ML
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