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.
26
This package handles ordinary <GL>unification</GL> and <GL>matching</GL>
28
The methods are probably different from what you learned in your
29
logic course, so pay close attention.
31
In situations where you consider instantiating the variables of a term
32
t, you will have an associated Context c. The Context
33
keeps track of the terms that are substituted for the variables---
34
think of it as a substitution table indexed by the variable number.
36
Contexts allow you to separate variables of two terms without
37
creating a renamed copy of one of the terms. Say we have
38
two terms with different Contexts: (t1,c1) and (t2,c2).
39
If t1 and t2 share a variable, say v3, occurrences in
40
t1 are a different variable from occurrences in t2, because
41
the contexts are different.
42
Think of the those variables as (v3,c1) and (v3,c2).
43
In fact, when an instantiation is recorded in a Context,
44
the variable in question is set to a pair, say (t4,c4) rather
45
than just t4, because we have to know how to interpret the
48
There are situations where the terms being unified really do
49
share variables, for example when factoring the literals of
50
a clause; in those cases, you simply use the same context
53
When you call unify(), match(), or any other routine that
54
tries to make terms identical by instantiation, the terms you
55
give are not changed---all of the action happens in their contexts
56
(and in the trail, see below).
57
So you do not have to copy terms before calling the routine.
59
When a unify or match routine succeeds, the Contexts are updated
60
to reflect the common instance of the terms. Also, a Trail is
61
returned. A Trail is a linked list of (variable,context)
62
pairs telling exactly which variables were instantiated during
63
the operation. Its purpose is to quickly restore the Contexts to
64
their previous states.
66
You must explicitly allocate and free Contexts.
67
To save time, we don't initialize the arrays each
68
time a Context is re-allocated, and we don't check that Contexts
69
are clear when they are freed. Therefore, <I>you must make
70
sure that a Context is clear before freeing it</I>.
71
See undo_subst(). Also, if you forget to clear the Context with
72
undo_subst(), you will have a memory leak, because the Trail will be
74
(If you suspect that you have a bug which causes a non-empty
75
context to be freed, you can enable a run-time check in free_context()
76
and recompile unify.c.)
78
When you wish to find out what a context does to a term t, you can
79
call apply(), which builds a new copy of the term with all of
80
the instantiations of the context applied to the term t.
81
But I wrote above that (v3,c1) is a different variable
82
from (v3,c2)---what does apply do with uninstantiated variables?
83
Each context has a unique multiplier (a small natural number);
84
When apply() gets to an uninstantiated variable v, it returns
85
a variable with index (multiplier*MAX_VARS)+VARNUM(v).
86
Of course, this can give you VARNUMs > MAX_VARS, so you may
87
have to rename variables of the result before calling a unification
88
routine on the result.
90
Unification and matching can be used incrementally. For example,
91
you can all unify() with a context which has entries from a
92
previous call to unify(). Hyperresolution can be implemented by
93
backtracking through the negative literals of a nucleus
94
and the satellites that unify with a given literal of the nucleus,
95
constructing and undoing partial substitutions along the way.
96
Another example is subsumption.
97
Checking whether one clause subsumes another can be done by
98
incremental matching, backtracking through the literals of the
99
potential subsumer, trying to map them to the literals of the
102
Associative-commutative unification and matching, and commutative
103
unification and matching, use different unification code, because they
104
have to deal with multiple unifiers for a pair of terms. (These other
105
kinds of unification and matching may use the Context data
109
/* Public definitions */
111
/* Dereference a variable. */
113
#define DEREFERENCE(t, c) { int i; \
114
while (c!=NULL && VARIABLE(t) && c->terms[i=VARNUM(t)]) \
115
{ t = c->terms[i]; c = c->contexts[i]; } }
117
/* A Context records a substitution of terms for variables. */
119
typedef struct context * Context;
122
Term terms[MAX_VARS]; /* terms substituted for variables */
123
Context contexts[MAX_VARS]; /* Contexts corresponding to terms */
124
int multiplier; /* for getting separate vars in apply */
125
Term partial_term; /* for AC matching */
128
typedef struct trail * Trail;
130
/* The following type is for backtrack unification and matching. */
132
typedef enum { NO_ALT = 0,
137
/* End of public definitions */
139
/* Public function prototypes from unify.c */
141
Context get_context(void);
143
void free_context(Context p);
145
void fprint_unify_mem(FILE *fp, BOOL heading);
149
BOOL unify(Term t1, Context c1,
150
Term t2, Context c2, Trail *trp);
152
BOOL variant(Term t1, Context c1,
153
Term t2, Trail *trp);
155
BOOL occur_check(int vn, Context vc, Term t, Context c);
157
BOOL match(Term t1, Context c1, Term t2, Trail *trp);
159
Term apply(Term t, Context c);
161
Term apply_substitute(Term t, Term beta, Context c_from,
162
Term into_term, Context c_into);
164
Term apply_substitute2(Term t, Term beta, Context c_from,
165
Ilist into_pos, Context c_into);
167
Term apply_demod(Term t, Context c, int flag);
169
void undo_subst(Trail tr);
171
void undo_subst_2(Trail tr, Trail sub_tr);
173
void fprint_context(FILE *fp, Context c);
175
void p_context(Context c);
177
void fprint_trail(FILE *fp, Trail t);
179
void p_trail(Trail t);
181
BOOL match_weight(Term t1, Context c1, Term t2, Trail *trp, int var_sn);
183
Ilist vars_in_trail(Trail tr);
185
Plist context_to_pairs(Ilist varnums, Context c);
187
BOOL empty_substitution(Context s);
189
BOOL variable_substitution(Context s);
191
BOOL subst_changes_term(Term t, Context c);
193
#endif /* conditional compilation of whole file */
added
removed
ladr/unify.h.bak
