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 */
/*---------------------------------------------------------------------*/
|