def _formulate_smt_constraints_fully_connected_layer(
    z3_optimizer, nn_first_layer, smt_first_layer, top_k, gamma):
  """Formulates smt constraints using first layer activations.

  Generates constraints for the top_k nodes in the first hidden layer by setting
  the masked activation to be greater than that of the unmasked activation.

  Args:
    z3_optimizer: instance of z3.Optimizer, z3 optimizer.
    nn_first_layer: numpy array with shape (num_hidden_nodes_first_layer,)
    smt_first_layer: list of z3.ExprRef with length
        num_hidden_nodes_first_layer.
    top_k: int, constrain the nodes with top k activations in the first hidden
        layer.
    gamma: float, masked activation is greater than gamma times the unmasked
        activation. Its value is always between [0,1).

  Returns:
    z3 optimizer with added smt constraints.
  """
  for index in nn_first_layer.argsort()[-top_k:]:
    if nn_first_layer[index] > 0:
      # we constrain only those nodes whose activations are positive.
      # In future we might handle nodes with negative values as well.
      z3_optimizer.solver.add(
          smt_first_layer[index] > gamma * nn_first_layer[index])
  return z3_optimizer