| Sun, 04 May 2014 19:08:29 +0200 |
blanchet |
tuned structure name
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:57:45 +0200 |
blanchet |
renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:53:58 +0200 |
blanchet |
added 'satx' proof method to Try0
|
file |
diff |
annotate
|
| Sun, 04 May 2014 16:17:53 +0200 |
boehmes |
removed obsolete internal SAT solvers
|
file |
diff |
annotate
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 16:54:01 +0100 |
wenzelm |
prefer more robust Synchronized.var;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:31:18 +0100 |
wenzelm |
removed odd comments -- inferred types are shown by Prover IDE;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 13:46:18 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 12 May 2013 14:25:16 +0200 |
wenzelm |
decentralized historic settings;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 20:52:41 +0200 |
wenzelm |
moved bash operations to Isabelle_System (cf. Scala version);
|
file |
diff |
annotate
|
| Fri, 08 Jul 2011 13:59:54 +0200 |
wenzelm |
comment;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 16:01:51 +0100 |
wenzelm |
modernized structure Prop_Logic;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 10:48:55 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Fri, 24 Sep 2010 15:53:13 +0200 |
wenzelm |
modernized structure Ord_List;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 18:49:32 +0200 |
blanchet |
move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
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 =)
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 15:51:22 +0100 |
wenzelm |
proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
|
file |
diff |
annotate
|
| Sat, 06 Feb 2010 14:50:55 +0100 |
wenzelm |
renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2009 22:29:46 +0000 |
webertj |
read_dimacs_cnf_file can now read DIMACS files that contain successive
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 23:08:51 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 15:23:25 +0100 |
blanchet |
make "auto" SAT solver less verbose
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 16:03:06 +0100 |
wenzelm |
more thread-safe access to global refs;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:12:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:09:37 +0200 |
haftmann |
curried inter as canonical list operation (beware of argument order)
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 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
|