app/willard/test2

   1 Input:
   2 {[x,y]: x in S, y in T, z in U | (((exists y in U.((z = x) and(x = y))) and (exists z in U.(z = 1))) or(not (exists i in U.(x >= y))))}
   3 {[x,y]: x in S, y in T, z in U | (((exists y in U.((z = x) and(x = y))) and (exists z in U.(z = 1))) or(not (exists i in U.(x >= y))))}
   4
   5 [Renaming phase]
   6
   7 {[x,y]: x in S, y in T, z in U | (((exists y_1 in U.((z = x) and(x = y_1))) and (exists z_2 in U.(z_2 = 1))) or(not (exists i in U.(x >= y))))}
   8
   9 [DNF construction and simplification phase]
  10
  11 {[x,y]: x in S, y in T, z in U | (((z = x) and((exists y_1 in U.(x = y_1)) and (exists z_2 in U.(z_2 = 1)))) or(not (exists i in U.(x >= y))))}
  12
  13 [Constructing the query graph]
  14
  15 [Query Graph]
  16    edge x -> y_1
  17    edge x -> y
  18    edge x -> z
  19 {[x,y]: x in S, y in T, z in U | (((z = x) and((exists y_1 in U.(x = y_1)) and (exists z_2 in U.(z_2 = 1)))) or(not (exists i in U.(x >= y))))}
  20
  21 [Quantifier elimination phase]
  22
  23    let
  24       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
  25       C_4={z_2: z_2 in U | (z_2 = 1)}
  26    in
  27       {[x,y]:[x,y,z] in [S,T,U] | (((z = x) and((C_3(x) > 0) and(nonempty C_4))) or((not(nonempty U)) or(x < y)))}
  28    end
  29
  30
  31 [Disjunction removal phase]
  32
  33    let
  34       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
  35       C_4={z_2: z_2 in U | (z_2 = 1)}
  36       Q_5={[x,y]:[x,y,z] in [S,T,U] | ((z = x) and((C_3(x) > 0) and(nonempty C_4)))}
  37       Q_6={[x,y]:[x,y,z] in [S,T,U] | (not(nonempty U))}
  38       Q_7={[x,y]:[x,y,z] in [S,T,U] | (x < y)}
  39    in
  40       union(Q_7,Q_6,Q_5)
  41    end
  42
  43
  44 [Conjunctive query decomposition phase]
  45
  46 [Query Graph]
  47    edge x -> y_1
  48    edge x -> y
  49    edge x -> z
  50    let
  51       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
  52       C_4={z_2: z_2 in U | (z_2 = 1)}
  53       Q_8={[x,y]:[x,y,z] in [S,T,U] | (z = x)}
  54       Q_9={[x,y]:[x,y,z] in [S,T,U] | (C_3(x) > 0)}
  55       Q_10={[x,y]:[x,y,z] in [S,T,U] | (nonempty C_4)}
  56       Q_5= join(Q_10,Q_9,Q_8)
  57       Q_6={[x,y]:[x,y,z] in [S,T,U] | (not(nonempty U))}
  58       Q_7={[x,y]:[x,y,z] in [S,T,U] | (x < y)}
  59    in
  60       union(Q_7,Q_6,Q_5)
  61    end
  62
  63
  64 [Projection recognition phase]
  65
  66    let
  67       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
  68       C_4={z_2: z_2 in U | (z_2 = 1)}
  69       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
  70       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
  71       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
  72       Q_5= join(Q_10,Q_9,Q_8)
  73       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
  74       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
  75    in
  76       union(Q_7,Q_6,Q_5)
  77    end
  78
  79
  80 [Simple find/count query decomposition phase]
  81
  82    let
  83       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
  84       C_4={z_2: z_2 in U | (z_2 = 1)}
  85       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
  86       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
  87       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
  88       Q_5= join(Q_10,Q_9,Q_8)
  89       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
  90       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
  91    in
  92       union(Q_7,Q_6,Q_5)
  93    end
  94
  95
  96 [Reiterating the transformation]
  97
  98    let
  99       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 100       C_4={z_2: z_2 in U | (z_2 = 1)}
 101       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
 102       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
 103       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
 104       Q_5= join(Q_10,Q_9,Q_8)
 105       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
 106       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
 107    in
 108       union(Q_7,Q_6,Q_5)
 109    end
 110
 111
 112 [Renaming phase]
 113
 114    let
 115       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 116       C_4={z_2: z_2 in U | (z_2 = 1)}
 117       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
 118       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
 119       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
 120       Q_5= join(Q_10,Q_9,Q_8)
 121       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
 122       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
 123    in
 124       union(Q_7,Q_6,Q_5)
 125    end
 126
 127
 128 [DNF construction and simplification phase]
 129
 130    let
 131       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 132       C_4={z_2: z_2 in U | (z_2 = 1)}
 133       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
 134       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
 135       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
 136       Q_5= join(Q_10,Q_9,Q_8)
 137       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
 138       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
 139    in
 140       union(Q_7,Q_6,Q_5)
 141    end
 142
 143
 144 [Constructing the query graph]
 145
 146 [Query Graph]
 147    edge x -> y_1
 148    edge x -> y
 149    edge x -> z
 150    let
 151       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 152       C_4={z_2: z_2 in U | (z_2 = 1)}
 153       Q_8={[x,y]:[x,y] in [S,T] |  (exists z in U.(z = x))}
 154       Q_9={[x,y]:[x,y] in [S,T] |  (exists z in U.(C_3(x) > 0))}
 155       Q_10={[x,y]:[x,y] in [S,T] |  (exists z in U.(nonempty C_4))}
 156       Q_5= join(Q_10,Q_9,Q_8)
 157       Q_6={[x,y]:[x,y] in [S,T] |  (exists z in U.(not(nonempty U)))}
 158       Q_7={[x,y]:[x,y] in [S,T] |  (exists z in U.(x < y))}
 159    in
 160       union(Q_7,Q_6,Q_5)
 161    end
 162
 163
 164 [Quantifier elimination phase]
 165
 166    let
 167       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 168       C_4={z_2: z_2 in U | (z_2 = 1)}
 169       Q_8={[x,y]:[x,y] in [S,T] | (C_11(x) > 0)}
 170       Q_9= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (C_3(x) > 0)} else {}
 171       Q_10= if((nonempty U) and(nonempty C_4)) then{[x,y]:[x,y] in [S,T]} else {}
 172       Q_5= join(Q_10,Q_9,Q_8)
 173       Q_6= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (not(nonempty U))} else {}
 174       C_11={[x,(#{[x,z]: z in U | (z = x)})]: x in S}
 175       Q_7= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (x < y)} else {}
 176    in
 177       union(Q_7,Q_6,Q_5)
 178    end
 179
 180
 181 [Disjunction removal phase]
 182
 183    let
 184       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 185       C_4={z_2: z_2 in U | (z_2 = 1)}
 186       Q_8={[x,y]:[x,y] in [S,T] | (C_11(x) > 0)}
 187       Q_9= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (C_3(x) > 0)} else {}
 188       Q_10= if((nonempty U) and(nonempty C_4)) then{[x,y]:[x,y] in [S,T]} else {}
 189       Q_5= join(Q_10,Q_9,Q_8)
 190       Q_6= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (not(nonempty U))} else {}
 191       C_11={[x,(#{[x,z]: z in U | (z = x)})]: x in S}
 192       Q_7= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (x < y)} else {}
 193    in
 194       union(Q_7,Q_6,Q_5)
 195    end
 196
 197
 198 [Conjunctive query decomposition phase]
 199
 200 [Query Graph]
 201    edge x -> y_1
 202    edge x -> y
 203    edge x -> z
 204    let
 205       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 206       C_4={z_2: z_2 in U | (z_2 = 1)}
 207       Q_8={[x,y]:[x,y] in [S,T] | (C_11(x) > 0)}
 208       Q_9= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (C_3(x) > 0)} else {}
 209       Q_10= if((nonempty U) and(nonempty C_4)) then{[x,y]:[x,y] in [S,T]} else {}
 210       Q_5= join(Q_10,Q_9,Q_8)
 211       Q_6= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (not(nonempty U))} else {}
 212       C_11={[x,(#{[x,z]: z in U | (z = x)})]: x in S}
 213       Q_7= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (x < y)} else {}
 214    in
 215       union(Q_7,Q_6,Q_5)
 216    end
 217
 218
 219 [Projection recognition phase]
 220
 221    let
 222       C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 223       C_4={z_2: z_2 in U | (z_2 = 1)}
 224       Q_8={[x,y]:[x,y] in [S,T] | (C_11(x) > 0)}
 225       Q_9= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (C_3(x) > 0)} else {}
 226       Q_10= if((nonempty U) and(nonempty C_4)) then{[x,y]:[x,y] in [S,T]} else {}
 227       Q_5= join(Q_10,Q_9,Q_8)
 228       Q_6= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (not(nonempty U))} else {}
 229       C_11={[x,(#{[x,z]: z in U | (z = x)})]: x in S}
 230       Q_7= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (x < y)} else {}
 231    in
 232       union(Q_7,Q_6,Q_5)
 233    end
 234
 235
 236 [Simple find/count query decomposition phase]
 237
 238 Output:
 239 let
 240    C_3={[x,(#{[x,y_1]: y_1 in U | (x = y_1)})]: x in S}
 241    C_4={z_2: z_2 in U | (z_2 = 1)}
 242    Q_8={[x,y]:[x,y] in [S,T] | (C_11(x) > 0)}
 243    Q_9= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (C_3(x) > 0)} else {}
 244    Q_10= if((nonempty U) and(nonempty C_4)) then{[x,y]:[x,y] in [S,T]} else {}
 245    Q_5= join(Q_10,Q_9,Q_8)
 246    Q_6= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (not(nonempty U))} else {}
 247    C_11={[x,(#{[x,z]: z in U | (z = x)})]: x in S}
 248    Q_7= if(nonempty U) then{[x,y]:[x,y] in [S,T] | (x < y)} else {}
 249 in
 250    union(Q_7,Q_6,Q_5)
 251 end
 252