Tue, 29 Jun 2010 09:05:37 +0200 move functions not needed by Metis out of "Metis_Clauses"
blanchet [Tue, 29 Jun 2010 09:05:37 +0200] rev 37623
move functions not needed by Metis out of "Metis_Clauses"
Mon, 28 Jun 2010 18:47:07 +0200 no setup is necessary anymore
blanchet [Mon, 28 Jun 2010 18:47:07 +0200] rev 37622
no setup is necessary anymore
Mon, 28 Jun 2010 18:46:42 +0200 adapt call
blanchet [Mon, 28 Jun 2010 18:46:42 +0200] rev 37621
adapt call
Mon, 28 Jun 2010 18:15:40 +0200 remove obsolete component of CNF clause tuple (and reorder it)
blanchet [Mon, 28 Jun 2010 18:15:40 +0200] rev 37620
remove obsolete component of CNF clause tuple (and reorder it)
Mon, 28 Jun 2010 18:08:36 +0200 killed "expand_defs_tac";
blanchet [Mon, 28 Jun 2010 18:08:36 +0200] rev 37619
killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem
Mon, 28 Jun 2010 18:02:36 +0200 get rid of Skolem cache by performing CNF-conversion after fact selection
blanchet [Mon, 28 Jun 2010 18:02:36 +0200] rev 37618
get rid of Skolem cache by performing CNF-conversion after fact selection
Mon, 28 Jun 2010 17:32:28 +0200 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet [Mon, 28 Jun 2010 17:32:28 +0200] rev 37617
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
Mon, 28 Jun 2010 17:31:38 +0200 always perform relevance filtering on original formulas
blanchet [Mon, 28 Jun 2010 17:31:38 +0200] rev 37616
always perform relevance filtering on original formulas
Tue, 29 Jun 2010 11:25:30 +0200 merged
haftmann [Tue, 29 Jun 2010 11:25:30 +0200] rev 37615
merged
Tue, 29 Jun 2010 11:25:25 +0200 split off predicate compiler into separate theory
haftmann [Tue, 29 Jun 2010 11:25:25 +0200] rev 37614
split off predicate compiler into separate theory
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip