Skip to content

Commit

Permalink
Add global output name var for the model parsing in marabou block
Browse files Browse the repository at this point in the history
  • Loading branch information
ryma-bmzz committed Dec 5, 2024
1 parent f4d19e6 commit 4a7a037
Showing 1 changed file with 12 additions and 7 deletions.
19 changes: 12 additions & 7 deletions airobas/blocks_hub/marabou_block.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
from maraboupy.MarabouNetwork import MarabouNetwork # (pip install maraboupy)
from tensorflow.keras.layers import Activation, Dense
from tensorflow.keras.models import Sequential

from keras.models import clone_model
from airobas.verif_pipeline import (
BlockVerif,
BlockVerifOutput,
Expand All @@ -18,6 +18,7 @@

logger = logging.getLogger(__name__)

output_name='OUTPUT'

def separate_activations(model: Sequential):
"""
Expand All @@ -28,6 +29,7 @@ def separate_activations(model: Sequential):
"""
l = []
new_model = Sequential()
#copy_model = clone_model(model)
for layer in model.layers:
if isinstance(layer, Dense):
# Add a new Dense layer without activation
Expand Down Expand Up @@ -66,18 +68,18 @@ def __init__(self, model: Sequential):

def build(self):
for layer in self.layers:

# get input_shape
input_dim = np.prod(layer.input_shape[1:])
self.varMap[layer.name] = []
for i in range(input_dim):
j = self.getNewVariable()
self.varMap[layer.name].append(j)
output_dim = np.prod(self.keras_model.output_shape[1:])
self.varMap["output"] = []
global output_name
self.varMap[output_name] = []
for i in range(output_dim):
j = self.getNewVariable()
self.varMap["output"].append(j)
self.varMap[output_name].append(j)

self._init_input_vars()
self._init_output_vars()
Expand All @@ -91,7 +93,8 @@ def _init_input_vars(self):
]

def _init_output_vars(self):
self.outputVars = np.asarray(self.varMap["output"], dtype="int")[None, None]
global output_name
self.outputVars = np.asarray(self.varMap[output_name], dtype="int")[None, None]

def buildEquations(self, index_layer, update_relu=True):
layer = self.layers[index_layer]
Expand All @@ -109,8 +112,9 @@ def buildEquations(self, index_layer, update_relu=True):
raise NotImplemented(layer)

def get_output_layer(self, index_layer):
global output_name
if index_layer + 1 == len(self.layers):
output_var = self.varMap["output"]
output_var = self.varMap[output_name]
else:
output_var = self.varMap[self.layers[index_layer + 1].name]

Expand Down Expand Up @@ -149,7 +153,8 @@ def add_relu(self, index_layer):
self.addRelu(i, j)

def get_output_dim(self):
return len(self.varMap["output"])
global output_name
return len(self.varMap[output_name])

def solve_query(self, options=None):
if options is None:
Expand Down

0 comments on commit 4a7a037

Please sign in to comment.