diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2e5f670c3b3d3167808d890769b6a2a4776dec95..98bc7308a37502f681d6e2962326c61ebcae2d27 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -12,11 +12,9 @@ option(RUN_REGRESS_TEST "run regression tests on build" OFF)
option(RUN_SYSTEM_TEST "run system tests on build" OFF)
option(RUN_MEMORY_TEST "run cxxtest testing with ASAN ON" ON)
option(RUN_PYTHON_TEST "run python API tests if building with python" OFF)
-
-# To run coverage we need to add -g and -O0 flags, so we allow it only in debug mode
-option(CODE_COVERAGE "add code coverage" OFF)
-
option(ENABLE_GUROBI "Enable use the Gurobi optimizer" OFF)
+option(ENABLE_OPENBLAS "Do symbolic bound tighting using blas" ON) # Not available on windows
+option(CODE_COVERAGE "add code coverage" OFF) # Available only in debug mode
set(DEFAULT_PYTHON_VERSION "3" CACHE STRING "Default Python version 2/3")
set(PYTHON_VERSIONS_SUPPORTED 2 3)
@@ -39,9 +37,11 @@ set(REGRESS_DIR "${PROJECT_SOURCE_DIR}/regress")
set(ENGINE_DIR "${SRC_DIR}/engine")
set(PYBIND11_DIR "${TOOLS_DIR}/pybind11-2.3.0")
set(BOOST_DIR "${TOOLS_DIR}/boost_1_68_0")
+set(OPENBLAS_DIR "${TOOLS_DIR}/OpenBLAS-0.3.9")
set(COMMON_DIR "${SRC_DIR}/common")
set(BASIS_DIR "${SRC_DIR}/basis_factorization")
+set(OPENBLAS_LIB openblas)
set(BIN_DIR "${CMAKE_BINARY_DIR}/bin")
@@ -200,6 +200,20 @@ if (${ENABLE_GUROBI})
target_include_directories(${GUROBI_LIB2} INTERFACE ${GUROBI_DIR}/include/)
endif()
+if (${ENABLE_OPENBLAS} AND NOT MSVC)
+ message(STATUS "using openblas for matrix multiplication")
+ add_compile_definitions(ENABLE_OPENBLAS)
+ #OpenBLAS
+ if(NOT EXISTS "${OPENBLAS_DIR}/installed/lib/libopenblas.a")
+ execute_process(COMMAND ${TOOLS_DIR}/get-openBLAS.sh)
+ endif()
+
+ add_library(${OPENBLAS_LIB} SHARED IMPORTED)
+ set_target_properties(${OPENBLAS_LIB} PROPERTIES IMPORTED_LOCATION ${OPENBLAS_DIR}/installed/lib/libopenblas.a)
+ list(APPEND LIBS ${OPENBLAS_LIB})
+ target_include_directories(${OPENBLAS_LIB} INTERFACE ${OPENBLAS_DIR}/installed/include)
+endif()
+
# pthread
set(THREADS_PREFER_PTHREAD_FLAG ON)
find_package(Threads REQUIRED)
diff --git a/COPYING b/COPYING
index b73692117641d8e064faeb0e1cb5628f932a91bd..d923325fcb0c5061e70e460476028becfcd15001 100644
--- a/COPYING
+++ b/COPYING
@@ -4,8 +4,8 @@ affiliations. All rights reserved.
The source code of Marabou is open and available to study, to modify, and to
redistribute original or modified versions; distribution is under the terms of
-the modified BSD license (reproduced below). Marabou links against Boost which
-is separately licensed under the Boost Software License.
+the modified BSD license (reproduced below). Marabou links against multiple
+third-party libraries, see details below.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
@@ -34,4 +34,17 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------
+-------------------------------------------------------------------------------
+ Third-Party Software
+-------------------------------------------------------------------------------
+
+The Marabou source code includes third-party software which has its own copyright
+and licensing terms, as described below.
+
+Marabou links (by default) against the following libraries:
+ Boost Boost Software License (https://www.boost.org)
+ OpenBlas BSD license (https://www.openblas.net)
+
+Marabou can also be linked (however, by default it is not) against the following libraries:
+ Gurobi (https://www.gurobi.com)
+
diff --git a/src/common/CMakeLists.txt b/src/common/CMakeLists.txt
index bf622119dd72a6b356ff5403ae64af1f70c83c4d..5899bae338f571e31fae32d6207cd1774a001621 100644
--- a/src/common/CMakeLists.txt
+++ b/src/common/CMakeLists.txt
@@ -32,6 +32,7 @@ common_add_unit_test(Queue)
common_add_unit_test(Set)
common_add_unit_test(Stack)
common_add_unit_test(Vector)
+common_add_unit_test(MatrixMultiplication)
if (${BUILD_PYTHON})
target_include_directories(${MARABOU_PY} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}")
diff --git a/src/common/MatrixMultiplication.cpp b/src/common/MatrixMultiplication.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..909467e61119bf6502d87c4674497f94ee6f590b
--- /dev/null
+++ b/src/common/MatrixMultiplication.cpp
@@ -0,0 +1,50 @@
+/********************* */
+/*! \file MatrixMultiplication.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+
+**/
+
+#include "MatrixMultiplication.h"
+
+#ifdef ENABLE_OPENBLAS
+#include "cblas.h"
+void matrixMultiplication( const double *matA, const double *matB, double *matC,
+ unsigned rowsA, unsigned columnsA,
+ unsigned columnsB )
+{
+ double alpha = 1;
+ double beta = 1;
+ // cblas_dgemm is executing: C <- alpha * A B + beta * C
+ // See https://developer.apple.com/documentation/accelerate/1513282-cblas_dgemm?language=objc
+ // for the documentation of cblas_dgemm.
+
+ cblas_dgemm( CblasRowMajor, CblasNoTrans, CblasNoTrans, rowsA, columnsB,
+ columnsA, alpha, matA, columnsA, matB, columnsB, beta, matC, columnsB);
+}
+#else
+void matrixMultiplication( const double *matA, const double *matB, double *matC,
+ unsigned rowsA, unsigned columnsA,
+ unsigned columnsB )
+{
+ for ( unsigned i = 0; i < rowsA; ++i )
+ {
+ for ( unsigned j = 0; j < columnsB; ++j )
+ {
+ for ( unsigned k = 0; k < columnsA; ++k )
+ {
+ matC[i * columnsB + j] += matA[i * columnsA + k]
+ * matB[k * columnsB + j];
+ }
+ }
+ }
+}
+#endif
diff --git a/src/common/MatrixMultiplication.h b/src/common/MatrixMultiplication.h
new file mode 100644
index 0000000000000000000000000000000000000000..0ee81714c6c305f675b4b79b129864498d772627
--- /dev/null
+++ b/src/common/MatrixMultiplication.h
@@ -0,0 +1,14 @@
+
+#ifndef __MatrixMultiplication_h__
+#define __MatrixMultiplication_h__
+
+/*
+ The size of matA is rowsA x columnsA,
+ and the size of matB is columnsA x columnsB.
+ Compute matA * matB + matC and store the result in matC
+*/
+void matrixMultiplication( const double *matA, const double *matB, double *matC,
+ unsigned rowsA, unsigned columnsA,
+ unsigned columnsB );
+
+#endif // __MatrixMultiplication_h__
diff --git a/src/common/tests/Test_MatrixMultiplication.h b/src/common/tests/Test_MatrixMultiplication.h
new file mode 100644
index 0000000000000000000000000000000000000000..d36419d2cac557c001b25093441444c87130c58e
--- /dev/null
+++ b/src/common/tests/Test_MatrixMultiplication.h
@@ -0,0 +1,66 @@
+/********************* */
+/*! \file Test_FloatUtils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "MatrixMultiplication.h"
+
+class MatrixMultiplicationTestSuite : public CxxTest::TestSuite
+{
+public:
+
+ void test_vector_matrix()
+ {
+ double matA[] = {1,2};
+ double matB[] = {1,2,3,1};
+ double matC[2] = {0};
+ unsigned rowsA = 1;
+ unsigned columnsA = 2;
+ unsigned columnsB = 2;
+ matrixMultiplication(matA, matB, matC, rowsA, columnsA, columnsB);
+
+ // matC[0] = 1*1+2*3 = 7
+ // matC[1] = 1*2+2*1 = 4
+ TS_ASSERT(matC[0] == 7);
+ TS_ASSERT(matC[1] == 4);
+ }
+
+ void test_matrix_matrix()
+ {
+ double matA[] = {1,2,3,4,5,6}; // [1,2], [3,4], [5,6]
+ double matB[] = {1,2,3,4}; // [1,2], [3,4]
+ double matC[6] = {0};
+ unsigned rowsA = 3;
+ unsigned columnsA = 2;
+ unsigned columnsB = 2;
+ matrixMultiplication(matA, matB, matC, rowsA, columnsA, columnsB);
+
+ TS_ASSERT(matC[0] == 7);
+ TS_ASSERT(matC[1] == 10);
+ TS_ASSERT(matC[2] == 15);
+ TS_ASSERT(matC[3] == 22);
+ TS_ASSERT(matC[4] == 23);
+ TS_ASSERT(matC[5] == 34);
+ }
+};
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index ecd72963a792f1b0f7da2743e030bd1e529e389b..4d46839952f82759742d41a78f344d9906aa4220 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -1782,15 +1782,16 @@ void Engine::performSymbolicBoundTightening()
for ( const auto &tightening : tightenings )
{
+
if ( tightening._type == Tightening::LB &&
- _tableau->getLowerBound( tightening._variable ) < tightening._value )
+ FloatUtils::gt ( tightening._value, _tableau->getLowerBound( tightening._variable ) ) )
{
_tableau->tightenLowerBound( tightening._variable, tightening._value );
++numTightenedBounds;
}
if ( tightening._type == Tightening::UB &&
- _tableau->getUpperBound( tightening._variable ) > tightening._value )
+ FloatUtils::lt ( tightening._value, _tableau->getUpperBound( tightening._variable ) ) )
{
_tableau->tightenUpperBound( tightening._variable, tightening._value );
++numTightenedBounds;
diff --git a/src/nlr/Layer.cpp b/src/nlr/Layer.cpp
index 081e628c8d510cc036aee6a4fad640dde4cbc67f..705c032d845ce553c6a68e3c8d7125c9fd4bac77 100644
--- a/src/nlr/Layer.cpp
+++ b/src/nlr/Layer.cpp
@@ -879,37 +879,35 @@ void Layer::computeSymbolicBoundsForWeightedSum()
const Layer *sourceLayer = _layerOwner->getLayer( sourceLayerEntry.first );
/*
- Perform the multiplication.
+ Perform the multiplication
newUB = oldUB * posWeights + oldLB * negWeights
newLB = oldUB * negWeights + oldLB * posWeights
*/
- for ( unsigned i = 0; i < _inputLayerSize; ++i )
+
+ matrixMultiplication( sourceLayer->getSymbolicUb(), _layerToPositiveWeights[sourceLayerIndex],
+ _symbolicUb, _inputLayerSize,
+ sourceLayerSize, _size);
+ matrixMultiplication( sourceLayer->getSymbolicLb(), _layerToNegativeWeights[sourceLayerIndex],
+ _symbolicUb, _inputLayerSize,
+ sourceLayerSize, _size);
+ matrixMultiplication( sourceLayer->getSymbolicLb(), _layerToPositiveWeights[sourceLayerIndex],
+ _symbolicLb, _inputLayerSize,
+ sourceLayerSize, _size);
+ matrixMultiplication( sourceLayer->getSymbolicUb(), _layerToNegativeWeights[sourceLayerIndex],
+ _symbolicLb, _inputLayerSize, sourceLayerSize,
+ _size);
+
+ // Restore the zero bound on eliminated neurons
+ unsigned index;
+ for ( const auto &eliminated : _eliminatedNeurons )
{
- for ( unsigned j = 0; j < _size; ++j )
+ for ( unsigned i = 0; i < _inputLayerSize; ++i )
{
- if ( _eliminatedNeurons.exists( j ) )
- continue;
-
- for ( unsigned k = 0; k < sourceLayerSize; ++k )
- {
- _symbolicLb[i * _size + j] +=
- sourceLayer->getSymbolicUb()[i * sourceLayerSize + k] *
- _layerToNegativeWeights[sourceLayerIndex][k * _size + j];
-
- _symbolicLb[i * _size + j] +=
- sourceLayer->getSymbolicLb()[i * sourceLayerSize + k] *
- _layerToPositiveWeights[sourceLayerIndex][k * _size + j];
-
- _symbolicUb[i * _size + j] +=
- sourceLayer->getSymbolicUb()[i * sourceLayerSize + k] *
- _layerToPositiveWeights[sourceLayerIndex][k * _size + j];
-
- _symbolicUb[i * _size + j] +=
- sourceLayer->getSymbolicLb()[i * sourceLayerSize + k] *
- _layerToNegativeWeights[sourceLayerIndex][k * _size + j];
- }
+ index = i * _size + eliminated.first;
+ _symbolicLb[index] = 0;
+ _symbolicUb[index] = 0;
}
}
diff --git a/src/nlr/Layer.h b/src/nlr/Layer.h
index 64adc9e5d3d0bfafd06c672d27d1e5476b92e62d..c2572962691354a3ff7dd4cf0a0837c9c08fbba9 100644
--- a/src/nlr/Layer.h
+++ b/src/nlr/Layer.h
@@ -21,6 +21,7 @@
#include "FloatUtils.h"
#include "LayerOwner.h"
#include "MarabouError.h"
+#include "MatrixMultiplication.h"
#include "NeuronIndex.h"
#include "ReluConstraint.h"
diff --git a/tools/get-openBLAS.sh b/tools/get-openBLAS.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f02d2a148b87d3afba06d3b1195708676f623d43
--- /dev/null
+++ b/tools/get-openBLAS.sh
@@ -0,0 +1,18 @@
+#!/bin/bash
+curdir=$pwd
+mydir="${0%/*}"
+
+cd $mydir
+
+echo "downloding openBLAS"
+wget http://github.com/xianyi/OpenBLAS/archive/v0.3.9.tar.gz
+echo "unzipping openBLAS"
+tar -xzf v0.3.9.tar.gz >> /dev/null
+echo "installing openBLAS"
+cd OpenBLAS-0.3.9
+make NO_SHARED=1 CBLAS_ONLY=1 USE_THREAD=0 >> /dev/null
+mkdir installed/
+make PREFIX=installed NO_SHARED=1 install >> /dev/null
+cd $curdir
+
+## TODO: open blas is in single thread mode. Is this what reluval uses?