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 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 = 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, 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, costs, 0) for i in range(Q)]) # Define a Z3 array valid_inspections valid_inspections = Array('valid_inspections', IntSort(), IntSort()) # Constraint: If x is true, set valid_inspections = i for i in range(Q): solver.add(If(x, valid_inspections == i, valid_inspections == -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)] # 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.") Continue reading...
