// This namespace contains helpful operations for you to use during the tutorial
open Quantum.Kata.ExploringGroversAlgorithm;

function ConvertSATInstanceToString () : Unit {
    // Function "Message" prints its string argument to the output
    Message(SATInstanceAsString( [[(0, true)], [(0, false), (1, false)]] ));
}

%simulate ConvertSATInstanceToString

open Microsoft.Quantum.Convert;
open Microsoft.Quantum.Measurement;
open Quantum.Kata.ExploringGroversAlgorithm;

operation RunGroversAlgorithm_SimpleLoop () : Unit {
    // Create a data structure describing the SAT instance we want to solve
    let problem = [[(0, true)], [(0, false), (1, false)]];
    // The number of variables in this formula is 2
    let variableCount = 2;
    
    Message($"Solving SAT problem {SATInstanceAsString(problem)}...");
    
    // We start by defining a quantum oracle for the instance of a SAT problem we want to solve.
    // We use a pre-written operation "CreateOracleForSATInstance" to do that.
    let oracle = CreateOracleForSATInstance(problem);
    
    // We will discuss choosing the right number of iterations later
    let iterationCount = 1;
    
    // Allocate the qubits for running the algorithm
    use register = Qubit[variableCount];
    // Run the iterations using a pre-written operation
    GroversAlgorithm_Loop(register, oracle, iterationCount);

    // Perform measurements to get the variables assignment.
    // "MultiM" operation measures all qubits and returns an array of measurement results, and
    // "ResultArrayAsBoolArray" converts it to an array of boolean variables.
    let assignment = ResultArrayAsBoolArray(MultiM(register));

    // Output the results
    Message($"{VariableAssignmentAsString(assignment)}");

    // Reset the qubits before releasing them, otherwise you'll get a ReleasedQubitsAreNotInZeroState exception
    ResetAll(register);
}

%simulate RunGroversAlgorithm_SimpleLoop

open Microsoft.Quantum.Convert;
open Microsoft.Quantum.Measurement;
open Quantum.Kata.ExploringGroversAlgorithm;

operation RunGroversAlgorithm_OutputVerification () : Unit {
    // Use a different SAT instance to get a higher probability of failure
    let problem = [[(0, true), (1, true)], [(0, false), (1, false)]];
    let variableCount = 2;
    
    Message($"Solving SAT problem {SATInstanceAsString(problem)}...");
    
    let oracle = CreateOracleForSATInstance(problem);
    let iterationCount = 1;
    
    use register = Qubit[variableCount];
    GroversAlgorithm_Loop(register, oracle, iterationCount);
    let assignment = ResultArrayAsBoolArray(MultiM(register));
    Message($"{VariableAssignmentAsString(assignment)}");

    // ========================== Check that the answer is correct. ==========================

    // Allocate another qubit to keep the result of evaluating the function. 
    // You can allocate a single qubit with the following syntax in using statement: <variable name> = Qubit()
    use ... 
    // After measuring "register" on line 17, the qubits in "register" end up 
    // in the state that encodes the answer produced by the algorithm (decoded in "assignment" variable).
    // Call oracle with "register" as the first parameter (function input x) 
    // and the newly allocated qubit as the second parameter (function output f(x))
    // to evaluate the function on that answer.
    ...

    // Measure the newly allocated qubit and check if the measurement result is Zero or One;
    // One means the algorithm returned correct answer, Zero - incorrect.
    // You can measure the qubit and reset it immediately using MResetZ operation, 
    // and compare the measurement result to the constants Zero or One using "==" operator.
    if ... {
        // Report the correct/incorrect result using Message function.
        Message(...);
    } else {
        Message(...);
    }

    ResetAll(register);
}

%simulate RunGroversAlgorithm_OutputVerification

open Microsoft.Quantum.Convert;
open Microsoft.Quantum.Measurement;
open Quantum.Kata.ExploringGroversAlgorithm;

operation RunGroversAlgorithm_RerunIncorrectAnswer () : Unit {
    // Use a different SAT instance to get a higher probability of failure
    let problem = [[(0, true), (1, true)], [(0, false), (1, false)]];
    let variableCount = 2;
    
    Message($"Solving SAT problem {SATInstanceAsString(problem)}...");
    
    let oracle = CreateOracleForSATInstance(problem);
    let iterationCount = 1;
    
    use register = Qubit[variableCount];

    // ======== Use repeat-until-success loop to re-run algorithm in case of a failure ========

    // Define a mutable variable to serve as the exit condition.
    mutable isAnswerCorrect = false;
    // Define a mutable variable to store the answer once you've found a correct one.
    mutable finalAnswer = [false, false];

    repeat {
        // Loop body: run Grover's search using "GroversAlgorithm_Loop",
        // measure the answer and check whether it is correct.
        // Use "set <variable name> = <value>;" to update mutable variables.
        ...

        // Remember to reset the qubits in "register" at the end of each iteration!
    } until (isAnswerCorrect);

    // Output the final answer.
    Message($"{finalAnswer}");
}

%simulate RunGroversAlgorithm_RerunIncorrectAnswer

open Microsoft.Quantum.Convert;
open Microsoft.Quantum.Measurement;
open Quantum.Kata.ExploringGroversAlgorithm;

operation RunGroversAlgorithm_CalculateSuccessProbability () : Unit {
    // Here are the SAT instances with different success probabilities mentioned earlier to get you started
    // 1 solution: [[(0, true)], [(0, false), (1, false)], [(1, true), (2, true)]]
    // 2 solutions: [[(0, true), (1, true)], [(0, false), (1, false)], [(1, true), (2, true)], [(1, false), (2, false)]]
    // 3 solutions: [[(1, false)], [(0, true), (2, true)]]
    // 4 solutions: [[(0, true), (1, true)], [(0, false), (1, false)]]
    let variableCount = 3;
    let problem = [[(1, false)], [(0, true), (2, true)]];
    
    Message($"Solving SAT problem {SATInstanceAsString(problem)}...");
    
    let oracle = CreateOracleForSATInstance(problem);
    let iterationCount = 1;
    
    use register = Qubit[variableCount];

    // ======== Use for loop to run algorithm a fixed number of times ========

    // Define a mutable variable to store the number of times the algorithm succeeded.
    mutable successCount = 0;

    for i in 1 .. 100 {
        // Loop body: run Grover's search using "GroversAlgorithm_Loop",
        // measure the answer and check whether it is correct.
        // Use "set successCount += 1;" to increment the success counter.
        ...

        // Remember to reset the qubits in "register" at the end of each iteration!
    }

    // Output the success probability of the algorithm.
    Message($"The algorithm succeeds with {successCount}% probability.");
}

%simulate RunGroversAlgorithm_CalculateSuccessProbability