triggers error messages printed from pb_solver.cpp

ReproduceZ3Bug.cpp

#include "z3++.h"
#include <iostream>
#include <random>

struct RandomSource {
  std::uniform_real_distribution<double> RandomDistribution;
  unsigned RandomSeed;
  std::mt19937 RandomGenerator;
  RandomSource(unsigned RandomSeed)
      : RandomDistribution(0.0, 1.0), RandomSeed(RandomSeed) {
    RandomGenerator = std::mt19937(RandomSeed);
  }
  RandomSource() : RandomDistribution(0.0, 1.0) {
    std::random_device RandomDevice;
    RandomSeed = RandomDevice();
    RandomGenerator = std::mt19937(RandomSeed);
  }
  double operator()() { return RandomDistribution(RandomGenerator); }
};

z3::expr buildZ3Problem(z3::context &Z3Context, z3::optimize &Z3Optimizer,
                        z3::expr_vector &XSupport, z3::expr_vector &ZSupport,
                        z3::expr_vector &Support, std::vector<bool> Bits) {
  for (size_t QubitIndex = 0; QubitIndex < 37; ++QubitIndex) {
    XSupport.push_back(
        Z3Context.bool_const(("X_" + std::to_string(QubitIndex)).c_str()));
    ZSupport.push_back(
        Z3Context.bool_const(("Z_" + std::to_string(QubitIndex)).c_str()));
    Support.push_back(XSupport[QubitIndex] || ZSupport[QubitIndex]);
  }

  // Add code parity check constraints.
  std::vector<std::vector<size_t>> XSupports = {{0, 1, 2, 3},
                                                {},
                                                {4, 5, 6, 7},
                                                {},
                                                {8, 9, 10, 11},
                                                {},
                                                {6, 1, 12, 13, 0, 7},
                                                {},
                                                {10, 5, 4, 15, 14, 11},
                                                {},
                                                {16, 9, 8, 17},
                                                {},
                                                {13, 18, 2, 1},
                                                {},
                                                {15, 20, 19, 12, 6, 5},
                                                {},
                                                {22, 16, 14, 10, 21, 9},
                                                {},
                                                {20, 24, 13, 18, 23, 12},
                                                {},
                                                {22, 25, 14, 26, 15, 19},
                                                {},
                                                {26, 27, 23, 28, 20, 19},
                                                {},
                                                {25, 29, 22, 21},
                                                {},
                                                {28, 23, 30, 24},
                                                {},
                                                {26, 31, 29, 27, 32, 25},
                                                {},
                                                {32, 28, 33, 34, 30, 27},
                                                {},
                                                {33, 35, 32, 31},
                                                {},
                                                {35, 36, 34, 33},
                                                {}};
  std::vector<std::vector<size_t>> ZSupports = {{}, {0, 1, 2, 3},
                                                {}, {4, 5, 6, 7},
                                                {}, {8, 9, 10, 11},
                                                {}, {6, 1, 12, 13, 0, 7},
                                                {}, {10, 5, 4, 15, 14, 11},
                                                {}, {16, 9, 8, 17},
                                                {}, {13, 18, 2, 1},
                                                {}, {15, 20, 19, 12, 6, 5},
                                                {}, {22, 16, 14, 10, 21, 9},
                                                {}, {20, 24, 13, 18, 23, 12},
                                                {}, {22, 25, 14, 26, 15, 19},
                                                {}, {26, 27, 23, 28, 20, 19},
                                                {}, {25, 29, 22, 21},
                                                {}, {28, 23, 30, 24},
                                                {}, {26, 31, 29, 27, 32, 25},
                                                {}, {32, 28, 33, 34, 30, 27},
                                                {}, {33, 35, 32, 31},
                                                {}, {35, 36, 34, 33}};
  for (size_t StabIndex = 0; StabIndex < 36; StabIndex++) {
    z3::expr Anticommutes = Z3Context.bool_val(false);
    for (size_t QubitIndex : XSupports.at(StabIndex))
      Anticommutes = Anticommutes ^ ZSupport[QubitIndex];
    for (size_t QubitIndex : ZSupports.at(StabIndex))
      Anticommutes = Anticommutes ^ XSupport[QubitIndex];
    Z3Optimizer.add(Anticommutes == Z3Context.bool_val(Bits.at(StabIndex)));
  }
  return z3::sum(Support);
}

void produceErrorZ3(RandomSource& Rand) {
  // These bits work on my macbook with z3@b9b5377c6
  // std::vector<bool> Bits = {0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0,
  //                           0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0,
  //                           1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1};
  // To trigger on more platforms we just try random bitstrings
  std::vector<bool> Bits;
  for (size_t i=0; i<36; i++)
    Bits.push_back(Rand() < 0.39);

  z3::context Z3Context;
  z3::optimize Z3Optimizer(Z3Context);
  z3::expr_vector XSupport(Z3Context), ZSupport(Z3Context), Support(Z3Context);
  z3::expr TotalWeight =
      buildZ3Problem(Z3Context, Z3Optimizer, XSupport, ZSupport, Support, Bits);
  z3::optimize::handle Z3Handle = Z3Optimizer.minimize(TotalWeight);
  assert(Z3Optimizer.check() == z3::sat && "Z3 Error.");

  z3::model Z3Model = Z3Optimizer.get_model();
  assert(Z3Model.eval(TotalWeight).get_numeral_int64() ==
             Z3Optimizer.lower(Z3Handle).get_numeral_int64() &&
         "Z3 mismatch in minimum objective value.");
  int FoundTotalWeight = Z3Optimizer.lower(Z3Handle).get_numeral_int64();
  std::cout << "FoundTotalWeight = " << FoundTotalWeight << "\n";

  // Verify that no correction with lower weight is possible.
  if (FoundTotalWeight > 0) {
    Z3Optimizer.add(TotalWeight < Z3Context.int_val(FoundTotalWeight));
    assert(Z3Optimizer.check() == z3::unsat &&
           "Error -- Z3 could not certify the optimal weight solution.");
  }
}

int main() {
  RandomSource Rand(42);
  while(true)
    produceErrorZ3(Rand);
  std::cout << "Done\n";
}