| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 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
|
| Thu, 01 May 2014 22:56:59 +0200 |
boehmes |
added internal proof-producing SAT solver
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:43:23 +0100 |
wenzelm |
proper config options;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 21:09:53 +0100 |
wenzelm |
more standard file/module names;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 13:03:24 +0100 |
webertj |
Avoid ML warning about unreferenced identifier.
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 16:01:51 +0100 |
wenzelm |
modernized structure Prop_Logic;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 14:07:09 +0200 |
wenzelm |
expanded some aliases from structure Unsynchronized;
|
file |
diff |
annotate
|
| Tue, 17 Aug 2010 17:57:19 +0100 |
webertj |
Tuned.
|
file |
diff |
annotate
|
| Sat, 07 Nov 2009 18:55:30 +0000 |
webertj |
Due to popular demand: added a function that benchmarks proof reconstruction
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:33:14 +0200 |
wenzelm |
Unsynchronized.set etc.;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 23:17:40 +0200 |
wenzelm |
proper context for SAT tactics;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Fri, 06 Jul 2007 17:21:18 +0200 |
webertj |
cosmetic (line length fixed)
|
file |
diff |
annotate
|
| Wed, 10 Jan 2007 19:18:29 +0100 |
webertj |
minor comment change
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2006 13:02:55 +0100 |
webertj |
profiling disabled
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 16:27:53 +0200 |
webertj |
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 00:57:41 +0200 |
webertj |
proof reconstruction now uses its own data structure to manage hyps; should be both faster and more robust
|
file |
diff |
annotate
|
| Tue, 01 Aug 2006 15:28:55 +0200 |
webertj |
comment (timing information for last example) added
|
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 18:13:58 +0200 |
webertj |
"solver" reference added to make the SAT solver configurable
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 17:17:41 +0200 |
webertj |
CNF tactic invocations moved into comments
|
file |
diff |
annotate
|
| Tue, 02 May 2006 19:23:48 +0200 |
webertj |
beta_eta_conversion added to pre_cnf_tac
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:31:50 +0100 |
webertj |
clauses now use (meta-)hyps instead of (meta-)implications; significant speedup
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Sat, 24 Sep 2005 07:21:46 +0200 |
webertj |
code reformatted and restructured, many minor modifications
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|