File: ccl_relevance.h

package info (click to toggle)
eprover 2.6%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 21,288 kB
  • sloc: ansic: 331,111; csh: 12,026; python: 10,178; awk: 5,825; makefile: 461; sh: 389
file content (86 lines) | stat: -rw-r--r-- 2,431 bytes parent folder | download | duplicates (2)
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                                  */
/*---------------------------------------------------------------------*/