isabelle: File revisions

src/HOL/Tools/sat_solver.ML

2005-09-24	webertj	2005-09-24	bugfix in "zchaff_with_proofs"	file \| diff \| annotate
2005-09-24	webertj	2005-09-24	parse_std_result_file renamed to read_std_result_file	file \| diff \| annotate
2005-09-22	webertj	2005-09-22	solver "auto" does not reverse the list of solvers anymore	file \| diff \| annotate
2005-09-21	webertj	2005-09-21	zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore	file \| diff \| annotate
2005-09-21	haftmann	2005-09-21	introduced AList module	file \| diff \| annotate
2005-09-20	webertj	2005-09-20	bugfix in "zchaff_with_proofs"	file \| diff \| annotate
2005-09-20	webertj	2005-09-20	using curried Inttab.update_new function now	file \| diff \| annotate
2005-09-19	webertj	2005-09-19	SAT solver interface modified to support proofs of unsatisfiability	file \| diff \| annotate
2005-07-26	webertj	2005-07-26	write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks	file \| diff \| annotate
2005-07-26	webertj	2005-07-26	replaced calls to PropLogic.auxcnf by PropLogic.defcnf again	file \| diff \| annotate
2005-07-26	webertj	2005-07-26	write_dimacs_sat_file writes outer parentheses again	file \| diff \| annotate
2005-07-26	webertj	2005-07-26	replaced calls to PropLogic.defcnf by PropLogic.auxcnf	file \| diff \| annotate
2005-07-21	webertj	2005-07-21	write_dimacs_sat_file now generates slightly smaller files	file \| diff \| annotate
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);	file \| diff \| annotate
2005-03-11	webertj	2005-03-11	minor Library.option related modifications	file \| diff \| annotate
2005-03-03	skalberg	2005-03-03	Move towards standard functions.	file \| diff \| annotate
2005-02-13	skalberg	2005-02-13	Deleted Library.option type.	file \| diff \| annotate
2004-11-25	webertj	2004-11-25	added ZCHAFF_VERSION	file \| diff \| annotate
2004-11-24	webertj	2004-11-24	Removed a "Matches are not exhaustive" warning	file \| diff \| annotate
2004-11-23	webertj	2004-11-23	external solvers may now overwrite existing temporary files	file \| diff \| annotate
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)	file \| diff \| annotate
2004-08-14	webertj	2004-08-14	bugfix in read_dimacs_cnf_file	file \| diff \| annotate
2004-07-12	webertj	2004-07-12	read_dimacs_cnf_file added	file \| diff \| annotate
2004-06-22	webertj	2004-06-22	faster conversion into DIMACS CNF and DIMACS SAT format	file \| diff \| annotate
2004-06-17	webertj	2004-06-17	new SAT solver interface	file \| diff \| annotate
2004-05-26	webertj	2004-05-26	solver "auto" now issues a warning when it uses solver "enumerate"	file \| diff \| annotate
2004-05-17	webertj	2004-05-17	Comments fixed	file \| diff \| annotate
2004-05-04	webertj	2004-05-04	redundant clause removed	file \| diff \| annotate
2004-04-02	webertj	2004-04-02	fixed dpll solver (now uses NNF)	file \| diff \| annotate
2004-03-26	webertj	2004-03-26	satsolver=dpll	file \| diff \| annotate
2004-03-26	webertj	2004-03-26	Installed solvers now determined at call time (as opposed to compile time)	file \| diff \| annotate
2004-03-11	webertj	2004-03-11	SML/NJ compatibility fixes	file \| diff \| annotate
2004-03-10	webertj	2004-03-10	Internal and external SAT solvers	file \| diff \| annotate

isabelle

RSS Atom