| 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
|