1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
|
/*-----------------------------------------------------------------------
File : ccl_relevance.h
Author: Stephan Schulz (schulz@eprover.org)
Contents
Code implementing some limited relevance analysis for function
symbols and clauses/formulas.
Copyright 2009 by the author.
This code is released under the GNU General Public Licence and
the GNU Lesser General Public License.
See the file COPYING in the main E directory for details.
Run "eprover -h" for contact information.
Changes
<1> Sun May 31 11:20:27 CEST 2009
New
-----------------------------------------------------------------------*/
#ifndef CCL_RELEVANCE
#define CCL_RELEVANCE
#include <clb_plist.h>
#include <ccl_findex.h>
#include <ccl_proofstate.h>
/*---------------------------------------------------------------------*/
/* Data type declarations */
/*---------------------------------------------------------------------*/
/* Data structure for computing the relevance of function symbols with
* respect to a set of conjectures/goals */
typedef struct relevance_cell
{
Sig_p sig;
PList_p clauses_core;
PList_p formulas_core;
PList_p clauses_rest;
PList_p formulas_rest;
FIndex_p clauses_index;
FIndex_p formulas_index;
long max_level;
PDArray_p fcode_relevance;
PStack_p new_codes;
PStack_p relevance_levels;
}RelevanceCell, *Relevance_p;
/*---------------------------------------------------------------------*/
/* Exported Functions and Variables */
/*---------------------------------------------------------------------*/
#define RelevanceCellAlloc() (RelevanceCell*)SizeMalloc(sizeof(RelevanceCell))
#define RelevanceCellFree(junk) SizeFree(junk, sizeof(RelevanceCell))
Relevance_p RelevanceAlloc(void);
void RelevanceFree(Relevance_p junk);
void ClausePListPrint(FILE* out, PList_p list);
void FormulaPListPrint(FILE* out, PList_p list);
long RelevanceDataInit(ProofState_p state, Relevance_p data);
Relevance_p RelevanceDataCompute(ProofState_p state);
long ProofStateRelevancyProcess(ProofState_p state, long level);
#endif
/*---------------------------------------------------------------------*/
/* End of File */
/*---------------------------------------------------------------------*/
|