| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * CONGRUENCE CLOSURE ALGORITHM * */ |
| /* * * */ |
| /* * $Module: CLOSURE * */ |
| /* * * */ |
| /* * Copyright (C) 1999, 2000, 2001 MPI fuer Informatik * */ |
| /* * * */ |
| /* * This program is free software; you can redistribute * */ |
| /* * it and/or modify it under the terms of the GNU * */ |
| /* * General Public License as published by the Free * */ |
| /* * Software Foundation; either version 2 of the License, * */ |
| /* * or (at your option) any later version. * */ |
| /* * * */ |
| /* * This program is distributed in the hope that it will * */ |
| /* * be useful, but WITHOUT ANY WARRANTY; without even * */ |
| /* * the implied warranty of MERCHANTABILITY or FITNESS * */ |
| /* * FOR A PARTICULAR PURPOSE. See the GNU General Public * */ |
| /* * License for more details. * */ |
| /* * * */ |
| /* * You should have received a copy of the GNU General * */ |
| /* * Public License along with this program; if not, write * */ |
| /* * to the Free Software Foundation, Inc., 59 Temple * */ |
| /* * Place, Suite 330, Boston, MA 02111-1307 USA * */ |
| /* * * */ |
| /* * * */ |
| /* $Revision$ * */ |
| /* $State$ * */ |
| /* $Date$ * */ |
| /* $Author$ * */ |
| /* * * */ |
| /* * Contact: * */ |
| /* * Christoph Weidenbach * */ |
| /* * MPI fuer Informatik * */ |
| /* * Stuhlsatzenhausweg 85 * */ |
| /* * 66123 Saarbruecken * */ |
| /* * Email: weidenb@mpi-sb.mpg.de * */ |
| /* * Germany * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| /**************************************************************/ |
| /* Include */ |
| /**************************************************************/ |
| |
| #include "closure.h" |
| |
| |
| /**************************************************************/ |
| /* Global constants and variable */ |
| /**************************************************************/ |
| |
| /* standard initial size of a closure's stacks */ |
| static const int cc_RASSTDSIZE = 64; |
| /* cc_RASSTDSIZE * ld(cc_RASSTDSIZE) */ |
| static const int cc_SIZELDSIZE = 384; |
| /* the virtual term "true" has number 0 */ |
| static const ELEMENT cc_NOOFTRUE = 0; |
| |
| |
| static struct { |
| PARTITION partition; |
| TABLE table; |
| RAS car, cdr, size, pending, combine; |
| } cc_CLOSURE; |
| |
| /* the closure consists of a partition, a signature table, stacks for */ |
| /* (circularly linked) lists of predecessors of equivalence classes (i. e. */ |
| /* terms with direct subterms from this class), for the sizes of these lists, */ |
| /* for pending terms (the ones to be worked off) and for terms to be combined */ |
| /* in the same equivalence class */ |
| |
| |
| /**************************************************************/ |
| /* Inline functions */ |
| /**************************************************************/ |
| |
| static __inline__ PARTITION cc_GetPartition(void) |
| { |
| return cc_CLOSURE.partition; |
| } |
| |
| |
| static __inline__ void cc_SetPartition(PARTITION partition) |
| { |
| cc_CLOSURE.partition = partition; |
| } |
| |
| |
| static __inline__ TABLE cc_GetTable(void) |
| { |
| return cc_CLOSURE.table; |
| } |
| |
| |
| static __inline__ void cc_SetTable(TABLE table) |
| { |
| cc_CLOSURE.table = table; |
| } |
| |
| |
| static __inline__ RAS cc_GetCars(void) |
| { |
| return cc_CLOSURE.car; |
| } |
| |
| |
| static __inline__ TERM cc_GetCar(int index) |
| { |
| return (TERM) ras_Get(cc_GetCars(), index); |
| } |
| |
| |
| static __inline__ void cc_SetCars(RAS car) |
| { |
| cc_CLOSURE.car = car; |
| } |
| |
| |
| static __inline__ RAS cc_GetCdrs(void) |
| { |
| return cc_CLOSURE.cdr; |
| } |
| |
| |
| static __inline__ int cc_GetCdr(int index) |
| { |
| return (int) ras_Get(cc_GetCdrs(), index); |
| } |
| |
| |
| static __inline__ void cc_SetCdrs(RAS cdr) |
| { |
| cc_CLOSURE.cdr = cdr; |
| } |
| |
| |
| static __inline__ void cc_SetCdr(int index, int cdr) |
| { |
| ras_Set(cc_GetCdrs(), index, (POINTER) cdr); |
| } |
| |
| |
| static __inline__ RAS cc_GetSizes(void) |
| { |
| return cc_CLOSURE.size; |
| } |
| |
| |
| static __inline__ int cc_GetSize(int index) |
| { |
| return (int) ras_Get(cc_GetSizes(), index); |
| } |
| |
| |
| static __inline__ void cc_SetSizes(RAS size) |
| { |
| cc_CLOSURE.size = size; |
| } |
| |
| |
| static __inline__ void cc_SetSize(int index, int size) |
| { |
| ras_Set(cc_GetSizes(), index, (POINTER) size); |
| } |
| |
| |
| static __inline__ RAS cc_GetPending(void) |
| { |
| return cc_CLOSURE.pending; |
| } |
| |
| |
| static __inline__ void cc_SetPending(RAS pending) |
| { |
| cc_CLOSURE.pending = pending; |
| } |
| |
| |
| static __inline__ RAS cc_GetCombine(void) |
| { |
| return cc_CLOSURE.combine; |
| } |
| |
| |
| static __inline__ void cc_SetCombine(RAS combine) |
| { |
| cc_CLOSURE.combine = combine; |
| } |
| |
| |
| /**************************************************************/ |
| /* Functions */ |
| /**************************************************************/ |
| |
| static int cc_Number(int actno, TERM term, TERM pred) |
| /*************************************************************** |
| INPUT: the actual number of terms, the term to be numbered |
| and its predecessor (may be the empty term |
| term_Null()) |
| RETURNS: the new number of terms after recursively numbering |
| the term and its subterms |
| EFFECT: stores a term's number as its size, partially |
| initializes its predecessor list and pushes all |
| subterms to the pending stack |
| ***************************************************************/ |
| { |
| LIST terms; |
| |
| #ifdef CHECK |
| if (actno < 0) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cc_Number: negative actual number of terms."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| term_SetSize(term, actno++); |
| cc_SetCars(ras_Push(cc_GetCars(), pred)); |
| cc_SetPending(ras_Push(cc_GetPending(), term)); |
| for (terms = term_ArgumentList(term); !list_Empty(terms); terms = |
| list_Cdr(terms)) |
| actno = cc_Number(actno, list_Car(terms), term); |
| return actno; |
| } |
| |
| |
| static void cc_Union(ECLASS c1, ECLASS c2) |
| /*************************************************************** |
| EFFECT: unions c1 and c2, therefore the signatures of the |
| predecessors of one class change, so these |
| predecessors have to be deleted from the signature |
| table and become pending again; sets new class's |
| predecessor list and its size to the concatenation of |
| the old lists resp. the sum of the old sizes |
| ***************************************************************/ |
| { |
| int aux, size; |
| TERM term; |
| |
| #ifdef CHECK |
| if (part_Find(cc_GetPartition(), c1) != c1) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cc_Union: first class corrupted, i. e. is not "); |
| misc_ErrorReport("the representative."); |
| misc_FinishErrorReport(); |
| } |
| if (part_Find(cc_GetPartition(), c2) != c2) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cc_Union: second class corrupted, i. e. is not "); |
| misc_ErrorReport("the representative."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| if (c1 != c2) { |
| |
| /* make c1 the class with the bigger (or at least not smaller) list: */ |
| if (cc_GetSize(c1) < cc_GetSize(c2)) { |
| aux = c1; |
| c1 = c2; |
| c2 = aux; |
| } |
| |
| /* delete c2's predecessors from signature table and add them to pending: */ |
| for (size = cc_GetSize(c2), aux = c2; size > 0; size--) { |
| term = cc_GetCar(aux); |
| aux = cc_GetCdr(aux); |
| table_Delete(cc_GetTable(), term); |
| cc_SetPending(ras_Push(cc_GetPending(), term)); |
| } |
| |
| if (cc_GetSize(c2) > 0) { /* then GetSize(c1) ( >= GetSize(c2) ) > 0 too */ |
| |
| /* union circularly linked lists by exchanging cdrs: */ |
| aux = cc_GetCdr(c1); |
| cc_SetCdr(c1, cc_GetCdr(c2)); |
| cc_SetCdr(c2, aux); |
| |
| cc_SetSize(c1, cc_GetSize(c1) + cc_GetSize(c2)); |
| } |
| part_Union(cc_GetPartition(), c1, c2); |
| } |
| } |
| |
| |
| static void cc_InitData(CLAUSE clause) |
| /*************************************************************** |
| INPUT: the clause to investigate |
| EFFECT: pushes clause's atoms and their subterms on the |
| pending stack, initializes each predecessor list with |
| the list containing only a term's father, and unions |
| the equivalence classes of the terms of the same |
| antecedent equation |
| ***************************************************************/ |
| { |
| int last, actno, i, ld; |
| TERM atom; |
| RAS cdr, size; |
| |
| cc_SetCars(ras_InitWithSize(cc_GetCars(), cc_RASSTDSIZE)); |
| cc_SetPending(ras_InitWithSize(cc_GetPending(), cc_RASSTDSIZE)); |
| ras_FastPush(cc_GetCars(), term_Null()); /* "true" has no predecessors */ |
| actno = 1; |
| last = clause_LastLitIndex(clause); |
| for (i = clause_FirstLitIndex(); i <= last; i++) { |
| atom = clause_GetLiteralAtom(clause, i); |
| if (fol_IsEquality(atom)) { |
| actno = cc_Number(actno, term_FirstArgument(atom), term_Null()); |
| actno = cc_Number(actno, term_SecondArgument(atom), term_Null()); |
| } |
| else |
| actno = cc_Number(actno, atom, term_Null()); |
| } |
| cc_SetPartition(part_Init(cc_GetPartition(), actno)); |
| cc_SetTable(table_Init(cc_GetTable(), symbol_ActIndex() - 1, |
| clause_MaxVar(clause), actno - 1)); |
| cdr = ras_InitWithSize(cc_GetCdrs(), actno); |
| size = ras_InitWithSize(cc_GetSizes(), actno); |
| for (i = 0; i < actno; i++) { |
| ras_FastPush(cdr, (POINTER) i); /* form a cycle */ |
| ras_FastPush(size, (POINTER) (cc_GetCar(i) == term_Null()? 0 : 1)); |
| } |
| cc_SetCdrs(cdr); |
| cc_SetSizes(size); |
| |
| /* compute ceil(ld(actno)) avoiding mathbib-logarithm's rounding errors: */ |
| for (ld = 0, i = actno - 1; i > 0; i >>= 1) |
| ld++; |
| |
| cc_SetCombine(ras_InitWithSize(cc_GetCombine(), actno * ld + 1)); |
| |
| /* for every antecedent equation union equivalence classes of its terms */ |
| /* (a non-equational atom is represented as the equation atom = "true"): */ |
| last = clause_LastAntecedentLitIndex(clause); |
| for (i = clause_FirstLitIndex(); i <= last; i++) { |
| atom = clause_GetLiteralAtom(clause, i); |
| if (fol_IsEquality(atom)) |
| cc_Union(term_Size(term_FirstArgument(atom)), /* clause not shared, therefore */ |
| term_Size(term_SecondArgument(atom))); /* here no cc_Find needed */ |
| else |
| cc_Union(term_Size(atom), part_Find(cc_GetPartition(), cc_NOOFTRUE)); |
| } |
| |
| } |
| |
| |
| static BOOL cc_Outit(CLAUSE clause) |
| /*************************************************************** |
| RETURNS: the decision, if the clause is a tautology |
| ***************************************************************/ |
| { |
| int last, i; |
| BOOL result; |
| TERM atom; |
| |
| #ifdef CHECK |
| if (!ras_Empty(cc_GetPending())) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In cc_Outit: there are terms left to work off."); |
| misc_FinishErrorReport(); |
| } |
| #endif |
| |
| last = clause_LastLitIndex(clause); |
| for (i = clause_FirstSuccedentLitIndex(clause), result = FALSE; |
| i <= last && !result; i++) { |
| atom = clause_GetLiteralAtom(clause, i); |
| if (fol_IsEquality(atom)) |
| result = part_Equivalent(cc_GetPartition(), |
| term_Size(term_FirstArgument(atom)), |
| term_Size(term_SecondArgument(atom))); |
| else |
| result = part_Equivalent(cc_GetPartition(), term_Size(atom), cc_NOOFTRUE); |
| } |
| return result; |
| } |
| |
| |
| /**************************************************************/ |
| /* Main functions */ |
| /**************************************************************/ |
| |
| void cc_Init(void) |
| { |
| cc_SetPartition(part_Create(cc_RASSTDSIZE)); |
| cc_SetTable(table_Create(cc_RASSTDSIZE, cc_RASSTDSIZE, cc_RASSTDSIZE)); |
| cc_SetCars(ras_CreateWithSize(cc_RASSTDSIZE)); |
| cc_SetCdrs(ras_CreateWithSize(cc_RASSTDSIZE)); |
| cc_SetSizes(ras_CreateWithSize(cc_RASSTDSIZE)); |
| cc_SetPending(ras_CreateWithSize(cc_RASSTDSIZE)); |
| cc_SetCombine(ras_CreateWithSize(cc_SIZELDSIZE)); |
| } |
| |
| |
| void cc_Free(void) |
| { |
| part_Free(cc_GetPartition()); |
| table_Free(cc_GetTable()); |
| ras_Free(cc_GetCars()); |
| ras_Free(cc_GetCdrs()); |
| ras_Free(cc_GetSizes()); |
| ras_Free(cc_GetPending()); |
| ras_Free(cc_GetCombine()); |
| } |
| |
| |
| BOOL cc_Tautology(CLAUSE clause) |
| /*************************************************************** |
| INPUT: the clause to test |
| RETURNS: the decision, if the clause - where all variables are |
| regarded as skolem constants - is a tautology, using |
| the congruence closure algorithm of Downey, Sethi and |
| Tarjan |
| CAUTION: overrides the sizes of the clause's terms |
| ***************************************************************/ |
| { |
| TERM term, query; |
| |
| cc_InitData(clause); |
| while (!ras_Empty(cc_GetPending())) { |
| |
| /* propagate the closure: */ |
| while (!ras_Empty(cc_GetPending())) { |
| term = ras_Pop(cc_GetPending()); |
| query = table_QueryAndEnter(cc_GetTable(), cc_GetPartition(), term); |
| if (query != term_Null()) { |
| ras_FastPush(cc_GetCombine(), term); |
| ras_FastPush(cc_GetCombine(), query); |
| } |
| } |
| while (!ras_Empty(cc_GetCombine())) |
| cc_Union(part_Find(cc_GetPartition(), term_Size(ras_Pop(cc_GetCombine()))), |
| part_Find(cc_GetPartition(), term_Size(ras_Pop(cc_GetCombine())))); |
| } |
| return cc_Outit(clause); |
| } |
| |