Merge pull request #1 from guykatzz/master

merging from guykatzz/master

maraboupy/MarabouCore.cpp

@@ -151,6 +151,7 @@ PYBIND11_MODULE(MarabouCore, m) {
         .def("setLowerBound", &InputQuery::setLowerBound)
         .def("getUpperBound", &InputQuery::getUpperBound)
         .def("getLowerBound", &InputQuery::getLowerBound)
+        .def("dump", &InputQuery::dump)
         .def("setNumberOfVariables", &InputQuery::setNumberOfVariables)
         .def("addEquation", &InputQuery::addEquation)
         .def("getSolutionValue", &InputQuery::getSolutionValue)

maraboupy/tests.py

@@ -0,0 +1,40 @@
+from maraboupy import MarabouCore
+import pytest
+
+large = 100
+def define_network():
+    network = MarabouCore.InputQuery()
+    network.setNumberOfVariables(3)
+
+    # x
+    network.setLowerBound(0, -1)
+    network.setUpperBound(0, 1)
+
+    network.setLowerBound(1, 1)
+    network.setUpperBound(1, 2)
+
+    # y
+    network.setLowerBound(2, -large)
+    network.setUpperBound(2, large)
+
+    MarabouCore.addReluConstraint(network, 0, 1)
+
+    # y - relu(x) >= 0
+    output_equation = MarabouCore.Equation()
+    output_equation.addAddend(1, 2)
+    output_equation.addAddend(-1, 1)
+    output_equation.setScalar(0)
+    # output_equation.dump()
+    network.addEquation(output_equation)
+
+    # y <= n * 0.01
+    property_eq = MarabouCore.Equation(MarabouCore.Equation.LE)
+    property_eq.addAddend(1, 1)
+    property_eq.setScalar(3)
+
+    return network
+
+def test_dump_query():
+    network = define_network()
+    MarabouCore.solve(network, "", 0)
+    network.dump()

src/configuration/GlobalConfiguration.cpp

@@ -71,6 +71,7 @@ const GlobalConfiguration::BasisFactorizationType GlobalConfiguration::BASIS_FAC
     GlobalConfiguration::SPARSE_FORREST_TOMLIN_FACTORIZATION;
 
 // Logging
+const bool GlobalConfiguration::DNC_MANAGER_LOGGING = false;
 const bool GlobalConfiguration::ENGINE_LOGGING = false;
 const bool GlobalConfiguration::TABLEAU_LOGGING = false;
 const bool GlobalConfiguration::SMT_CORE_LOGGING = false;

src/configuration/GlobalConfiguration.h

@@ -187,6 +187,7 @@ class GlobalConfiguration
     /*
       Logging options
     */
+    static const bool DNC_MANAGER_LOGGING;
     static const bool ENGINE_LOGGING;
     static const bool TABLEAU_LOGGING;
     static const bool SMT_CORE_LOGGING;

src/engine/DnCManager.cpp

@@ -31,12 +31,13 @@
 #include <cmath>
 #include <thread>
 
-static void dncSolve( WorkerQueue *workload, std::shared_ptr<Engine> engine,
-                      std::atomic_uint &numUnsolvedSubQueries,
-                      std::atomic_bool &shouldQuitSolving,
-                      unsigned threadId, unsigned onlineDivides,
-                      float timeoutFactor, DivideStrategy divideStrategy )
+void DnCManager::dncSolve( WorkerQueue *workload, std::shared_ptr<Engine> engine,
+                           std::atomic_uint &numUnsolvedSubQueries,
+                           std::atomic_bool &shouldQuitSolving,
+                           unsigned threadId, unsigned onlineDivides,
+                           float timeoutFactor, DivideStrategy divideStrategy )
 {
+    log( Stringf( "Thread #%u on CPU %u", threadId, sched_getcpu() ) );
     DnCWorker worker( workload, engine, std::ref( numUnsolvedSubQueries ),
                       std::ref( shouldQuitSolving ), threadId, onlineDivides,
                       timeoutFactor, divideStrategy );
@@ -365,6 +366,12 @@ void DnCManager::updateTimeoutReached( timespec startTime, unsigned long long
         timeoutInMicroSeconds;
 }
 
+void DnCManager::log( const String &message )
+{
+    if ( GlobalConfiguration::DNC_MANAGER_LOGGING )
+        printf( "DnCManager: %s\n", message.ascii() );
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/engine/DnCManager.h

@@ -63,6 +63,15 @@ class DnCManager
     String getResultString();
 
 private:
+    /*
+      Create and run a DnCWorker
+    */
+    static void dncSolve( WorkerQueue *workload, std::shared_ptr<Engine> engine,
+                          std::atomic_uint &numUnsolvedSubQueries,
+                          std::atomic_bool &shouldQuitSolving,
+                          unsigned threadId, unsigned onlineDivides,
+                          float timeoutFactor, DivideStrategy divideStrategy );
+
     /*
       Create the base engine from the network and property files,
       and if necessary, create engines for workers
@@ -91,6 +100,8 @@ class DnCManager
     void updateTimeoutReached( timespec startTime,
                                unsigned long long timeoutInMicroSeconds );
 
+    static void log( const String &message );
+
     /*
       The base engine that is used to perform the initial divides
     */

src/engine/InputQuery.cpp

@@ -404,6 +404,32 @@ void InputQuery::printInputOutputBounds() const
     }
 }
 
+void InputQuery::dump() const
+{
+    printf( "Variable bounds:\n" );
+    for ( unsigned i = 0; i < _numberOfVariables; ++i )
+    {
+        printf( "\t %u: [%s, %s]\n", i,
+                _lowerBounds.exists( i ) ? Stringf( "%lf", _lowerBounds[i] ).ascii() : "-inf",
+                _upperBounds.exists( i ) ? Stringf( "%lf", _upperBounds[i] ).ascii() : "inf" );
+    }
+
+    printf( "Constraints:\n" );
+    String constraintString;
+    for ( const auto &pl : _plConstraints )
+    {
+        pl->dump( constraintString );
+        printf( "\t%s\n", constraintString.ascii() );
+    }
+
+    printf( "Equations:\n" );
+    for ( const auto &e : _equations )
+    {
+        printf( "\t" );
+        e.dump();
+    }
+}
+
 void InputQuery::setSymbolicBoundTightener( SymbolicBoundTightener *sbt )
 {
     _sbt = sbt;

src/engine/InputQuery.h

@@ -116,6 +116,7 @@ class InputQuery
       Print input and output bounds
     */
     void printInputOutputBounds() const;
+    void dump() const;
 
     /*
       Adjsut the input/output variable mappings because variables have been merged

src/engine/ReluConstraint.cpp

@@ -476,17 +476,27 @@ PiecewiseLinearCaseSplit ReluConstraint::getValidCaseSplit() const
 
 void ReluConstraint::dump( String &output ) const
 {
-    output = Stringf( "ReluConstraint: x%u = ReLU( x%u ). Active? %s. PhaseStatus = %u (%s). "
-                      "b in [%lf, %lf]. f in [%lf, %lf]",
+    output = Stringf( "ReluConstraint: x%u = ReLU( x%u ). Active? %s. PhaseStatus = %u (%s).\n",
                       _f, _b,
                       _constraintActive ? "Yes" : "No",
-                      _phaseStatus, phaseToString( _phaseStatus ).ascii(),
-                      _lowerBounds[_b], _upperBounds[_b], _lowerBounds[_f], _upperBounds[_f]
+                      _phaseStatus, phaseToString( _phaseStatus ).ascii()
                       );
 
+    output += Stringf( "b in [%s, %s], ",
+                       _lowerBounds.exists( _b ) ? Stringf( "%lf", _lowerBounds[_b] ).ascii() : "-inf",
+                       _upperBounds.exists( _b ) ? Stringf( "%lf", _upperBounds[_b] ).ascii() : "inf" );
+
+    output += Stringf( "f in [%s, %s]",
+                       _lowerBounds.exists( _f ) ? Stringf( "%lf", _lowerBounds[_f] ).ascii() : "-inf",
+                       _upperBounds.exists( _f ) ? Stringf( "%lf", _upperBounds[_f] ).ascii() : "inf" );
+
     if ( _auxVarInUse )
-        output += Stringf( ". Aux var: %u. Range: [%lf, %lf]\n",
-                           _aux, _lowerBounds[_aux], _upperBounds[_aux] );
+    {
+        output += Stringf( ". Aux var: %u. Range: [%s, %s]\n",
+                           _aux,
+                           _lowerBounds.exists( _aux ) ? Stringf( "%lf", _lowerBounds[_aux] ).ascii() : "-inf",
+                           _upperBounds.exists( _aux ) ? Stringf( "%lf", _upperBounds[_aux] ).ascii() : "inf" );
+    }
 }
 
 void ReluConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex )