-
Notifications
You must be signed in to change notification settings - Fork 2
/
congclosure.maude
310 lines (270 loc) · 14.7 KB
/
congclosure.maude
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
fmod UNSORTIFY-FOFORM is
pr UNSORTIFY .
pr FOFORM .
var F1 F2 : QFForm .
var T T' : Term .
var QPS : QidPairSet .
var M : Module .
--- lift unsorted/sorted conversions to modules
op unsortify : Module QFForm? -> QFForm? .
eq unsortify(M,mtForm) = mtForm .
eq unsortify(M,F1 /\ F2) = unsortify(M,F1) /\ unsortify(M,F2) .
eq unsortify(M,F1 \/ F2) = unsortify(M,F1) \/ unsortify(M,F2) .
eq unsortify(M,~ F1) = ~ unsortify(M,F1) .
eq unsortify(M,T ?= T') = unsortify(M,T) ?= unsortify(M,T') .
eq unsortify(M,T != T') = unsortify(M,T) != unsortify(M,T') .
endfm
--- this module provides functions to check that a module is usuable for
--- congruence closure; essentially, we mean no adhoc-overloading
--- (except for constants, since this is an easy to handle case)
--- and all subsorted-overloaded families of operators are labelled
--- with the same unique number (rep. term order)
fmod CONG-CLOSURE-SAFETY is
pr OPDECL-EXTRA . --- provides metadata() function
pr OP-FAMILY . --- provides getOpFamilies() and OpFamilyMap datastructure
pr CONVERSION . --- provides rat() function
pr STRING-LIST . --- provides split function for strings
pr MAYBE-QID .
pr QID-JOIN .
pr SET{Nat} .
var O O' : OpDecl . var OS : OpDeclSet . var Q QI : Qid . var QIS : QidSet .
var TYL : TypeList . var OFM OFM' : OpFamilyMap . var U : Module . var MD NUM ID FVP REST : String .
var N M : Nat . var NS : Set{Nat} .
sort CCMetadata .
op cc : Nat -> CCMetadata [ctor] .
op cc : Nat Qid -> CCMetadata [ctor] .
--- OUT: set of id elements from this module
--- PRE: [1] Module should have a total ordering of its operators by the metadata attribute
--- [2] There should be no ad-hoc overloading of a symbol name with the same rank (# of args)
--- except in the case of constants, which we handle
op ccModData : Module ~> QidSet [memo] .
eq ccModData(U) = ccOpFamDataInit(U,getOpFamilies(U,false),nil) .
--- Implementation of ccModData
-------------------------------
--- NB: this module gathers operators into families based on arity except for constants
--- which are gathered based on coarity
op ccOpFamDataInit : Module OpFamily OpFamily ~> QidSet .
eq ccOpFamDataInit(U,((Q,nil) |-> OS) OFM,OFM') = ccOpFamDataInit(U,OFM,getOpFamilies(U,true,OS) OFM') .
eq ccOpFamDataInit(U, OFM,OFM') = if adhoc-overloaded(OFM,false,none) == none
then ccOpFamData(U,OFM OFM',empty,none)
else errQid('Adhoc-overloaded 'syms: tolist(adhoc-overloaded(OFM,false,none)))
fi [owise] .
op ccOpFamData : Module OpFamily Set{Nat} QidSet ~> QidSet .
eq ccOpFamData(U,((Q,TYL) |-> OS) OFM,NS,QIS) = ccOpFamData*(U,OFM,Q,ccDeclSetData(U,OS),NS,QIS) .
eq ccOpFamData(U,nil,NS,QIS) = QIS .
--- NB: NS records all observed numbers in the operator ordering for totality checking
--- QIS records all observed unit elements based on values embedded in metadata
op ccOpFamData* : Module OpFamily Qid CCMetadata Set{Nat} QidSet ~> QidSet .
eq ccOpFamData*(U,OFM,Q,cc(N), NS,QIS) =
if N in NS
then errQid('Operator 'id qid(string(N,10)) 'occurred 'in 'multiple 'operator 'families)
else ccOpFamData(U,OFM,(NS,N),QIS)
fi .
eq ccOpFamData*(U,OFM,Q,cc(N,QI),NS,QIS) =
if N in NS
then errQid('Operator 'id qid(string(N,10)) 'occurred 'in 'multiple 'operator 'families)
else ccOpFamData(U,OFM,(NS,N),QIS ; QI)
fi .
eq ccOpFamData*(U,OFM,Q,CC:[CCMetadata],NS,QIS) = errQid('Operator 'family Q 'metadata 'could 'not 'be 'parsed) .
--- OUT: either cc(NUM) or cc(NUM,ID) where NUM is the position of this operator family
--- the total order and ID is the unit associated with this operator, if it exists
--- PRE: [1] each OpDecl in OpDeclset should have the same metadata value
--- [2] the metadata should have the format "<num>" or "<num> <id>"
op ccDeclSetData : Module OpDeclSet ~> CCMetadata .
ceq ccDeclSetData(U,O O' OS) = ccDeclSetData(U,O OS) if metadata(O) == metadata(O') .
eq ccDeclSetData(U,O) = ccParseDeclData(U,metadata(O)) .
op ccParseDeclData : Module String ~> CCMetadata .
ceq ccParseDeclData(U,MD) = cc(rat(MD, 10)) if rat(MD,10) :: Nat .
ceq ccParseDeclData(U,MD) = cc(rat(NUM,10)) if NUM FVP := split(MD," ") /\ rat(NUM,10) :: Nat .
ceq ccParseDeclData(U,MD) = cc(rat(NUM,10),qid(ID)) if NUM "ID" ID := split(MD," ") /\ rat(NUM,10) :: Nat /\ wellFormed(U,qid(ID)) .
ceq ccParseDeclData(U,MD) = cc(rat(NUM,10),qid(ID)) if NUM FVP "ID" ID := split(MD," ") /\ rat(NUM,10) :: Nat /\ wellFormed(U,qid(ID)) .
op ccMaxId : Module ~> Nat .
eq ccMaxId(U) = ccMaxId(U,0,getOps(U)) .
op ccMaxId : Module Nat OpDeclSet ~> Nat .
eq ccMaxId(U,N,O OS) = ccMaxId(U,N,OS,ccParseDeclData(U,metadata(O))) .
eq ccMaxId(U,N,none) = N .
op ccMaxId : Module Nat OpDeclSet CCMetadata ~> Nat .
eq ccMaxId(U,N,OS,cc(M)) = ccMaxId(U,max(N,M),OS) .
eq ccMaxId(U,N,OS,cc(M,QI)) = ccMaxId(U,max(N,M),OS) .
endfm
--- As it turns out, we can use this struct for two related but different tasks
--- 1. For the module enrichment, where we do two things:
--- a. add given variables into the module as constants and
--- return a corresponding var-to-const substitution (components 1+2)
--- b. extract the id equations out of the module (component 3)
--- 2. For congruence closure, return:
--- a. identical to above
--- b. the identity equations after reduction by congruence closure +
--- the generated equations resulting from congruence closure
fmod CONG-CLOSURE-RESULT is
pr META-LEVEL .
sort CCResult .
op ((_,_,_)) : Module Substitution EquationSet -> CCResult [ctor] .
op errCCResult : QidList ~> CCResult [ctor] .
endfm
fmod CONG-CLOSURE-ENRICHMENT is
pr UNIT-FM .
pr VARIABLES-TO-CONSTANTS .
pr CONG-CLOSURE-RESULT .
pr STRING-PAIR .
var T T' : Term . var VS : QidSet .
var TY : Type . var TYL : TypeList .
var U : Module . var OS OS' : OpDeclSet .
var AS : AttrSet . var V : Variable .
var E : Equation . var ES : EquationSet .
var N M : Nat . var STR STR' : String .
var I P : Qid . var S : Substitution .
--- OUT: Module that has been enriched with constant bindings for each variable in the variable set
--- plus a substitution that maps each variable into the constant it was transformed into
--- Needed to perform congruence closure plus has had all identity equations extracted that
--- were tagged by the removeIds() operator
--- PRE: [1] Module should have a total order on all of its operators that lifts into an AC-RPO
--- [2] This ordering should be compatible with the rewrite relation defined by the equational theory of Module
--- [3] The identity elements for any operators should be minimal in the ordering
--- [4] The Nat argument should be equal to the number of identity elements in the order
op enrichModuleForCongClosure : Module Nat VariableSet -> CCResult .
eq enrichModuleForCongClosure(U,N,VS) =
extractTaggedIdEqs(varsToConstsWithMetadata#(shiftMetadata(U,N,| VS |),N,VS)) .
--- OUT: convert module into a new one with [a] variables added as fresh constants [b] metadata order updated appropriately
op varsToConstsWithMetadata# : Module Nat QidSet -> ModuleSubstPair .
eq varsToConstsWithMetadata#(U,N,VS) = varsToConstsWithMetadata#(U,N,VS,qid(opPrefix(U)),none,none) .
op varsToConstsWithMetadata# : Module Nat QidSet Qid OpDeclSet Substitution -> ModuleSubstPair .
eq varsToConstsWithMetadata#(U,N,V ; VS,P,OS,S) = varsToConstsWithMetadata#(U,s(N),VS,P,OS op join(P getName(V)) : nil -> getType(V) [metadata(string(s(N),10))].,S ; V <- join(P getName(V) '. getType(V))) .
eq varsToConstsWithMetadata#(U,N,none,P,OS,S) = (addOps(OS,U),S) .
--- NB: this function is called with the same first two arguments every time while working in one module;
--- only the third argument varies depending on how many variables are in a formula. Typically, the
--- number will not vary too much when proving things and it will repeat often --- a perfect memo candidate.
op shiftMetadata : Module Nat Nat -> Module [memo] .
eq shiftMetadata(U,N,M) = setOps(U,shiftMetadata(N,M,getOps(U),none)) .
op shiftMetadata : Nat Nat OpDeclSet OpDeclSet -> OpDeclSet .
eq shiftMetadata(N,M,op I : TYL -> TY [AS metadata(STR)] . OS,OS') = shiftMetadata(N,M,OS,OS' op I : TYL -> TY [AS metadata(shiftMetadata(STR,N,M))] .) .
eq shiftMetadata(N,M,none,OS') = OS' .
op shiftMetadata : String Nat Nat ~> String .
eq shiftMetadata(STR,N,M) = if rat(STR,10) :: Nat then if rat(STR,10) > N then string(rat(STR,10) + M,10) else STR fi else shiftMetadata2(split1(STR," "),N,M) fi .
op shiftMetadata2 : StringPair Nat Nat ~> String .
ceq shiftMetadata2((STR,STR'),N,M) = shiftMetadata(STR,N,M) if rat(STR,10) :: Nat .
--- OUT: extract equations from EquationSet tagged by removeIds() function
op extractTaggedIdEqs : ModuleSubstPair -> CCResult .
eq extractTaggedIdEqs((U,S)) = extractTaggedIdEqs(getTaggedIdEqs(getEqs(U)),(U,S)) .
op extractTaggedIdEqs : EquationSet ModuleSubstPair -> CCResult .
eq extractTaggedIdEqs(ES,(U,S)) = (setEqs(U,getEqs(U) - ES),S,ES) .
op getTaggedIdEqs : Module -> EquationSet .
eq getTaggedIdEqs(U) = getTaggedIdEqs(getEqs(U)) .
op getTaggedIdEqs : EquationSet -> EquationSet .
eq getTaggedIdEqs(E ES) = if substr(metadata(E),0,3) == "id" then E else none fi getTaggedIdEqs(ES) .
eq getTaggedIdEqs(none) = none .
endfm
--- In this module, we put together all of the pieces for congruence closure
--- on a conjunction of positive equality atoms.
--- Here is a list of all of the steps we take when performing this process:
--- Module Pre-processing:
--- [1] extract and remove identity equations from the module
---- [2] check module metadata and extract unit elements.
--- [3] convert variables in conjunction into constants in the module,
--- being sure to shift the metadata in the module appropriately +
--- save var-to-const substitution.
--- [4] convert module+constants into many-sorted form + compute inversion table
--- [5] apply equationset functor to many-sorted module+constants
--- Conjunction Preprocessing:
--- [a] Convert all variables in conjunction into constants (using substitution from step 3)
--- [b] Convert conjunction into many-sorted form (using module in step 3)
--- [c] Convert to term by equationset functor (using module in step 4)
--- Next, do congruence closure with module and term.
--- Take congruence closure generated equations and convert back to
--- order-sorted form (using inversion table from step 4)
--- Return to the user the following:
--- [i] module from step 3 (no id eqs + variables as constants)
--- [ii] order-sorted equations generated by congruence closure
--- [iii] the var-to-const substitution from step 3
fmod CONG-CLOSURE-LIB is
pr UNIT-FM .
pr STMT-EXTRA .
pr DEBUG-PRINT .
pr FOFORM-SUBSTITUTION .
pr FOFORM-OPERATIONS .
pr UNSORTIFY-FOFORM .
pr QIDPAIRSET-TERMAPPLY .
pr EQUALITY-FUNCTOR . --- pruneBool()
pr CTOR-REFINE .
pr CONG-CLOSURE-SAFETY .
pr CONG-CLOSURE-ENRICHMENT .
pr CONG-CLOSURE *
(op `[_`,_`] to mr,
op `{_`} to res) .
pr REMOVE-IDS .
var U UCC CU : Module .
var Q : Qid .
var Y : Sort .
var IDS : QidSet .
var ID-ES ES ES' : EquationSet .
var MS-PCT T T' : Term .
var M M' : Marking .
var N : Nat .
var PC : PosEqConj .
var PC? : PosEqConj? .
var S : Substitution .
var U2OMap : QidPairSet .
var MRL : List{MRule<} .
var B : Bool .
var V : Variable .
var C : Constant .
var QPS : QidPairSet .
var OS : OpDeclSet .
var AS : AttrSet .
var CSK : [CCState] .
var TA : TruthAtom .
op congClosure : Module Bool PosEqConj? -> CCResult .
eq congClosure(U,B,mtForm) = (U,none,none) .
eq congClosure(U,B,TA) = (U,none,none) .
eq congClosure(U,B,PC) =
if ccModData(U) :: QidSet and-then wellFormed(U,PC)
then congClosure1(U,B,ccModData(U),PC)
else errCCResult(qidErrMsg(ccModData(U)))
fi .
op congClosure1 : Module Bool QidSet PosEqConj -> CCResult .
eq congClosure1(U,B,IDS,PC) =
congClosure2(enrichModuleForCongClosure(U,| IDS |,vars(PC)),B,IDS,PC) .
--- NOTE: two unsortify inverse maps below never conflict because:
--- one maps only constants and the other only variables
op congClosure2 : CCResult Bool QidSet PosEqConj -> CCResult .
eq congClosure2((UCC,S,ID-ES),B,IDS,PC) =
congClosure3(UCC,
S,
unsortify-1(pruneBool(getSig(UCC))) | unsortify-1(pruneBool(getSig(UCC)),vars(ID-ES)),
init-acu-cc(
unsortify(pruneBool(getSig(UCC))),
markVarConstsAsCtors(getVarConsts(S),pruneBool(getSig(UCC))),
unsortify-1(pruneBool(getSig(UCC))) | unsortify-1(pruneBool(getSig(UCC)),vars(ID-ES)),
S,
B,
unsortify(pruneBool(getSig(UCC)),ID-ES),
unsortify(pruneBool(getSig(UCC)),IDS),
toMRules(unsortify(pruneBool(getSig(UCC))),ctor-refine(markVarConstsAsCtors(getVarConsts(S),pruneBool(getSig(UCC)))),
unsortify-1(pruneBool(getSig(UCC))) | unsortify-1(pruneBool(getSig(UCC)),vars(ID-ES)),S,
B,unsortify(pruneBool(getSig(UCC)),PC << S)))) .
op congClosure3 : Module Substitution QidPairSet CCState -> CCResult .
eq congClosure3(UCC,S,U2OMap,[ES,N,MRL]) =
if MRL == nil
then (UCC,S,congClosureDebugPrint(false,apply(U2OMap,true,ES)))
else errCCResult('Congruence 'closure 'did 'not 'terminate)
fi .
eq congClosure3(UCC,S,U2OMap,CSK) = errCCResult('Congruence 'closure 'failed) [owise] .
op toMRules : Module Module QidPairSet Substitution Bool PosEqConj -> List{MRule<} .
eq toMRules(U,CU,QPS,S,B,T ?= T' /\ PC?) = make-rule(U,CU,QPS,S,B,T,T') toMRules(U,CU,QPS,S,B,PC?) .
eq toMRules(U,CU,QPS,S,B,mtForm) = nil .
op congClosureDebugPrint : Bool EquationSet -> EquationSet .
eq congClosureDebugPrint(false,ES) = ES .
eq congClosureDebugPrint(true, ES) = congClosureDebugPrint2(ES - getTaggedIdEqs(ES),ES) .
op congClosureDebugPrint2 : EquationSet EquationSet -> EquationSet .
eq congClosureDebugPrint2(ES',ES) = ES [print "CCRESULT: " ES'] .
op markVarConstsAsCtors : QidPairSet Module -> Module .
eq markVarConstsAsCtors(QPS,U) = markVarConstsAsCtors(QPS,getOps(U),U) .
op markVarConstsAsCtors : QidPairSet OpDeclSet Module -> Module .
eq markVarConstsAsCtors(qp(Q,Y) | QPS,op Q : nil -> Y [AS]. OS, U) =
markVarConstsAsCtors(QPS,op Q : nil -> Y [ctor AS]. OS, U) .
eq markVarConstsAsCtors(none, OS, U) = setOps(U,OS) .
eq markVarConstsAsCtors(qp(Q,Y) | QPS,OS,U) = noModule [owise] .
op getVarConsts : Substitution -> QidPairSet .
eq getVarConsts(V <- C ; S) = qp(getName(C),getType(C)) | getVarConsts(S) .
eq getVarConsts(none) = none .
endfm