Commit | Line | Data |
51650966 |
1 | vocabulary V3 { |
2 | extern vocabulary V |
3 | type Class |
4 | ClassOf(Manuscript): Class |
5 | Copy: Class |
6 | Revert: Class |
7 | Source: Class |
8 | IndirectAncestor(Manuscript,Manuscript) |
9 | type N isa nat |
10 | NbOfSources : N |
11 | NbOfReverts : N |
12 | } |
13 | |
14 | theory T3 : V3 { |
15 | ! x : (ClassOf(x)=Copy) <=> ? y : CopiedBy(y,x) & VariantOf(y) = VariantOf(x). |
16 | ! x : (ClassOf(x)=Revert) <=> (ClassOf(x)~=Copy) & ? y : IndirectAncestor(y,x) & VariantOf(y) = VariantOf(x). |
17 | |
18 | { !x y: IndirectAncestor(x,y) <- ?z: CopiedBy(x,z) & IndirectAncestor(z,y). |
19 | !x y: IndirectAncestor(x,y) <- ?z: CopiedBy(x,z) & CopiedBy(z,y). } |
20 | |
21 | NbOfSources = #{x: ClassOf(x)=Source}. |
22 | NbOfReverts = #{x: ClassOf(x)=Revert}. |
23 | } |
24 | |
25 | term TotalCost : V3 { |
26 | 3 * NbOfSources + NbOfReverts |
27 | } |
28 | |
29 | procedure minSourcesAndReverts(sample) { |
30 | stdoptions.groundwithbounds=false |
c92f1684 |
31 | stdoptions.symmetrybreaking="static" |
51650966 |
32 | stdoptions.cpsupport=true |
33 | addClasses(sample) |
34 | return minimize(T3, sample, TotalCost)[1] |
35 | } |
36 | |
37 | structure SClass : V3 { |
38 | Class = { copy; revert; source } |
39 | Copy = copy |
40 | Revert = revert |
41 | Source = source |
42 | } |
43 | |
44 | procedure addClasses(struct) { |
45 | idpintern.setvocabulary(struct,V3) |
46 | struct[V3::Class.type] = SClass[V3::Class.type] |
47 | struct[V3::Copy] = SClass[V3::Copy] |
48 | struct[V3::Revert] = SClass[V3::Revert] |
49 | struct[V3::Source] = SClass[V3::Source] |
50 | struct[V3::N.type] = range(0,#totable(struct[V::Manuscript.type])) |
51 | } |
52 | |
53 | procedure findClasses(samples) { |
54 | local result = {} |
55 | for _,sample in ipairs(samples) do |
56 | local model = minSourcesAndReverts(sample) |
57 | if model then |
58 | table.insert(result,{ getGrouping(model), getClasses(model) }) |
59 | else |
60 | table.insert(result,{ getGrouping(sample), {} }) |
61 | end |
62 | end |
63 | return result |
64 | } |
65 | |
66 | procedure getClasses(model) { |
67 | local classes = {} |
68 | for tuple in tuples(model[V3::ClassOf].graph.ct) do |
69 | local manuscript, class = tuple[1], tuple[2] |
70 | if classes[class] == nil then |
71 | classes[class] = {manuscript} |
72 | else |
73 | table.insert(classes[class],manuscript) |
74 | end |
75 | end |
76 | return classes |
77 | } |
78 | |