File: ccl_ext_index.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 (65 lines) | stat: -rw-r--r-- 1,760 bytes parent folder | download
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
/*-----------------------------------------------------------------------

File  : ccl_overlap_index.h

Author: Stephan Schulz (schulz@eprover.org)

Contents

  A simple index mapping symbols to ClauseTPos trees.
  See .c file for details on functionality.

Changes

<1> Thu Jun  3 11:30:36 CEST 2010
    New

-----------------------------------------------------------------------*/

#include <ccl_clauses.h>
#include <clb_intmap.h>

#ifndef CCL_EXT_DEC_IDX

#define CCL_EXT_DEC_IDX


/*---------------------------------------------------------------------*/
/*                    Data type declarations                           */
/*---------------------------------------------------------------------*/

typedef IntMap_p ExtIndex_p;
#define TYPE_EXT_ELIGIBLE(t) (TypeIsArrow((t)))



/*---------------------------------------------------------------------*/
/*                Exported Functions and Variables                     */
/*---------------------------------------------------------------------*/

#define ExtIdxAlloc()   IntMapAlloc()

bool TermHasExtEligSubterm(Term_p t);


void CollectExtSupFromPos(Clause_p cl, PStack_p pos_stack);
void CollectExtSupIntoPos(Clause_p cl, PStack_p pos_stack);

void ExtIndexInsertIntoClause(ExtIndex_p into_index, Clause_p cl);
void ExtIndexDeleteIntoClause(ExtIndex_p into_index, Clause_p cl);
void ExtIndexInsertFromClause(ExtIndex_p into_index, Clause_p cl);
void ExtIndexDeleteFromClause(ExtIndex_p into_index, Clause_p cl);
void ExtIndexFree(ExtIndex_p into_index);



#endif

/*---------------------------------------------------------------------*/
/*                        End of File                                  */
/*---------------------------------------------------------------------*/