basic signal handling: allow user to request a timeout

regress/Makefile

@@ -22,6 +22,7 @@ SOURCES += \
 	Error.cpp \
 	FloatUtils.cpp \
 	MString.cpp \
+	SignalHandler.cpp \
 	TimeUtils.cpp \
 	\
 	AcasNeuralNetwork.cpp \

src/common/SignalHandler.cpp

@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \signalHandler SignalHandler.h
+** \verbatim
+** Top contributors (to current version):
+**   Guy Katz
+** This signalHandler is part of the Marabou project.
+** Copyright (c) 2016-2017 by the authors listed in the signalHandler AUTHORS
+** in the top-level source directory) and their institutional affiliations.
+** All rights reserved. See the signalHandler COPYING in the top-level source
+** directory for licensing information.\endverbatim
+**/
+
+#include "SignalHandler.h"
+#include <cstring>
+#include <signal.h>
+
+void got_signal( int signalNumber )
+{
+    SignalHandler::getInstance()->signalReceived( signalNumber );
+}
+
+SignalHandler *SignalHandler::getInstance()
+{
+    static SignalHandler handler;
+    return &handler;
+}
+
+void SignalHandler::registerClient( Signalable *client )
+{
+    _clients.append( client );
+}
+
+void SignalHandler::initialize()
+{
+    struct sigaction sa;
+    memset( &sa, 0, sizeof(sa) );
+    sa.sa_handler = got_signal;
+    sigfillset( &sa.sa_mask );
+    sigaction( SIGQUIT, &sa, NULL );
+}
+
+void SignalHandler::signalReceived( unsigned /* signalNumber */ )
+{
+    for ( const auto &signalable : _clients )
+        signalable->quitSignal();
+}
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-signalHandler-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/SignalHandler.h

@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file SignalHandler.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2016-2017 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
+ **/
+
+#ifndef __SignalHandler_h__
+#define __SignalHandler_h__
+
+#include "List.h"
+
+class SignalHandler
+{
+public:
+    class Signalable
+    {
+    public:
+        virtual void quitSignal() = 0;
+    };
+
+    /*
+      Get the singleton signal handler
+    */
+    static SignalHandler *getInstance();
+
+    /*
+      Register a client to receive signals
+    */
+    void registerClient( Signalable *client );
+
+    /*
+      Initialize the signal handling
+    */
+    void initialize();
+
+    /*
+      Called when a signal is received
+    */
+    void signalReceived( unsigned signalNumber );
+
+private:
+    List<Signalable *> _clients;
+
+    /*
+      Prevent additional instantiations of the class
+    */
+    SignalHandler() {}
+    SignalHandler( const SignalHandler & ) {}
+};
+
+#endif // __SignalHandler_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/engine/Engine.cpp

@@ -32,6 +32,7 @@ Engine::Engine()
     , _basisRestorationRequired( Engine::RESTORATION_NOT_NEEDED )
     , _basisRestorationPerformed( Engine::NO_RESTORATION_PERFORMED )
     , _costFunctionManager( _tableau )
+    , _quitRequested( false )
 {
     _smtCore.setStatistics( &_statistics );
     _tableau->setStatistics( &_statistics );
@@ -68,6 +69,9 @@ void Engine::adjustWorkMemorySize()
 
 bool Engine::solve()
 {
+    SignalHandler::getInstance()->initialize();
+    SignalHandler::getInstance()->registerClient( this );
+
     storeInitialEngineState();
 
     printf( "\nEngine::solve: Initial statistics\n" );
@@ -81,6 +85,16 @@ bool Engine::solve()
         _statistics.addTimeMainLoop( TimeUtils::timePassed( mainLoopStart, mainLoopEnd ) );
         mainLoopStart = mainLoopEnd;
 
+        if ( _quitRequested )
+        {
+            printf( "\n\nEngine: quitting due to external request...\n\n" );
+            printf( "Final statistics:\n" );
+            _statistics.print();
+
+            // Todo: return a separate exit code for tiemouts
+            return false;
+        }
+
         try
         {
             DEBUG( _tableau->verifyInvariants() );
@@ -993,6 +1007,11 @@ void Engine::checkBoundCompliancyWithDebugSolution()
     }
 }
 
+void Engine::quitSignal()
+{
+    _quitRequested = true;
+}
+
 //
 // Local Variables:
 // compile-command: "make -C ../.. "

src/engine/Engine.h

@@ -25,6 +25,7 @@
 #include "Map.h"
 #include "PrecisionRestorer.h"
 #include "Preprocessor.h"
+#include "SignalHandler.h"
 #include "SmtCore.h"
 #include "Statistics.h"
 
@@ -33,7 +34,7 @@ class InputQuery;
 class PiecewiseLinearConstraint;
 class String;
 
-class Engine : public IEngine
+class Engine : public IEngine, public SignalHandler::Signalable
 {
 public:
     Engine();
@@ -66,6 +67,11 @@ class Engine : public IEngine
     void restoreState( const EngineState &state );
     void setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints );
 
+    /*
+      A request from the user to terminate
+    */
+    void quitSignal();
+
     const Statistics *getStatistics() const;
 
 private:
@@ -181,6 +187,11 @@ class Engine : public IEngine
     */
     AutoCostFunctionManager _costFunctionManager;
 
+    /*
+      Indicates a user request to quit
+    */
+    bool _quitRequested;
+
     /*
       Perform a simplex step: compute the cost function, pick the
       entering and leaving variables and perform a pivot.

src/engine/tests/Makefile

@@ -17,6 +17,7 @@ SOURCES += \
 	Error.cpp \
 	FloatUtils.cpp \
 	MString.cpp \
+	SignalHandler.cpp \
 	TimeUtils.cpp \
 	\
 	BasisFactorizationFactory.cpp \

src/input_parsers/acas_example/Makefile

@@ -22,6 +22,7 @@ SOURCES += \
 	Error.cpp \
 	FloatUtils.cpp \
 	MString.cpp \
+	SignalHandler.cpp \
 	TimeUtils.cpp \
 	\
 	BasisFactorizationFactory.cpp \

src/input_parsers/berkeley_example/Makefile

@@ -26,6 +26,7 @@ SOURCES += \
 	FloatUtils.cpp \
 	HeapData.cpp \
 	MString.cpp \
+	SignalHandler.cpp \
 	TimeUtils.cpp \
 	\
 	BasisFactorizationFactory.cpp \

src/input_parsers/mps_generic/Makefile

@@ -20,6 +20,7 @@ SOURCES += \
 	Equation.cpp \
 	FloatUtils.cpp \
 	MString.cpp \
+	SignalHandler.cpp \
 	TimeUtils.cpp \
 	\
 	BasisFactorizationFactory.cpp \