Wed, 06 Sep 2006 17:39:52 +0200 |
webertj |
rawsat_thm: mk_conjunction_list replaced by Conjunction.mk_conjunction_list
|
file |
diff |
annotate
|
Sat, 02 Sep 2006 03:10:27 +0200 |
webertj |
tuned
|
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, 09 Aug 2006 15:48:51 +0200 |
webertj |
tuned: string_of_list, string_of_pair
|
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
|
Thu, 20 Jul 2006 14:34:57 +0200 |
webertj |
comments fixed, member function renamed
|
file |
diff |
annotate
|
Mon, 10 Jul 2006 21:02:29 +0200 |
webertj |
minor optimization wrt. certifying terms
|
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:27:09 +0200 |
webertj |
comments fixed, minor optimization wrt. certifying terms
|
file |
diff |
annotate
|
Wed, 03 May 2006 12:05:53 +0200 |
webertj |
pre_cnf_tac: beta-eta-normalization restricted to the current subgoal
|
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
|
Wed, 12 Oct 2005 18:17:48 +0200 |
webertj |
counter added to SAT signature
|
file |
diff |
annotate
|
Wed, 12 Oct 2005 17:06:22 +0200 |
webertj |
no proof reconstruction when quick_and_dirty is set
|
file |
diff |
annotate
|
Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
Wed, 28 Sep 2005 14:41:43 +0200 |
webertj |
pre_sat_tac moved towards end of file
|
file |
diff |
annotate
|
Wed, 28 Sep 2005 14:16:12 +0200 |
webertj |
comment fixed
|
file |
diff |
annotate
|
Sat, 24 Sep 2005 07:57:50 +0200 |
webertj |
replay_proof optimized: now performs backwards proof search
|
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
|