diff --git a/regress/Makefile b/regress/Makefile index 2d915b968..b4ef926a7 100644 --- a/regress/Makefile +++ b/regress/Makefile @@ -22,6 +22,7 @@ SOURCES += \ Error.cpp \ FloatUtils.cpp \ MString.cpp \ + SignalHandler.cpp \ TimeUtils.cpp \ \ AcasNeuralNetwork.cpp \ diff --git a/src/common/SignalHandler.cpp b/src/common/SignalHandler.cpp new file mode 100644 index 000000000..0cda5c9bf --- /dev/null +++ b/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 +#include + +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: +// diff --git a/src/common/SignalHandler.h b/src/common/SignalHandler.h new file mode 100644 index 000000000..cf3729eaf --- /dev/null +++ b/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 _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: +// diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 93c4a8cde..f26879e1b 100644 --- a/src/engine/Engine.cpp +++ b/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 ../.. " diff --git a/src/engine/Engine.h b/src/engine/Engine.h index 5dfec42ef..9e13dc130 100644 --- a/src/engine/Engine.h +++ b/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. diff --git a/src/engine/tests/Makefile b/src/engine/tests/Makefile index 50e62c051..b78f422da 100644 --- a/src/engine/tests/Makefile +++ b/src/engine/tests/Makefile @@ -17,6 +17,7 @@ SOURCES += \ Error.cpp \ FloatUtils.cpp \ MString.cpp \ + SignalHandler.cpp \ TimeUtils.cpp \ \ BasisFactorizationFactory.cpp \ diff --git a/src/input_parsers/acas_example/Makefile b/src/input_parsers/acas_example/Makefile index ef7d40bc4..eaf4372b9 100644 --- a/src/input_parsers/acas_example/Makefile +++ b/src/input_parsers/acas_example/Makefile @@ -22,6 +22,7 @@ SOURCES += \ Error.cpp \ FloatUtils.cpp \ MString.cpp \ + SignalHandler.cpp \ TimeUtils.cpp \ \ BasisFactorizationFactory.cpp \ diff --git a/src/input_parsers/berkeley_example/Makefile b/src/input_parsers/berkeley_example/Makefile index 85dcab673..62eea0c1d 100644 --- a/src/input_parsers/berkeley_example/Makefile +++ b/src/input_parsers/berkeley_example/Makefile @@ -26,6 +26,7 @@ SOURCES += \ FloatUtils.cpp \ HeapData.cpp \ MString.cpp \ + SignalHandler.cpp \ TimeUtils.cpp \ \ BasisFactorizationFactory.cpp \ diff --git a/src/input_parsers/mps_generic/Makefile b/src/input_parsers/mps_generic/Makefile index 4dcf53b8b..cefb5ac9e 100644 --- a/src/input_parsers/mps_generic/Makefile +++ b/src/input_parsers/mps_generic/Makefile @@ -20,6 +20,7 @@ SOURCES += \ Equation.cpp \ FloatUtils.cpp \ MString.cpp \ + SignalHandler.cpp \ TimeUtils.cpp \ \ BasisFactorizationFactory.cpp \