Add abs constraint support to maraboupy (#327)

* Add abs constraint support to maraboupy

* Add test for abs constraint

* Fix test

* Fix test

* remove a too-strong assertion

* attempt to fix the windows bug

* oops

* assertion

Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>
Co-authored-by: Guy <katz911@gmail.com>

Author: 3 people

maraboupy/MarabouCore.cpp

@@ -96,6 +96,10 @@ void addMaxConstraint(InputQuery& ipq, std::set<unsigned> elements, unsigned v){
     ipq.addPiecewiseLinearConstraint(m);
 }
 
+void addAbsConstraint(InputQuery& ipq, unsigned b, unsigned f){
+    ipq.addPiecewiseLinearConstraint(new AbsoluteValueConstraint(b, f));
+}
+
 void createInputQuery(InputQuery &inputQuery, std::string networkFilePath, std::string propertyFilePath){
   AcasParser* acasParser = new AcasParser( String(networkFilePath) );
   acasParser->generateQuery( inputQuery );
@@ -265,6 +269,15 @@ PYBIND11_MODULE(MarabouCore, m) {
             v (int): Output variable from max constraint
         )pbdoc",
         py::arg("inputQuery"), py::arg("elements"), py::arg("v"));
+    m.def("addAbsConstraint", &addAbsConstraint, R"pbdoc(
+        Add an Abs constraint to the InputQuery
+
+        Args:
+            inputQuery (:class:`~maraboupy.MarabouCore.InputQuery`): Marabou input query to be solved
+            b (int): Input variable
+            f (int): Output variable
+        )pbdoc",
+        py::arg("inputQuery"), py::arg("b"), py::arg("f"));
     py::class_<InputQuery>(m, "InputQuery")
         .def(py::init())
         .def("setUpperBound", &InputQuery::setUpperBound)

maraboupy/MarabouNetwork.py

@@ -26,6 +26,7 @@ class MarabouNetwork:
         equList (list of :class:`~maraboupy.MarabouUtils.Equation`): Network equations
         reluList (list of tuples): List of relu constraint tuples, where each tuple contains the backward and forward variables
         maxList (list of tuples): List of max constraint tuples, where each tuple conatins the set of input variables and output variable
+        absList (list of tuples): List of abs constraint tuples, where each tuple conatins the input variable and the output variable
         varsParticipatingInConstraints (set of int): Variables involved in some constraint
         lowerBounds (Dict[int, float]): Lower bounds of variables
         upperBounds (Dict[int, float]): Upper bounds of variables
@@ -44,6 +45,7 @@ def clear(self):
         self.equList = []
         self.reluList = []
         self.maxList = []
+        self.absList = []
         self.varsParticipatingInConstraints = set()
         self.lowerBounds = dict()
         self.upperBounds = dict()
@@ -110,6 +112,17 @@ def addMaxConstraint(self, elements, v):
         for i in elements:
             self.varsParticipatingInConstraints.add(i)
 
+    def addAbsConstraint(self, b, f):
+        """Function to add a new Abs constraint
+
+        Args:
+            b (int): Variable representing input of the Abs constraint
+            f (int): Variable representing output of the Abs constraint
+        """
+        self.absList += [(b, f)]
+        self.varsParticipatingInConstraints.add(b)
+        self.varsParticipatingInConstraints.add(f)
+
     def lowerBoundExists(self, x):
         """Function to check whether lower bound for a variable is known
 
@@ -209,6 +222,9 @@ def getMarabouQuery(self):
                 assert e < self.numVars
             MarabouCore.addMaxConstraint(ipq, m[0], m[1])
 
+        for b, f in self.absList:
+            MarabouCore.addAbsConstraint(ipq, b, f)
+
         for l in self.lowerBounds:
             assert l < self.numVars
             ipq.setLowerBound(l, self.lowerBounds[l])

maraboupy/test/test_network.py

@@ -0,0 +1,58 @@
+# Tests MarabouNetwork features not tested by it's subclasses
+import pytest
+from .. import Marabou
+import os
+import numpy as np
+
+# Global settings
+OPT = Marabou.createOptions(verbosity = 0) # Turn off printing
+TOL = 1e-6                                 # Set tolerance for checking Marabou evaluations
+NETWORK_FOLDER = "../../resources/nnet/"   # Folder for test networks
+
+def test_abs_constraint():
+    """
+    Tests the absolute value constraint.
+    Based on the acas_1_1 test, with abs constraint added to the outputs.
+    """
+    filename =  "acasxu/ACASXU_experimental_v2a_1_1.nnet"
+    testInputs = [
+        [-0.31182839647533234, 0.0, -0.2387324146378273, -0.5, -0.4166666666666667],
+        [-0.16247807039378703, -0.4774648292756546, -0.2387324146378273, -0.3181818181818182, -0.25],
+        [-0.2454504737724233, -0.4774648292756546, 0.0, -0.3181818181818182, 0.0]
+    ]
+    testOutputs = [
+        [abs(0.45556007), 0.44454904, abs(0.49616356), 0.38924966, 0.50136678, abs(testInputs[0][0])],
+        [abs(-0.02158248), -0.01885345, abs(-0.01892334), -0.01892597, -0.01893113, abs(testInputs[1][0])],
+        [abs(0.05990158), 0.05273383, abs(0.10029709), 0.01883183, 0.10521622, abs(testInputs[2][0])]
+    ]
+
+    network = loadNetwork(filename)
+
+    # Replace two output variables with their's absolute value
+    for out in [0, 2]:
+        abs_out = network.getNewVariable()
+        network.addAbsConstraint(network.outputVars[0][out], abs_out)
+        network.outputVars[0][out] = abs_out
+
+    abs_inp = network.getNewVariable()
+    network.outputVars = np.array([list(network.outputVars[0])+[abs_inp]]) 
+    network.addAbsConstraint(network.inputVars[0][0], abs_inp)
+
+    evaluateNetwork(network, testInputs, testOutputs)
+
+def loadNetwork(filename):
+    # Load network relative to this file's location
+    filename = os.path.join(os.path.dirname(__file__), NETWORK_FOLDER, filename)
+    return Marabou.read_nnet(filename)
+
+def evaluateNetwork(network, testInputs, testOutputs):
+    """
+    Load network and evaluate testInputs with Marabou
+    """
+
+    for testInput, testOutput in zip(testInputs, testOutputs):
+        marabouEval = network.evaluateWithMarabou([testInput], options = OPT, filename = "").flatten()
+
+    assert max(abs(marabouEval - testOutput)) < TOL
+    return network
+

src/basis_factorization/CSRMatrix.cpp

@@ -104,8 +104,6 @@ void CSRMatrix::initializeToEmpty( unsigned m, unsigned n )
 
 void CSRMatrix::increaseCapacity()
 {
-    ASSERT( _m > 0 && _n > 0 );
-
     unsigned estimatedNumRowEntries = std::max( 2U, _n / ROW_DENSITY_ESTIMATE );
     unsigned newEstimatedNnz = _estimatedNnz + ( estimatedNumRowEntries * _m );
 

src/engine/AbsoluteValueConstraint.cpp

@@ -267,7 +267,7 @@ PiecewiseLinearCaseSplit AbsoluteValueConstraint::getValidCaseSplit() const
 void AbsoluteValueConstraint::eliminateVariable( unsigned variable, double /* fixedValue */ )
 {
     (void)variable;
-    ASSERT( variable = _b );
+    ASSERT( ( variable == _f ) || ( variable == _b ) );
 
     // In an absolute value constraint, if a variable is removed the
     // entire constraint can be discarded

src/engine/Preprocessor.cpp

@@ -529,12 +529,9 @@ void Preprocessor::collectFixedValues()
         usedVariables.insert( merged.first );
 
     // Collect any variables with identical lower and upper bounds, or
-    // which are unused, unless they are input/output variables
+    // which are unused
 	for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( _inputOutputVariables.exists( i ) )
-            continue;
-
         if ( FloatUtils::areEqual( _preprocessed.getLowerBound( i ), _preprocessed.getUpperBound( i ) ) )
         {
             _fixedVariables[i] = _preprocessed.getLowerBound( i );
@@ -613,19 +610,30 @@ void Preprocessor::eliminateVariables()
         }
     }
 
-    // Inform the NLR about eliminated varibales
-    if ( _preprocessed._networkLevelReasoner )
-    {
-        for ( const auto &fixed : _fixedVariables )
-            _preprocessed._networkLevelReasoner->eliminateVariable( fixed.first, fixed.second );
-    }
+    // Inform the NLR about eliminated varibales, unless they are
+    // input/output variables
+	if ( _preprocessed._networkLevelReasoner )
+	{
+		for ( const auto &fixed : _fixedVariables )
+		{
+			if ( _inputOutputVariables.exists( fixed.first ) )
+				continue;
+
+			_preprocessed._networkLevelReasoner->eliminateVariable( fixed.first, fixed.second );
+		}
+	}
 
     // Compute the new variable indices, after the elimination of fixed variables
  	int offset = 0;
+    unsigned numEliminated = 0;
 	for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) )
+        if ( ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) ) &&
+			 !_inputOutputVariables.exists( i ) )
+        {
+            ++numEliminated;
             ++offset;
+        }
         else
             _oldIndexToNewIndex[i] = i - offset;
 	}
@@ -720,7 +728,8 @@ void Preprocessor::eliminateVariables()
     // Update the lower/upper bound maps
     for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i )
 	{
-        if ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) )
+        if ( ( _fixedVariables.exists( i ) || _mergedVariables.exists( i ) ) &&
+			 !_inputOutputVariables.exists( i ) )
             continue;
 
         ASSERT( _oldIndexToNewIndex.at( i ) <= i );
@@ -748,7 +757,7 @@ void Preprocessor::eliminateVariables()
     }
 
     // Adjust the number of variables in the query
-    _preprocessed.setNumberOfVariables( _preprocessed.getNumberOfVariables() - _fixedVariables.size() - _mergedVariables.size() );
+    _preprocessed.setNumberOfVariables( _preprocessed.getNumberOfVariables() - numEliminated );
 
     // Adjust the input/output mappings in the query
     _preprocessed.adjustInputOutputMapping( _oldIndexToNewIndex, _mergedVariables );