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