| Sat, 02 Sep 2006 01:10:10 +0200 |
webertj |
zchaff_with_proofs: proof is a reference now
|
file |
diff |
annotate
|
| Thu, 31 Aug 2006 02:22:05 +0200 |
webertj |
read_dimacs_cnf_file ignores more comment lines
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 02:35:22 +0200 |
webertj |
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
|
file |
diff |
annotate
|
| Mon, 17 Jul 2006 15:16:17 +0200 |
webertj |
butlast removed (use fst o split_last instead)
|
file |
diff |
annotate
|
| Mon, 17 Jul 2006 00:37:06 +0200 |
webertj |
support for MiniSat proof traces added
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 02:12:52 +0200 |
webertj |
added support for MiniSat 1.14
|
file |
diff |
annotate
|
| Sun, 05 Mar 2006 18:49:13 +0100 |
webertj |
fixed a typo in a comment
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 07:10:57 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 02:53:08 +0200 |
webertj |
parse_std_result_file renamed to read_std_result_file
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 13:52:55 +0200 |
webertj |
solver "auto" does not reverse the list of solvers anymore
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 22:01:09 +0200 |
webertj |
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 10:33:59 +0200 |
haftmann |
introduced AList module
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 19:38:35 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 00:16:29 +0200 |
webertj |
using curried Inttab.update_new function now
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 23:45:59 +0200 |
webertj |
SAT solver interface modified to support proofs of unsatisfiability
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 15:29:37 +0200 |
webertj |
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 14:31:42 +0200 |
webertj |
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 12:40:52 +0200 |
webertj |
write_dimacs_sat_file writes outer parentheses again
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 12:23:10 +0200 |
webertj |
replaced calls to PropLogic.defcnf by PropLogic.auxcnf
|
file |
diff |
annotate
|
| Thu, 21 Jul 2005 18:52:17 +0200 |
webertj |
write_dimacs_sat_file now generates slightly smaller files
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:57:14 +0200 |
wenzelm |
replaced File.sysify_path by Path.pack;
|
file |
diff |
annotate
|
| Fri, 11 Mar 2005 16:56:48 +0100 |
webertj |
minor Library.option related modifications
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 25 Nov 2004 14:44:52 +0100 |
webertj |
added ZCHAFF_VERSION
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 19:51:33 +0100 |
webertj |
Removed a "Matches are not exhaustive" warning
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 15:36:39 +0100 |
webertj |
external solvers may now overwrite existing temporary files
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Sat, 14 Aug 2004 16:27:56 +0200 |
webertj |
bugfix in read_dimacs_cnf_file
|
file |
diff |
annotate
|
| Mon, 12 Jul 2004 19:56:58 +0200 |
webertj |
read_dimacs_cnf_file added
|
file |
diff |
annotate
|
| Tue, 22 Jun 2004 14:14:08 +0200 |
webertj |
faster conversion into DIMACS CNF and DIMACS SAT format
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 22:01:23 +0200 |
webertj |
new SAT solver interface
|
file |
diff |
annotate
|
| Wed, 26 May 2004 17:42:46 +0200 |
webertj |
solver "auto" now issues a warning when it uses solver "enumerate"
|
file |
diff |
annotate
|
| Mon, 17 May 2004 14:05:06 +0200 |
webertj |
Comments fixed
|
file |
diff |
annotate
|
| Tue, 04 May 2004 18:04:28 +0200 |
webertj |
redundant clause removed
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:28:16 +0200 |
webertj |
fixed dpll solver (now uses NNF)
|
file |
diff |
annotate
|
| Fri, 26 Mar 2004 19:58:43 +0100 |
webertj |
satsolver=dpll
|
file |
diff |
annotate
|
| Fri, 26 Mar 2004 12:21:50 +0100 |
webertj |
Installed solvers now determined at call time (as opposed to compile time)
|
file |
diff |
annotate
|
| Thu, 11 Mar 2004 00:15:24 +0100 |
webertj |
SML/NJ compatibility fixes
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 20:28:18 +0100 |
webertj |
Internal and external SAT solvers
|
file |
diff |
annotate
|