1
/* Copyright (C) 2006, 2007 William McCune
3
This file is part of the LADR Deduction Library.
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,
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.
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.
28
A Topform can be used to store a formula or a clause.
29
The field is_formula says which it is.
32
In earlier versions of LADR, this data structure was called Clause.
33
When we decided to put non-clausal formulas in proofs, they
34
needed to have IDs, attributes, and justifications, so we elevated
35
the data structure to include non-clausal formulas and changed
36
the name to Topform (top formula).
39
In many cases, when we say "clause", we mean a list of Literals.
40
For example, most of the functions that tell the properties
41
of clauses (positive_clause, number_of_literals, etc.) take
42
a list of Literals, not a Topform.
45
If C had data structures with inheritance, this would
46
be a good place to use it.
49
/* Public definitions */
51
typedef struct topform * Topform;
55
/* for both clauses and formulas */
58
struct clist_pos *containers; /* Clists that contain the Topform */
60
struct just *justification;
62
char *compressed; /* if nonNULL, a compressed form */
63
Topform matching_hint; /* hint that matches clause, if any */
65
/* for clauses only */
67
Literals literals; /* NULL can mean the empty clause */
69
/* for formulas only */
73
int semantics; /* evaluation in interpretations */
75
/* The rest of the fields are flags. These could be bits. */
77
char is_formula; /* is this really a formula? */
78
char normal_vars; /* variables have been renumbered */
79
char used; /* used to infer a clause that was kept */
80
char official_id; /* Topform is in the ID table */
81
char initial; /* existed at the start of the search */
82
char neg_compressed; /* negative and compressed */
83
char subsumer; /* has this clause back subsumed anything? */
87
/* End of public definitions */
89
/* Public function prototypes from topform.c */
91
Topform get_topform(void);
93
void fprint_topform_mem(FILE *fp, int heading);
97
void zap_topform(Topform tf);
99
void fprint_clause(FILE *fp, Topform c);
101
void p_clause(Topform c);
103
Topform term_to_clause(Term t);
105
Topform term_to_topform(Term t, BOOL is_formula);
107
Term topform_to_term(Topform tf);
109
Term topform_to_term_without_attributes(Topform tf);
111
void clause_set_variables(Topform c, int max_vars);
113
void renumber_variables(Topform c, int max_vars);
115
void term_renumber_variables(Term t, int max_vars);
117
Plist renum_vars_map(Topform c);
119
void upward_clause_links(Topform c);
121
BOOL check_upward_clause_links(Topform c);
123
Topform copy_clause(Topform c);
125
Topform copy_clause_with_flags(Topform c);
127
Topform copy_clause_with_flag(Topform c, int flag);
129
void inherit_attributes(Topform par1, Context s1,
130
Topform par2, Context s2,
133
void gather_symbols_in_topform(Topform c, I2list *rsyms, I2list *fsyms);
135
void gather_symbols_in_topforms(Plist lst, I2list *rsyms, I2list *fsyms);
137
Ilist fsym_set_in_topforms(Plist lst);
139
Ilist rsym_set_in_topforms(Plist lst);
141
BOOL min_depth(Literals lit);
143
BOOL initial_clause(Topform c);
145
BOOL negative_clause_possibly_compressed(Topform c);
147
Term topform_properties(Topform c);
149
void append_label_attribute(Topform tf, char *s);
151
Ordertype cl_id_compare(Topform c1, Topform c2);
153
Ordertype cl_wt_id_compare(Topform c1, Topform c2);
155
#endif /* conditional compilation of whole file */
added
removed
ladr/topform.h.bak
