← Back to branch summary

~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to ladr/flatterm.h.bak

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
ladr/flatterm.h.bak
1
 
/*  Copyright (C) 2006, 2007 William McCune
2
 
 
3
 
    This file is part of the LADR Deduction Library.
4
 
 
5
 
    The LADR Deduction Library is free software; you can redistribute it
6
 
    and/or modify it under the terms of the GNU General Public License,
7
 
    version 2.
8
 
 
9
 
    The LADR Deduction Library is distributed in the hope that it will be
10
 
    useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
    GNU General Public License for more details.
13
 
 
14
 
    You should have received a copy of the GNU General Public License
15
 
    along with the LADR Deduction Library; if not, write to the Free Software
16
 
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
17
 
*/
18
 
 
19
 
#ifndef TP_FLATTERM_H
20
 
#define TP_FLATTERM_H
21
 
 
22
 
#include "term.h"
23
 
 
24
 
/* INTRODUCTION
25
 
<P>
26
 
The Term macros VARIABLE(f), CONSTANT(f), COMPLEX(f), SYMNUM(f),
27
 
VARNUM(f), ARITY(f) are used for Flatterms as well.  The Term macro
28
 
ARG(t,i) is NOT used for Flatterms.
29
 
<P>
30
 
Traversing Flatterms.  It can be done recursively or iteratively.
31
 
When building flatterms, recursive is better, because you have to
32
 
make a Flatterm point to its end.
33
 
 
34
 
Iterative:
35
 
 
36
 
   Flatterm fi;
37
 
   for (f = fi; fi != f->end->next; fi = fi->next)
38
 
      ...
39
 
 
40
 
Recursive:
41
 
 
42
 
   int i;
43
 
   Flatterm fi = f->next;
44
 
   for (i = 0; i < ARITY(f); i++) {
45
 
     ...
46
 
     fi = fi->end->next;
47
 
   }
48
 
   
49
 
*/
50
 
 
51
 
/* Public definitions */
52
 
 
53
 
typedef struct flatterm * Flatterm;
54
 
 
55
 
struct flatterm {
56
 
  short         private_symbol; /* const/func/pred/var symbol ID */
57
 
  unsigned char arity;          /* number of auguments */
58
 
  Flatterm prev, next, end;
59
 
 
60
 
  /* The rest of the fields are for index retrieval and demodulation. */
61
 
  
62
 
  int size;                      /* symbol count */
63
 
  struct discrim *alternative;   /* subtree to try next */
64
 
  int varnum_bound_to;           /* -1 for not bound */
65
 
  BOOL reduced_flag;             /* fully demodulated */
66
 
};
67
 
 
68
 
/* End of public definitions */
69
 
 
70
 
/* Public function prototypes from flatterm.c */
71
 
 
72
 
Flatterm get_flatterm(void);
73
 
 
74
 
void fprint_flatterm_mem(FILE *fp, BOOL heading);
75
 
 
76
 
void p_flatterm_mem();
77
 
 
78
 
BOOL flatterm_ident(Flatterm a, Flatterm b);
79
 
 
80
 
void zap_flatterm(Flatterm f);
81
 
 
82
 
Flatterm term_to_flatterm(Term t);
83
 
 
84
 
Term flatterm_to_term(Flatterm f);
85
 
 
86
 
Flatterm copy_flatterm(Flatterm f);
87
 
 
88
 
void print_flatterm(Flatterm f);
89
 
 
90
 
int flatterm_symbol_count(Flatterm f);
91
 
 
92
 
void p_flatterm(Flatterm f);
93
 
 
94
 
BOOL flat_occurs_in(Flatterm t1, Flatterm t2);
95
 
 
96
 
I2list flat_multiset_vars(Flatterm f);
97
 
 
98
 
BOOL flat_variables_multisubset(Flatterm a, Flatterm b);
99
 
 
100
 
int flatterm_count_without_vars(Flatterm f);
101
 
 
102
 
#endif  /* conditional compilation of whole file */