# (1) Run this cell for obtaining the suitable Grover's operator for the defined satisfiability problem

from sat_circuits_engine import SATInterface
    
# Defining constraints and varibales in a high-level fashion
high_level_constraints_string = (
    "(x0 != x1)," \
    "(x3 != x4)," \
    "(x1 != x3)," \
    "(x3 != x5)," \
    "(x5 != x6)," \
    "(x0 != x2)," \
    "(x1 != x6)," \
    "(x4 != x6)"
)
high_level_vars = {"x0": 1, "x1": 1, "x2": 1, "x3": 2, "x4": 1, "x5": 1, "x6": 1}

# Initialization of the interface, `save_data=True` for exporting data into a dedicated directory
demo_1 = SATInterface(
    high_level_constraints_string=high_level_constraints_string,
    high_level_vars=high_level_vars,
    name="demo_1",
    save_data=True
)

# `obtain_grover_operator()` returns a dictionary of the form: `{
#     'operator': QC_OBJ,
#     'decomposed_operator': QC_OBJ,
#     'transpiled_operator': QC_OBJ,
#     'high_level_to_bit_indexes_map': MAP_OBJ
# }`.
# Transpilation is done according to the `transpile_kwargs` arg, which by default is set to:
# {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
grover_operator_data = demo_1.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)

demo_1.save_display_grover_operator(grover_operator_data, display=True)

# (2) Run this cell for obtaining the overall SAT circuit:
# A `QuantumCircuit` object that solves the satisfiability problem, ready for execution on a backend.

from qiskit_aer import AerSimulator

# The number of iterations over Grover's iterator (= operator + diffuser) depends on the number of solutions.
# If the number of solutions is known, it is best to provide it.
# If the number of solutions is unknown, `solutions_num=-1` will initiate an classical
# iterative stochastic process that looks for an adequate number of iterations for the problem.
# Needless to mention, this process add some computational overheads.
# `solutions_num=-2` will generate a dynamic circuit to overcome the need for providing the number of solutions.
# NOTE - this is a BETA feature which is currently under development. For now it failes 
# to scale and works properly only for small circuits (~ < 15 qubits).
overall_circuit_data = demo_1.obtain_overall_sat_circuit(
    grover_operator=grover_operator_data['operator'],
    solutions_num=6,
    backend=AerSimulator()
)

demo_1.save_display_overall_circuit(overall_circuit_data, display=True)

# (3) Run this cell for executing the overall SAT circuit and obtaining the results.

results_data = demo_1.run_overall_sat_circuit(
    circuit=overall_circuit_data['circuit'],
    backend=AerSimulator(),
    shots=300
)

demo_1.save_display_results(results_data, display=True)

# (1) Run this cell to obtain Grover's operator for the defined constraints

from sat_circuits_engine import SATInterface

# Initialization of the interface, `save_data=False` = not saving and exporting data
demo_2 = SATInterface(
    constraints_string="([4][3][2] == [0]),([2] == [3]),([3] == [4]),([0] != [1]),([8][7] == [3][2])",
    num_input_qubits=9,
    name="demo_2",
    save_data=False
)


# Obtaining Grover's operator objects
grover_operator_data = demo_2.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)
operator = grover_operator_data['operator']
decomposed_operator = grover_operator_data['decomposed_operator']
transpiled_operator = grover_operator_data['transpiled_operator']


# Displaying results
print("The high level operator circuit diagram:")
display(operator.draw('mpl', fold=-1))

print("The decomposed operator circuit diagram:")
display(decomposed_operator.draw('mpl', fold=-1))

print(f"Gates count in the transpiled operator: {transpiled_operator.count_ops()}")

# Run this cell to initiate an interactive user interface

from sat_circuits_engine import SATInterface

SATInterface()

# (1) Run this cell for obtaining the suitable Grover's operator for the defined satisfiability problem

from sat_circuits_engine import SATInterface

# Defining constraints and varibales in a high-level fashion
high_level_constraints_string = (
    "(x0 != x1)," \
    "(x2 + 2 != x3)," \
    "(x3 != x4)," \
    "(x3 != x1)," \
    "(x5 != x6)," \
    "(x0 != x2)," \
    "(x1 != x5)," \
    "(x4 != x6)," \
    "(x3 == 2)," \
    "(x2 + x4 + x3 == 3)"
)
high_level_vars = {"x0": 1, "x1": 1, "x2": 1, "x3": 2, "x4": 1, "x5": 1, "x6": 1}

# Initialization of the interface, `save_data=True` for exporting data into a dedicated directory
benchmark_demo = SATInterface(
    high_level_constraints_string=high_level_constraints_string,
    high_level_vars=high_level_vars,
    name="benchmark_demo",
    save_data=True
)

grover_operator_data = benchmark_demo.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)

benchmark_demo.save_display_grover_operator(grover_operator_data, display=True)

# (2) Run this cell for obtaining the overall SAT circuit:
# a `QuantumCircuit` object that solves the satisfiability problem, ready for execution on a backend.

from qiskit_aer import AerSimulator

overall_circuit_data = benchmark_demo.obtain_overall_sat_circuit(
    grover_operator=grover_operator_data['operator'],
    solutions_num=1,
    backend=AerSimulator()
)

benchmark_demo.save_display_overall_circuit(overall_circuit_data, display=True)

# (3) Run this cell for executing the overall SAT circuit and obtaining the results.
# WARNING: this specific circuit is heavy for a classical computer to simualte, it might take a while.

results_data = benchmark_demo.run_overall_sat_circuit(
    circuit=overall_circuit_data['circuit'],
    backend=AerSimulator(),
    shots=50
)

benchmark_demo.save_display_results(results_data, display=True)

from sat_circuits_engine import SATInterface

SATInterface()