| Thu, 21 May 2009 15:23:32 +0100 |
webertj |
write_dimacs_{sat,cnf}_file now write the DIMACS file on the fly, without building it in memory first
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 10:19:51 +0100 |
blanchet |
Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 24 Feb 2009 16:12:27 +0100 |
blanchet |
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.
|
file |
diff |
annotate
|
| Tue, 10 Feb 2009 18:57:02 +0100 |
blanchet |
Added serial_string to SAT solver input and output files, to prevent multithreading chaos.
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:11 +0200 |
wenzelm |
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
|
file |
diff |
annotate
|
| Wed, 31 Jan 2007 16:05:13 +0100 |
haftmann |
dropped Output.update_warn
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 18:58:52 +0100 |
webertj |
timing/tracing code removed
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 18:48:45 +0100 |
webertj |
interpreters for fst and snd added
|
file |
diff |
annotate
|
| 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
|