Merge pull request #2 from guykatzz/bnn_opt

Printing of BNN layers
NeuralNetworkVerification · Aug 20, 2020 · 637455e · 637455e
2 parents 0ac47f3 + 6450e43
commit 637455e
Show file tree

Hide file tree

Showing 7 changed files with 107 additions and 5 deletions.
diff --git a/src/engine/InputQuery.cpp b/src/engine/InputQuery.cpp
@@ -573,7 +573,8 @@ bool InputQuery::constructNetworkLevelReasoner()
     unsigned newLayerIndex = 1;
     // Now, repeatedly attempt to construct addditional layers
     while ( constructWeighedSumLayer( nlr, handledVariableToLayer, newLayerIndex ) ||
-            constructReluLayer( nlr, handledVariableToLayer, newLayerIndex ) )
+            constructReluLayer( nlr, handledVariableToLayer, newLayerIndex ) ||
+            constructSignLayer( nlr, handledVariableToLayer, newLayerIndex ) )
     {
         ++newLayerIndex;
     }
@@ -780,6 +781,82 @@ bool InputQuery::constructReluLayer( NLR::NetworkLevelReasoner *nlr,
     return true;
 }
 
+bool InputQuery::constructSignLayer( NLR::NetworkLevelReasoner *nlr,
+                                     Map<unsigned, unsigned> &handledVariableToLayer,
+                                     unsigned newLayerIndex )
+{
+    struct NeuronInformation
+    {
+    public:
+
+        NeuronInformation( unsigned variable, unsigned neuron, unsigned sourceVariable )
+            : _variable( variable )
+            , _neuron( neuron )
+            , _sourceVariable( sourceVariable )
+        {
+        }
+
+        unsigned _variable;
+        unsigned _neuron;
+        unsigned _sourceVariable;
+    };
+
+    List<NeuronInformation> newNeurons;
+
+    // Look for Signs where the b variables have already been handled
+    const List<PiecewiseLinearConstraint *> &plConstraints =
+        getPiecewiseLinearConstraints();
+
+    for ( const auto &plc : plConstraints )
+    {
+        // Only consider Signs
+        if ( plc->getType() != SIGN )
+            continue;
+
+        const SignConstraint *sign = (const SignConstraint *)plc;
+
+        // Has the b variable been handled?
+        unsigned b = sign->getB();
+        if ( !handledVariableToLayer.exists( b ) )
+            continue;
+
+        // If the f variable has also been handled, ignore this constraint
+        unsigned f = sign->getF();
+        if ( handledVariableToLayer.exists( f ) )
+            continue;
+
+        // B has been handled, f hasn't. Add f
+        newNeurons.append( NeuronInformation( f, newNeurons.size(), b ) );
+    }
+
+    // No neurons found for the new layer
+    if ( newNeurons.empty() )
+        return false;
+
+    nlr->addLayer( newLayerIndex, NLR::Layer::SIGN, newNeurons.size() );
+    for ( const auto &newNeuron : newNeurons )
+    {
+        handledVariableToLayer[newNeuron._variable] = newLayerIndex;
+
+        unsigned sourceLayer = handledVariableToLayer[newNeuron._sourceVariable];
+        unsigned sourceNeuron = nlr->getLayer( sourceLayer )->variableToNeuron( newNeuron._sourceVariable );
+
+        // Mark the layer dependency
+        nlr->addLayerDependency( sourceLayer, newLayerIndex );
+
+        // Add the new neuron
+        nlr->setNeuronVariable( NLR::NeuronIndex( newLayerIndex, newNeuron._neuron ), newNeuron._variable );
+
+        // Mark the activation connection
+        nlr->addActivationSource( sourceLayer,
+                                  sourceNeuron,
+                                  newLayerIndex,
+                                  newNeuron._neuron );
+    }
+
+    return true;
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

diff --git a/src/engine/InputQuery.h b/src/engine/InputQuery.h
@@ -157,7 +157,9 @@ class InputQuery
     bool constructReluLayer( NLR::NetworkLevelReasoner *nlr,
                              Map<unsigned, unsigned> &handledVariableToLayer,
                              unsigned newLayerIndex );
-
+    bool constructSignLayer( NLR::NetworkLevelReasoner *nlr,
+                             Map<unsigned, unsigned> &handledVariableToLayer,
+                             unsigned newLayerIndex );
 
 public:
     /*

diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h
@@ -152,7 +152,7 @@ class ReluConstraint : public PiecewiseLinearConstraint
     String serializeToString() const;
 
     /*
-      Get the index of the B variable.
+      Get the index of the B and F variables.
     */
     unsigned getB() const;
     unsigned getF() const;

diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp
@@ -412,3 +412,13 @@ void SignConstraint::eliminateVariable( __attribute__((unused)) unsigned variabl
     // In a Sign constraint, if a variable is removed the entire constraint can be discarded.
     _haveEliminatedVariables = true;
 }
+
+unsigned SignConstraint::getB() const
+{
+    return _b;
+}
+
+unsigned SignConstraint::getF() const
+{
+    return _f;
+}
diff --git a/src/engine/SignConstraint.h b/src/engine/SignConstraint.h
@@ -139,6 +139,12 @@ class SignConstraint : public PiecewiseLinearConstraint
     */
     String serializeToString() const;
 
+    /*
+      Get the index of the B and F variables.
+    */
+    unsigned getB() const;
+    unsigned getF() const;
+
 private:
     unsigned _b, _f;
     PhaseStatus _phaseStatus;

diff --git a/src/nlr/Layer.cpp b/src/nlr/Layer.cpp
@@ -244,15 +244,15 @@ double Layer::getBias( unsigned neuron ) const
 
 void Layer::addActivationSource( unsigned sourceLayer, unsigned sourceNeuron, unsigned targetNeuron )
 {
-    ASSERT( _type == RELU || _type == ABSOLUTE_VALUE || _type == MAX );
+    ASSERT( _type == RELU || _type == ABSOLUTE_VALUE || _type == MAX || _type == SIGN );
 
     if ( !_neuronToActivationSources.exists( targetNeuron ) )
         _neuronToActivationSources[targetNeuron] = List<NeuronIndex>();
 
     _neuronToActivationSources[targetNeuron].append( NeuronIndex( sourceLayer, sourceNeuron ) );
 
     DEBUG({
-            if ( _type == RELU || _type == ABSOLUTE_VALUE )
+            if ( _type == RELU || _type == ABSOLUTE_VALUE || _type == SIGN )
                 ASSERT( _neuronToActivationSources[targetNeuron].size() == 1 );
         });
 }
@@ -1281,6 +1281,10 @@ String Layer::typeToString( Type type )
         return "MAX";
         break;
 
+    case SIGN:
+        return "SIGN";
+        break;
+
     default:
         return "UNKNOWN TYPE";
         break;
@@ -1337,6 +1341,7 @@ void Layer::dump() const
     case RELU:
     case ABSOLUTE_VALUE:
     case MAX:
+    case SIGN:
 
         for ( unsigned i = 0; i < _size; ++i )
         {

diff --git a/src/nlr/Layer.h b/src/nlr/Layer.h
@@ -24,6 +24,7 @@
 #include "MatrixMultiplication.h"
 #include "NeuronIndex.h"
 #include "ReluConstraint.h"
+#include "SignConstraint.h"
 
 namespace NLR {
 
@@ -39,6 +40,7 @@ class Layer
         RELU,
         ABSOLUTE_VALUE,
         MAX,
+        SIGN,
     };
 
     /*