Skip to content

Commit

Permalink
⚗️🏁 try a try catch block
Browse files Browse the repository at this point in the history
  • Loading branch information
burgholzer committed Dec 12, 2023
1 parent 04b6807 commit dc00175
Showing 1 changed file with 34 additions and 29 deletions.
63 changes: 34 additions & 29 deletions src/SatEncoder.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,36 +3,41 @@
bool SatEncoder::testEqual(qc::QuantumComputation& circuitOne,
qc::QuantumComputation& circuitTwo,
const std::vector<std::string>& inputs) {
std::cout << "Entering testEqual\n";
if (!isClifford(circuitOne) || !isClifford(circuitTwo)) {
std::cerr << "Circuits are not Clifford circuits" << std::endl;
return false;
}
if (circuitOne.empty() || circuitTwo.empty()) {
std::cerr << "Both circuits must be non-empy" << std::endl;
return false;
try {
std::cout << "Entering testEqual\n";
if (!isClifford(circuitOne) || !isClifford(circuitTwo)) {
std::cerr << "Circuits are not Clifford circuits" << std::endl;
return false;
}
if (circuitOne.empty() || circuitTwo.empty()) {
std::cerr << "Both circuits must be non-empy" << std::endl;
return false;
}
std::cout << "Circuits are Clifford circuits and non-empty\n";
stats.nrOfDiffInputStates = inputs.size();
stats.nrOfQubits = circuitOne.getNqubits();
qc::DAG dagOne = qc::CircuitOptimizer::constructDAG(circuitOne);
qc::DAG dagTwo = qc::CircuitOptimizer::constructDAG(circuitTwo);
std::cout << "DAGs constructed\n";
SatEncoder::CircuitRepresentation circOneRep =
preprocessCircuit(dagOne, inputs);
std::cout << "First circuit preprocessed\n";
SatEncoder::CircuitRepresentation circTwoRep =
preprocessCircuit(dagTwo, inputs);
std::cout << "Second circuit preprocessed\n";
z3::context ctx{};
z3::solver solver(ctx);
constructMiterInstance(circOneRep, circTwoRep, solver);
std::cout << "Miter instance constructed\n";

bool equal = !isSatisfiable(solver);
stats.equal = equal;

return equal;
} catch (std::exception const& e) {
std::cerr << "Exception: " << e.what() << std::endl;
throw;
}
std::cout << "Circuits are Clifford circuits and non-empty\n";
stats.nrOfDiffInputStates = inputs.size();
stats.nrOfQubits = circuitOne.getNqubits();
qc::DAG dagOne = qc::CircuitOptimizer::constructDAG(circuitOne);
qc::DAG dagTwo = qc::CircuitOptimizer::constructDAG(circuitTwo);
std::cout << "DAGs constructed\n";
SatEncoder::CircuitRepresentation circOneRep =
preprocessCircuit(dagOne, inputs);
std::cout << "First circuit preprocessed\n";
SatEncoder::CircuitRepresentation circTwoRep =
preprocessCircuit(dagTwo, inputs);
std::cout << "Second circuit preprocessed\n";
z3::context ctx{};
z3::solver solver(ctx);
constructMiterInstance(circOneRep, circTwoRep, solver);
std::cout << "Miter instance constructed\n";

bool equal = !isSatisfiable(solver);
stats.equal = equal;

return equal;
}

bool SatEncoder::testEqual(qc::QuantumComputation& circuitOne,
Expand Down

0 comments on commit dc00175

Please sign in to comment.