tuple01.fq

// This test illustrates how you can get an exponential VC from nested tuples

bind 0 cat   : {v: int | v = 100 }
bind 1 dog   : {v: int | v = 200 }
bind 2 frog  : {v: int | v = 400 }
bind 3 mouse : {v: int | v = 500 }
bind 4 hippo : {v: int | v = 600 }
bind 5 goose : {v: int | v = 700 }
bind 6 crow  : {v: int | v = 800 }
bind 7 pig   : {v: int | v = 900 }

bind 20 x_1_1 : {v: int | $k_1_1 }
bind 21 x_1_2 : {v: int | $k_1_2 }
bind 22 x_2_1 : {v: int | $k_2_1 }
bind 23 x_2_2 : {v: int | $k_2_2 }
bind 24 x_3_1 : {v: int | $k_3_1 }
bind 25 x_3_2 : {v: int | $k_3_2 }
bind 26 x_4_1 : {v: int | $k_4_1 }
bind 27 x_4_2 : {v: int | $k_4_2 }

// pack $k_1_1 : 1
// pack $k_1_2 : 1
// pack $k_2_1 : 2
// pack $k_2_2 : 2
// pack $k_3_1 : 3
// pack $k_3_2 : 3
// pack $k_4_1 : 4
// pack $k_4_2 : 4
// pack $k_5_1 : 5
// pack $k_5_2 : 5

constraint:
  env [ 0; 1; 2; 3; 4; 5; 6; 7 ]
  lhs {v : int | v = 1}
  rhs {v : int | $k_1_1}
  id 1 tag []

constraint:
  env [ 0; 1; 2; 3; 4; 5; 6; 7 ]
  lhs {v : int | v = 2}
  rhs {v : int | $k_1_2}
  id 2 tag []

constraint:
  env [ 20; 21 ]
  lhs {v : int | v = x_1_1 }
  rhs {v : int | $k_2_1    }
  id 3 tag []

constraint:
  env [ 20; 21 ]
  lhs {v : int | v = x_1_2 }
  rhs {v : int | $k_2_2    }
  id 4 tag []

constraint:
  env [ 22; 23 ]
  lhs {v : int | v = x_2_1 }
  rhs {v : int | $k_3_1    }
  id 5 tag []

constraint:
  env [ 22; 23 ]
  lhs {v : int | v = x_2_2 }
  rhs {v : int | $k_3_2    }
  id 6 tag []

constraint:
  env [ 24; 25 ]
  lhs {v : int | v = x_3_1 }
  rhs {v : int | $k_4_1    }
  id 7 tag []

constraint:
  env [ 24; 25 ]
  lhs {v : int | v = x_3_2 }
  rhs {v : int | $k_4_2    }
  id 8 tag []

constraint:
  env [ 26; 27 ]
  lhs {v : int | v = x_4_1 }
  rhs {v : int | $k_5_1    }
  id 9 tag []

constraint:
  env [ 26; 27 ]
  lhs {v : int | v = x_4_2 }
  rhs {v : int | $k_5_2    }
  id 10 tag []

constraint:
  env [ ]
  lhs {v : int | $k_5_1 }
  rhs {v : int | v = 1  }
  id 11 tag []

wf:
  env [ ]
  reft {v: int | $k_1_1}

wf:
  env [ ]
  reft {v: int | $k_1_2}

wf:
  env [ ]
  reft {v: int | $k_2_1}

wf:
  env [ ]
  reft {v: int | $k_2_2}

wf:
  env [ ]
  reft {v: int | $k_3_1}

wf:
  env [ ]
  reft {v: int | $k_3_2}


wf:
  env [ ]
  reft {v: int | $k_4_1}

wf:
  env [ ]
  reft {v: int | $k_4_2}

wf:
  env [ ]
  reft {v: int | $k_5_1}

wf:
  env [ ]
  reft {v: int | $k_5_2}