| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * TOP MODULE OF SPASS * */ |
| /* * * */ |
| /* * $Module: TOP * */ |
| /* * * */ |
| /* * Copyright (C) 1996, 1997, 1998, 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 * */ |
| /* * * */ |
| /* ********************************************************** */ |
| /**************************************************************/ |
| |
| |
| /* $RCSfile$ */ |
| |
| /*** MAIN LOOP *************************************************/ |
| |
| |
| /**************************************************************/ |
| /* Includes */ |
| /**************************************************************/ |
| |
| #include "dfg.h" |
| #include "defs.h" |
| #include "ia.h" |
| #include "rules-inf.h" |
| #include "rules-sort.h" |
| #include "rules-split.h" |
| #include "terminator.h" |
| #include "rules-red.h" |
| #include "analyze.h" |
| #include "clock.h" |
| #include "stringsx.h" |
| #include "options.h" |
| #include "context.h" |
| #include "cnf.h" |
| #include "search.h" |
| #include "hasharray.h" |
| #include "closure.h" |
| #include <errno.h> |
| #include <stdlib.h> |
| |
| |
| static const char *mybasename(const char *str) { |
| const char *base = strrchr(str, '/'); |
| return base ? base+1 : str; |
| } |
| |
| /**************************************************************/ |
| /* Types and Variables */ |
| /**************************************************************/ |
| |
| static const char *top_InputFile; |
| |
| static OPTID top_RemoveFileOptId; |
| |
| typedef enum {top_PROOF, top_COMPLETION, top_RESOURCE} top_SEARCHRESULT; |
| |
| |
| /**************************************************************/ |
| /* Catch Signals Section */ |
| /**************************************************************/ |
| |
| #if (defined(SPASS_SIGNALS)) |
| #include <signal.h> |
| |
| static PROOFSEARCH *top_PROOFSEARCH; |
| |
| static void top_SigHandler(int Signal) |
| /************************************************************** |
| INPUT: |
| RETURNS: |
| EFFECT: |
| ***************************************************************/ |
| { |
| if (Signal == SIGSEGV || Signal == SIGBUS) { |
| puts("\n\n\tSPASS is going to crash. This is probably caused by a"); |
| puts("\tbug in SPASS. Please send a copy of the input file(s) together"); |
| puts("\twith the used options to weidenb@mpi-sb.mpg.de, and someone will"); |
| puts("\ttry to fix the problem.\n"); |
| abort(); |
| } |
| |
| if (Signal == SIGINT || Signal == SIGTERM) { |
| clock_StopPassedTime(clock_OVERALL); |
| printf("\nSPASS %s ", misc_VERSION); |
| puts("\nSPASS beiseite: Ran out of time. SPASS was killed."); |
| printf("Problem: %s ", |
| (top_InputFile != (char*)NULL ? mybasename(top_InputFile) : "Read from stdin.")); |
| printf("\nSPASS derived %d clauses, backtracked %d clauses " |
| "and kept %d clauses.", |
| (*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_DerivedClauses(*top_PROOFSEARCH)), |
| (*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_BacktrackedClauses(*top_PROOFSEARCH)), |
| (*top_PROOFSEARCH == (PROOFSEARCH)NULL ? 0 : prfs_KeptClauses(*top_PROOFSEARCH))); |
| fputs("\nSPASS spent\t", stdout); |
| clock_PrintTime(clock_OVERALL); |
| fputs(" on the problem.\n\t\t", stdout); |
| clock_PrintTime(clock_INPUT); |
| fputs(" for the input.\n\t\t", stdout); |
| clock_PrintTime(clock_CNF); |
| fputs(" for the FLOTTER CNF translation.\n\t\t", stdout); |
| clock_PrintTime(clock_INFERENCE); |
| fputs(" for inferences.\n\t\t", stdout); |
| clock_PrintTime(clock_BACKTRACK); |
| fputs(" for the backtracking.\n\t\t", stdout); |
| clock_PrintTime(clock_REDUCTION); |
| puts(" for the reduction."); |
| } |
| |
| if (opts_IsSet(top_RemoveFileOptId)) |
| remove(top_InputFile); |
| |
| exit(EXIT_FAILURE); |
| } |
| |
| #endif |
| |
| |
| /**************************************************************/ |
| /* Clause Selection Functions */ |
| /**************************************************************/ |
| |
| static CLAUSE top_SelectClauseDepth(LIST List, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A list of clauses and a flag store. |
| RETURNS: A clause selected from the list. |
| EFFECT: This function selects a clause from the list according |
| to the following criteria: |
| 1. minimal depth |
| 2. minimal weight |
| 3a. maximal number of variable occurrences, if the flag |
| 'PrefVar' is TRUE |
| 3b. minimal number of variable occurrences, if 'PrefVar' |
| is FALSE |
| ***************************************************************/ |
| { |
| CLAUSE Result; |
| NAT Vars,NewVars,Weight,Depth,NewDepth; |
| |
| Result = (CLAUSE)list_Car(List); |
| Depth = clause_Depth(Result); |
| Weight = clause_Weight(Result); |
| Vars = clause_NumberOfVarOccs(Result); |
| List = list_Cdr(List); |
| |
| while (!list_Empty(List)) { |
| NewDepth = clause_Depth(list_Car(List)); |
| if (NewDepth <= Depth) { |
| if (NewDepth < Depth || clause_Weight(list_Car(List)) < Weight) { |
| Depth = NewDepth; |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = clause_NumberOfVarOccs(list_Car(List)); |
| } |
| else |
| if (clause_Weight(list_Car(List)) == Weight) { |
| NewVars = clause_NumberOfVarOccs(list_Car(List)); |
| if (flag_GetFlagValue(Flags, flag_PREFVAR)) { |
| if (Vars < NewVars) { |
| Depth = NewDepth; |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = NewVars; |
| } |
| } |
| else |
| if (Vars > NewVars) { |
| Depth = NewDepth; |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = NewVars; |
| } |
| } |
| } |
| List = list_Cdr(List); |
| } |
| |
| return Result; |
| } |
| |
| |
| static CLAUSE top_SelectMinimalWeightClause(LIST List, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A list of clauses and a flag store. |
| RETURNS: A clause selected from the list. |
| EFFECT: This function selects a clause with minimal weight. |
| If more than one clause has minimal weight and the flag |
| 'PrefVar' is TRUE, a clause with maximal number of variable |
| occurrences is selected. If 'PrefVar' is FALSE, a clause with |
| minimal number of variable occurrences is selected. |
| If two clauses are equal with respect to the two criteria |
| the clause with the smaller list position is selected. |
| CAUTION: THE LIST HAS TO BY SORTED BY WEIGHT IN ASCENDING ORDER! |
| ***************************************************************/ |
| { |
| CLAUSE Result; |
| NAT Vars, NewVars, Weight; |
| |
| #ifdef CHECK |
| /* Check invariant: List has to be sorted by weight (ascending) */ |
| LIST Scan; |
| Weight = clause_Weight(list_Car(List)); |
| for (Scan = list_Cdr(List); !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| NAT NewWeight; |
| NewWeight = clause_Weight(list_Car(Scan)); |
| if (NewWeight < Weight) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In top_SelectMinimalConWeightClause: clause list "); |
| misc_ErrorReport("isn't sorted by weight"); |
| misc_FinishErrorReport(); |
| } |
| Weight = NewWeight; |
| } |
| #endif |
| |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = clause_NumberOfVarOccs(Result); |
| List = list_Cdr(List); |
| |
| while (!list_Empty(List)) { |
| if (clause_Weight(list_Car(List)) == Weight) { |
| NewVars = clause_NumberOfVarOccs(list_Car(List)); |
| if (flag_GetFlagValue(Flags, flag_PREFVAR)) { |
| if (Vars < NewVars) { |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = NewVars; |
| } |
| } |
| else |
| if (Vars > NewVars) { |
| Result = (CLAUSE)list_Car(List); |
| Weight = clause_Weight(Result); |
| Vars = NewVars; |
| } |
| } |
| else |
| return Result; |
| List = list_Cdr(List); |
| } |
| return Result; |
| } |
| |
| |
| static CLAUSE top_SelectMinimalConWeightClause(LIST List, FLAGSTORE Flags) |
| /************************************************************** |
| INPUT: A non-empty list of clauses and a flag store. |
| RETURNS: A clause selected from the list. |
| EFFECT: This function selects a clause from the list in a |
| similar way as the function top_SelectMinimalWeightClause. |
| The only difference is that conjecture clauses are |
| preferred over axiom clauses, because their weight |
| is divided by a factor given by the flag 'PrefCon'. |
| ***************************************************************/ |
| { |
| CLAUSE Result; |
| NAT NewWeight,Weight, NewVars, Vars, Factor; |
| |
| Result = (CLAUSE)list_Car(List); |
| Factor = flag_GetFlagValue(Flags, flag_PREFCON); |
| Weight = clause_Weight(Result); |
| if (clause_GetFlag(Result, CONCLAUSE)) |
| Weight = Weight / Factor; |
| Vars = clause_NumberOfVarOccs(list_Car(List)); |
| List = list_Cdr(List); |
| |
| while (!list_Empty(List)) { |
| NewWeight = clause_Weight(list_Car(List)); |
| if (clause_GetFlag(list_Car(List),CONCLAUSE)) |
| NewWeight = NewWeight / Factor; |
| if (NewWeight < Weight) { |
| Weight = NewWeight; |
| Result = list_Car(List); |
| Vars = clause_NumberOfVarOccs(list_Car(List)); |
| } |
| else { |
| if (NewWeight == Weight) { |
| NewVars = clause_NumberOfVarOccs(list_Car(List)); |
| if (flag_GetFlagValue(Flags, flag_PREFVAR)) { |
| if (Vars < NewVars) { |
| Result = (CLAUSE)list_Car(List); |
| Weight = NewWeight; |
| Vars = NewVars; |
| } |
| } |
| else |
| if (Vars > NewVars) { |
| Result = (CLAUSE)list_Car(List); |
| Weight = NewWeight; |
| Vars = NewVars; |
| } |
| } |
| } |
| |
| List = list_Cdr(List); |
| } |
| return Result; |
| } |
| |
| |
| /*static CLAUSE top_SelectClauseDepth(LIST List)*/ |
| /************************************************************** |
| INPUT: A list of clauses. |
| RETURNS: A clause selected from the list. |
| EFFECT: |
| ***************************************************************/ |
| /*{ |
| CLAUSE Result; |
| int Min, Depth; |
| |
| Result = (CLAUSE)list_Car(List); |
| Depth = clause_Depth(Result); |
| Min = Depth * clause_Weight(Result); |
| List = list_Cdr(List); |
| |
| if (Depth == 0) |
| return Result; |
| |
| while (!list_Empty(List)) { |
| Depth = clause_Depth(list_Car(List)); |
| if (Min > Depth * clause_Weight(list_Car(List))) { |
| Result = list_Car(List); |
| if (Depth == 0) |
| return Result; |
| Min = clause_Depth(Result) * clause_Weight(Result); |
| } |
| List = list_Cdr(List); |
| } |
| |
| return Result; |
| }*/ |
| |
| |
| static LIST top_GetLiteralsForSplitting(CLAUSE Clause) |
| /************************************************************** |
| INPUT: A clause. |
| RETURNS: A list of succedent literal indices where every single |
| literal doesn't share any variables with other literals. |
| If the clause is horn, an empty list is returned. |
| ***************************************************************/ |
| { |
| LIST* Variables; /* An array, mapping literal index to list of variables */ |
| int i, j; |
| BOOL Stop; |
| LIST Failed, Result; |
| |
| Result = list_Nil(); |
| |
| /* Special case: horn clause */ |
| if (clause_IsHornClause(Clause)) |
| return Result; |
| |
| /* Special case: clause is ground, so return all succedent literals */ |
| if (clause_IsGround(Clause)) { |
| for (i = clause_LastSuccedentLitIndex(Clause); |
| i >= clause_FirstSuccedentLitIndex(Clause); i--) |
| Result = list_Cons((POINTER)i, Result); |
| return Result; |
| } |
| |
| Variables = memory_Malloc(sizeof(LIST) * clause_Length(Clause)); |
| /* Initialize the array */ |
| for (i = clause_FirstLitIndex(); i <= clause_LastLitIndex(Clause); i++) |
| Variables[i] = term_VariableSymbols(clause_GetLiteralAtom(Clause, i)); |
| |
| /* <Failed> is the set of literals that share variables with other literals */ |
| Failed = list_Nil(); |
| for (i = clause_LastSuccedentLitIndex(Clause); |
| i >= clause_FirstSuccedentLitIndex(Clause); i--) { |
| if (list_Empty(Variables[i])) |
| Result = list_Cons((POINTER)i, Result); |
| else if (!list_PointerMember(Failed, (POINTER)i)) { |
| /* We don't know yet whether the literal shares variables */ |
| Stop = FALSE; |
| for (j = clause_FirstLitIndex(); |
| j <= clause_LastLitIndex(Clause) && !Stop; j++) { |
| if (i != j && list_HasIntersection(Variables[i], Variables[j])) { |
| Stop = TRUE; /* Literal isn´t candidate for "optimal" splitting */ |
| Failed = list_Cons((POINTER)i, Failed); |
| Failed = list_Cons((POINTER)j, Failed); |
| } |
| } |
| if (!Stop) |
| Result = list_Cons((POINTER)i, Result); |
| } |
| } |
| |
| /* Cleanup */ |
| for (i = clause_FirstLitIndex(); i <= clause_LastLitIndex(Clause); i++) |
| list_Delete(Variables[i]); |
| memory_Free(Variables, sizeof(LIST) * clause_Length(Clause)); |
| list_Delete(Failed); |
| return Result; |
| } |
| |
| |
| static int top_GetOptimalSplitLiteralIndex(PROOFSEARCH Search, CLAUSE Clause, |
| BOOL Usables) |
| /************************************************************** |
| INPUT: A proofsearch object, a clause and a boolean flag. |
| RETURNS: The index of the positive literal from <Clause> |
| with the greatest number of instances (maybe 0) within |
| the WorkedOff/Usable sets of the proof search object. |
| The literal mustn't share any variables with other literals. |
| If the clause doesn't have a suitable literal, a negative |
| number is returned. |
| EFFECT: If <Usables> is FALSE, only the number of instances |
| within the WorkedOff set is considered, otherwise |
| the number of instances within both clause sets is considered. |
| ***************************************************************/ |
| { |
| LIST SplitLits; |
| LITERAL Literal; |
| NAT Count, MaxInstances; |
| int Result; |
| |
| MaxInstances = -1; |
| SplitLits = top_GetLiteralsForSplitting(Clause); |
| Result = -1; |
| |
| for ( ; !list_Empty(SplitLits); SplitLits = list_Pop(SplitLits)) { |
| Literal = clause_GetLiteral(Clause, (int)list_Car(SplitLits)); |
| /* Count the number of instances */ |
| Count = prfs_GetNumberOfInstances(Search, Literal, Usables); |
| if (Count > MaxInstances) { |
| Result = (int)list_Car(SplitLits); |
| MaxInstances = Count; |
| } |
| } |
| return Result; |
| } |
| |
| |
| /* EK: hier lassen oder nach search.c oder nach rules-split.c? */ |
| static CLAUSE top_GetPowerfulSplitClause(PROOFSEARCH Search, BOOL Usables, |
| int* LitIndex) |
| /************************************************************** |
| INPUT: A proofsearch object, a boolean flag and a pointer to a literal |
| index which is used as return value. |
| RETURNS: A clause from the usable set that was selected as given clause. |
| Iff no suitable clause was found NULL is returned and <*LitIndex> |
| is set to -1. |
| Iff a suitable clause was found, this clause is returned and |
| <*LitIndex> is set to the index of the "optimal" literal. |
| EFFECT: This function selects a clause from the "usable" set and |
| a literal that are "optimal" for the application of the splitting |
| rule with respect to the following criteria: |
| 1) the literal must occur in the succedent of the non-horn clause, |
| 2) the literal mustn't share any variables with other literals, |
| 3) the clause must have a solved constraint, |
| 4) the atom must have the maximum number of instances |
| a) within the set of "workedoff" clauses, iff <Usables>=FALSE |
| b) within the set of "usable" and "workedoff" clauses, |
| iff "Usables"=TRUE |
| 5) the atom must have at least one instance in another clause. |
| ***************************************************************/ |
| { |
| LIST Scan, SplitLits; |
| NAT MaxNrOfInstances, NrOfInstances; |
| CLAUSE Clause, OptimalClause; |
| TERM Atom; |
| SHARED_INDEX WOIndex, UsIndex; |
| |
| OptimalClause = NULL; |
| *LitIndex = -1; |
| MaxNrOfInstances = 0; |
| WOIndex = prfs_WorkedOffSharingIndex(Search); |
| UsIndex = prfs_UsableSharingIndex(Search); |
| |
| /* Prepare the term stamp */ |
| if (term_StampOverflow(sharing_StampID(WOIndex))) |
| sharing_ResetAllTermStamps(WOIndex); |
| if (Usables && term_StampOverflow(sharing_StampID(UsIndex))) |
| sharing_ResetAllTermStamps(UsIndex); |
| term_StartStamp(); |
| |
| for (Scan = prfs_UsableClauses(Search); !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) { |
| Clause = list_Car(Scan); |
| if (clause_HasSolvedConstraint(Clause) && !clause_IsHornClause(Clause)) { |
| /* Get a list of splittable literal indices */ |
| SplitLits = top_GetLiteralsForSplitting(Clause); |
| for ( ; !list_Empty(SplitLits); SplitLits = list_Pop(SplitLits)) { |
| LITERAL Literal; |
| |
| Literal = clause_GetLiteral(Clause, (int)list_Car(SplitLits)); |
| Atom = clause_LiteralAtom(Literal); |
| if (!term_AlreadyVisited(Atom)) { |
| /* Don't visit atom more than once */ |
| term_SetTermStamp(Atom); |
| /* Count the number of instances */ |
| NrOfInstances = prfs_GetNumberOfInstances(Search, Literal, Usables); |
| if (NrOfInstances > MaxNrOfInstances || OptimalClause == NULL || |
| (NrOfInstances == MaxNrOfInstances && |
| /* Prefer shorter clauses for splitting! */ |
| clause_Length(Clause) < clause_Length(OptimalClause))) { |
| OptimalClause = Clause; |
| MaxNrOfInstances = NrOfInstances; |
| *LitIndex = (int)list_Car(SplitLits); |
| } |
| } |
| } |
| } |
| } |
| term_StopStamp(); |
| |
| /* The splittable literal must have at least one instance to be useful */ |
| /* reducing other clauses. If <Usables> is TRUE, the literal must even */ |
| /* have two instances, since the literal of the given clause is in the */ |
| /* usable index, too. */ |
| if (MaxNrOfInstances == 0 || (Usables && MaxNrOfInstances == 1)) { |
| *LitIndex = -1; |
| OptimalClause = NULL; |
| } |
| |
| return OptimalClause; |
| } |
| |
| |
| static LIST top_FullReductionSelectGivenComputeDerivables(PROOFSEARCH Search, |
| CLAUSE *SplitClause, |
| int *Counter) |
| /************************************************************** |
| INPUT: A proof search object, a pointer to a clause resulting from a |
| previous splitting step, and a pointer to an integer counter. |
| RETURNS: A list of derived clauses. |
| EFFECT: In this function a clause is selected from the set of |
| "usable" clauses. After a clause was selected as "given clause", |
| inferences between the given clause and the "worked off" clauses |
| are made. The selection works as follows: |
| 1) If <*SplitClause> is not NULL, the split clause |
| is selected as "given clause". <*SplitClause> should result |
| from splitting |
| 2) If <*SplitClause> is NULL, we try to find a clause that is |
| "optimal" for splitting. This is done by selecting a literal |
| <L> in a clause, such that <L> is variable-disjoint from |
| the rest of the clause, and the atom of <L> has the maximum |
| number of instances within the set of "usable" and "workoff" |
| clauses. |
| 3) If the previous steps failed, a clause is selected by weight |
| or by depth, depending on the parameters "WDRatio", "PrefVar" |
| and "PrefCon". Then splitting is tried on the selected clause. |
| If the clause is a non-horn clause, we try to find a positive |
| literal <L> and a set of negative literals <N>, such that <N> |
| and <L> are variable disjoint from the rest of the clause. |
| ***************************************************************/ |
| { |
| CLAUSE GivenClause, TerminatorClause; |
| LIST Derivables, SplitLits; |
| FLAGSTORE Flags; |
| PRECEDENCE Precedence; |
| int LitIndex; |
| |
| GivenClause = NULL; |
| Derivables = list_Nil(); |
| Flags = prfs_Store(Search); |
| Precedence = prfs_Precedence(Search); |
| |
| /* 1) If the last given clause was split or if backtracking was applied, */ |
| /* then choose the clause resulting from the splitting step as */ |
| /* given clause. */ |
| /* ATTENTION: Since the <SplitClause> might have been reduced since */ |
| /* the time the variable was set, we have to check whether */ |
| /* <SplitClause> is still element of the set of usable clauses. */ |
| if (*SplitClause != NULL && |
| list_PointerMember(prfs_UsableClauses(Search), *SplitClause)) |
| GivenClause = *SplitClause; |
| |
| *SplitClause = NULL; |
| |
| if (GivenClause == NULL) { |
| if (prfs_SplitCounter(Search) != 0) |
| /* 2) Try to find an "optimal" splitting clause, that doesn't share */ |
| /* variables with any other literal. */ |
| GivenClause = top_GetPowerfulSplitClause(Search, FALSE, &LitIndex); |
| |
| if (GivenClause != NULL) { |
| /* Found "optimal" split clause, so apply splitting */ |
| SplitLits = list_List(clause_GetLiteral(GivenClause, LitIndex)); |
| *SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits); |
| list_Delete(SplitLits); |
| } else { |
| /* 3) Splitting wasn't applied, so use the other strategies */ |
| if ((*Counter) % flag_GetFlagValue(Flags, flag_WDRATIO) == 0) |
| GivenClause = top_SelectClauseDepth(prfs_UsableClauses(Search), Flags); |
| else { |
| if (flag_GetFlagValue(Flags, flag_PREFCON) != flag_PREFCONUNCHANGED) |
| GivenClause = top_SelectMinimalConWeightClause(prfs_UsableClauses(Search), |
| Flags); |
| else |
| GivenClause = top_SelectMinimalWeightClause(prfs_UsableClauses(Search), |
| Flags); |
| } |
| (*Counter)++; /* EK: hier lassen, oder eine Klammerebene nach aussen? */ |
| } |
| } |
| |
| if (*SplitClause == NULL && prfs_SplitCounter(Search) != 0) { |
| /* Try to find the "optimal" literal for splitting the clause. */ |
| /* This makes sense for a clause that is the right part of a */ |
| /* splitting step. */ |
| LitIndex = top_GetOptimalSplitLiteralIndex(Search, GivenClause, FALSE); |
| if (LitIndex >= 0) { |
| SplitLits = list_List(clause_GetLiteral(GivenClause, LitIndex)); |
| *SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits); |
| list_Delete(SplitLits); |
| } else { |
| /* Optimal splitting wasn't possible, so try the old-style splitting. */ |
| /* Here a split is done if a positive literal doesn't share variables */ |
| /* with another POSITIVE literal. */ |
| *SplitClause = prfs_PerformSplitting(Search, GivenClause); |
| } |
| } |
| |
| prfs_ExtractUsable(Search, GivenClause); |
| |
| if (flag_GetFlagValue(Flags, flag_PGIVEN)) { |
| fputs("\n\tGiven clause: ", stdout); |
| clause_Print(GivenClause); |
| fflush(stdout); |
| } |
| |
| if (*SplitClause != NULL) |
| Derivables = list_List(*SplitClause); |
| else { |
| /* No splitting was applied */ |
| if (flag_GetFlagValue(Flags, flag_RTER) != flag_RTEROFF) { |
| clock_StartCounter(clock_REDUCTION); |
| TerminatorClause = red_Terminator(GivenClause, |
| flag_GetFlagValue(Flags, flag_RTER), |
| prfs_WorkedOffSharingIndex(Search), |
| prfs_UsableSharingIndex(Search), Flags, |
| Precedence); |
| clock_StopAddPassedTime(clock_REDUCTION); |
| |
| if (TerminatorClause != NULL) { |
| /* An empty clause was derived by the "terminator" rule */ |
| Derivables = list_List(TerminatorClause); |
| prfs_InsertUsableClause(Search, GivenClause); |
| } |
| } |
| if (list_Empty(Derivables)) { |
| /* No splitting was applied, no empty clause was found by terminator */ |
| clause_SelectLiteral(GivenClause, Flags); |
| /*clause_SetSpecialFlags(GivenClause,ana_SortDecreasing());*/ |
| prfs_InsertWorkedOffClause(Search, GivenClause); |
| clock_StartCounter(clock_INFERENCE); |
| Derivables = inf_DerivableClauses(Search, GivenClause); |
| clock_StopAddPassedTime(clock_INFERENCE); |
| } |
| } |
| |
| prfs_IncDerivedClauses(Search, list_Length(Derivables)); |
| |
| return Derivables; |
| } |
| |
| |
| static LIST top_LazyReductionSelectGivenComputeDerivables(PROOFSEARCH Search, |
| CLAUSE *SplitClause, |
| int *Counter) |
| /************************************************************** |
| INPUT: A proof search object, a pointer to a clause resulting from a |
| previous splitting step, and a pointer to an integer counter. |
| RETURNS: A list of derived clauses. |
| EFFECT: In this function a clause is selected from the set of |
| "usable" clauses. After a clause was selected as "given clause", |
| inferences between the given clause and the "worked off" clauses |
| are made. Take a look at the description of the function |
| top_FullReduction... for more details. |
| This function is more complicated than the other function, |
| since clauses in the set of usable clauses may be reducible. |
| Because of this fact, the selection of the given clause |
| has to be done in a loop. After picking a "candidate" clause |
| the clause is inter-reduced with the "worked off" set. |
| If the candidate still exists after the reduction it is |
| selected as given clause, else another usable clause is picked |
| as candidate. |
| ***************************************************************/ |
| { |
| CLAUSE GivenClause, TerminatorClause; |
| LIST Derivables; |
| FLAGSTORE Flags; |
| PRECEDENCE Precedence; |
| int LitIndex; |
| |
| GivenClause = (CLAUSE)NULL; |
| TerminatorClause = (CLAUSE)NULL; |
| Derivables = list_Nil(); |
| Flags = prfs_Store(Search); |
| Precedence = prfs_Precedence(Search); |
| |
| while (GivenClause == (CLAUSE)NULL && |
| !list_Empty(prfs_UsableClauses(Search))) { |
| /* The selected clause may be redundant */ |
| |
| if (*SplitClause != NULL && |
| list_PointerMember(prfs_UsableClauses(Search), *SplitClause)) |
| GivenClause = *SplitClause; |
| |
| *SplitClause = NULL; |
| |
| /* Try selecting a clause that is optimal for splitting */ |
| if (GivenClause == NULL) { |
| if (prfs_SplitCounter(Search) != 0) { |
| GivenClause = top_GetPowerfulSplitClause(Search, FALSE, &LitIndex); |
| /* The value of <LitIndex> isn't used here. */ |
| } |
| |
| if (GivenClause == NULL) { |
| /* No optimal clause for splitting found */ |
| if ((*Counter) % flag_GetFlagValue(Flags, flag_WDRATIO) == 0) |
| GivenClause = top_SelectClauseDepth(prfs_UsableClauses(Search), Flags); |
| else { |
| if (flag_GetFlagValue(Flags, flag_PREFCON) != flag_PREFCONUNCHANGED) |
| GivenClause = top_SelectMinimalConWeightClause(prfs_UsableClauses(Search), |
| Flags); |
| else |
| GivenClause = top_SelectMinimalWeightClause(prfs_UsableClauses(Search), |
| Flags); |
| } |
| (*Counter)++; |
| } |
| } |
| prfs_ExtractUsable(Search, GivenClause); |
| |
| /* Reduce the selected clause */ |
| clock_StartCounter(clock_REDUCTION); |
| GivenClause = red_CompleteReductionOnDerivedClause(Search, GivenClause, |
| red_WORKEDOFF); |
| clock_StopAddPassedTime(clock_REDUCTION); |
| } |
| |
| if (GivenClause == (CLAUSE)NULL) |
| /* Set of usable clauses is empty */ |
| return list_Nil(); |
| |
| |
| if (clause_IsEmptyClause(GivenClause)) { |
| Derivables = list_List(GivenClause); |
| return Derivables; |
| } |
| else { |
| /* Reduce Workedoff clauses with selected clause */ |
| clock_StartCounter(clock_REDUCTION); |
| Derivables = red_BackReduction(Search, GivenClause, red_WORKEDOFF); |
| clock_StopAddPassedTime(clock_REDUCTION); |
| } |
| |
| /* Print selected clause */ |
| if (flag_GetFlagValue(Flags, flag_PGIVEN)) { |
| fputs("\n\tGiven clause: ", stdout); |
| clause_Print(GivenClause); |
| fflush(stdout); |
| } |
| |
| /* Try splitting */ |
| if (prfs_SplitCounter(Search) != 0) { |
| /* First try "optimal" splitting on the selected clause */ |
| LitIndex = top_GetOptimalSplitLiteralIndex(Search, GivenClause, FALSE); |
| |
| if (LitIndex >= 0) { |
| LIST SplitLits; |
| |
| SplitLits = list_List(clause_GetLiteral(GivenClause, LitIndex)); |
| *SplitClause = prfs_DoSplitting(Search, GivenClause, SplitLits); |
| list_Delete(SplitLits); |
| } else { |
| /* Try the old splitting that allows negative literals */ |
| /* sharing variables with the selected positive literal. */ |
| *SplitClause = prfs_PerformSplitting(Search, GivenClause); |
| } |
| } |
| |
| if (*SplitClause != NULL) { |
| Derivables = list_Cons(*SplitClause, Derivables); |
| } else { |
| /* Try terminator reduction only for a clause that wasn't splitted. */ |
| if (flag_GetFlagValue(Flags, flag_RTER) != flag_RTEROFF) { |
| TerminatorClause = red_Terminator(GivenClause, |
| flag_GetFlagValue(Flags, flag_RTER), |
| prfs_WorkedOffSharingIndex(Search), |
| prfs_UsableSharingIndex(Search), |
| Flags, Precedence); |
| if (TerminatorClause != NULL) { |
| Derivables = list_Cons(TerminatorClause, Derivables); |
| prfs_InsertUsableClause(Search, GivenClause); |
| } |
| } |
| if (TerminatorClause == (CLAUSE)NULL) { |
| clause_SelectLiteral(GivenClause, Flags); |
| /* clause_SetSpecialFlags(GivenClause,ana_SortDecreasing());*/ |
| prfs_InsertWorkedOffClause(Search, GivenClause); |
| clock_StartCounter(clock_INFERENCE); |
| Derivables = list_Nconc(Derivables, |
| inf_DerivableClauses(Search, GivenClause)); |
| clock_StopAddPassedTime(clock_INFERENCE); |
| } |
| } |
| |
| prfs_IncDerivedClauses(Search, list_Length(Derivables)); |
| |
| return Derivables; |
| } |
| |
| |
| static PROOFSEARCH top_ProofSearch(PROOFSEARCH Search, LIST ProblemClauses, |
| FLAGSTORE InputFlags, LIST UserPrecedence, int *BoundApplied) |
| /************************************************************** |
| INPUT: A proof search object, a list of clauses, a flag store |
| containing the flags from the command line and from |
| the input file, a list containing the precedence as |
| specified by the user, and a pointer to an integer. |
| RETURNS: The same proof search object |
| EFFECTS: |
| ***************************************************************/ |
| { |
| LIST Scan,EmptyClauses,Derivables; |
| LIST UsedEmptyClauses; |
| CLAUSE SplitClause,HighestLevelEmptyClause; |
| FLAGSTORE Flags; |
| PRECEDENCE Precedence; |
| int Counter, ActBound, BoundMode, BoundLoops; |
| |
| HighestLevelEmptyClause = (CLAUSE)NULL; |
| UsedEmptyClauses = list_Nil(); |
| EmptyClauses = list_Nil(); |
| Derivables = list_Nil(); |
| Flags = prfs_Store(Search); |
| Precedence = prfs_Precedence(Search); |
| Counter = 1; |
| |
| clock_InitCounter(clock_REDUCTION); |
| clock_InitCounter(clock_BACKTRACK); |
| clock_InitCounter(clock_INFERENCE); |
| |
| /* Important ! Recomputes Weight ! */ |
| ana_AnalyzeProblem(Search, ProblemClauses); |
| if (flag_GetFlagValue(Flags, flag_AUTO)) { |
| prfs_InstallFiniteMonadicPredicates(Search, ProblemClauses, ana_FinMonPredList()); |
| ana_AutoConfiguration(ProblemClauses, Flags, Precedence); |
| /* File and input flags have higher precedence */ |
| flag_TransferSetFlags(InputFlags, Flags); |
| } |
| |
| /* Rearrange automatically determined precedence according to user's specification. */ |
| symbol_RearrangePrecedence(Precedence, UserPrecedence); |
| |
| for (Scan = ProblemClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| clause_OrientAndReInit(list_Car(Scan), Flags, Precedence); |
| |
| /* Must be called after ana_AnalyzeProblem and Reorientation */ |
| ana_AnalyzeSortStructure(ProblemClauses, Flags, Precedence); |
| |
| if (flag_GetFlagValue(Flags, flag_AUTO)) { |
| ana_ExploitSortAnalysis(Flags); |
| /* File and input flags have higher precedence */ |
| flag_TransferSetFlags(InputFlags, Flags); |
| } |
| prfs_SetSplitCounter(Search, flag_GetFlagValue(Flags, flag_SPLITS)); |
| |
| ActBound = flag_GetFlagValue(Flags, flag_BOUNDSTART); |
| BoundMode = flag_GetFlagValue(Flags, flag_BOUNDMODE); |
| BoundLoops = flag_GetFlagValue(Flags, flag_BOUNDLOOPS); |
| *BoundApplied = -1; |
| |
| if (flag_GetFlagValue(Flags, flag_PPROBLEM)) { |
| puts(""); |
| puts("--------------------------SPASS-START-----------------------------"); |
| puts("Input Problem:"); |
| clause_ListPrint(ProblemClauses); |
| ana_Print(Flags, Precedence); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_SORTS) != flag_SORTSOFF) { |
| BOOL Strong; |
| Strong = (flag_GetFlagValue(Flags, flag_SORTS) == flag_SORTSMONADICALL); |
| for (Scan = ProblemClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| clause_SetSortConstraint((CLAUSE)list_Car(Scan),Strong,Flags, Precedence); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_RINPUT)) { |
| clock_StartCounter(clock_REDUCTION); |
| EmptyClauses = red_ReduceInput(Search, ProblemClauses); |
| clock_StopAddPassedTime(clock_REDUCTION); |
| if (list_Empty(EmptyClauses) && flag_GetFlagValue(Flags, flag_SATINPUT)) |
| EmptyClauses = red_SatInput(Search); |
| } |
| else { |
| for (Scan=ProblemClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| prfs_InsertUsableClause(Search, list_Car(Scan)); |
| } |
| Derivables = list_Nil(); |
| |
| if (ana_SortRestrictions() || |
| (ana_UnsolvedSortRestrictions() && |
| flag_GetFlagValue(Flags,flag_SORTS) == flag_SORTSMONADICALL)) { |
| if (flag_GetFlagValue(Flags, flag_RSST)) |
| prfs_SetStaticSortTheory(Search,sort_ApproxStaticSortTheory(prfs_UsableClauses(Search),Flags,Precedence)); |
| prfs_SetDynamicSortTheory(Search,sort_TheoryCreate()); |
| } |
| |
| /* Fix literal order in clauses in the usable set. |
| Since they are shared, we have to extract them from |
| the sharing before fixing them. Afterwards, we have to |
| insert them in the sharing again. |
| */ |
| for (Scan = prfs_UsableClauses(Search); |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) { |
| CLAUSE clause; |
| clause = list_Car(Scan); |
| clause_MakeUnshared(clause,prfs_UsableSharingIndex(Search)); |
| clause_FixLiteralOrder(clause, Flags, Precedence); |
| clause_InsertIntoSharing(clause, prfs_UsableSharingIndex(Search), |
| prfs_Store(Search), prfs_Precedence(Search)); |
| } |
| |
| /* Calculate the frequency counts for the symbols in the usable set. */ |
| for (Scan = prfs_UsableClauses(Search); |
| !list_Empty(Scan); |
| Scan = list_Cdr(Scan)) { |
| CLAUSE clause; |
| clause = list_Car(Scan); |
| |
| clause_CountSymbols(clause); |
| } |
| |
| /* Sort usable set. */ |
| prfs_SetUsableClauses(Search, |
| list_Sort(prfs_UsableClauses(Search), |
| (BOOL (*) (void *, void *)) clause_CompareAbstractLEQ)); |
| |
| if (flag_GetFlagValue(Flags, flag_SOS)) { |
| Derivables = list_Copy(prfs_UsableClauses(Search)); |
| for (Scan=Derivables;!list_Empty(Scan);Scan=list_Cdr(Scan)) |
| if (!clause_GetFlag(list_Car(Scan), CONCLAUSE)) |
| prfs_MoveUsableWorkedOff(Search,list_Car(Scan)); |
| list_Delete(Derivables); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_PPROBLEM)) { |
| puts("\nProcessed Problem:"); |
| puts("\nWorked Off Clauses:"); |
| clause_ListPrint(prfs_WorkedOffClauses(Search)); |
| puts("\nUsable Clauses:"); |
| clause_ListPrint(prfs_UsableClauses(Search)); |
| } |
| |
| while ((list_Empty(EmptyClauses) || !prfs_SplitStackEmpty(Search)) && |
| prfs_Loops(Search) != 0 && |
| ((*BoundApplied != -1) || !list_Empty(prfs_UsableClauses(Search))) && |
| (flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED || |
| flag_GetFlagValue(Flags,flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) { |
| |
| Derivables = list_Nil(); |
| SplitClause = (CLAUSE)NULL; |
| *BoundApplied = -1; |
| |
| while ((list_Empty(EmptyClauses) || !prfs_SplitStackEmpty(Search)) && |
| prfs_Loops(Search) != 0 && |
| (!list_Empty(prfs_UsableClauses(Search)) || !list_Empty(EmptyClauses)) && |
| (flag_GetFlagValue(Flags,flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED || |
| flag_GetFlagValue(Flags,flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL))) { |
| |
| if (!list_Empty(EmptyClauses)) { |
| /* Backtracking */ |
| clock_StartCounter(clock_BACKTRACK); |
| Derivables = split_Backtrack(Search, HighestLevelEmptyClause, |
| &SplitClause); |
| clock_StopAddPassedTime(clock_BACKTRACK); |
| prfs_IncBacktrackedClauses(Search, list_Length(Derivables)); |
| |
| if (prfs_SplitStackEmpty(Search)) |
| Derivables = list_Nconc(EmptyClauses, Derivables); |
| else { |
| for ( ; !list_Empty(EmptyClauses); EmptyClauses = list_Pop(EmptyClauses)) |
| if (list_Car(EmptyClauses) != HighestLevelEmptyClause) |
| clause_Delete(list_Car(EmptyClauses)); |
| prfs_InsertDocProofClause(Search, HighestLevelEmptyClause); |
| /* Keep HighestLevelEmptyClause for finding the terms required */ |
| /* for the proof. */ |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF)) |
| UsedEmptyClauses = list_Cons(HighestLevelEmptyClause, UsedEmptyClauses); |
| if (flag_GetFlagValue(Flags, flag_DOCSPLIT)) |
| printf("\n\t Split Backtracking level %d:",prfs_ValidLevel(Search)); |
| } |
| EmptyClauses = list_Nil(); |
| HighestLevelEmptyClause = (CLAUSE)NULL; |
| } |
| else { /* no empty clause found */ |
| |
| #ifdef CHECK |
| if (!prfs_Check(Search)) { |
| misc_StartErrorReport(); |
| misc_ErrorReport("\n In top_ProofSearch: Illegal state of search in SPASS.\n"); |
| misc_FinishErrorReport(); |
| } |
| if (!ana_Equations()) |
| red_CheckSplitSubsumptionCondition(Search); |
| #endif |
| |
| if (flag_GetFlagValue(Flags, flag_FULLRED)) |
| Derivables = top_FullReductionSelectGivenComputeDerivables(Search, &SplitClause, &Counter); |
| else |
| Derivables = top_LazyReductionSelectGivenComputeDerivables(Search, &SplitClause, &Counter); |
| } |
| |
| /* Print the derived clauses, if required */ |
| if (flag_GetFlagValue(Flags, flag_PDER)) |
| for (Scan=Derivables; !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| fputs("\nDerived: ", stdout); |
| clause_Print(list_Car(Scan)); |
| } |
| |
| /* Partition the derived clauses into empty and non-empty clauses */ |
| Derivables = split_ExtractEmptyClauses(Derivables, &EmptyClauses); |
| |
| /* Apply reduction rules */ |
| clock_StartCounter(clock_REDUCTION); |
| if (flag_GetFlagValue(Flags, flag_FULLRED)) { |
| EmptyClauses = |
| list_Nconc(EmptyClauses, |
| red_CompleteReductionOnDerivedClauses(Search, Derivables, |
| red_ALL, ActBound, |
| BoundMode, |
| BoundApplied)); |
| } else { |
| EmptyClauses = |
| list_Nconc(EmptyClauses, |
| red_CompleteReductionOnDerivedClauses(Search, Derivables, |
| red_WORKEDOFF, |
| ActBound, BoundMode, |
| BoundApplied)); |
| } |
| clock_StopAddPassedTime(clock_REDUCTION); |
| |
| |
| if (!list_Empty(EmptyClauses)) { |
| HighestLevelEmptyClause = split_SmallestSplitLevelClause(EmptyClauses); |
| if (flag_GetFlagValue(Flags, flag_PEMPTYCLAUSE)) { |
| fputs("\nEmptyClause: ", stdout); |
| clause_Print(HighestLevelEmptyClause); |
| } |
| } |
| prfs_DecLoops(Search); |
| } |
| |
| if (ActBound != flag_BOUNDSTARTUNLIMITED && |
| BoundMode != flag_BOUNDMODEUNLIMITED) { |
| BoundLoops--; |
| if (BoundLoops == flag_BOUNDLOOPSMIN) |
| ActBound = flag_BOUNDSTARTUNLIMITED; |
| else |
| ActBound = *BoundApplied; |
| if (*BoundApplied != -1) { |
| prfs_SwapIndexes(Search); |
| if (flag_GetFlagValue(Flags,flag_PBINC)) |
| printf("\n\n\t ---- New Clause %s Bound: %2d ----\n", |
| (BoundMode==flag_BOUNDMODERESTRICTEDBYDEPTH) ? "Term Depth" : "Weight",ActBound); |
| } |
| } |
| } |
| prfs_SetEmptyClauses(Search, EmptyClauses); |
| prfs_SetUsedEmptyClauses(Search, UsedEmptyClauses); |
| |
| return Search; |
| } |
| |
| |
| static void top_Flotter(int argc, const char* argv[], LIST InputClauses) |
| /************************************************************** |
| INPUT: |
| RETURNS: Nothing. |
| EFFECT: |
| ***************************************************************/ |
| { |
| FILE *Output; |
| char *description; |
| const char *creator = "\n\tCNF generated by FLOTTER " misc_VERSION " *}"; |
| int size; |
| int creator_size; |
| |
| if (argc < opts_Indicator()+2) |
| Output = stdout; |
| else |
| Output = misc_OpenFile(argv[opts_Indicator()+1],"w"); |
| |
| creator_size = (int)strlen(creator); |
| size = (int)strlen(dfg_ProblemDescription()) + creator_size; |
| description = (char*)memory_Malloc(sizeof(char)*size); |
| strncpy(description,dfg_ProblemDescription(),size-creator_size-3); |
| strcpy(description+size-creator_size-3, creator); |
| |
| |
| clause_FPrintCnfDFGProblem(Output, dfg_ProblemName(), dfg_ProblemAuthor(), |
| dfg_ProblemStatusString(), description, InputClauses); |
| |
| fputs("\nFLOTTER needed\t", stdout); |
| clock_PrintTime(clock_INPUT); |
| puts(" for the input."); |
| fputs("\t\t", stdout); |
| clock_PrintTime(clock_CNF); |
| fputs(" for the CNF translation.", stdout); |
| |
| |
| if (Output != stdout) |
| misc_CloseFile(Output,argv[opts_Indicator()+1]); |
| memory_Free(description, sizeof(char)*size); |
| } |
| |
| static BOOL top_CalledFlotter(const char* Call) |
| { |
| int length; |
| length = strlen(Call); |
| return string_Equal((Call + (length > 7 ? length - 7 : 0)), "FLOTTER"); |
| } |
| |
| |
| |
| /**************************************************************/ |
| /* Main Function */ |
| /**************************************************************/ |
| |
| int main(int argc, const char* argv[]) |
| { |
| LIST InputClauses,Scan,Axioms,Conjectures, Sorts, QueryClauses, |
| LabelClauses, QueryPair, ProblemClauses, Labellist, Sortlabellist, |
| Symblist, UserPrecedence; |
| PROOFSEARCH Search, FlotterSearch; |
| /* <InputFlags> are the flags from the problem file and the command line. */ |
| FLAGSTORE InputFlags, Flags; |
| /* <InputPrecedence> is the precedence after reading the problem file. */ |
| PRECEDENCE InputPrecedence, Precedence; |
| FILE* InputStream; |
| HASH TermLabelToClauselist, ClauseToTermLabellist; |
| top_SEARCHRESULT Result; |
| |
| Search = (PROOFSEARCH)NULL; |
| |
| #if (defined(SPASS_SIGNALS)) |
| top_PROOFSEARCH = &Search; |
| signal(SIGINT, top_SigHandler); |
| signal(SIGTERM, top_SigHandler); |
| signal(SIGSEGV, top_SigHandler); |
| signal(SIGBUS, top_SigHandler); |
| #endif |
| |
| clock_Init(); |
| clock_StartCounter(clock_OVERALL); |
| memory_Init(memory__UNLIMITED); |
| atexit(memory_FreeAllMem); |
| symbol_Init(TRUE); |
| stack_Init(); |
| hash_Init(); |
| sort_Init(); |
| term_Init(); |
| |
| InputPrecedence = symbol_CreatePrecedence(); |
| fol_Init(TRUE, InputPrecedence); |
| cont_Init(); |
| unify_Init(); |
| flag_Init(); |
| subs_Init(); |
| clause_Init(); |
| red_Init(); |
| ren_Init(); |
| dp_Init(); |
| opts_Init(); |
| ana_Init(); |
| cc_Init(); |
| |
| /* Build proof search object to store definitions in */ |
| Search = prfs_Create(); |
| InputFlags = flag_CreateStore(); |
| |
| /* declare all options */ |
| opts_DeclareSPASSFlagsAsOptions(); |
| top_RemoveFileOptId = opts_Declare("rf", opts_NOARGTYPE); |
| |
| if (!opts_Read(argc, argv)) |
| return EXIT_FAILURE; |
| |
| /* Check whether flag_STDIN is set in the command line */ |
| flag_InitStoreByDefaults(InputFlags); |
| opts_SetFlags(InputFlags); |
| |
| if (argc < opts_Indicator()+1 && !flag_GetFlagValue(InputFlags,flag_STDIN)) { |
| /* No input file, no stdin input */ |
| printf("\n\t %s %s",argv[0],misc_VERSION); |
| if (top_CalledFlotter(argv[0]) || |
| flag_GetFlagValue(InputFlags, flag_FLOTTER)) |
| puts("\n\t Usage: FLOTTER [options] [<input-file>] [<output-file>]\n"); |
| else |
| puts("\n\t Usage: SPASS [options] [<input-file>] \n"); |
| puts("Possible options:\n"); |
| opts_PrintSPASSNames(); |
| return EXIT_FAILURE; |
| } |
| FlotterSearch = NULL; |
| |
| Axioms = Conjectures = Sorts = Labellist = Sortlabellist = UserPrecedence = list_Nil(); |
| |
| if (flag_GetFlagValue(InputFlags, flag_STDIN)) { |
| top_InputFile = (char*)NULL; |
| InputStream = stdin; |
| } else { |
| top_InputFile = argv[opts_Indicator()]; |
| InputStream = misc_OpenFile(top_InputFile, "r"); |
| } |
| |
| clock_StartCounter(clock_INPUT); |
| flag_CleanStore(InputFlags); /* Mark all flags as unset */ |
| |
| /* Now add flags from file to InputFlags and set precedence */ |
| InputClauses = dfg_DFGParser(InputStream, InputFlags, InputPrecedence, &Axioms, |
| &Conjectures, &Sorts, &UserPrecedence); |
| |
| /* Add/overwrite with command line flags */ |
| opts_SetFlags(InputFlags); |
| Flags = prfs_Store(Search); |
| Precedence = prfs_Precedence(Search); |
| /* The Flags were initialized with the default flag values. */ |
| /* This values are now overwritten by command line flags and flags */ |
| /* from the input file. */ |
| flag_TransferSetFlags(InputFlags, Flags); |
| /* From now on the input flags are not changed! */ |
| |
| /* Transfer input precedence to search object */ |
| symbol_TransferPrecedence(InputPrecedence, Precedence); |
| |
| |
| /* Complain about missing input clauses/formulae when in */ |
| /* non-interactive mode */ |
| if (!flag_GetFlagValue(Flags, flag_INTERACTIVE) && list_Empty(Axioms) && |
| list_Empty(Conjectures) && list_Empty(InputClauses)) { |
| misc_StartUserErrorReport(); |
| misc_UserErrorReport("\n No formulae and clauses found in input file!\n"); |
| misc_FinishUserErrorReport(); |
| } |
| |
| cnf_Init(Flags); /* Depends on Strong Skolemization Flag */ |
| |
| /* DocProof is required for interactive mode */ |
| if (flag_GetFlagValue(Flags, flag_INTERACTIVE)) { |
| flag_SetFlagValue(Flags, flag_DOCPROOF, flag_DOCPROOFON); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF)) |
| prfs_AddDocProofSharingIndex(Search); |
| |
| /* Create necessary hasharrays */ |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { |
| TermLabelToClauselist = hsh_Create(); |
| ClauseToTermLabellist = hsh_Create(); |
| } |
| else { |
| TermLabelToClauselist = NULL; |
| ClauseToTermLabellist = NULL; |
| } |
| |
| /* Build conjecture formula and negate it: Conjectures are taken disjunctively!!*/ |
| for (Scan = Conjectures; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| list_Rplacd(list_Car(Scan), (LIST)term_Create(fol_Not(), |
| list_List(list_PairSecond(list_Car(Scan))))); |
| |
| clock_StopPassedTime(clock_INPUT); |
| |
| if (top_InputFile) { |
| misc_CloseFile(InputStream,top_InputFile); |
| if (opts_IsSet(top_RemoveFileOptId)) |
| remove(top_InputFile); |
| } |
| |
| clock_StartCounter(clock_CNF); |
| |
| if (list_Empty(InputClauses)) { |
| NAT Termcount; |
| |
| Termcount = 0; |
| |
| /* Create labels for formulae without them */ |
| for (Scan = Axioms; !list_Empty(Scan); Scan = list_Cdr(Scan), Termcount++) { |
| if (list_PairFirst(list_Car(Scan)) == NULL) { |
| char L[100]; |
| char* Label; |
| sprintf(L, "axiom%d", Termcount); |
| Label = string_StringCopy(L); |
| list_Rplaca(list_Car(Scan), Label); |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF) && |
| flag_GetFlagValue(Flags, flag_PLABELS)) { |
| printf("\nAdded label %s for axiom \n", Label); |
| fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan))); |
| } |
| } |
| } |
| Termcount = 0; |
| for (Scan = Sorts; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| char L[100]; |
| char* Label; |
| sprintf(L, "declaration%d", Termcount); |
| Label = string_StringCopy(L); |
| list_Rplaca(list_Car(Scan), Label); |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF) && |
| flag_GetFlagValue(Flags, flag_PLABELS)) { |
| printf("\nAdded label %s for declaration \n", Label); |
| fol_PrettyPrintDFG((TERM) list_PairSecond(list_Car(Scan))); |
| } |
| Sortlabellist = list_Cons(Label, Sortlabellist); |
| } |
| Axioms = list_Nconc(Axioms, Sorts); |
| |
| |
| if (flag_GetFlagValue(Flags, flag_APPLYDEFS) != flag_APPLYDEFSOFF) { |
| def_ExtractDefsFromTermlist(Search, Axioms, Conjectures); |
| Conjectures = def_ApplyDefinitionToTermList(prfs_Definitions(Search), |
| Conjectures, Flags, |
| Precedence); |
| } |
| |
| /* We must keep the list of symbols because they can't be freed in cnf_Flotter */ |
| Symblist = list_Nil(); |
| |
| /* Axioms is list of pairs, conjectures is list of terms */ |
| /* A ProofSearch object is only returned and the symbols kept in Symblist |
| if flag_INTERACTIVE is set */ |
| FlotterSearch = cnf_Flotter(Axioms,Conjectures,&InputClauses, &Labellist, |
| TermLabelToClauselist, ClauseToTermLabellist, |
| Flags, Precedence, &Symblist); |
| |
| InputClauses = clause_ListSortWeighed(InputClauses); |
| clause_SetCounter(1); |
| for (Scan = InputClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) { |
| clause_NewNumber(list_Car(Scan)); |
| } |
| } |
| else { |
| dfg_DeleteFormulaPairList(Axioms); |
| dfg_DeleteFormulaPairList(Sorts); |
| dfg_DeleteFormulaPairList(Conjectures); |
| if (flag_GetFlagValue(Flags, flag_APPLYDEFS) != flag_APPLYDEFSOFF) { |
| /* Extract list of definitions */ |
| def_ExtractDefsFromClauselist(Search, InputClauses); |
| def_FlattenDefinitionsDestructive(Search); |
| for (Scan=prfs_Definitions(Search); !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| InputClauses = def_ApplyDefToClauselist(Search, (DEF) list_Car(Scan), |
| InputClauses, TRUE); |
| } |
| } |
| |
| clock_StopPassedTime(clock_CNF); |
| |
| if (top_CalledFlotter(argv[0]) || flag_GetFlagValue(Flags, flag_FLOTTER)) { |
| top_Flotter(argc,argv,InputClauses); |
| flag_SetFlagValue(Flags, flag_TIMELIMIT, 0); /* Exit No Output */ |
| flag_SetFlagValue(Flags, flag_INTERACTIVE, flag_INTERACTIVEOFF); |
| flag_SetFlagValue(Flags, flag_PPROBLEM, flag_PPROBLEMOFF); |
| } |
| |
| memory_Restrict(flag_GetFlagValue(Flags, flag_MEMORY)); |
| |
| do { |
| LIST deflist; |
| int BoundApplied; |
| ProblemClauses = list_Nil(); |
| LabelClauses = list_Nil(); |
| Result = top_RESOURCE; |
| |
| if (flag_GetFlagValue(Flags, flag_INTERACTIVE)) { |
| QueryPair = ia_GetNextRequest(InputStream, Flags); |
| /* A pair (<formula,labellist>) */ |
| /* Get list of clauses derivable from formulae with labels in labellist */ |
| if (list_Empty(QueryPair)) { |
| break; |
| } |
| for (Scan=list_PairSecond(QueryPair);!list_Empty(Scan);Scan=list_Cdr(Scan)) { |
| LIST l; |
| l = hsh_GetWithCompareFunc(TermLabelToClauselist, list_Car(Scan), |
| (BOOL (*)(POINTER, POINTER)) cnf_LabelEqual, |
| (unsigned long (*)(POINTER)) hsh_StringHashKey); |
| |
| l = list_PointerDeleteDuplicates(list_Copy(l)); |
| LabelClauses = list_Nconc(l, LabelClauses); |
| } |
| /* Get list of clauses derivable from sorts */ |
| for (Scan=Sortlabellist; !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| LIST l; |
| l = hsh_GetWithCompareFunc(TermLabelToClauselist, list_Car(Scan), |
| (BOOL (*)(POINTER, POINTER)) cnf_LabelEqual, |
| (unsigned long (*)(POINTER)) hsh_StringHashKey); |
| |
| l = list_PointerDeleteDuplicates(list_Copy(l)); |
| LabelClauses = list_Nconc(l, LabelClauses); |
| } |
| |
| /* For labelclauses copies are introduced */ |
| /* So an update to the clause to term mapping is necessary */ |
| for (Scan=LabelClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) { |
| CLAUSE C; |
| LIST l; |
| C = (CLAUSE) list_Car(Scan); |
| l = list_Copy(hsh_Get(ClauseToTermLabellist, C)); |
| l = cnf_DeleteDuplicateLabelsFromList(l); |
| list_Rplaca(Scan, clause_Copy(C)); |
| hsh_PutList(ClauseToTermLabellist, list_Car(Scan), l); |
| } |
| QueryClauses = cnf_QueryFlotter(FlotterSearch, list_PairFirst(QueryPair), |
| &Symblist); |
| ProblemClauses = list_Nconc(QueryClauses, LabelClauses); |
| |
| for (Scan=list_PairSecond(QueryPair); !list_Empty(Scan); Scan= list_Cdr(Scan)) |
| string_StringFree(list_Car(Scan)); /* Free the label strings */ |
| list_Delete(list_PairSecond(QueryPair)); |
| list_PairFree(QueryPair); |
| clock_InitCounter(clock_OVERALL); |
| clock_StartCounter(clock_OVERALL); |
| } |
| else { |
| ProblemClauses = InputClauses; |
| InputClauses = list_Nil(); |
| } |
| |
| |
| prfs_SetSplitCounter(Search,flag_GetFlagValue(Flags, flag_SPLITS)); |
| prfs_SetLoops(Search,flag_GetFlagValue(Flags, flag_LOOPS)); |
| prfs_SetBacktrackedClauses(Search, 0); |
| BoundApplied = -1; |
| Search = top_ProofSearch(Search, ProblemClauses, InputFlags, UserPrecedence, &BoundApplied); |
| |
| if ((flag_GetFlagValue(Flags, flag_TIMELIMIT) == flag_TIMELIMITUNLIMITED || |
| flag_GetFlagValue(Flags, flag_TIMELIMIT) > clock_GetSeconds(clock_OVERALL)) && |
| prfs_Loops(Search) != 0 && |
| (BoundApplied == -1 || !list_Empty(prfs_EmptyClauses(Search)))) { |
| if (list_Empty(prfs_EmptyClauses(Search))) |
| Result = top_COMPLETION; |
| else |
| Result = top_PROOF; |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_TIMELIMIT) != 0) { |
| /* Stop SPASS immediately */ |
| printf("\nSPASS %s ", misc_VERSION); |
| fputs("\nSPASS beiseite: ", stdout); |
| switch (Result) { |
| case top_RESOURCE: |
| if (prfs_Loops(Search) != 0) |
| fputs("Ran out of time.", stdout); |
| else |
| fputs("Maximal number of loops exceeded.", stdout); |
| break; |
| case top_PROOF: |
| fputs("Proof found.", stdout); |
| break; |
| default: /* Completion */ |
| fputs("Completion found.", stdout); |
| } |
| printf("\nProblem: %s ", |
| (top_InputFile != (char*)NULL ? mybasename(top_InputFile) : "Read from stdin.")); |
| if (flag_GetFlagValue(Flags, flag_PSTATISTIC)) { |
| clock_StopPassedTime(clock_OVERALL); |
| printf("\nSPASS derived %d clauses,", prfs_DerivedClauses(Search)); |
| printf(" backtracked %d clauses", prfs_BacktrackedClauses(Search)); |
| printf(" and kept %d clauses.", prfs_KeptClauses(Search)); |
| fputs("\nSPASS spent\t", stdout); |
| clock_PrintTime(clock_OVERALL); |
| fputs(" on the problem.\n\t\t", stdout); |
| clock_PrintTime(clock_INPUT); |
| fputs(" for the input.\n\t\t", stdout); |
| clock_PrintTime(clock_CNF); |
| fputs(" for the FLOTTER CNF translation.\n\t\t", stdout); |
| clock_PrintTime(clock_INFERENCE); |
| fputs(" for inferences.\n\t\t", stdout); |
| clock_PrintTime(clock_BACKTRACK); |
| fputs(" for the backtracking.\n\t\t", stdout); |
| clock_PrintTime(clock_REDUCTION); |
| puts(" for the reduction."); |
| } |
| if (Result != top_PROOF && |
| flag_GetFlagValue(Flags, flag_FPMODEL) != flag_FPMODELOFF) { |
| FILE *Output; |
| char name[100]; |
| const char * creator = "{*SPASS " misc_VERSION " *}"; |
| BOOL PrintPotProductive; |
| |
| strcpy(name, (top_InputFile != (char*)NULL ? top_InputFile : "SPASS")); |
| if (Result == top_COMPLETION) |
| strcat(name, ".model"); |
| else |
| strcat(name, ".clauses"); |
| Output = misc_OpenFile(name,"w"); |
| PrintPotProductive = (flag_GetFlagValue(Flags, flag_FPMODEL) == |
| flag_FPMODELPOTENTIALLYPRODUCTIVECLAUSES); |
| if (Result == top_COMPLETION) |
| clause_FPrintCnfFormulasDFGProblem(Output, PrintPotProductive, |
| "{*Completion_by_SPASS*}", |
| creator, "satisfiable", |
| dfg_ProblemDescription(), |
| prfs_WorkedOffClauses(Search), |
| list_Nil(), Flags, Precedence); |
| else |
| clause_FPrintCnfFormulasDFGProblem(Output, PrintPotProductive, |
| "{*Clauses_generated_by_SPASS*}", |
| creator, "unknown", |
| dfg_ProblemDescription(), |
| prfs_WorkedOffClauses(Search), |
| prfs_UsableClauses(Search), Flags, |
| Precedence); |
| misc_CloseFile(Output, name); |
| if (Result == top_COMPLETION) |
| printf("\nCompletion printed to: %s\n", name); |
| else |
| printf("\nClauses printed to: %s\n", name); |
| } |
| |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF) && Result != top_RESOURCE) { |
| if (Result == top_COMPLETION) { |
| puts("\n\n The saturated set of worked-off clauses is :"); |
| clause_ListPrint(prfs_WorkedOffClauses(Search)); |
| } |
| else { |
| LIST UsedClauses, UsedTerms; |
| if (!top_InputFile) |
| top_InputFile = "SPASS"; |
| UsedClauses = dp_PrintProof(Search, prfs_EmptyClauses(Search), |
| top_InputFile); |
| /* Find terms required for proof */ |
| UsedTerms = list_Nil(); |
| |
| for (Scan = UsedClauses; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (clause_IsFromInput((CLAUSE) list_Car(Scan))) { |
| LIST L; |
| L = hsh_Get(ClauseToTermLabellist, list_Car(Scan)); |
| L = list_Copy(L); |
| L = cnf_DeleteDuplicateLabelsFromList(L); |
| UsedTerms = list_Nconc(UsedTerms, L); |
| } |
| list_Delete(UsedClauses); |
| UsedTerms = cnf_DeleteDuplicateLabelsFromList(UsedTerms); |
| fputs("\nFormulae used in the proof :", stdout); |
| for (Scan = UsedTerms; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| if (!(strncmp((char*) list_Car(Scan), "_SORT_", 6) == 0)) |
| printf(" %s", (char*) list_Car(Scan)); |
| putchar('\n'); |
| list_Delete(UsedTerms); |
| } |
| } |
| } |
| |
| /* Delete mapping for the clause copies of the labelclauses */ |
| for (Scan = LabelClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| hsh_DelItem(ClauseToTermLabellist, list_Car(Scan)); |
| |
| list_Delete(ProblemClauses); |
| |
| fflush(stdout); |
| |
| /* Keep definitions */ |
| deflist = prfs_Definitions(Search); |
| prfs_SetDefinitions(Search, list_Nil()); |
| prfs_Clean(Search); |
| prfs_SetDefinitions(Search, deflist); |
| |
| symbol_TransferPrecedence(InputPrecedence, Precedence); |
| if (flag_GetFlagValue(Flags, flag_PPROBLEM)) |
| fputs("\n--------------------------SPASS-STOP------------------------------", stdout); |
| } while (flag_GetFlagValue(Flags, flag_INTERACTIVE) && |
| (flag_GetFlagValue(Flags, flag_TIMELIMIT) != 0)); |
| |
| for (Scan = InputClauses; !list_Empty(Scan); Scan=list_Cdr(Scan)) |
| clause_OrientAndReInit(list_Car(Scan), Flags, Precedence); |
| |
| /* Cleanup Flotter data structures */ |
| if (flag_GetFlagValue(Flags, flag_INTERACTIVE)) { |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF)) |
| list_Delete(Symblist); |
| else |
| symbol_DeleteSymbolList(Symblist); |
| /* symbol_ResetSkolemIndex(); */ |
| if (FlotterSearch != NULL) |
| prfs_Delete(FlotterSearch); |
| } |
| if (flag_GetFlagValue(Flags, flag_PFLAGS)) { |
| putchar('\n'); |
| flag_Print(Flags); |
| } |
| if (flag_GetFlagValue(Flags, flag_DOCPROOF)) { |
| hsh_Delete(TermLabelToClauselist); |
| hsh_Delete(ClauseToTermLabellist); |
| } |
| for (Scan = Labellist; !list_Empty(Scan); Scan = list_Cdr(Scan)) |
| string_StringFree(list_Car(Scan)); |
| list_Delete(Labellist); |
| list_Delete(Sortlabellist); |
| list_Delete(UserPrecedence); |
| |
| cnf_Free(Flags); |
| |
| prfs_Delete(Search); |
| clause_DeleteClauseList(InputClauses); |
| flag_DeleteStore(InputFlags); |
| symbol_DeletePrecedence(InputPrecedence); |
| |
| cc_Free(); |
| ana_Free(); |
| sort_Free(); |
| unify_Free(); |
| cont_Free(); |
| fol_Free(); |
| symbol_FreeAllSymbols(); |
| dfg_Free(); |
| opts_Free(); |
| #ifdef CHECK |
| memory_Print(); |
| memory_PrintLeaks(); |
| #endif |
| putchar('\n'); |
| return 0; |
| } |
