14
15
16:- module(are_equivalent, [
17 check_equivalence/2,
18 are_equivalent/2,
19 are_equivalent/3
20 ]).
48:- use_module(drs_to_ascii). 49:- use_module(is_wellformed). 50:- use_module(drs_ops). 51
52:- dynamic conds_unify/2.
60check_equivalence(Drs1, Drs2) :-
61 are_equivalent(Drs1, Drs2),
62 write('OK: the DRSs are equivalent.'), nl,
63 !.
64
65check_equivalence(Drs1, Drs2) :-
66 write('ERROR: the DRSs are NOT equivalent.'), nl,
67 display_drs(Drs1),
68 display_drs(Drs2).
89are_equivalent(Drs1, Drs2) :-
90 are_equivalent(Drs1, Drs2, []).
91
92are_equivalent(Drs1, Drs2, []) :-
93 are_equivalent(Drs1, Drs2, [ignore_sid(false)]).
94
95are_equivalent(Drs1, Drs2, [ignore_sid(false)]) :-
96 retractall(conds_unify(_, _)),
97 assert(conds_unify(C-Id, C-Id)),
98 assert(conds_unify(C-SId/_, C-SId)),
99 assert(conds_unify(C-SId, C-SId/_)),
100 !,
101 are_equivalent_x(Drs1, Drs2).
102
103are_equivalent(Drs1, Drs2, [ignore_sid(true)]) :-
104 retractall(conds_unify(_, _)),
105 assert(conds_unify(C-_, C-_)),
106 !,
107 are_equivalent_x(Drs1, Drs2).
108
109are_equivalent_x(Drs1, Drs2) :-
110 is_wellformed(Drs1),
111 is_wellformed(Drs2),
112 is_subdrs_of(Drs1, Drs2),
113 is_subdrs_of(Drs2, Drs1).
127is_subdrs_of(drs(_, Conds1), drs(_, Conds2)) :-
128 copy_term(Conds1, Conds1Copy),
129 copy_term(Conds2, Conds2Copy),
130 numbervars(Conds2Copy, 0, _),
131 is_subdrs_of_x(drs(_, Conds1Copy), drs(_, Conds2Copy)).
132
133is_subdrs_of_x(drs(_, Conds1), drs(_, Conds2)) :-
134 is_subcl_of(Conds1, Conds2).
145is_subcl_of([], _).
146
147is_subcl_of([Condition | ConditionList1], ConditionList2) :-
148 member_of_conds(Condition, ConditionList2),
149 is_subcl_of(ConditionList1, ConditionList2).
160member_of_conds([H1|T1], [[H2|T2] | _]) :-
161 is_subdrs_of_x(drs([],[H1|T1]), drs([],[H2|T2])).
162
163member_of_conds(Drs1, [Drs2 | _]) :-
164 Drs1 =.. [Op, SubDrs1],
165 Drs2 =.. [Op, SubDrs2],
166 unary_drs_operator(Op),
167 is_subdrs_of_x(SubDrs1, SubDrs2).
168
172member_of_conds(v(SubDrs1a, SubDrs1b), [v(SubDrs2a, SubDrs2b) | _]) :-
173 is_subdrs_of_x(SubDrs1a, SubDrs2b), is_subdrs_of_x(SubDrs1b, SubDrs2a).
174
175member_of_conds(Drs1, [Drs2 | _]) :-
176 Drs1 =.. [Op, SubDrs1a, SubDrs1b],
177 Drs2 =.. [Op, SubDrs2a, SubDrs2b],
178 binary_drs_operator(Op),
179 is_subdrs_of_x(SubDrs1a, SubDrs2a),
180 is_subdrs_of_x(SubDrs1b, SubDrs2b).
181
182member_of_conds(Label:Drs1, [Label:Drs2 | _]) :-
183 is_subdrs_of_x(Drs1, Drs2).
184
185member_of_conds(Cond1, [Cond2 | _]) :-
186 conds_unify(Cond1, Cond2).
187
188member_of_conds(Cond, [_ | CondsTail]) :-
189 member_of_conds(Cond, CondsTail)
Equivalence checking of two Attempto DRSs
BUG: Think if this code is correct and complete.
OBSOLETE COMMENT: Note that the DRACE-tester also uses the notion of equivalence defined here, but for DRACE it is sometimes too strict, e.g. DRACE NP considers reversing the arguments of `be' equivalence-preserving, to be able to perform the transformation:
But given the definition of equivalence here, they are not. Similarly:
*/