cexgen.smt2

(assert (forall ((pkt_0_2_2_0  Int  )(state_group_0_state_0_3_3_0  Int  )) (let ((_n0 state_group_0_state_0_3_3_0 ))
(let ((_n1 true ))
(let ((_n2 2 ))
(let ((_n3 (ite (=  _n0  (- 8))  _n2   (ite  _n1  1 0)  ) ))
(let ((_n4 false ))
(let ((_n5 (ite (=  _n0  13)  (ite  _n4  1 0)   _n3  ) ))
(let ((_n6 16 ))
(let ((_n7 (+   _n0   _n6 ) ))
(let ((_n8 (=   _n7   (ite  _n4  1 0) ) ))
(let ((_n9 (not  _n8 ) ))
(let ((_n10 (ite (=  _n0  (- 16))  _n7   (ite  _n4  1 0)  ) ))
(let ((_n11 (+   _n10   (ite  _n9  1 0) ) ))
(let ((_n12 (+   _n7   (ite  _n8  1 0) ) ))
(let ((_n13 (ite (=  _n0  (- 16))  _n12   _n11  ) ))
(let ((_n14 (=   _n13   _n5 ) ))
(let ((_n16 pkt_0_2_2_0 ))
(implies  (and (and (>= state_group_0_state_0_3_3_0 0) (< state_group_0_state_0_3_3_0 16 ))  (and (>= pkt_0_2_2_0 0) (< pkt_0_2_2_0 16 )) )    _n14  )))))))))))))))))))
(check-sat)
(get-model)
(exit)

cexgen_success.smt2

(set-option :produce-proofs true)
(set-option :unsat-core true)
(declare-const pkt_0_2_2_0 Int)
(declare-const state_group_0_state_0_3_3_0 Int)
(assert (not (let ((_n0 state_group_0_state_0_3_3_0 ))
(let ((_n1 true ))
(let ((_n2 2 ))
(let ((_n3 (ite (=  _n0  (- 8))  _n2   (ite  _n1  1 0)  ) ))
(let ((_n4 false ))
(let ((_n5 (ite (=  _n0  13)  (ite  _n4  1 0)   _n3  ) ))
(let ((_n6 16 ))
(let ((_n7 (+   _n0   _n6 ) ))
(let ((_n8 (=   _n7   (ite  _n4  1 0) ) ))
(let ((_n9 (not  _n8 ) ))
(let ((_n10 (ite (=  _n0  (- 16))  _n7   (ite  _n4  1 0)  ) ))
(let ((_n11 (+   _n10   (ite  _n9  1 0) ) ))
(let ((_n12 (+   _n7   (ite  _n8  1 0) ) ))
(let ((_n13 (ite (=  _n0  (- 16))  _n12   _n11  ) ))
(let ((_n14 (=   _n13   _n5 ) ))
(let ((_n16 pkt_0_2_2_0 ))
(implies  (and (and (>= state_group_0_state_0_3_3_0 0) (<
state_group_0_state_0_3_3_0 16 ))  (and (>= pkt_0_2_2_0 0) (< pkt_0_2_2_0 16 ))
)    _n14  )))))))))))))))))))
(check-sat)
(get-model)
(eval pkt_0_2_2_0)
(eval state_group_0_state_0_3_3_0)
(exit)

sampling_revised_if_else_raw_3_3_cexgen_iteration_1_bits_4.sk

// This is an autogenerated sketch file corresponding to
// the router's data path and is used to solve the Chipmunk compilation problem.
// program_file = example_specs/sampling_revised.sk num_pipeline_stages = 3
// num_alus_per_stage = 3
// num_phv_containers = 3

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_0_global = 2;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_0_global = 1;
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_1_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_2_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_immediate = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1_ctrl = 2;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_1_global = 2;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_opcode = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_opcode = 6;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_1_global = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_2_global = 0;
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_2_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1_ctrl = 2;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_immediate = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_rel_op_0_global = 2;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_2_global = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_rel_op_0_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_immediate = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_1_global = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_1_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_opcode = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_opcode = 4;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_0_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_immediate = 3;
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_0_ctrl = 1;
int sampling_revised_if_else_raw_3_3_output_mux_phv_0_2_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_2_global = 2;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_1_global = 2;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_2_global = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_2_global = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_0_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_immediate = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_2_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_opcode = 3;
int sampling_revised_if_else_raw_3_3_output_mux_phv_0_1_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2_ctrl = 0;
int sampling_revised_if_else_raw_3_3_salu_config_1_0 = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_immediate = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_immediate = 2;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_2_global = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_0_global = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_1_global = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2_ctrl = 2;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_immediate = 3;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_opcode = 0;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1_ctrl = 2;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_0_global = 0;
int sampling_revised_if_else_raw_3_3_salu_config_0_0 = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_opcode = 4;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_rel_op_0_global = 3;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2_ctrl = 1;
int sampling_revised_if_else_raw_3_3_salu_config_2_0 = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_opcode = 1;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_immediate = 1;
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_1_global = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_1_global = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_0_global = 2;
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_1_global = 0;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_2_global = 0;
int sampling_revised_if_else_raw_3_3_output_mux_phv_0_0_ctrl = 1;
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_0_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1_ctrl = 2;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_2_ctrl = 1;
int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1_ctrl = 0;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_opcode = 1;
int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_0_global = 2;
int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2_ctrl = 3;
int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_0_global = 0;

// Definitions of muxes and ALUs of the router
// Operand muxes for each ALU in each stage
// Total of 3 * 3 * 3 3-to-1 muxes
// The 3 is for two stateless operands and one stateful operand.

int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}
int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}


// Output mux for each PHV container
// Allows the container to be written from either its own stateless ALU or any stateful ALU

int sampling_revised_if_else_raw_3_3_output_mux_phv_0_0(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_0_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_0_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_0_1(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_0_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_0_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_0_2(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_0_2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_0_2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_0(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_1_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_1_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_1(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_1_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_1_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_1_2(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_1_2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_1_2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_0(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_2_0_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_2_0_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_1(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_2_1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_2_1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}
int sampling_revised_if_else_raw_3_3_output_mux_phv_2_2(int input0,int input1, int sampling_revised_if_else_raw_3_3_output_mux_phv_2_2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_output_mux_phv_2_2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }


    else { return input1; }
}


// Definition for ALUs

int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_0_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}



int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_0(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_0(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_0(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

bit sampling_revised_if_else_raw_3_3_stateful_alu_0_0_rel_op_0(int operand1, int operand2, int opcode) {
    if (opcode == 0) {
      return operand1 != operand2;
    } else if (opcode == 1) {
      return operand1 < operand2;
    } else if (opcode == 2) {
      return operand1 > operand2;
    } else {
      assert(opcode == 3);
      return operand1 == operand2;
    }
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_1(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_1(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_1(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_2(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_2(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_2(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

|StateGroup| sampling_revised_if_else_raw_3_3_stateful_alu_0_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
 |StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (sampling_revised_if_else_raw_3_3_stateful_alu_0_0_rel_op_0(sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_0(state_0,Opt_0),sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_0(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_0(const_0),Mux3_0),rel_op_0)) {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_1(state_0,Opt_1)+sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_1(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_1(const_1),Mux3_1);}else {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_2(state_0,Opt_2)+sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_2(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
; return old_state_group;
}
int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_1_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}



int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_0(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_0(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_0(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

bit sampling_revised_if_else_raw_3_3_stateful_alu_1_0_rel_op_0(int operand1, int operand2, int opcode) {
    if (opcode == 0) {
      return operand1 != operand2;
    } else if (opcode == 1) {
      return operand1 < operand2;
    } else if (opcode == 2) {
      return operand1 > operand2;
    } else {
      assert(opcode == 3);
      return operand1 == operand2;
    }
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_1(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_1(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_1(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_2(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_2(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_2(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

|StateGroup| sampling_revised_if_else_raw_3_3_stateful_alu_1_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
 |StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (sampling_revised_if_else_raw_3_3_stateful_alu_1_0_rel_op_0(sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_0(state_0,Opt_0),sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_0(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_0(const_0),Mux3_0),rel_op_0)) {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_1(state_0,Opt_1)+sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_1(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_1(const_1),Mux3_1);}else {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_2(state_0,Opt_2)+sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_2(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
; return old_state_group;
}
int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_0(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_1(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}
int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2(int input0,int input1,int input2, int sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2_ctrl_local) {
    int mux_ctrl = sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2_ctrl_local;
    if (mux_ctrl == 0) {
      return input0;
    }

      else if (mux_ctrl == 1) {
        return input1;
      }

    else { return input2; }
}int sampling_revised_if_else_raw_3_3_stateless_alu_2_2(int input0,int input1,int input2, int opcode_hole_local, int immediate_operand_hole_local, int mux1_ctrl_hole_local, int mux2_ctrl_hole_local) {
  int opcode = opcode_hole_local;
  int immediate_operand = immediate_operand_hole_local;

  int x = sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1(input0,input1,input2, mux1_ctrl_hole_local);
  int y = sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2(input0,input1,input2, mux2_ctrl_hole_local);

  if (opcode == 0) {
    return immediate_operand;
  } else if (opcode == 1) {
    return x + y;
  } else if (opcode == 2) {
    return x + immediate_operand;
  } else if (opcode == 3) {
    return x - y;
  } else if (opcode == 4) {
    return x - immediate_operand;
  } else if (opcode == 5) {
    return immediate_operand - x;
  } else if (opcode == 6) {
    return (x != 0) || (y != 0);
  } else if (opcode == 7) {
    return (x != 0) || (immediate_operand != 0);
  } else if (opcode == 8) {
    return (x != 0) && (y != 0);
  } else if (opcode == 9) {
    return (x != 0) && (immediate_operand != 0);
  } else if (opcode == 10) {
    return ! (x != 0);
  } else if (opcode == 11) {
    return x != y;
  } else if (opcode == 12) {
    return x != immediate_operand;
  } else if (opcode == 13) {
    return x == y;
  } else if (opcode == 14) {
    return x == immediate_operand;
  } else if (opcode == 15) {
    return x >= y;
  } else if (opcode == 16) {
    return x >= immediate_operand;
  } else if (opcode == 17) {
    return x < y;
  } else {
    return x < immediate_operand;
  }
}



int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_0(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_0(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_0(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

bit sampling_revised_if_else_raw_3_3_stateful_alu_2_0_rel_op_0(int operand1, int operand2, int opcode) {
    if (opcode == 0) {
      return operand1 != operand2;
    } else if (opcode == 1) {
      return operand1 < operand2;
    } else if (opcode == 2) {
      return operand1 > operand2;
    } else {
      assert(opcode == 3);
      return operand1 == operand2;
    }
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_1(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_1(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_1(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_2(int op1, int enable) {
    if (enable != 0) return 0;
    return op1;
    } 

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_2(int const) {
    return const;
    }

int sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_2(int op1, int op2, int op3, int choice) {
    if (choice == 0) return op1;
    else if (choice == 1) return op2;
    else return op3;
    } 

|StateGroup| sampling_revised_if_else_raw_3_3_stateful_alu_2_0(ref |StateGroup| state_group, int pkt_0,int pkt_1, int Mux3_0,int Mux3_1,int Mux3_2,int Opt_0,int Opt_1,int Opt_2,int const_0,int const_1,int const_2,int rel_op_0) {
 |StateGroup| old_state_group = state_group;
int state_0 = state_group.state_0;if (sampling_revised_if_else_raw_3_3_stateful_alu_2_0_rel_op_0(sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_0(state_0,Opt_0),sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_0(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_0(const_0),Mux3_0),rel_op_0)) {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_1(state_0,Opt_1)+sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_1(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_1(const_1),Mux3_1);}else {state_0 = sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_2(state_0,Opt_2)+sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_2(pkt_0,pkt_1,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_C_2(const_2),Mux3_2);}
state_group.state_0 = state_0;
; return old_state_group;
}

struct StateGroup {
    int state_0;
}

// Data type for holding result from spec and implementation
struct StateAndPacket {
    int pkt_0;
      int state_group_0_state_0;
}

// Specification
/* 
// Original program: 
// Sample every 30th packet in a flow
#define N 30

struct Packet {
  int sample;
};

int count = 0;

void func(struct Packet pkt) {
  if (count == N - 1) {
    count = 0;
  } else if (count == 8){
    count = 2;
  } else{
    count = 1;
  }
  pkt.sample = 1;
}
 */

// Output the rename map:
// stateless variable rename list: 

// state_and_packet.pkt_0 = pkt.sample

// stateful variable rename list: 

// state_and_packet.state_group_0_state_0 = count

|StateAndPacket| program (|StateAndPacket| state_and_packet) {if (state_and_packet.state_group_0_state_0==30-1) {state_and_packet.state_group_0_state_0=0;}else {if (state_and_packet.state_group_0_state_0==8) {state_and_packet.state_group_0_state_0=2;}else {state_and_packet.state_group_0_state_0=1;}}state_and_packet.pkt_0=1; return state_and_packet;
}


// Implementation
  |StateAndPacket| pipeline (|StateAndPacket| state_and_packet) {
  // Any additional constraints to speed up synthesis through parallel execution.
  

  // Consolidate all constraints on holes here.
  assert((sampling_revised_if_else_raw_3_3_stateless_alu_0_0_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_0_1_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_0_2_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_1_0_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_1_1_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_1_2_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_2_0_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_2_1_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_stateless_alu_2_2_opcode == 1)|| (sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1_ctrl <= sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2_ctrl));
assert((sampling_revised_if_else_raw_3_3_salu_config_0_0 + 0) <= 3);
assert((sampling_revised_if_else_raw_3_3_salu_config_1_0 + 0) <= 3);
assert((sampling_revised_if_else_raw_3_3_salu_config_2_0 + 0) <= 3);
assert((sampling_revised_if_else_raw_3_3_salu_config_0_0 + sampling_revised_if_else_raw_3_3_salu_config_1_0 + sampling_revised_if_else_raw_3_3_salu_config_2_0 + 0) <= 1);


  // One variable for each container in the PHV
  // Container i will be allocated to packet field i from the spec.
    int input_0_0 = 0;
    int input_0_1 = 0;
    int input_0_2 = 0;

  // One variable for each stateful ALU's state operand
  // This will be allocated to a state variable from the program using indicator variables.
      |StateGroup| state_operand_salu_0_0 =  |StateGroup|(
                                                                                       state_0 = 0
                                                                                 );
      |StateGroup| state_operand_salu_1_0 =  |StateGroup|(
                                                                                       state_0 = 0
                                                                                 );
      |StateGroup| state_operand_salu_2_0 =  |StateGroup|(
                                                                                       state_0 = 0
                                                                                 );

    /*********** Stage 0 *********/

    // Inputs
      // Read each PHV container from corresponding packet field.
        input_0_0 = state_and_packet.pkt_0;


    // Stateless ALUs
      int destination_0_0 = sampling_revised_if_else_raw_3_3_stateless_alu_0_0(
          input_0_0,
          input_0_1,
          input_0_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_0_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_0_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_0_mux2_ctrl
      );
      int destination_0_1 = sampling_revised_if_else_raw_3_3_stateless_alu_0_1(
          input_0_0,
          input_0_1,
          input_0_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_1_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_1_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_1_mux2_ctrl
      );
      int destination_0_2 = sampling_revised_if_else_raw_3_3_stateless_alu_0_2(
          input_0_0,
          input_0_1,
          input_0_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_2_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_2_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_0_2_mux2_ctrl
      );

    // Stateful operands
        int packet_operand_salu0_0_0 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0(
            input_0_0,
            input_0_1,
            input_0_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_0_ctrl);
        int packet_operand_salu0_0_1 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1(
            input_0_0,
            input_0_1,
            input_0_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_0_0_1_ctrl);

    // Read stateful ALU slots from allocated state vars.
        if (sampling_revised_if_else_raw_3_3_salu_config_0_0 == 1) {
          state_operand_salu_0_0 =
          |StateGroup|(                           state_0 = state_and_packet.state_group_0_state_0
);}

    // Stateful ALUs
      |StateGroup| old_state_group_0_0 = sampling_revised_if_else_raw_3_3_stateful_alu_0_0(state_operand_salu_0_0,
        packet_operand_salu0_0_0,
        packet_operand_salu0_0_1,
      sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Mux3_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_Opt_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_const_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_0_0_rel_op_0_global);

    // Outputs
      int output_0_0 = sampling_revised_if_else_raw_3_3_output_mux_phv_0_0(
          old_state_group_0_0.state_0,
      destination_0_0,
      sampling_revised_if_else_raw_3_3_output_mux_phv_0_0_ctrl
      );
      int output_0_1 = sampling_revised_if_else_raw_3_3_output_mux_phv_0_1(
          old_state_group_0_0.state_0,
      destination_0_1,
      sampling_revised_if_else_raw_3_3_output_mux_phv_0_1_ctrl
      );
      int output_0_2 = sampling_revised_if_else_raw_3_3_output_mux_phv_0_2(
          old_state_group_0_0.state_0,
      destination_0_2,
      sampling_revised_if_else_raw_3_3_output_mux_phv_0_2_ctrl
      );

      // Write state_0
        if (sampling_revised_if_else_raw_3_3_salu_config_0_0 == 1) {
          state_and_packet.state_group_0_state_0 = state_operand_salu_0_0.state_0;
        }

    /*********** Stage 1 *********/

    // Inputs
      // Input of this stage is the output of the previous one.
        int input_1_0 = output_0_0;
        int input_1_1 = output_0_1;
        int input_1_2 = output_0_2;


    // Stateless ALUs
      int destination_1_0 = sampling_revised_if_else_raw_3_3_stateless_alu_1_0(
          input_1_0,
          input_1_1,
          input_1_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_0_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_0_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_0_mux2_ctrl
      );
      int destination_1_1 = sampling_revised_if_else_raw_3_3_stateless_alu_1_1(
          input_1_0,
          input_1_1,
          input_1_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_1_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_1_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_1_mux2_ctrl
      );
      int destination_1_2 = sampling_revised_if_else_raw_3_3_stateless_alu_1_2(
          input_1_0,
          input_1_1,
          input_1_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_2_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_2_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_1_2_mux2_ctrl
      );

    // Stateful operands
        int packet_operand_salu1_0_0 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0(
            input_1_0,
            input_1_1,
            input_1_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_0_ctrl);
        int packet_operand_salu1_0_1 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1(
            input_1_0,
            input_1_1,
            input_1_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_1_0_1_ctrl);

    // Read stateful ALU slots from allocated state vars.
        if (sampling_revised_if_else_raw_3_3_salu_config_1_0 == 1) {
          state_operand_salu_1_0 =
          |StateGroup|(                           state_0 = state_and_packet.state_group_0_state_0
);}

    // Stateful ALUs
      |StateGroup| old_state_group_1_0 = sampling_revised_if_else_raw_3_3_stateful_alu_1_0(state_operand_salu_1_0,
        packet_operand_salu1_0_0,
        packet_operand_salu1_0_1,
      sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Mux3_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_Opt_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_const_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_1_0_rel_op_0_global);

    // Outputs
      int output_1_0 = sampling_revised_if_else_raw_3_3_output_mux_phv_1_0(
          old_state_group_1_0.state_0,
      destination_1_0,
      sampling_revised_if_else_raw_3_3_output_mux_phv_1_0_ctrl
      );
      int output_1_1 = sampling_revised_if_else_raw_3_3_output_mux_phv_1_1(
          old_state_group_1_0.state_0,
      destination_1_1,
      sampling_revised_if_else_raw_3_3_output_mux_phv_1_1_ctrl
      );
      int output_1_2 = sampling_revised_if_else_raw_3_3_output_mux_phv_1_2(
          old_state_group_1_0.state_0,
      destination_1_2,
      sampling_revised_if_else_raw_3_3_output_mux_phv_1_2_ctrl
      );

      // Write state_0
        if (sampling_revised_if_else_raw_3_3_salu_config_1_0 == 1) {
          state_and_packet.state_group_0_state_0 = state_operand_salu_1_0.state_0;
        }

    /*********** Stage 2 *********/

    // Inputs
      // Input of this stage is the output of the previous one.
        int input_2_0 = output_1_0;
        int input_2_1 = output_1_1;
        int input_2_2 = output_1_2;


    // Stateless ALUs
      int destination_2_0 = sampling_revised_if_else_raw_3_3_stateless_alu_2_0(
          input_2_0,
          input_2_1,
          input_2_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_0_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_0_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_0_mux2_ctrl
      );
      int destination_2_1 = sampling_revised_if_else_raw_3_3_stateless_alu_2_1(
          input_2_0,
          input_2_1,
          input_2_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_1_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_1_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_1_mux2_ctrl
      );
      int destination_2_2 = sampling_revised_if_else_raw_3_3_stateless_alu_2_2(
          input_2_0,
          input_2_1,
          input_2_2
,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_2_opcode,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_2_immediate,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux1_ctrl,
      sampling_revised_if_else_raw_3_3_stateless_alu_2_2_mux2_ctrl
      );

    // Stateful operands
        int packet_operand_salu2_0_0 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0(
            input_2_0,
            input_2_1,
            input_2_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_0_ctrl);
        int packet_operand_salu2_0_1 = sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1(
            input_2_0,
            input_2_1,
            input_2_2
      , sampling_revised_if_else_raw_3_3_stateful_operand_mux_2_0_1_ctrl);

    // Read stateful ALU slots from allocated state vars.
        if (sampling_revised_if_else_raw_3_3_salu_config_2_0 == 1) {
          state_operand_salu_2_0 =
          |StateGroup|(                           state_0 = state_and_packet.state_group_0_state_0
);}

    // Stateful ALUs
      |StateGroup| old_state_group_2_0 = sampling_revised_if_else_raw_3_3_stateful_alu_2_0(state_operand_salu_2_0,
        packet_operand_salu2_0_0,
        packet_operand_salu2_0_1,
      sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Mux3_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_Opt_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_0_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_1_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_const_2_global,sampling_revised_if_else_raw_3_3_stateful_alu_2_0_rel_op_0_global);

    // Outputs
      int output_2_0 = sampling_revised_if_else_raw_3_3_output_mux_phv_2_0(
          old_state_group_2_0.state_0,
      destination_2_0,
      sampling_revised_if_else_raw_3_3_output_mux_phv_2_0_ctrl
      );
      int output_2_1 = sampling_revised_if_else_raw_3_3_output_mux_phv_2_1(
          old_state_group_2_0.state_0,
      destination_2_1,
      sampling_revised_if_else_raw_3_3_output_mux_phv_2_1_ctrl
      );
      int output_2_2 = sampling_revised_if_else_raw_3_3_output_mux_phv_2_2(
          old_state_group_2_0.state_0,
      destination_2_2,
      sampling_revised_if_else_raw_3_3_output_mux_phv_2_2_ctrl
      );

      // Write state_0
        if (sampling_revised_if_else_raw_3_3_salu_config_2_0 == 1) {
          state_and_packet.state_group_0_state_0 = state_operand_salu_2_0.state_0;
        }


    // Write pkt_0
    state_and_packet.pkt_0 = output_2_0;

  // Return updated packet fields and state vars
  return state_and_packet;
}

  harness void main(
    int pkt_0
        , int state_group_0_state_0
) {

    |StateAndPacket| x = |StateAndPacket|(      pkt_0 = pkt_0 + 16,
          state_group_0_state_0 = state_group_0_state_0 + 16
);

  |StateAndPacket| pipeline_result = pipeline(x);
  |StateAndPacket| program_result = program(x);

      assert(pipeline_result.state_group_0_state_0
      == program_result.state_group_0_state_0);

    assert(pipeline_result.pkt_0 == program_result.pkt_0);

  

  }