src/HOL/Tools/sat_solver.ML
2006-07-19 webertj 2006-07-19 MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
2006-07-17 webertj 2006-07-17 butlast removed (use fst o split_last instead)
2006-07-17 webertj 2006-07-17 support for MiniSat proof traces added
2006-07-07 webertj 2006-07-07 added support for MiniSat 1.14
2006-03-05 webertj 2006-03-05 fixed a typo in a comment
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-09-24 webertj 2005-09-24 bugfix in "zchaff_with_proofs"
2005-09-24 webertj 2005-09-24 parse_std_result_file renamed to read_std_result_file
2005-09-22 webertj 2005-09-22 solver "auto" does not reverse the list of solvers anymore
2005-09-21 webertj 2005-09-21 zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
2005-09-21 haftmann 2005-09-21 introduced AList module
2005-09-20 webertj 2005-09-20 bugfix in "zchaff_with_proofs"
2005-09-20 webertj 2005-09-20 using curried Inttab.update_new function now
2005-09-19 webertj 2005-09-19 SAT solver interface modified to support proofs of unsatisfiability
2005-07-26 webertj 2005-07-26 write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
2005-07-26 webertj 2005-07-26 replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
2005-07-26 webertj 2005-07-26 write_dimacs_sat_file writes outer parentheses again
2005-07-26 webertj 2005-07-26 replaced calls to PropLogic.defcnf by PropLogic.auxcnf
2005-07-21 webertj 2005-07-21 write_dimacs_sat_file now generates slightly smaller files
2005-06-05 wenzelm 2005-06-05 replaced File.sysify_path by Path.pack; avoid "handle _" (which is not well-defined due to erratic Interrupt exceptions);
2005-03-11 webertj 2005-03-11 minor Library.option related modifications
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-11-25 webertj 2004-11-25 added ZCHAFF_VERSION
2004-11-24 webertj 2004-11-24 Removed a "Matches are not exhaustive" warning
2004-11-23 webertj 2004-11-23 external solvers may now overwrite existing temporary files
2004-11-19 webertj 2004-11-19 solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
2004-08-14 webertj 2004-08-14 bugfix in read_dimacs_cnf_file
2004-07-12 webertj 2004-07-12 read_dimacs_cnf_file added
2004-06-22 webertj 2004-06-22 faster conversion into DIMACS CNF and DIMACS SAT format
2004-06-17 webertj 2004-06-17 new SAT solver interface
2004-05-26 webertj 2004-05-26 solver "auto" now issues a warning when it uses solver "enumerate"
2004-05-17 webertj 2004-05-17 Comments fixed
2004-05-04 webertj 2004-05-04 redundant clause removed
2004-04-02 webertj 2004-04-02 fixed dpll solver (now uses NNF)
2004-03-26 webertj 2004-03-26 satsolver=dpll
2004-03-26 webertj 2004-03-26 Installed solvers now determined at call time (as opposed to compile time)
2004-03-11 webertj 2004-03-11 SML/NJ compatibility fixes
2004-03-10 webertj 2004-03-10 Internal and external SAT solvers