analysis/idp_server/findClasses.idp

   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
  31   stdoptions.symmetrybreaking="static"
  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