Refactor verification.py

[darioguidotti]

As we add support for non-sequential NNs, I believe we should refactor the class NeverVerification as, right now, it is very specialised for ReLU FC NNs. In particular we need to solve the following issues:

1. we need to find a better way to pass the heuristic and parameters to use for the abstract transformers of the node (maybe a dictionary?) since, in principle, we could need specifications regarding heuristic and related parameters for non-ReLU nodes.

2. __build_abst_network(...) need to be rewritten to support non-sequential networks. We also need to understand if this kind of function wouldn't make more sense in conversion.py. (Eventually connected to #26)

3. __compute_output_starset(...) should be rewritten to make use of (or substituted altogether with) the forward(...) methods of the related concrete AbsNeuralNetworks (or corresponding class following #25 and #23).

[sdemarch]

I second the idea in point 1. to use a dictionary for the verification parameters. It is the way we handle it in SearchVerification and it could be a dictionary defined by the base class, with all verification strategies using it to store their parameters.

[darioguidotti]

Some notes and considerations:

• LocalRobustnessProperty should probably removed, as right now I do not think is of any use. It would likely make more sense as an alternate constructor for NeverProperty.
• We need to reason about if and how we want to support properties for networks with multiple inputs and outputs. Consequently, we need to update NeverProperty and how we manage the input/output ids (e.g., if in the forward the AbsElement assume the identifier of the last node they traversed, we will likely need to force the output ids to be the same as the leaf node ids).
• At least regarding the ReLU heuristic, we could define a Callable (or a class with a related methods if we need to keep track of some attribute) in which to encapsulate the code and related info that are used to chose the neurone to refine (mixed_single_relu_forward).
• More in general we could define a dictionary whose keys are the names of the supported nodes (i.e., the node.__class__.__name__) and whose values depend on the specific nodes but contains all the needed data, functions etc.

[sdemarch]

We decided to structure the properties like this:

• Create a base class NeverProperty which is characterized by a predicate_matrix and a predicate_bias Cx <= d
• Create the classes VnnLibProperty initialized by a SMT-LIB file and LocalRobustnessProperty initialized by a sample and a noise
• Internally, the derived classes will build Cx <= d based on their constructor