The issue I am facing is that I cannot convert the Z3 array to a python integer list. I want to call a python function inside Z3 objective function and the python function takes an integer list. I am having a Z3 array but the code gives me an error when I am converting it to a list. Below is the error message I am getting:

Traceback (most recent call last):
  File "C:\Users\sarda\Desktop\Dr. Kovalenkov\Python Coding\cybersecurity\inspection_state_placement.py", line 132, in <module>
    solver.add(D == get_paths_and_sum(connectivity, distance, valid_inspections)[1])
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\sarda\Desktop\Dr. Kovalenkov\Python Coding\cybersecurity\inspection_state_placement.py", line 120, in get_paths_and_sum
    result = max_path_with_path(connectivity, distance, inspections, i, j)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\sarda\Desktop\Dr. Kovalenkov\Python Coding\cybersecurity\inspection_state_placement.py", line 100, in max_path_with_path
    return dfs(start, target, frozenset({start}))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\sarda\Desktop\Dr. Kovalenkov\Python Coding\cybersecurity\inspection_state_placement.py", line 82, in dfs
    if connectivity[current, neighbor] == 1:
       ~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^
IndexError: only integers, slices (`:`), ellipsis (`...`), numpy.newaxis (`None`) and integer or boolean arrays are valid indices

I intend to have the optimizer found the optimal set of x[i] for which selection_cost and get_paths_and_sum. I don't know how to describe the get_paths_and_sum using Z3 idioms. Can someone help me fix the code? Is there a way I don't change my python code and convert the array before it is being used by the function?

from z3 import *
import numpy as np
from functools import lru_cache

Q = 11  # Number of states
connectivity = np.zeros((Q, Q), dtype=int)


# Helper to add edges
def add_edge(u, v):
    connectivity[u, v] = 1


n = 5  # Number of inspection states
initial_state = 0  # Ensure this is an inspection state
last_state = 4  # Ensure this is an inspection state

# Cost of placing inspection states
costs = [1 for i in range(Q)]  # Adjust as needed

# Define edges between states
add_edge(0, 1)
add_edge(0, 5)
add_edge(0, 8)
add_edge(1, 2)
add_edge(2, 3)
add_edge(3, 4)
add_edge(5, 2)
add_edge(5, 6)
add_edge(6, 3)
add_edge(6, 7)
add_edge(7, 4)
add_edge(8, 9)
add_edge(9, 5)
add_edge(9, 7)
add_edge(9, 10)
add_edge(10, 4)

# Distance = 1 per edge
distance = connectivity.astype(float)

# Solver setup
solver = Optimize()

# Decision variables: x[i] = True if state i is an inspection state
x = [Bool(f"x_{i}") for i in range(Q)]

# Ensure exactly n states are selected
solver.add(Sum([If(x[i], 1, 0) for i in range(Q)]) == n)

# Force the initial and last states to be inspection states
solver.add(x[initial_state] == True)
solver.add(x[last_state] == True)

# Cost function: sum of selected inspection state costs
selection_cost = Sum([If(x[i], costs[i], 0) for i in range(Q)])

# Define a Z3 array valid_inspections
valid_inspections = Array('valid_inspections', IntSort(), IntSort())

# Constraint: If x[i] is true, set valid_inspections[i] = i
for i in range(Q):
    solver.add(If(x[i], valid_inspections[i] == i, valid_inspections[i] == -1))


# Compute sum of the longest paths between neighboring inspection states
def max_path_with_path(connectivity, distance, inspections, start, target):
    """
    Returns (max_length, path) for the maximum-length path from 'start' to 'target'
    that does NOT pass through any inspection state except at the endpoints.
    If no valid path exists, returns None.
    """
    n = connectivity.shape[0]

    @lru_cache(None)
    def dfs(current, target, visited):
        if current == target:
            return (0, (current,))  # Reached target -> path length = 0 from here, path is just (target,)

        best = None  # Will hold (length, path) for the best route found
        for neighbor in range(n):
            if connectivity[current, neighbor] == 1:
                # Avoid cycles
                if neighbor in visited:
                    continue
                # Skip if neighbor is an inspection state (and not the target)
                if neighbor in inspections and neighbor != target:
                    continue

                result = dfs(neighbor, target, visited | {neighbor})
                if result is not None:
                    sub_len, sub_path = result
                    total_len = distance[current, neighbor] + sub_len
                    candidate_path = (current,) + sub_path
                    if best is None or total_len > best[0]:
                        best = (total_len, candidate_path)

        return best

    return dfs(start, target, frozenset({start}))


def get_paths_and_sum(connectivity, distance, inspections):
    """
    For every ordered pair (i, j) of distinct inspection states, find the maximum-length path
    from i to j that doesn't pass through any OTHER inspection state.

    Returns:
      paths_dict: dict[(i,j)] = (path, length)
      total_sum:   sum of all such maximum path lengths
    """
    # Convert valid_inspections Z3 array to a list of integers

    paths_dict = {}
    total_sum = 0
    for i in inspections:
        for j in inspections:
            if i == j:
                continue
            result = max_path_with_path(connectivity, distance, inspections, i, j)
            if result is not None:
                length, path = result
                paths_dict[(i, j)] = (path, length)
                total_sum += length
    return paths_dict, total_sum


# Define an integer variable for path sum (D)
D = Int("D")

# Add the constraint that D is equal to the total sum of paths
solver.add(D == get_paths_and_sum(connectivity, distance, valid_inspections)[1])

# Add the constraint to ensure D is non-negative
solver.add(D >= 0)

# Objective function: minimize selection cost + weighted sum of longest paths
lambda_penalty = 1
solver.minimize(selection_cost + lambda_penalty * D)

# Solve the problem
if solver.check() == sat:
    model = solver.model()

    # Extract selected inspection states
    selected_states = [i for i in range(Q) if model.evaluate(x[i])]

    # Calculate total cost
    paths_dict_f, max_distance = get_paths_and_sum(connectivity, distance, valid_inspections)

    total_cost = model.evaluate(selection_cost).as_long() + lambda_penalty * max_distance

    print(f"Selected inspection states: {selected_states}")
    print(f"Sum of longest paths between neighboring inspection states: {max_distance}")
    print(f"Total cost: {total_cost}")
else:
    print("No solution found.")