src/HOL/Tools/sat_solver.ML
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-07-08 wenzelm 2011-07-08 comment;
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2011-01-08 wenzelm 2011-01-08 modernized structure Prop_Logic; avoid ML structure aliases;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-05-31 blanchet 2010-05-31 move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-02-06 wenzelm 2010-02-06 proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-12-01 webertj 2009-12-01 read_dimacs_cnf_file can now read DIMACS files that contain successive white-space characters.
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 make "auto" SAT solver less verbose
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 more thread-safe access to global refs;
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-05-21 webertj 2009-05-21 write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first
2009-03-05 blanchet 2009-03-05 Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-24 blanchet 2009-02-24 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. I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it). These changes have no inpacts on already working Isabelle installations.
2009-02-10 blanchet 2009-02-10 Added serial_string to SAT solver input and output files, to prevent multithreading chaos. Bug reported by Tobias.
2007-04-03 wenzelm 2007-04-03 removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-01-31 haftmann 2007-01-31 dropped Output.update_warn
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-11-09 webertj 2006-11-09 timing/tracing code removed
2006-11-09 webertj 2006-11-09 interpreters for fst and snd added
2006-09-02 webertj 2006-09-02 zchaff_with_proofs: proof is a reference now
2006-08-31 webertj 2006-08-31 read_dimacs_cnf_file ignores more comment lines
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.