From 2be7381d4e2859c1e57fe143de72824739c12e8f Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 18 Feb 2022 17:02:10 -0800 Subject: [PATCH 01/39] Add MockBoundManager --- src/engine/tests/MockBoundManager.h | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/engine/tests/MockBoundManager.h b/src/engine/tests/MockBoundManager.h index fe5bd9145e..fd26df67b1 100644 --- a/src/engine/tests/MockBoundManager.h +++ b/src/engine/tests/MockBoundManager.h @@ -219,15 +219,16 @@ class MockBoundManager : public IBoundManager private: unsigned _size; - double *_lowerBounds; - double *_upperBounds; - bool *_tightenedLower; - bool *_tightenedUpper; - /* Map _lowerBounds; */ - /* Map _upperBounds; */ - /* Map _tightenedLower; */ - /* Map _tightenedUpper; */ -}; + Map _lowerBounds; + Map _upperBounds; + Map _tightenedLower; + Map _tightenedUpper; + + /* double *_lowerBounds; */ + /* double *_upperBounds; */ + + /* bool *_tightenedLower; */ + /* bool *_tightenedUpper; */ #endif // __MockBoundManager_h__ From 663aba89ae8c044759aa1e8f7b068f47230bd7df Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 8 Apr 2022 11:34:30 -0700 Subject: [PATCH 02/39] Remove CBT from Engine --- src/engine/Engine.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 7776587e52..f176bed39f 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1258,6 +1258,12 @@ void Engine::initializeTableau( const double *constraintMatrix, const ListsetDimensions(); + + // Register the boundManager with all the PL constraints + for ( auto &plConstraint : _preprocessedQuery->getPiecewiseLinearConstraints() ) + plConstraint->registerBoundManager( &_boundManager ); + _plConstraints = _preprocessedQuery->getPiecewiseLinearConstraints(); for ( const auto &constraint : _plConstraints ) { @@ -1371,11 +1377,6 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess ) } } - for ( const auto &constraint : _plConstraints ) - { - constraint->registerTableau( _tableau ); - } - if ( Options::get()->getBool( Options::DUMP_BOUNDS ) ) _networkLevelReasoner->dumpBounds(); From e5a20fae328978457814561c61ec68a47ff42275 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 8 Apr 2022 11:59:18 -0700 Subject: [PATCH 03/39] Restore registerTableau method in PiecewiseLinearConstraint --- src/engine/Engine.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index f176bed39f..6312264e20 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1377,6 +1377,11 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess ) } } + for ( const auto &constraint : _plConstraints ) + { + constraint->registerTableau( _tableau ); + } + if ( Options::get()->getBool( Options::DUMP_BOUNDS ) ) _networkLevelReasoner->dumpBounds(); @@ -1916,6 +1921,7 @@ void Engine::applyAllRowTightenings() applyBoundTightenings(); } +// This method becomes obsolete since bound updates should occur directly void Engine::applyAllConstraintTightenings() { applyBoundTightenings(); From 63d485f4658d403b679f8f790fc3494425655753 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 8 Apr 2022 12:45:23 -0700 Subject: [PATCH 04/39] Update ReluConstraint tests --- src/engine/tests/Test_ReluConstraint.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h index 4fd37923a8..8d35a44f64 100644 --- a/src/engine/tests/Test_ReluConstraint.h +++ b/src/engine/tests/Test_ReluConstraint.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file Test_ReluConstraint.h +/*! \file _Test_ReluConstraint.h ** \verbatim ** Top contributors (to current version): ** Guy Katz, Parth Shah, Duligur Ibeling, Haoze (Andrew) Wu From 59e24364f200dde67e2d0ffaf5555bf7c52a767a Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 8 Apr 2022 15:58:09 -0700 Subject: [PATCH 05/39] Update Sign and Abs tests --- src/engine/tests/Test_SignConstraint.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/engine/tests/Test_SignConstraint.h b/src/engine/tests/Test_SignConstraint.h index 285791abeb..ad7bb93ce8 100644 --- a/src/engine/tests/Test_SignConstraint.h +++ b/src/engine/tests/Test_SignConstraint.h @@ -364,10 +364,10 @@ class SignConstraintTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( splits.size(), 2U ); sign.notifyLowerBound( 4, -0.5 ); - TS_ASSERT_THROWS_EQUALS( splits = sign.getCaseSplits(), - const MarabouError &e, - e.getCode(), - MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT ); + /* TS_ASSERT_THROWS_EQUALS( splits = sign.getCaseSplits(), */ + /* const MarabouError &e, */ + /* e.getCode(), */ + /* MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT ); */ sign.unregisterAsWatcher( &tableau ); } From 1c9206803516f2aadda1fedbcde8704fba9395f1 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Tue, 19 Apr 2022 13:06:42 -0700 Subject: [PATCH 06/39] Add constraint bound tightening call --- src/engine/Engine.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 6312264e20..80988da985 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1921,7 +1921,6 @@ void Engine::applyAllRowTightenings() applyBoundTightenings(); } -// This method becomes obsolete since bound updates should occur directly void Engine::applyAllConstraintTightenings() { applyBoundTightenings(); From 576710a0df40545e7898a31804df77d332b04c38 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Tue, 19 Apr 2022 16:54:48 -0700 Subject: [PATCH 07/39] Initialize CDOs in piece-wise linear constraints --- src/engine/Engine.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 80988da985..8213129a63 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1262,7 +1262,10 @@ void Engine::initializeBoundsAndConstraintWatchersInTableau( unsigned // Register the boundManager with all the PL constraints for ( auto &plConstraint : _preprocessedQuery->getPiecewiseLinearConstraints() ) + { plConstraint->registerBoundManager( &_boundManager ); + plConstraint->initializeCDOs( &_context ); + } _plConstraints = _preprocessedQuery->getPiecewiseLinearConstraints(); for ( const auto &constraint : _plConstraints ) From 2bcbde568a458ab7d7edfe4a85a5d470f31ca90b Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Tue, 26 Apr 2022 15:26:21 -0700 Subject: [PATCH 08/39] Register BoundManager with constraints after Tableau is initialized --- src/engine/Engine.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 8213129a63..c349793ddd 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1260,13 +1260,6 @@ void Engine::initializeBoundsAndConstraintWatchersInTableau( unsigned { _rowBoundTightener->setDimensions(); - // Register the boundManager with all the PL constraints - for ( auto &plConstraint : _preprocessedQuery->getPiecewiseLinearConstraints() ) - { - plConstraint->registerBoundManager( &_boundManager ); - plConstraint->initializeCDOs( &_context ); - } - _plConstraints = _preprocessedQuery->getPiecewiseLinearConstraints(); for ( const auto &constraint : _plConstraints ) { @@ -1287,6 +1280,12 @@ void Engine::initializeBoundsAndConstraintWatchersInTableau( unsigned _tableau->setUpperBound( i, _preprocessedQuery->getUpperBound( i ) ); } + // Register the boundManager with all the PL constraints + for ( auto &plConstraint : _preprocessedQuery->getPiecewiseLinearConstraints() ) + { + plConstraint->registerBoundManager( &_boundManager ); + } + _statistics.setUnsignedAttribute( Statistics::NUM_PL_CONSTRAINTS, _plConstraints.size() ); } From db76c256a8cde50ce605696981254fdcf02c1335 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 18 Feb 2022 17:02:10 -0800 Subject: [PATCH 09/39] Revert "Add MockBoundManager" This reverts commit 59db095a04ec0e80dd146f834422a6d0ee294387. --- src/engine/tests/MockBoundManager.h | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/engine/tests/MockBoundManager.h b/src/engine/tests/MockBoundManager.h index fd26df67b1..fe5bd9145e 100644 --- a/src/engine/tests/MockBoundManager.h +++ b/src/engine/tests/MockBoundManager.h @@ -219,16 +219,15 @@ class MockBoundManager : public IBoundManager private: unsigned _size; - Map _lowerBounds; - Map _upperBounds; - Map _tightenedLower; - Map _tightenedUpper; - - /* double *_lowerBounds; */ - /* double *_upperBounds; */ - - /* bool *_tightenedLower; */ - /* bool *_tightenedUpper; */ + double *_lowerBounds; + double *_upperBounds; + bool *_tightenedLower; + bool *_tightenedUpper; + /* Map _lowerBounds; */ + /* Map _upperBounds; */ + /* Map _tightenedLower; */ + /* Map _tightenedUpper; */ +}; #endif // __MockBoundManager_h__ From 6165f8bce050dceb20325e45455acca80f5406fd Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 27 Apr 2022 16:07:32 -0700 Subject: [PATCH 10/39] Update SignConstraint::notifyLower/UpperBound methods to use BoundManager correctly --- src/engine/SignConstraint.cpp | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index bf3d3492f1..656aecc4ba 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -380,21 +380,27 @@ String SignConstraint::phaseToString( PhaseStatus phase ) void SignConstraint::notifyLowerBound( unsigned variable, double bound ) { if ( _statistics ) - _statistics->incLongAttribute( Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); + _statistics->incLongAttribute( + Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); // If there's an already-stored tighter bound, return if ( _boundManager == nullptr && existsLowerBound( variable ) && !FloatUtils::gt( bound, getLowerBound( variable ) ) ) return; - // Otherwise - update bound - setLowerBound( variable, bound ); - - if ( variable == _f && FloatUtils::gt( bound, -1 ) ) + // Otherwise - update bound + setLowerBound( variable, bound ); + if ( variable == _f && FloatUtils::gt( bound, -1 ) ) + setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); + else if ( variable == _b && !FloatUtils::isNegative( bound ) ) + setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); + } + else if ( !phaseFixed() ) { setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); if ( _boundManager != nullptr ) { + setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); _boundManager->tightenLowerBound( _f, 1 ); _boundManager->tightenLowerBound( _b, 0 ); } @@ -410,21 +416,28 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound ) void SignConstraint::notifyUpperBound( unsigned variable, double bound ) { if ( _statistics ) - _statistics->incLongAttribute( Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); + _statistics->incLongAttribute( + Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); // If there's an already-stored tighter bound, return if ( _boundManager == nullptr && existsUpperBound( variable ) && !FloatUtils::lt( bound, getUpperBound( variable ) ) ) return; - // Otherwise - update bound - setUpperBound( variable, bound ); + // Otherwise - update bound + setUpperBound( variable, bound ); - if ( variable == _f && FloatUtils::lt( bound, 1 ) ) + if ( variable == _f && FloatUtils::lt( bound, 1 ) ) + setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); + else if ( variable == _b && FloatUtils::isNegative( bound ) ) + setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); + } + else if ( !phaseFixed() ) { setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); if ( _boundManager != nullptr ) { + setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); _boundManager->tightenUpperBound( _f, -1 ); _boundManager->tightenUpperBound( _b, 0 ); } @@ -434,6 +447,7 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound ) setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); if ( _boundManager != nullptr ) { + setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); _boundManager->tightenUpperBound( _f, -1 ); } } From 4f50e8b143de6759a0c04ca29df53775b2cf3aba Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 27 Apr 2022 16:20:55 -0700 Subject: [PATCH 11/39] Update AbsoluteValue::notifyL/UBound methods to use BoundManager correctly --- src/engine/AbsoluteValueConstraint.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index 41944d27e9..b28ace813c 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -127,7 +127,8 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound !FloatUtils::gt( bound, getLowerBound( variable ) ) ) return; - setLowerBound( variable, bound ); + setLowerBound( variable, bound ); + } // Check whether the phase has become fixed fixPhaseIfNeeded(); @@ -183,6 +184,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound // Check whether the phase has become fixed fixPhaseIfNeeded(); + // Update partner's bound if ( isActive() && _boundManager ) { From 1c6f77201c08d299ce95b5707b8ec45fc75457db Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 27 Apr 2022 17:18:08 -0700 Subject: [PATCH 12/39] Update notify*Bound methods to maintain semantics required by tests --- src/engine/AbsoluteValueConstraint.cpp | 4 +--- src/engine/SignConstraint.cpp | 32 ++++++++------------------ 2 files changed, 10 insertions(+), 26 deletions(-) diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index b28ace813c..41944d27e9 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -127,8 +127,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound !FloatUtils::gt( bound, getLowerBound( variable ) ) ) return; - setLowerBound( variable, bound ); - } + setLowerBound( variable, bound ); // Check whether the phase has become fixed fixPhaseIfNeeded(); @@ -184,7 +183,6 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound // Check whether the phase has become fixed fixPhaseIfNeeded(); - // Update partner's bound if ( isActive() && _boundManager ) { diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index 656aecc4ba..bf3d3492f1 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -380,27 +380,21 @@ String SignConstraint::phaseToString( PhaseStatus phase ) void SignConstraint::notifyLowerBound( unsigned variable, double bound ) { if ( _statistics ) - _statistics->incLongAttribute( - Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); + _statistics->incLongAttribute( Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); // If there's an already-stored tighter bound, return if ( _boundManager == nullptr && existsLowerBound( variable ) && !FloatUtils::gt( bound, getLowerBound( variable ) ) ) return; - // Otherwise - update bound - setLowerBound( variable, bound ); - if ( variable == _f && FloatUtils::gt( bound, -1 ) ) - setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); - else if ( variable == _b && !FloatUtils::isNegative( bound ) ) - setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); - } - else if ( !phaseFixed() ) + // Otherwise - update bound + setLowerBound( variable, bound ); + + if ( variable == _f && FloatUtils::gt( bound, -1 ) ) { setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); if ( _boundManager != nullptr ) { - setPhaseStatus( PhaseStatus::SIGN_PHASE_POSITIVE ); _boundManager->tightenLowerBound( _f, 1 ); _boundManager->tightenLowerBound( _b, 0 ); } @@ -416,28 +410,21 @@ void SignConstraint::notifyLowerBound( unsigned variable, double bound ) void SignConstraint::notifyUpperBound( unsigned variable, double bound ) { if ( _statistics ) - _statistics->incLongAttribute( - Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); + _statistics->incLongAttribute( Statistics::NUM_BOUND_NOTIFICATIONS_TO_PL_CONSTRAINTS ); // If there's an already-stored tighter bound, return if ( _boundManager == nullptr && existsUpperBound( variable ) && !FloatUtils::lt( bound, getUpperBound( variable ) ) ) return; - // Otherwise - update bound - setUpperBound( variable, bound ); + // Otherwise - update bound + setUpperBound( variable, bound ); - if ( variable == _f && FloatUtils::lt( bound, 1 ) ) - setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); - else if ( variable == _b && FloatUtils::isNegative( bound ) ) - setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); - } - else if ( !phaseFixed() ) + if ( variable == _f && FloatUtils::lt( bound, 1 ) ) { setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); if ( _boundManager != nullptr ) { - setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); _boundManager->tightenUpperBound( _f, -1 ); _boundManager->tightenUpperBound( _b, 0 ); } @@ -447,7 +434,6 @@ void SignConstraint::notifyUpperBound( unsigned variable, double bound ) setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); if ( _boundManager != nullptr ) { - setPhaseStatus( PhaseStatus::SIGN_PHASE_NEGATIVE ); _boundManager->tightenUpperBound( _f, -1 ); } } From 0d4c73b7e4b52664b941272b8ebcc435b5ce9503 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Mon, 2 May 2022 10:26:48 -0700 Subject: [PATCH 13/39] Register BoundManager with PiecewiseLinearConstraints when solving starts. This change is to avoid violating preconditions of the PiecewiseLinearConstraints::registerBoundManager method. --- src/engine/Engine.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index c349793ddd..7e4b136133 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1280,12 +1280,6 @@ void Engine::initializeBoundsAndConstraintWatchersInTableau( unsigned _tableau->setUpperBound( i, _preprocessedQuery->getUpperBound( i ) ); } - // Register the boundManager with all the PL constraints - for ( auto &plConstraint : _preprocessedQuery->getPiecewiseLinearConstraints() ) - { - plConstraint->registerBoundManager( &_boundManager ); - } - _statistics.setUnsignedAttribute( Statistics::NUM_PL_CONSTRAINTS, _plConstraints.size() ); } From 1b3a462675d63b822c81a6119c2d680876c51c82 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 26 May 2022 10:40:10 -0700 Subject: [PATCH 14/39] Fix stray search replace --- src/engine/tests/Test_ReluConstraint.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h index 8d35a44f64..4fd37923a8 100644 --- a/src/engine/tests/Test_ReluConstraint.h +++ b/src/engine/tests/Test_ReluConstraint.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file _Test_ReluConstraint.h +/*! \file Test_ReluConstraint.h ** \verbatim ** Top contributors (to current version): ** Guy Katz, Parth Shah, Duligur Ibeling, Haoze (Andrew) Wu From adb23cc125dcc0a3c420413bf97d756e86226a67 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 26 May 2022 10:44:54 -0700 Subject: [PATCH 15/39] Revert commented out code in Test_SignConstraint --- src/engine/tests/Test_SignConstraint.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/engine/tests/Test_SignConstraint.h b/src/engine/tests/Test_SignConstraint.h index ad7bb93ce8..285791abeb 100644 --- a/src/engine/tests/Test_SignConstraint.h +++ b/src/engine/tests/Test_SignConstraint.h @@ -364,10 +364,10 @@ class SignConstraintTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( splits.size(), 2U ); sign.notifyLowerBound( 4, -0.5 ); - /* TS_ASSERT_THROWS_EQUALS( splits = sign.getCaseSplits(), */ - /* const MarabouError &e, */ - /* e.getCode(), */ - /* MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT ); */ + TS_ASSERT_THROWS_EQUALS( splits = sign.getCaseSplits(), + const MarabouError &e, + e.getCode(), + MarabouError::REQUESTED_CASE_SPLITS_FROM_FIXED_CONSTRAINT ); sign.unregisterAsWatcher( &tableau ); } From e2570b57ab67608a6a68a06721308edb3e1f56e1 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Mon, 6 Jun 2022 08:48:48 -0700 Subject: [PATCH 16/39] Bulk test fixes --- src/engine/CDSmtCore.cpp | 479 ---------------------------- src/engine/CDSmtCore.h | 333 -------------------- src/engine/DnCWorker.cpp | 4 +- src/engine/Engine.cpp | 125 ++------ src/engine/Engine.h | 11 - src/engine/IEngine.h | 11 - src/engine/SmtCore.cpp | 440 ++++++++++++-------------- src/engine/SmtCore.h | 211 ++++++++----- src/engine/oldSmtCore | 257 +++++++++++++++ src/engine/oldSmtCoreCpp | 533 ++++++++++++++++++++++++++++++++ src/engine/tests/Test_SmtCore.h | 339 ++++++++++---------- 11 files changed, 1311 insertions(+), 1432 deletions(-) delete mode 100644 src/engine/CDSmtCore.cpp delete mode 100644 src/engine/CDSmtCore.h create mode 100644 src/engine/oldSmtCore create mode 100644 src/engine/oldSmtCoreCpp diff --git a/src/engine/CDSmtCore.cpp b/src/engine/CDSmtCore.cpp deleted file mode 100644 index 46888c1b57..0000000000 --- a/src/engine/CDSmtCore.cpp +++ /dev/null @@ -1,479 +0,0 @@ -/********************* */ -/*! \file CDSmtCore.cpp - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, Aleksandar Zeljic, Haoze Wu, Parth Shah - ** 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 - ** - ** See the description of the class in CDSmtCore.h. - **/ - -#include "CDSmtCore.h" - -#include "Debug.h" -#include "DivideStrategy.h" -#include "EngineState.h" -#include "FloatUtils.h" -#include "GlobalConfiguration.h" -#include "IEngine.h" -#include "MStringf.h" -#include "MarabouError.h" -#include "PseudoImpactTracker.h" -#include "ReluConstraint.h" - -using namespace CVC4::context; - -CDSmtCore::CDSmtCore( IEngine *engine, Context &ctx ) - : _statistics( NULL ) - , _context( ctx ) - , _trail( &_context ) - , _decisions( &_context ) - , _engine( engine ) - , _needToSplit( false ) - , _constraintForSplitting( NULL ) - , _constraintViolationThreshold - ( Options::CONSTRAINT_VIOLATION_THRESHOLD ) - , _deepSoIRejectionThreshold( Options::get()->getInt - ( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) - , _branchingHeuristic( Options::get()->getDivideStrategy() ) - , _scoreTracker( nullptr ) - , _numRejectedPhasePatternProposal( 0 ) -{ -} - -CDSmtCore::~CDSmtCore() -{ -} - -void CDSmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) -{ - ASSERT( !constraint->phaseFixed() ); - - if ( !_constraintToViolationCount.exists( constraint ) ) - _constraintToViolationCount[constraint] = 0; - - ++_constraintToViolationCount[constraint]; - - if ( _constraintToViolationCount[constraint] >= - _constraintViolationThreshold ) - { - _needToSplit = true; - if ( GlobalConfiguration::SPLITTING_HEURISTICS == - DivideStrategy::ReLUViolation || !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = constraint; - ASSERT( !_constraintForSplitting->phaseFixed() ); - } -} - -unsigned CDSmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) const -{ - if ( !_constraintToViolationCount.exists( constraint ) ) - return 0; - - return _constraintToViolationCount[constraint]; -} - -void CDSmtCore::initializeScoreTrackerIfNeeded( const - List - &plConstraints ) -{ - if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) - { - _scoreTracker = std::unique_ptr - ( new PseudoImpactTracker() ); - _scoreTracker->initialize( plConstraints ); - - SMT_LOG( "\tTracking Pseudo Impact..." ); - } -} - -void CDSmtCore::reportRejectedPhasePatternProposal() -{ - ++_numRejectedPhasePatternProposal; - - if ( _numRejectedPhasePatternProposal >= - _deepSoIRejectionThreshold ) - { - _needToSplit = true; - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = _scoreTracker->topUnfixed(); - } -} - -bool CDSmtCore::needToSplit() const -{ - return _needToSplit; -} - -void CDSmtCore::pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ) -{ - SMT_LOG( Stringf( "Decision @ %d )", _context.getLevel() + 1 ).ascii() ); - TrailEntry te( constraint, decision ); - applyTrailEntry( te, true ); - SMT_LOG( Stringf( "Decision push @ %d DONE", _context.getLevel() ).ascii() ); -} - -void CDSmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) -{ - ASSERT( constraint->isImplication() ); - SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); - TrailEntry te( constraint, constraint->nextFeasibleCase() ); - applyTrailEntry( te, false ); - SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); -} - -void CDSmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) -{ - if ( isDecision ) - { - _context.push(); - _decisions.push_back( te ); - } - - _trail.push_back( te ); - _engine->applySplit( te.getPiecewiseLinearCaseSplit() ); -} - -void CDSmtCore::decide() -{ - ASSERT( _needToSplit ); - SMT_LOG( "Performing a ReLU split" ); - - _numRejectedPhasePatternProposal = 0; - // Maybe the constraint has already become inactive - if so, ignore - // TODO: Ideally we will not ever reach this point - // TODO: Maintain a vector of constraints above the threshold - // Iterate until we find an active one - if ( !_constraintForSplitting->isActive() ) - { - _needToSplit = false; - _constraintToViolationCount[_constraintForSplitting] = 0; - _constraintForSplitting = nullptr; - return; - } - - ASSERT( _constraintForSplitting->isActive() ); - _needToSplit = false; - _constraintForSplitting->setActiveConstraint( false ); - - decideSplit( _constraintForSplitting ); -} - -void CDSmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) -{ - struct timespec start = TimeUtils::sampleMicro(); - - if ( _statistics ) - { - _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - if ( !constraint->isFeasible() ) - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - ASSERT( constraint->isFeasible() ); - ASSERT( !constraint->isImplication() ); - - PhaseStatus decision = constraint->nextFeasibleCase(); - pushDecision( constraint, decision ); - - if ( _statistics ) - { - unsigned level = _context.getLevel(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - SMT_LOG( "Performing a ReLU split - DONE" ); -} - - -unsigned CDSmtCore::getDecisionLevel() const -{ - return _decisions.size(); -} - -bool CDSmtCore::popDecisionLevel( TrailEntry &lastDecision ) -{ - //ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); - if ( _decisions.empty() ) - return false; - - SMT_LOG( "Popping trail ..." ); - lastDecision = _decisions.back(); - _context.pop(); - _engine->postContextPopHook(); - SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() ); - return true; -} - -void CDSmtCore::interruptIfCompliantWithDebugSolution() -{ - if ( checkSkewFromDebuggingSolution() ) - { - SMT_LOG( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } -} - -PiecewiseLinearCaseSplit CDSmtCore::getDecision( unsigned decisionLevel ) const -{ - ASSERT( decisionLevel <= getDecisionLevel() ); - ASSERT( decisionLevel > 0 ); - return _decisions[decisionLevel - 1].getPiecewiseLinearCaseSplit(); -} - -bool CDSmtCore::backtrackToFeasibleDecision( TrailEntry &lastDecision ) -{ - SMT_LOG( "Backtracking to a feasible decision..." ); - - if ( getDecisionLevel() == 0 ) - return false; - - popDecisionLevel( lastDecision ); - lastDecision.markInfeasible(); - - while ( !lastDecision.isFeasible() ) - { - interruptIfCompliantWithDebugSolution(); - - if ( !popDecisionLevel( lastDecision ) ) - return false; - - lastDecision.markInfeasible(); - } - - interruptIfCompliantWithDebugSolution(); - - return true; -} - -bool CDSmtCore::backtrackAndContinueSearch() -{ - TrailEntry feasibleDecision( nullptr, CONSTRAINT_INFEASIBLE ); - struct timespec start = TimeUtils::sampleMicro(); - - if ( !backtrackToFeasibleDecision( feasibleDecision ) ) - return false; - - ASSERT( feasibleDecision.isFeasible() ); - - if ( _statistics ) - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - - PiecewiseLinearConstraint *pwlc = feasibleDecision._pwlConstraint; - if ( pwlc->isImplication() ) - pushImplication( pwlc ); - else - decideSplit( pwlc ); - - if ( _statistics ) - { - unsigned level = _context.getLevel(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - - checkSkewFromDebuggingSolution(); - return true; -} - -void CDSmtCore::resetReportedViolations() -{ - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; - _needToSplit = false; -} - -void CDSmtCore::allSplitsSoFar( List &result ) const -{ - result.clear(); - - for ( auto trailEntry : _trail ) - result.append( trailEntry.getPiecewiseLinearCaseSplit() ); -} - -void CDSmtCore::setStatistics( Statistics *statistics ) -{ - _statistics = statistics; -} - -void CDSmtCore::storeDebuggingSolution( const Map &debuggingSolution ) -{ - _debuggingSolution = debuggingSolution; -} - -// Return true if stack is currently compliant, false otherwise -// If there is no stored solution, return false --- incompliant. -bool CDSmtCore::checkSkewFromDebuggingSolution() -{ - if ( _debuggingSolution.empty() ) - return false; - - String error; - - int decisionLevel = 0; - bool isDecision = false; - // First check that the valid splits implied at the root level are okay - for ( const auto &trailEntry : _trail ) - { - if ( trailEntry._pwlConstraint != _decisions[decisionLevel]._pwlConstraint ) - isDecision = false; - else - { - ASSERT( trailEntry._phase == _decisions[decisionLevel]._phase ); - isDecision = true; - ++decisionLevel; - } - - PiecewiseLinearCaseSplit caseSplit = trailEntry.getPiecewiseLinearCaseSplit(); - if ( decisionLevel == 0 ) - { - if ( !splitAllowsStoredSolution( caseSplit, error ) ) - { - printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - else - { - // If the active split is non-compliant but there are alternatives, - // i.e. it was a decision, that's fine - if ( isDecision && !splitAllowsStoredSolution( caseSplit, error ) ) - { - // Active split is non-compliant but this is fine, because there - // are alternatives. We're done. - return false; - } - else // Implied split - { - if ( !splitAllowsStoredSolution( caseSplit, error ) ) - { - printf( "Error with one of the splits implied at this stack level:\n\t%s\n", - error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - } - } - - // No problems were detected, the stack is compliant with the stored solution - return true; -} - -bool CDSmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const -{ - // False if the split prevents one of the values in the stored solution, true otherwise. - error = ""; - if ( _debuggingSolution.empty() ) - return true; - - for ( const auto bound : split.getBoundTightenings() ) - { - unsigned variable = bound._variable; - - // If the possible solution doesn't care about this variable, - // ignore it - if ( !_debuggingSolution.exists( variable ) ) - continue; - - // Otherwise, check that the bound is consistent with the solution - double solutionValue = _debuggingSolution[variable]; - double boundValue = bound._value; - - if ( ( bound._type == Tightening::LB ) && FloatUtils::gt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new LB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - else if ( ( bound._type == Tightening::UB ) && FloatUtils::lt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new UB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - } - - return true; -} - -void CDSmtCore::setConstraintViolationThreshold( unsigned threshold ) -{ - _constraintViolationThreshold = threshold; -} - -PiecewiseLinearConstraint *CDSmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const -{ - ASSERT( !_violatedPlConstraints.empty() ); - - if ( !GlobalConfiguration::USE_LEAST_FIX ) - return *_violatedPlConstraints.begin(); - - PiecewiseLinearConstraint *candidate; - - // Apply the least fix heuristic - auto it = _violatedPlConstraints.begin(); - - candidate = *it; - unsigned minFixes = getViolationCounts( candidate ); - - PiecewiseLinearConstraint *contender; - unsigned contenderFixes; - while ( it != _violatedPlConstraints.end() ) - { - contender = *it; - contenderFixes = getViolationCounts( contender ); - if ( contenderFixes < minFixes ) - { - minFixes = contenderFixes; - candidate = contender; - } - - ++it; - } - - return candidate; -} - -bool CDSmtCore::pickSplitPLConstraint() -{ - if ( _needToSplit ) - _constraintForSplitting = _engine->pickSplitPLConstraint - ( _branchingHeuristic ); - return _constraintForSplitting != NULL; -} - -void CDSmtCore::reset() -{ - _context.popto( 0 ); - _engine->postContextPopHook(); - _needToSplit = false; - _constraintForSplitting = NULL; - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; -} diff --git a/src/engine/CDSmtCore.h b/src/engine/CDSmtCore.h deleted file mode 100644 index 31dedf9813..0000000000 --- a/src/engine/CDSmtCore.h +++ /dev/null @@ -1,333 +0,0 @@ -/********************* */ -/*! \file CDSmtCore.h - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, AleksandarZeljic, Haoze Wu, Parth Shah - ** 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 - ** - ** The CDSmtCore class implements a context-dependent SmtCore class. - ** The CDSmtCore distinguishes between: **decisions** and **implications**. - ** - ** Decision is a case of PiecewiseLinearConstraint asserted on the trail. - ** A decision is a choice between multiple feasible cases of a - ** PiecewiseLinearConstraint and represents nodes in the search tree. - ** - ** Implication is the last feasible case of a PiecewiseLinearConstraint and as - ** soon as it is detected it is asserted on the trail. - ** - ** Case splitting on a PiecewiseLinearConstraint performs a decision. - ** Fixing a case of a PiecewiseLinearConstraint (e.g., via bound propagation or - ** by exhausting all other cases) performs an implication. - ** - ** The overall search state is stored in a distributed way: - ** - CDSmtCore::_trail is the current search state in a chronological order - ** - PiecewiseLinearConstraints' infeasible cases enumerate all the explored - ** states w.r.t to the chronological order on the _trail. - ** - ** _trail is a chronological list of cases of PiecewiseLinearConstraints - ** asserted to hold (as TrailEntries) - both decisions and implications. - ** _decisions is a chronological list of decisions stored on the trail. - ** _trail and _decisions are both context dependent and will synchronize in - ** unison with the _context object. - ** - ** When a search state is found to be infeasible, CDSmtCore backtracks to the - ** last decision and continues the search. - ** - ** PushDecision advances the decision level and context level. - ** popDecisionLevel backtracks the last decision and context level. - ** - ** Advancing a context level creates a synchronization point to which all - ** context dependent members can backtrack in unison. - ** Backtracking a context level restores all context dependent members to the - ** state of the last synchronization point. This operation is O(1) complexity. - ** - ** Since the entire search state is context dependent, backtracking the context - ** (via popDecisionLevel) backtracks the entire Marabou search state. - ** The only exception is the labeling of basic/non-basic variables in the - ** tableau, which may need to be recalculated using Tableau's - ** postContextPopHook exposed via Engine. - ** - ** Implementation relies on: - ** - ** - _context is a unique Context object from which all the context-dependent - ** structures are obtained. - ** - ** - PiecewiseLinearConstraint class stores its search state in a - ** context-dependent manner and exposes it using nextFeasibleCase() and - ** markInfeasible() methods. - ** - ** - Using BoundManager class to store bounds in a context-dependent manner - **/ - -#ifndef __CDSmtCore_h__ -#define __CDSmtCore_h__ - -#include "Options.h" -#include "PiecewiseLinearCaseSplit.h" -#include "PiecewiseLinearConstraint.h" -#include "PLConstraintScoreTracker.h" -#include "Stack.h" -#include "Statistics.h" -#include "TrailEntry.h" -#include "context/cdlist.h" -#include "context/context.h" - -#define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "CDSmtCore: %s\n", x ) - -class EngineState; -class Engine; -class String; - -class CDSmtCore -{ -public: - CDSmtCore( IEngine *engine, CVC4::context::Context &context ); - ~CDSmtCore(); - - /* - Clear the stack. - */ - void freeMemory(); - - /* - Initialize the score tracker with the given list of pl constraints. - */ - void initializeScoreTrackerIfNeeded( const List - &plConstraints ); - - /* - Inform the SMT core that a SoI phase pattern proposal is rejected. - */ - void reportRejectedPhasePatternProposal(); - - /* - Update the score of the constraint with the given score in the costTracker. - */ - inline void updatePLConstraintScore( PiecewiseLinearConstraint *constraint, - double score ) - { - ASSERT( _scoreTracker != nullptr ); - _scoreTracker->updateScore( constraint, score ); - } - - /* - Get the constraint in the score tracker with the highest score - */ - inline PiecewiseLinearConstraint *getConstraintsWithHighestScore() const - { - return _scoreTracker->topUnfixed(); - } - - /* - Inform the SMT core that a PL constraint is violated. - */ - void reportViolatedConstraint( PiecewiseLinearConstraint *constraint ); - - /* - Get the number of times a specific PL constraint has been reported as - violated. - */ - unsigned getViolationCounts( PiecewiseLinearConstraint *constraint ) const; - - /* - Reset all reported violation counts. - */ - void resetReportedViolations(); - - /* - Returns true iff the SMT core wants to perform a case split. - */ - bool needToSplit() const; - - /* - Push TrailEntry representing the decision onto the trail. - */ - void pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ); - - /* - Inform SmtCore of an implied (formerly valid) case split that was discovered. - */ - void pushImplication( PiecewiseLinearConstraint *constraint ); - - /* - Pushes trail entry onto trail, handles decision book-keeping and - update bounds and add equations to the engine. - */ - void applyTrailEntry( TrailEntry &te, bool isDecision = false ); - - /* - Decide and apply a case split using the constraint marked for splitting. - */ - void decide(); - - /* - Decide a constraint's feasible case. Update bounds, add equations - and trail. - */ - void decideSplit( PiecewiseLinearConstraint *constraint ); - - /* - Backtracks fully explored decisions and stores the last feasible decision - */ - bool backtrackToFeasibleDecision( TrailEntry &feasibleDecision ); - - /* - Return to a feasible state and resume search by asserting the next case - (as either a decision or implication) - */ - bool backtrackAndContinueSearch(); - - /* - Pop a stack frame. Return true if successful, false if the stack is empty. - */ - bool popSplit(); - - /* - Pop a context level - lazily backtracking trail, bounds, etc. - Return true if successful, false if the stack is empty. - */ - bool popDecisionLevel( TrailEntry &lastDecision ); - - /* - The current stack depth. - */ - unsigned getDecisionLevel() const; - - /* - Return a list of all splits performed so far, both SMT-originating and - valid ones, in the correct order. - */ - void allSplitsSoFar( List &result ) const; - - /* - Get trail begin iterator. - */ - CVC4::context::CDList::const_iterator trailBegin() const - { - return _trail.begin(); - }; - - /* - Get trail end iterator. - */ - CVC4::context::CDList::const_iterator trailEnd() const - { - return _trail.end(); - }; - - /* - Have the SMT core start reporting statistics. - */ - void setStatistics( Statistics *statistics ); - - /* - Have the SMT core choose, among a set of violated PL constraints, which - constraint should be repaired (without splitting) - */ - PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; - - void setConstraintViolationThreshold( unsigned threshold ); - - inline void setBranchingHeuristics( DivideStrategy strategy ) - { - _branchingHeuristic = strategy; - } - - /* - Pick the piecewise linear constraint for splitting, returns true - if a constraint for splitting is successfully picked - */ - bool pickSplitPLConstraint(); - - /* - * For testing purposes - */ - PiecewiseLinearCaseSplit getDecision( unsigned decisionLevel ) const; - - void reset(); - - /* - For debugging purposes only - store a correct possible solution - TODO: Create a user interface for this - */ - void storeDebuggingSolution( const Map &debuggingSolution ); - bool checkSkewFromDebuggingSolution(); - bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; - void interruptIfCompliantWithDebugSolution(); -private: - /* - Collect and print various statistics. - */ - Statistics *_statistics; - - /* - CVC4 Context, constructed in Engine - */ - CVC4::context::Context &_context; - - /* - Trail is context dependent and contains all the asserted PWLCaseSplits - */ - CVC4::context::CDList _trail; - - /* - * _decisions stores the decision TrailEntries - */ - CVC4::context::CDList _decisions; - - /* - The engine. - */ - IEngine *_engine; - - /* - Do we need to perform a split and on which constraint. - */ - bool _needToSplit; - PiecewiseLinearConstraint *_constraintForSplitting; - - /* - Count how many times each constraint has been violated. - */ - Map _constraintToViolationCount; - - /* - For debugging purposes only - */ - Map _debuggingSolution; - - /* - Split when some relu has been violated for this many times during the - Reluplex procedure - */ - unsigned _constraintViolationThreshold; - - /* - Split when there have been this many rejected phase pattern proposal - during the SoI-based local search. - */ - unsigned _deepSoIRejectionThreshold; - - /* - The strategy to pick the piecewise linear constraint to branch on. - */ - DivideStrategy _branchingHeuristic; - - /* - Heap to store the scores of each PLConstraint. - */ - std::unique_ptr _scoreTracker; - - /* - Number of times the phase pattern proposal has been rejected at the - current search state. - */ - unsigned _numRejectedPhasePatternProposal; - -}; - -#endif // __CDSmtCore_h__ diff --git a/src/engine/DnCWorker.cpp b/src/engine/DnCWorker.cpp index 455a8ef192..8420a8d483 100644 --- a/src/engine/DnCWorker.cpp +++ b/src/engine/DnCWorker.cpp @@ -101,7 +101,7 @@ void DnCWorker::popOneSubQueryAndSolve( bool restoreTreeStates ) bool fullSolveNeeded = true; // denotes whether we need to solve the subquery if ( restoreTreeStates && smtState ) - fullSolveNeeded = _engine->restoreSmtState( *smtState ); + fullSolveNeeded = true; //_engine->restoreSmtState( *smtState ); IEngine::ExitCode result = IEngine::NOT_DONE; if ( fullSolveNeeded ) { @@ -141,7 +141,7 @@ void DnCWorker::popOneSubQueryAndSolve( bool restoreTreeStates ) { newSmtStates.push_back( std::unique_ptr ( new SmtState() ) ); - _engine->storeSmtState( *( newSmtStates[i] ) ); + //_engine->storeSmtState( *( newSmtStates[i] ) ); } } diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 7e4b136133..31834422c2 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -40,7 +40,7 @@ Engine::Engine() , _tableau( _boundManager ) , _preprocessedQuery( nullptr ) , _rowBoundTightener( *_tableau ) - , _smtCore( this ) + , _smtCore( this, _context ) , _numPlConstraintsDisabledByValidSplits( 0 ) , _preprocessingEnabled( false ) , _initialStateStored( false ) @@ -263,7 +263,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) // Perform any SmtCore-initiated case splits if ( _smtCore.needToSplit() ) { - _smtCore.performSplit(); + _smtCore.decide(); splitJustPerformed = true; continue; } @@ -334,7 +334,7 @@ bool Engine::solve( unsigned timeoutInSeconds ) _tableau->toggleOptimization( false ); // The current query is unsat, and we need to pop. // If we're at level 0, the whole query is unsat. - if ( !_smtCore.popSplit() ) + if ( !_smtCore.backtrackAndContinueSearch() ) { struct timespec mainLoopEnd = TimeUtils::sampleMicro(); _statistics.incLongAttribute @@ -1635,39 +1635,39 @@ void Engine::storeState( EngineState &state, TableauStateStorageLevel level ) co state._numPlConstraintsDisabledByValidSplits = _numPlConstraintsDisabledByValidSplits; } -void Engine::restoreState( const EngineState &state ) +void Engine::restoreState( const EngineState &/*state*/ ) { - ENGINE_LOG( "Restore state starting" ); + //ENGINE_LOG( "Restore state starting" ); - if ( state._tableauStateStorageLevel == TableauStateStorageLevel::STORE_NONE ) - throw MarabouError( MarabouError::RESTORING_ENGINE_FROM_INVALID_STATE ); + // if ( state._tableauStateStorageLevel == TableauStateStorageLevel::STORE_NONE ) + // throw MarabouError( MarabouError::RESTORING_ENGINE_FROM_INVALID_STATE ); - ENGINE_LOG( "\tRestoring tableau state" ); - _tableau->restoreState( state._tableauState, - state._tableauStateStorageLevel ); + // ENGINE_LOG( "\tRestoring tableau state" ); + // _tableau->restoreState( state._tableauState, + // state._tableauStateStorageLevel ); - ENGINE_LOG( "\tRestoring constraint states" ); - for ( auto &constraint : _plConstraints ) - { - if ( !state._plConstraintToState.exists( constraint ) ) - throw MarabouError( MarabouError::MISSING_PL_CONSTRAINT_STATE ); + // ENGINE_LOG( "\tRestoring constraint states" ); + // for ( auto &constraint : _plConstraints ) + // { + // if ( !state._plConstraintToState.exists( constraint ) ) + // throw MarabouError( MarabouError::MISSING_PL_CONSTRAINT_STATE ); - constraint->restoreState( state._plConstraintToState[constraint] ); - } + // constraint->restoreState( state._plConstraintToState[constraint] ); + // } - _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; + // _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; - if ( _lpSolverType == LPSolverType::NATIVE ) - { - // Make sure the data structures are initialized to the correct size - _rowBoundTightener->setDimensions(); - adjustWorkMemorySize(); - _activeEntryStrategy->resizeHook( _tableau ); - _costFunctionManager->initialize(); - } + // if ( _lpSolverType == LPSolverType::NATIVE ) + // { + // // Make sure the data structures are initialized to the correct size + // _rowBoundTightener->setDimensions(); + // adjustWorkMemorySize(); + // _activeEntryStrategy->resizeHook( _tableau ); + // _costFunctionManager->initialize(); + //} // Reset the violation counts in the SMT core - _smtCore.resetSplitConditions(); + // _smtCore.resetSplitConditions(); } void Engine::setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints ) @@ -1956,14 +1956,13 @@ bool Engine::applyValidConstraintCaseSplit( PiecewiseLinearConstraint *constrain if ( constraint->isActive() && constraint->phaseFixed() ) { String constraintString; + // This is a performance issue constraint->dump( constraintString ); ENGINE_LOG( Stringf( "A constraint has become valid. Dumping constraint: %s", constraintString.ascii() ).ascii() ); constraint->setActiveConstraint( false ); - PiecewiseLinearCaseSplit validSplit = constraint->getValidCaseSplit(); - _smtCore.recordImpliedValidSplit( validSplit ); - applySplit( validSplit ); + _smtCore.pushImplication( constraint ); if ( _soiManager ) _soiManager->removeCostComponentFromHeuristicCost( constraint ); ++_numPlConstraintsDisabledByValidSplits; @@ -2592,7 +2591,7 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy PiecewiseLinearConstraint *candidatePLConstraint = NULL; if ( strategy == DivideStrategy::PseudoImpact ) { - if ( _smtCore.getStackDepth() > 3 ) + if ( _smtCore.getDecisionLevel() > 3 ) candidatePLConstraint = _smtCore.getConstraintsWithHighestScore(); else if ( _preprocessedQuery->getInputVariables().size() < GlobalConfiguration::INTERVAL_SPLITTING_THRESHOLD ) @@ -2605,7 +2604,7 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy else if ( strategy == DivideStrategy::EarliestReLU ) candidatePLConstraint = pickSplitPLConstraintBasedOnTopology(); else if ( strategy == DivideStrategy::LargestInterval && - ( _smtCore.getStackDepth() % + ( _smtCore.getDecisionLevel() % GlobalConfiguration::INTERVAL_SPLITTING_FREQUENCY == 0 ) ) { @@ -2633,68 +2632,6 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraintSnC( SnCDivideStrategy s return candidatePLConstraint; } -bool Engine::restoreSmtState( SmtState & smtState ) -{ - try - { - ASSERT( _smtCore.getStackDepth() == 0 ); - - // Step 1: all implied valid splits at root - for ( auto &validSplit : smtState._impliedValidSplitsAtRoot ) - { - applySplit( validSplit ); - _smtCore.recordImpliedValidSplit( validSplit ); - } - - tightenBoundsOnConstraintMatrix(); - applyAllBoundTightenings(); - // For debugging purposes - checkBoundCompliancyWithDebugSolution(); - do - performSymbolicBoundTightening(); - while ( applyAllValidConstraintCaseSplits() ); - - // Step 2: replay the stack - for ( auto &stackEntry : smtState._stack ) - { - _smtCore.replaySmtStackEntry( stackEntry ); - // Do all the bound propagation, and set ReLU constraints to inactive (at - // least the one corresponding to the _activeSplit applied above. - tightenBoundsOnConstraintMatrix(); - applyAllBoundTightenings(); - // For debugging purposes - checkBoundCompliancyWithDebugSolution(); - do - performSymbolicBoundTightening(); - while ( applyAllValidConstraintCaseSplits() ); - - } - } - catch ( const InfeasibleQueryException & ) - { - // The current query is unsat, and we need to pop. - // If we're at level 0, the whole query is unsat. - if ( !_smtCore.popSplit() ) - { - if ( _verbosity > 0 ) - { - printf( "\nEngine::solve: UNSAT query\n" ); - _statistics.print(); - } - _exitCode = Engine::UNSAT; - for ( PiecewiseLinearConstraint *p : _plConstraints ) - p->setActiveConstraint( true ); - return false; - } - } - return true; -} - -void Engine::storeSmtState( SmtState & smtState ) -{ - _smtCore.storeSmtState( smtState ); -} - bool Engine::solveWithMILPEncoding( unsigned timeoutInSeconds ) { try diff --git a/src/engine/Engine.h b/src/engine/Engine.h index a18297596d..2c39e71f38 100644 --- a/src/engine/Engine.h +++ b/src/engine/Engine.h @@ -173,17 +173,6 @@ class Engine : public IEngine, public SignalHandler::Signalable */ void setVerbosity( unsigned verbosity ); - /* - Apply the stack to the newly created SmtCore, returns false if UNSAT is - found in this process. - */ - bool restoreSmtState( SmtState &smtState ); - - /* - Store the current stack of the smtCore into smtState - */ - void storeSmtState( SmtState &smtState ); - /* Pick the piecewise linear constraint for splitting */ diff --git a/src/engine/IEngine.h b/src/engine/IEngine.h index 8a5c4c4c1c..4536b2156f 100644 --- a/src/engine/IEngine.h +++ b/src/engine/IEngine.h @@ -72,17 +72,6 @@ class IEngine virtual void restoreState( const EngineState &state ) = 0; virtual void setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints ) = 0; - /* - Store the current stack of the smtCore into smtState - */ - virtual void storeSmtState( SmtState &smtState ) = 0; - - /* - Apply the stack to the newly created SmtCore, returns false if UNSAT is - found in this process. - */ - virtual bool restoreSmtState( SmtState &smtState ) = 0; - /* Solve the encoded query. */ diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 0da2f5be06..a1f8481152 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -2,17 +2,18 @@ /*! \file SmtCore.cpp ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Parth Shah, Duligur Ibeling + ** Guy Katz, Aleksandar Zeljic, Haoze Wu, Parth Shah ** 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 ]] - + ** See the description of the class in SmtCore.h. **/ +#include "SmtCore.h" + #include "Debug.h" #include "DivideStrategy.h" #include "EngineState.h" @@ -21,20 +22,23 @@ #include "IEngine.h" #include "MStringf.h" #include "MarabouError.h" -#include "Options.h" #include "PseudoImpactTracker.h" #include "ReluConstraint.h" -#include "SmtCore.h" -SmtCore::SmtCore( IEngine *engine ) +using namespace CVC4::context; + +SmtCore::SmtCore( IEngine *engine, Context &ctx ) : _statistics( NULL ) + , _context( ctx ) + , _trail( &_context ) + , _decisions( &_context ) , _engine( engine ) - , _context( _engine->getContext() ) , _needToSplit( false ) , _constraintForSplitting( NULL ) - , _stateId( 0 ) - , _constraintViolationThreshold( Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) - , _deepSoIRejectionThreshold( Options::get()->getInt( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) + , _constraintViolationThreshold + ( (unsigned)Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) + , _deepSoIRejectionThreshold( Options::get()->getInt + ( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) , _branchingHeuristic( Options::get()->getDivideStrategy() ) , _scoreTracker( nullptr ) , _numRejectedPhasePatternProposal( 0 ) @@ -43,33 +47,12 @@ SmtCore::SmtCore( IEngine *engine ) SmtCore::~SmtCore() { - freeMemory(); -} - -void SmtCore::freeMemory() -{ - for ( const auto &stackEntry : _stack ) - { - delete stackEntry->_engineState; - delete stackEntry; - } - - _stack.clear(); -} - -void SmtCore::reset() -{ - freeMemory(); - _impliedValidSplitsAtRoot.clear(); - _needToSplit = false; - _constraintForSplitting = NULL; - _stateId = 0; - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; } void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) { + ASSERT( !constraint->phaseFixed() ); + if ( !_constraintToViolationCount.exists( constraint ) ) _constraintToViolationCount[constraint] = 0; @@ -79,10 +62,12 @@ void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) _constraintViolationThreshold ) { _needToSplit = true; - if ( !pickSplitPLConstraint() ) + if ( GlobalConfiguration::SPLITTING_HEURISTICS == + DivideStrategy::ReLUViolation || !pickSplitPLConstraint() ) // If pickSplitConstraint failed to pick one, use the native // relu-violation based splitting heuristic. _constraintForSplitting = constraint; + ASSERT( !_constraintForSplitting->phaseFixed() ); } } @@ -95,17 +80,17 @@ unsigned SmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) co } void SmtCore::initializeScoreTrackerIfNeeded( const - List - &plConstraints ) + List + &plConstraints ) { if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) - { - _scoreTracker = std::unique_ptr - ( new PseudoImpactTracker() ); - _scoreTracker->initialize( plConstraints ); + { + _scoreTracker = std::unique_ptr + ( new PseudoImpactTracker() ); + _scoreTracker->initialize( plConstraints ); - SMT_LOG( "\tTracking Pseudo Impact..." ); - } + SMT_LOG( "\tTracking Pseudo Impact..." ); + } } void SmtCore::reportRejectedPhasePatternProposal() @@ -114,15 +99,13 @@ void SmtCore::reportRejectedPhasePatternProposal() if ( _numRejectedPhasePatternProposal >= _deepSoIRejectionThreshold ) - { - _needToSplit = true; - _engine->applyAllBoundTightenings(); - _engine->applyAllValidConstraintCaseSplits(); - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = _scoreTracker->topUnfixed(); - } + { + _needToSplit = true; + if ( !pickSplitPLConstraint() ) + // If pickSplitConstraint failed to pick one, use the native + // relu-violation based splitting heuristic. + _constraintForSplitting = _scoreTracker->topUnfixed(); + } } bool SmtCore::needToSplit() const @@ -130,24 +113,63 @@ bool SmtCore::needToSplit() const return _needToSplit; } -void SmtCore::performSplit() +void SmtCore::pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ) +{ + SMT_LOG( Stringf( "Decision @ %d )", _context.getLevel() + 1 ).ascii() ); + TrailEntry te( constraint, decision ); + applyTrailEntry( te, true ); + SMT_LOG( Stringf( "Decision push @ %d DONE", _context.getLevel() ).ascii() ); +} + +void SmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) +{ + ASSERT( constraint->isImplication() ); + SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); + TrailEntry te( constraint, constraint->nextFeasibleCase() ); + applyTrailEntry( te, false ); + SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); +} + +void SmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) +{ + if ( isDecision ) + { + _context.push(); + _decisions.push_back( te ); + } + + _trail.push_back( te ); + _engine->applySplit( te.getPiecewiseLinearCaseSplit() ); +} + +void SmtCore::decide() { ASSERT( _needToSplit ); + SMT_LOG( "Performing a ReLU split" ); _numRejectedPhasePatternProposal = 0; // Maybe the constraint has already become inactive - if so, ignore + // TODO: Ideally we will not ever reach this point + // TODO: Maintain a vector of constraints above the threshold + // Iterate until we find an active one if ( !_constraintForSplitting->isActive() ) { _needToSplit = false; _constraintToViolationCount[_constraintForSplitting] = 0; - _constraintForSplitting = NULL; + _constraintForSplitting = nullptr; return; } - struct timespec start = TimeUtils::sampleMicro(); - ASSERT( _constraintForSplitting->isActive() ); _needToSplit = false; + _constraintForSplitting->setActiveConstraint( false ); + + decideSplit( _constraintForSplitting ); +} + +void SmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) +{ + struct timespec start = TimeUtils::sampleMicro(); if ( _statistics ) { @@ -155,60 +177,34 @@ void SmtCore::performSplit() _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); } - // Before storing the state of the engine, we: - // 1. Obtain the splits. - // 2. Disable the constraint, so that it is marked as disbaled in the EngineState. - List splits = _constraintForSplitting->getCaseSplits(); - ASSERT( !splits.empty() ); - ASSERT( splits.size() >= 2 ); // Not really necessary, can add code to handle this case. - _constraintForSplitting->setActiveConstraint( false ); - - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_BOUNDS_ONLY ); - _engine->preContextPushHook(); - pushContext(); - SmtStackEntry *stackEntry = new SmtStackEntry; - // Perform the first split: add bounds and equations - List::iterator split = splits.begin(); - ASSERT( split->getEquations().size() == 0 ); - _engine->applySplit( *split ); - stackEntry->_activeSplit = *split; - - // Store the remaining splits on the stack, for later - stackEntry->_engineState = stateBeforeSplits; - ++split; - while ( split != splits.end() ) - { - stackEntry->_alternativeSplits.append( *split ); - ++split; - } + if ( !constraint->isFeasible() ) + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + ASSERT( constraint->isFeasible() ); + ASSERT( !constraint->isImplication() ); - _stack.append( stackEntry ); + PhaseStatus decision = constraint->nextFeasibleCase(); + pushDecision( constraint, decision ); if ( _statistics ) { - unsigned level = getStackDepth(); + unsigned level = _context.getLevel(); _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, level ); if ( level > _statistics->getUnsignedAttribute ( Statistics::MAX_DECISION_LEVEL ) ) _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, level ); + struct timespec end = TimeUtils::sampleMicro(); _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); } - - _constraintForSplitting = NULL; + SMT_LOG( "Performing a ReLU split - DONE" ); } -unsigned SmtCore::getStackDepth() const + +unsigned SmtCore::getDecisionLevel() const { - ASSERT( _stack.size() == static_cast( _context.getLevel() ) ); - return _stack.size(); + return _decisions.size(); } void SmtCore::popContext() @@ -238,85 +234,83 @@ void SmtCore::pushContext() } bool SmtCore::popSplit() +bool SmtCore::popDecisionLevel( TrailEntry &lastDecision ) { - SMT_LOG( "Performing a pop" ); - - if ( _stack.empty() ) + //ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); + if ( _decisions.empty() ) return false; - struct timespec start = TimeUtils::sampleMicro(); + SMT_LOG( "Popping trail ..." ); + lastDecision = _decisions.back(); + _context.pop(); + _engine->postContextPopHook(); + SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() ); + return true; +} - if ( _statistics ) +void SmtCore::interruptIfCompliantWithDebugSolution() +{ + if ( checkSkewFromDebuggingSolution() ) { - _statistics->incUnsignedAttribute( Statistics::NUM_POPS ); - // A pop always sends us to a state that we haven't seen before - whether - // from a sibling split, or from a lower level of the tree. - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); + SMT_LOG( "Error! Popping from a compliant stack\n" ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); } +} - bool inconsistent = true; - while ( inconsistent ) - { - // Remove any entries that have no alternatives - String error; - while ( _stack.back()->_alternativeSplits.empty() ) - { - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } +PiecewiseLinearCaseSplit SmtCore::getDecision( unsigned decisionLevel ) const +{ + ASSERT( decisionLevel <= getDecisionLevel() ); + ASSERT( decisionLevel > 0 ); + return _decisions[decisionLevel - 1].getPiecewiseLinearCaseSplit(); +} - delete _stack.back()->_engineState; - delete _stack.back(); - _stack.popBack(); - popContext(); +bool SmtCore::backtrackToFeasibleDecision( TrailEntry &lastDecision ) +{ + SMT_LOG( "Backtracking to a feasible decision..." ); + if ( getDecisionLevel() == 0 ) + return false; - if ( _stack.empty() ) - return false; - } + popDecisionLevel( lastDecision ); + lastDecision.markInfeasible(); - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } + while ( !lastDecision.isFeasible() ) + { + interruptIfCompliantWithDebugSolution(); + + if ( !popDecisionLevel( lastDecision ) ) + return false; - SmtStackEntry *stackEntry = _stack.back(); + lastDecision.markInfeasible(); + } - popContext(); - _engine->postContextPopHook(); - // Restore the state of the engine - SMT_LOG( "\tRestoring engine state..." ); - _engine->restoreState( *( stackEntry->_engineState ) ); - SMT_LOG( "\tRestoring engine state - DONE" ); + interruptIfCompliantWithDebugSolution(); - // Apply the new split and erase it from the list - auto split = stackEntry->_alternativeSplits.begin(); + return true; +} + +bool SmtCore::backtrackAndContinueSearch() +{ + TrailEntry feasibleDecision( nullptr, CONSTRAINT_INFEASIBLE ); + struct timespec start = TimeUtils::sampleMicro(); - // Erase any valid splits that were learned using the split we just - // popped - stackEntry->_impliedValidSplits.clear(); + if ( !backtrackToFeasibleDecision( feasibleDecision ) ) + return false; - SMT_LOG( "\tApplying new split..." ); - ASSERT( split->getEquations().size() == 0 ); - _engine->preContextPushHook(); - pushContext(); - _engine->applySplit( *split ); - SMT_LOG( "\tApplying new split - DONE" ); + ASSERT( feasibleDecision.isFeasible() ); - stackEntry->_activeSplit = *split; - stackEntry->_alternativeSplits.erase( split ); + if ( _statistics ) + _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - inconsistent = !_engine->consistentBounds(); - } + PiecewiseLinearConstraint *pwlc = feasibleDecision._pwlConstraint; + if ( pwlc->isImplication() ) + pushImplication( pwlc ); + else + decideSplit( pwlc ); if ( _statistics ) { - unsigned level = getStackDepth(); + unsigned level = _context.getLevel(); _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, level ); if ( level > _statistics->getUnsignedAttribute @@ -328,40 +322,22 @@ bool SmtCore::popSplit() } checkSkewFromDebuggingSolution(); - return true; } -void SmtCore::resetSplitConditions() +void SmtCore::resetReportedViolations() { _constraintToViolationCount.clear(); _numRejectedPhasePatternProposal = 0; _needToSplit = false; } -void SmtCore::recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ) -{ - if ( _stack.empty() ) - _impliedValidSplitsAtRoot.append( validSplit ); - else - _stack.back()->_impliedValidSplits.append( validSplit ); - - checkSkewFromDebuggingSolution(); -} - void SmtCore::allSplitsSoFar( List &result ) const { result.clear(); - for ( const auto &it : _impliedValidSplitsAtRoot ) - result.append( it ); - - for ( const auto &it : _stack ) - { - result.append( it->_activeSplit ); - for ( const auto &impliedSplit : it->_impliedValidSplits ) - result.append( impliedSplit ); - } + for ( auto trailEntry : _trail ) + result.append( trailEntry.getPiecewiseLinearCaseSplit() ); } void SmtCore::setStatistics( Statistics *statistics ) @@ -383,41 +359,47 @@ bool SmtCore::checkSkewFromDebuggingSolution() String error; + int decisionLevel = 0; + bool isDecision = false; // First check that the valid splits implied at the root level are okay - for ( const auto &split : _impliedValidSplitsAtRoot ) + for ( const auto &trailEntry : _trail ) { - if ( !splitAllowsStoredSolution( split, error ) ) + if ( trailEntry._pwlConstraint != _decisions[decisionLevel]._pwlConstraint ) + isDecision = false; + else { - printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + ASSERT( trailEntry._phase == _decisions[decisionLevel]._phase ); + isDecision = true; + ++decisionLevel; } - } - // Now go over the stack from oldest to newest and check that each level is compliant - for ( const auto &stackEntry : _stack ) - { - // If the active split is non-compliant but there are alternatives, that's fine - if ( !splitAllowsStoredSolution( stackEntry->_activeSplit, error ) ) + PiecewiseLinearCaseSplit caseSplit = trailEntry.getPiecewiseLinearCaseSplit(); + if ( decisionLevel == 0 ) { - if ( stackEntry->_alternativeSplits.empty() ) + if ( !splitAllowsStoredSolution( caseSplit, error ) ) { - printf( "Error! Have a split that is non-compliant with the stored solution, " - "without alternatives:\n\t%s\n", error.ascii() ); + printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); throw MarabouError( MarabouError::DEBUGGING_ERROR ); } - - // Active split is non-compliant but this is fine, because there are alternatives. We're done. - return false; } - - // Did we learn any valid splits that are non-compliant? - for ( auto const &split : stackEntry->_impliedValidSplits ) + else { - if ( !splitAllowsStoredSolution( split, error ) ) + // If the active split is non-compliant but there are alternatives, + // i.e. it was a decision, that's fine + if ( isDecision && !splitAllowsStoredSolution( caseSplit, error ) ) { - printf( "Error with one of the splits implied at this stack level:\n\t%s\n", - error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + // Active split is non-compliant but this is fine, because there + // are alternatives. We're done. + return false; + } + else // Implied split + { + if ( !splitAllowsStoredSolution( caseSplit, error ) ) + { + printf( "Error with one of the splits implied at this stack level:\n\t%s\n", + error.ascii() ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } } } } @@ -433,7 +415,7 @@ bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, if ( _debuggingSolution.empty() ) return true; - for ( const auto &bound : split.getBoundTightenings() ) + for ( const auto bound : split.getBoundTightenings() ) { unsigned variable = bound._variable; @@ -467,6 +449,11 @@ bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, return true; } +void SmtCore::setConstraintViolationThreshold( unsigned threshold ) +{ + _constraintViolationThreshold = threshold; +} + PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const { ASSERT( !_violatedPlConstraints.empty() ); @@ -500,61 +487,20 @@ PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( ListincUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_ENTIRE_TABLEAU_STATE ); - stackEntry->_engineState = stateBeforeSplits; - - // Apply all the splits - _engine->applySplit( stackEntry->_activeSplit ); - for ( const auto &impliedSplit : stackEntry->_impliedValidSplits ) - _engine->applySplit( impliedSplit ); - - _stack.append( stackEntry ); - - if ( _statistics ) - { - unsigned level = getStackDepth(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } -} - -void SmtCore::storeSmtState( SmtState &smtState ) -{ - smtState._impliedValidSplitsAtRoot = _impliedValidSplitsAtRoot; - - for ( auto &stackEntry : _stack ) - smtState._stack.append( stackEntry->duplicateSmtStackEntry() ); - - smtState._stateId = _stateId; -} - bool SmtCore::pickSplitPLConstraint() { if ( _needToSplit ) - { _constraintForSplitting = _engine->pickSplitPLConstraint ( _branchingHeuristic ); - } return _constraintForSplitting != NULL; } + +void SmtCore::reset() +{ + _context.popto( 0 ); + _engine->postContextPopHook(); + _needToSplit = false; + _constraintForSplitting = NULL; + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; +} diff --git a/src/engine/SmtCore.h b/src/engine/SmtCore.h index db39ffa498..4e1aac1748 100644 --- a/src/engine/SmtCore.h +++ b/src/engine/SmtCore.h @@ -2,44 +2,90 @@ /*! \file SmtCore.h ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Parth Shah + ** Guy Katz, AleksandarZeljic, Haoze Wu, Parth Shah ** 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 ]] - -**/ + ** The SmtCore class implements a context-dependent SmtCore class. + ** The SmtCore distinguishes between: **decisions** and **implications**. + ** + ** Decision is a case of PiecewiseLinearConstraint asserted on the trail. + ** A decision is a choice between multiple feasible cases of a + ** PiecewiseLinearConstraint and represents nodes in the search tree. + ** + ** Implication is the last feasible case of a PiecewiseLinearConstraint and as + ** soon as it is detected it is asserted on the trail. + ** + ** Case splitting on a PiecewiseLinearConstraint performs a decision. + ** Fixing a case of a PiecewiseLinearConstraint (e.g., via bound propagation or + ** by exhausting all other cases) performs an implication. + ** + ** The overall search state is stored in a distributed way: + ** - SmtCore::_trail is the current search state in a chronological order + ** - PiecewiseLinearConstraints' infeasible cases enumerate all the explored + ** states w.r.t to the chronological order on the _trail. + ** + ** _trail is a chronological list of cases of PiecewiseLinearConstraints + ** asserted to hold (as TrailEntries) - both decisions and implications. + ** _decisions is a chronological list of decisions stored on the trail. + ** _trail and _decisions are both context dependent and will synchronize in + ** unison with the _context object. + ** + ** When a search state is found to be infeasible, SmtCore backtracks to the + ** last decision and continues the search. + ** + ** PushDecision advances the decision level and context level. + ** popDecisionLevel backtracks the last decision and context level. + ** + ** Advancing a context level creates a synchronization point to which all + ** context dependent members can backtrack in unison. + ** Backtracking a context level restores all context dependent members to the + ** state of the last synchronization point. This operation is O(1) complexity. + ** + ** Since the entire search state is context dependent, backtracking the context + ** (via popDecisionLevel) backtracks the entire Marabou search state. + ** The only exception is the labeling of basic/non-basic variables in the + ** tableau, which may need to be recalculated using Tableau's + ** postContextPopHook exposed via Engine. + ** + ** Implementation relies on: + ** + ** - _context is a unique Context object from which all the context-dependent + ** structures are obtained. + ** + ** - PiecewiseLinearConstraint class stores its search state in a + ** context-dependent manner and exposes it using nextFeasibleCase() and + ** markInfeasible() methods. + ** + ** - Using BoundManager class to store bounds in a context-dependent manner + **/ #ifndef __SmtCore_h__ #define __SmtCore_h__ -#include "DivideStrategy.h" +#include "Options.h" #include "PiecewiseLinearCaseSplit.h" #include "PiecewiseLinearConstraint.h" #include "PLConstraintScoreTracker.h" -#include "SmtState.h" #include "Stack.h" -#include "SmtStackEntry.h" #include "Statistics.h" +#include "TrailEntry.h" +#include "context/cdlist.h" #include "context/context.h" -#include - #define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "SmtCore: %s\n", x ) class EngineState; -class IEngine; +class Engine; class String; -using CVC4::context::Context; - class SmtCore { public: - SmtCore( IEngine *engine ); + SmtCore( IEngine *engine, CVC4::context::Context &context ); ~SmtCore(); /* @@ -47,11 +93,6 @@ class SmtCore */ void freeMemory(); - /* - Reset the SmtCore - */ - void reset(); - /* Initialize the score tracker with the given list of pl constraints. */ @@ -90,13 +131,12 @@ class SmtCore Get the number of times a specific PL constraint has been reported as violated. */ - unsigned getViolationCounts( PiecewiseLinearConstraint* constraint ) const; + unsigned getViolationCounts( PiecewiseLinearConstraint *constraint ) const; /* - Reset all reported violation counts and the number of rejected SoI - phase pattern proposal. + Reset all reported violation counts. */ - void resetSplitConditions(); + void resetReportedViolations(); /* Returns true iff the SMT core wants to perform a case split. @@ -104,44 +144,81 @@ class SmtCore bool needToSplit() const; /* - Perform the split according to the constraint marked for - splitting. Update bounds, add equations and update the stack. + Push TrailEntry representing the decision onto the trail. + */ + void pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus decision ); + + /* + Inform SmtCore of an implied (formerly valid) case split that was discovered. */ - void performSplit(); + void pushImplication( PiecewiseLinearConstraint *constraint ); /* - Pop an old split from the stack, and perform a new split as - needed. Return true if successful, false if the stack is empty. + Pushes trail entry onto trail, handles decision book-keeping and + update bounds and add equations to the engine. + */ + void applyTrailEntry( TrailEntry &te, bool isDecision = false ); + + /* + Decide and apply a case split using the constraint marked for splitting. */ - bool popSplit(); + void decide(); /* - Pop _context, record statistics + Decide a constraint's feasible case. Update bounds, add equations + and trail. */ - void popContext(); + void decideSplit( PiecewiseLinearConstraint *constraint ); /* - Push _context, record statistics + Backtracks fully explored decisions and stores the last feasible decision */ - void pushContext(); + bool backtrackToFeasibleDecision( TrailEntry &feasibleDecision ); + /* + Return to a feasible state and resume search by asserting the next case + (as either a decision or implication) + */ + bool backtrackAndContinueSearch(); /* - The current stack depth. + Pop a stack frame. Return true if successful, false if the stack is empty. + */ + bool popSplit(); + + /* + Pop a context level - lazily backtracking trail, bounds, etc. + Return true if successful, false if the stack is empty. */ - unsigned getStackDepth() const; + bool popDecisionLevel( TrailEntry &lastDecision ); /* - Let the smt core know of an implied valid case split that was discovered. + The current stack depth. */ - void recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ); + unsigned getDecisionLevel() const; /* - Return a list of all splits performed so far, both SMT-originating and valid ones, - in the correct order. + Return a list of all splits performed so far, both SMT-originating and + valid ones, in the correct order. */ void allSplitsSoFar( List &result ) const; + /* + Get trail begin iterator. + */ + CVC4::context::CDList::const_iterator trailBegin() const + { + return _trail.begin(); + }; + + /* + Get trail end iterator. + */ + CVC4::context::CDList::const_iterator trailEnd() const + { + return _trail.end(); + }; + /* Have the SMT core start reporting statistics. */ @@ -153,59 +230,60 @@ class SmtCore */ PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; + void setConstraintViolationThreshold( unsigned threshold ); + inline void setBranchingHeuristics( DivideStrategy strategy ) { _branchingHeuristic = strategy; } - /* - Replay a stackEntry - */ - void replaySmtStackEntry( SmtStackEntry *stackEntry ); - - /* - Store the current state of the SmtCore into smtState - */ - void storeSmtState( SmtState &smtState ); - /* Pick the piecewise linear constraint for splitting, returns true if a constraint for splitting is successfully picked */ bool pickSplitPLConstraint(); + /* + * For testing purposes + */ + PiecewiseLinearCaseSplit getDecision( unsigned decisionLevel ) const; + + void reset(); + /* For debugging purposes only - store a correct possible solution + TODO: Create a user interface for this */ void storeDebuggingSolution( const Map &debuggingSolution ); bool checkSkewFromDebuggingSolution(); bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; - + void interruptIfCompliantWithDebugSolution(); private: /* - Valid splits that were implied by level 0 of the stack. + Collect and print various statistics. */ - List _impliedValidSplitsAtRoot; + Statistics *_statistics; /* - Collect and print various statistics. + CVC4 Context, constructed in Engine */ - Statistics *_statistics; + CVC4::context::Context &_context; /* - The case-split stack. + Trail is context dependent and contains all the asserted PWLCaseSplits */ - List _stack; + CVC4::context::CDList _trail; + + /* + * _decisions stores the decision TrailEntries + */ + CVC4::context::CDList _decisions; /* The engine. */ IEngine *_engine; - /* - Context for synchronizing the search. - */ - Context &_context; /* Do we need to perform a split and on which constraint. */ @@ -222,12 +300,6 @@ class SmtCore */ Map _debuggingSolution; - /* - A unique ID allocated to every state that is stored, for - debugging purposes. - */ - unsigned _stateId; - /* Split when some relu has been violated for this many times during the Reluplex procedure @@ -255,14 +327,7 @@ class SmtCore current search state. */ unsigned _numRejectedPhasePatternProposal; + }; #endif // __SmtCore_h__ - -// -// Local Variables: -// compile-command: "make -C ../.. " -// tags-file-name: "../../TAGS" -// c-basic-offset: 4 -// End: -// diff --git a/src/engine/oldSmtCore b/src/engine/oldSmtCore new file mode 100644 index 0000000000..416268a11e --- /dev/null +++ b/src/engine/oldSmtCore @@ -0,0 +1,257 @@ +/********************* */ +/*! \file SmtCore.h + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz, Parth Shah + ** 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 ]] + +**/ + +#ifndef __SmtCore_h__ +#define __SmtCore_h__ + +#include "DivideStrategy.h" +#include "PiecewiseLinearCaseSplit.h" +#include "PiecewiseLinearConstraint.h" +#include "PLConstraintScoreTracker.h" +#include "SmtState.h" +#include "Stack.h" +#include "SmtStackEntry.h" +#include "Statistics.h" +#include "context/context.h" + +#include + +#define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "SmtCore: %s\n", x ) + +class EngineState; +class IEngine; +class String; + +using CVC4::context::Context; + +class SmtCore +{ +public: + SmtCore( IEngine *engine ); + ~SmtCore(); + + /* + Clear the stack. + */ + void freeMemory(); + + /* + Reset the SmtCore + */ + void reset(); + + /* + Initialize the score tracker with the given list of pl constraints. + */ + void initializeScoreTrackerIfNeeded( const List + &plConstraints ); + + /* + Inform the SMT core that a SoI phase pattern proposal is rejected. + */ + void reportRejectedPhasePatternProposal(); + + /* + Update the score of the constraint with the given score in the costTracker. + */ + inline void updatePLConstraintScore( PiecewiseLinearConstraint *constraint, + double score ) + { + ASSERT( _scoreTracker != nullptr ); + _scoreTracker->updateScore( constraint, score ); + } + + /* + Get the constraint in the score tracker with the highest score + */ + inline PiecewiseLinearConstraint *getConstraintsWithHighestScore() const + { + return _scoreTracker->topUnfixed(); + } + + /* + Inform the SMT core that a PL constraint is violated. + */ + void reportViolatedConstraint( PiecewiseLinearConstraint *constraint ); + + /* + Get the number of times a specific PL constraint has been reported as + violated. + */ + unsigned getViolationCounts( PiecewiseLinearConstraint* constraint ) const; + + /* + Reset all reported violation counts and the number of rejected SoI + phase pattern proposal. + */ + void resetSplitConditions(); + + /* + Returns true iff the SMT core wants to perform a case split. + */ + bool needToSplit() const; + + /* + Perform the split according to the constraint marked for + splitting. Update bounds, add equations and update the stack. + */ + void performSplit(); + + /* + Pop an old split from the stack, and perform a new split as + needed. Return true if successful, false if the stack is empty. + */ + bool popSplit(); + + /* + The current stack depth. + */ + unsigned getStackDepth() const; + + /* + Let the smt core know of an implied valid case split that was discovered. + */ + void recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ); + + /* + Return a list of all splits performed so far, both SMT-originating and valid ones, + in the correct order. + */ + void allSplitsSoFar( List &result ) const; + + /* + Have the SMT core start reporting statistics. + */ + void setStatistics( Statistics *statistics ); + + /* + Have the SMT core choose, among a set of violated PL constraints, which + constraint should be repaired (without splitting) + */ + PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; + + inline void setBranchingHeuristics( DivideStrategy strategy ) + { + _branchingHeuristic = strategy; + } + + /* + Replay a stackEntry + */ + void replaySmtStackEntry( SmtStackEntry *stackEntry ); + + /* + Store the current state of the SmtCore into smtState + */ + void storeSmtState( SmtState &smtState ); + + /* + Pick the piecewise linear constraint for splitting, returns true + if a constraint for splitting is successfully picked + */ + bool pickSplitPLConstraint(); + + /* + For debugging purposes only - store a correct possible solution + */ + void storeDebuggingSolution( const Map &debuggingSolution ); + bool checkSkewFromDebuggingSolution(); + bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; + +private: + /* + Valid splits that were implied by level 0 of the stack. + */ + List _impliedValidSplitsAtRoot; + + /* + Collect and print various statistics. + */ + Statistics *_statistics; + + /* + The case-split stack. + */ + List _stack; + + /* + The engine. + */ + IEngine *_engine; + + /* + Context for synchronizing the search. + */ + Context &_context; + /* + Do we need to perform a split and on which constraint. + */ + bool _needToSplit; + PiecewiseLinearConstraint *_constraintForSplitting; + + /* + Count how many times each constraint has been violated. + */ + Map _constraintToViolationCount; + + /* + For debugging purposes only + */ + Map _debuggingSolution; + + /* + A unique ID allocated to every state that is stored, for + debugging purposes. + */ + unsigned _stateId; + + /* + Split when some relu has been violated for this many times during the + Reluplex procedure + */ + unsigned _constraintViolationThreshold; + + /* + Split when there have been this many rejected phase pattern proposal + during the SoI-based local search. + */ + unsigned _deepSoIRejectionThreshold; + + /* + The strategy to pick the piecewise linear constraint to branch on. + */ + DivideStrategy _branchingHeuristic; + + /* + Heap to store the scores of each PLConstraint. + */ + std::unique_ptr _scoreTracker; + + /* + Number of times the phase pattern proposal has been rejected at the + current search state. + */ + unsigned _numRejectedPhasePatternProposal; +}; + +#endif // __SmtCore_h__ + +// +// Local Variables: +// compile-command: "make -C ../.. " +// tags-file-name: "../../TAGS" +// c-basic-offset: 4 +// End: +// diff --git a/src/engine/oldSmtCoreCpp b/src/engine/oldSmtCoreCpp new file mode 100644 index 0000000000..6d14b14e5b --- /dev/null +++ b/src/engine/oldSmtCoreCpp @@ -0,0 +1,533 @@ +/********************* */ +/*! \file SmtCore.cpp + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz, Parth Shah, Duligur Ibeling + ** 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 "Debug.h" +#include "DivideStrategy.h" +#include "EngineState.h" +#include "FloatUtils.h" +#include "GlobalConfiguration.h" +#include "IEngine.h" +#include "MStringf.h" +#include "MarabouError.h" +#include "Options.h" +#include "PseudoImpactTracker.h" +#include "ReluConstraint.h" +#include "SmtCore.h" + +SmtCore::SmtCore( IEngine *engine ) + : _statistics( NULL ) + , _engine( engine ) + , _context( _engine->getContext() ) + , _needToSplit( false ) + , _constraintForSplitting( NULL ) + , _stateId( 0 ) + , _constraintViolationThreshold( Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) + , _deepSoIRejectionThreshold( Options::get()->getInt( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) + , _branchingHeuristic( Options::get()->getDivideStrategy() ) + , _scoreTracker( nullptr ) + , _numRejectedPhasePatternProposal( 0 ) +{ +} + +SmtCore::~SmtCore() +{ + freeMemory(); +} + +void SmtCore::freeMemory() +{ + for ( const auto &stackEntry : _stack ) + { + delete stackEntry->_engineState; + delete stackEntry; + } + + _stack.clear(); +} + +void SmtCore::reset() +{ + freeMemory(); + _impliedValidSplitsAtRoot.clear(); + _needToSplit = false; + _constraintForSplitting = NULL; + _stateId = 0; + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; +} + +void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) +{ + if ( !_constraintToViolationCount.exists( constraint ) ) + _constraintToViolationCount[constraint] = 0; + + ++_constraintToViolationCount[constraint]; + + if ( _constraintToViolationCount[constraint] >= + _constraintViolationThreshold ) + { + _needToSplit = true; + if ( !pickSplitPLConstraint() ) + // If pickSplitConstraint failed to pick one, use the native + // relu-violation based splitting heuristic. + _constraintForSplitting = constraint; + } +} + +unsigned SmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) const +{ + if ( !_constraintToViolationCount.exists( constraint ) ) + return 0; + + return _constraintToViolationCount[constraint]; +} + +void SmtCore::initializeScoreTrackerIfNeeded( const + List + &plConstraints ) +{ + if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) + { + _scoreTracker = std::unique_ptr + ( new PseudoImpactTracker() ); + _scoreTracker->initialize( plConstraints ); + + SMT_LOG( "\tTracking Pseudo Impact..." ); + } +} + +void SmtCore::reportRejectedPhasePatternProposal() +{ + ++_numRejectedPhasePatternProposal; + + if ( _numRejectedPhasePatternProposal >= + _deepSoIRejectionThreshold ) + { + _needToSplit = true; + _engine->applyAllBoundTightenings(); + _engine->applyAllValidConstraintCaseSplits(); + if ( !pickSplitPLConstraint() ) + // If pickSplitConstraint failed to pick one, use the native + // relu-violation based splitting heuristic. + _constraintForSplitting = _scoreTracker->topUnfixed(); + } +} + +bool SmtCore::needToSplit() const +{ + return _needToSplit; +} + +void SmtCore::performSplit() +{ + ASSERT( _needToSplit ); + + _numRejectedPhasePatternProposal = 0; + // Maybe the constraint has already become inactive - if so, ignore + if ( !_constraintForSplitting->isActive() ) + { + _needToSplit = false; + _constraintToViolationCount[_constraintForSplitting] = 0; + _constraintForSplitting = NULL; + return; + } + + struct timespec start = TimeUtils::sampleMicro(); + + ASSERT( _constraintForSplitting->isActive() ); + _needToSplit = false; + + if ( _statistics ) + { + _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); + _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); + } + + // Before storing the state of the engine, we: + // 1. Obtain the splits. + // 2. Disable the constraint, so that it is marked as disbaled in the EngineState. + List splits = _constraintForSplitting->getCaseSplits(); + ASSERT( !splits.empty() ); + ASSERT( splits.size() >= 2 ); // Not really necessary, can add code to handle this case. + _constraintForSplitting->setActiveConstraint( false ); + + // Obtain the current state of the engine + EngineState *stateBeforeSplits = new EngineState; + stateBeforeSplits->_stateId = _stateId; + ++_stateId; + _engine->storeState( *stateBeforeSplits, + TableauStateStorageLevel::STORE_BOUNDS_ONLY ); + _engine->preContextPushHook(); + _context.push(); + SmtStackEntry *stackEntry = new SmtStackEntry; + // Perform the first split: add bounds and equations + List::iterator split = splits.begin(); + ASSERT( split->getEquations().size() == 0 ); + _engine->applySplit( *split ); + stackEntry->_activeSplit = *split; + + // Store the remaining splits on the stack, for later + stackEntry->_engineState = stateBeforeSplits; + ++split; + while ( split != splits.end() ) + { + stackEntry->_alternativeSplits.append( *split ); + ++split; + } + + _stack.append( stackEntry ); + + if ( _statistics ) + { + unsigned level = getStackDepth(); + _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, + level ); + if ( level > _statistics->getUnsignedAttribute + ( Statistics::MAX_DECISION_LEVEL ) ) + _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, + level ); + struct timespec end = TimeUtils::sampleMicro(); + _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); + } + + _constraintForSplitting = NULL; +} + +unsigned SmtCore::getStackDepth() const +{ + ASSERT( _stack.size() == static_cast( _context.getLevel() ) ); + return _stack.size(); +} + +bool SmtCore::popSplit() +{ + SMT_LOG( "Performing a pop" ); + + if ( _stack.empty() ) + return false; + + struct timespec start = TimeUtils::sampleMicro(); + + if ( _statistics ) + { + _statistics->incUnsignedAttribute( Statistics::NUM_POPS ); + // A pop always sends us to a state that we haven't seen before - whether + // from a sibling split, or from a lower level of the tree. + _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); + } + + bool inconsistent = true; + while ( inconsistent ) + { + // Remove any entries that have no alternatives + String error; + while ( _stack.back()->_alternativeSplits.empty() ) + { + if ( checkSkewFromDebuggingSolution() ) + { + // Pops should not occur from a compliant stack! + printf( "Error! Popping from a compliant stack\n" ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } + + delete _stack.back()->_engineState; + delete _stack.back(); + _stack.popBack(); + _context.pop(); + + if ( _stack.empty() ) + return false; + } + + if ( checkSkewFromDebuggingSolution() ) + { + // Pops should not occur from a compliant stack! + printf( "Error! Popping from a compliant stack\n" ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } + + SmtStackEntry *stackEntry = _stack.back(); + + _context.pop(); + _engine->postContextPopHook(); + // Restore the state of the engine + SMT_LOG( "\tRestoring engine state..." ); + _engine->restoreState( *( stackEntry->_engineState ) ); + SMT_LOG( "\tRestoring engine state - DONE" ); + + // Apply the new split and erase it from the list + auto split = stackEntry->_alternativeSplits.begin(); + + // Erase any valid splits that were learned using the split we just + // popped + stackEntry->_impliedValidSplits.clear(); + + SMT_LOG( "\tApplying new split..." ); + ASSERT( split->getEquations().size() == 0 ); + _engine->preContextPushHook(); + _context.push(); + _engine->applySplit( *split ); + SMT_LOG( "\tApplying new split - DONE" ); + + stackEntry->_activeSplit = *split; + stackEntry->_alternativeSplits.erase( split ); + + inconsistent = !_engine->consistentBounds(); + } + + if ( _statistics ) + { + unsigned level = getStackDepth(); + _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, + level ); + if ( level > _statistics->getUnsignedAttribute + ( Statistics::MAX_DECISION_LEVEL ) ) + _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, + level ); + struct timespec end = TimeUtils::sampleMicro(); + _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); + } + + checkSkewFromDebuggingSolution(); + + return true; +} + +void SmtCore::resetSplitConditions() +{ + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; + _needToSplit = false; +} + +void SmtCore::recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ) +{ + if ( _stack.empty() ) + _impliedValidSplitsAtRoot.append( validSplit ); + else + _stack.back()->_impliedValidSplits.append( validSplit ); + + checkSkewFromDebuggingSolution(); +} + +void SmtCore::allSplitsSoFar( List &result ) const +{ + result.clear(); + + for ( const auto &it : _impliedValidSplitsAtRoot ) + result.append( it ); + + for ( const auto &it : _stack ) + { + result.append( it->_activeSplit ); + for ( const auto &impliedSplit : it->_impliedValidSplits ) + result.append( impliedSplit ); + } +} + +void SmtCore::setStatistics( Statistics *statistics ) +{ + _statistics = statistics; +} + +void SmtCore::storeDebuggingSolution( const Map &debuggingSolution ) +{ + _debuggingSolution = debuggingSolution; +} + +// Return true if stack is currently compliant, false otherwise +// If there is no stored solution, return false --- incompliant. +bool SmtCore::checkSkewFromDebuggingSolution() +{ + if ( _debuggingSolution.empty() ) + return false; + + String error; + + // First check that the valid splits implied at the root level are okay + for ( const auto &split : _impliedValidSplitsAtRoot ) + { + if ( !splitAllowsStoredSolution( split, error ) ) + { + printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } + } + + // Now go over the stack from oldest to newest and check that each level is compliant + for ( const auto &stackEntry : _stack ) + { + // If the active split is non-compliant but there are alternatives, that's fine + if ( !splitAllowsStoredSolution( stackEntry->_activeSplit, error ) ) + { + if ( stackEntry->_alternativeSplits.empty() ) + { + printf( "Error! Have a split that is non-compliant with the stored solution, " + "without alternatives:\n\t%s\n", error.ascii() ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } + + // Active split is non-compliant but this is fine, because there are alternatives. We're done. + return false; + } + + // Did we learn any valid splits that are non-compliant? + for ( auto const &split : stackEntry->_impliedValidSplits ) + { + if ( !splitAllowsStoredSolution( split, error ) ) + { + printf( "Error with one of the splits implied at this stack level:\n\t%s\n", + error.ascii() ); + throw MarabouError( MarabouError::DEBUGGING_ERROR ); + } + } + } + + // No problems were detected, the stack is compliant with the stored solution + return true; +} + +bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const +{ + // False if the split prevents one of the values in the stored solution, true otherwise. + error = ""; + if ( _debuggingSolution.empty() ) + return true; + + for ( const auto &bound : split.getBoundTightenings() ) + { + unsigned variable = bound._variable; + + // If the possible solution doesn't care about this variable, + // ignore it + if ( !_debuggingSolution.exists( variable ) ) + continue; + + // Otherwise, check that the bound is consistent with the solution + double solutionValue = _debuggingSolution[variable]; + double boundValue = bound._value; + + if ( ( bound._type == Tightening::LB ) && FloatUtils::gt( boundValue, solutionValue ) ) + { + error = Stringf( "Variable %u: new LB is %.5lf, which contradicts possible solution %.5lf", + variable, + boundValue, + solutionValue ); + return false; + } + else if ( ( bound._type == Tightening::UB ) && FloatUtils::lt( boundValue, solutionValue ) ) + { + error = Stringf( "Variable %u: new UB is %.5lf, which contradicts possible solution %.5lf", + variable, + boundValue, + solutionValue ); + return false; + } + } + + return true; +} + +PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const +{ + ASSERT( !_violatedPlConstraints.empty() ); + + if ( !GlobalConfiguration::USE_LEAST_FIX ) + return *_violatedPlConstraints.begin(); + + PiecewiseLinearConstraint *candidate; + + // Apply the least fix heuristic + auto it = _violatedPlConstraints.begin(); + + candidate = *it; + unsigned minFixes = getViolationCounts( candidate ); + + PiecewiseLinearConstraint *contender; + unsigned contenderFixes; + while ( it != _violatedPlConstraints.end() ) + { + contender = *it; + contenderFixes = getViolationCounts( contender ); + if ( contenderFixes < minFixes ) + { + minFixes = contenderFixes; + candidate = contender; + } + + ++it; + } + + return candidate; +} + +void SmtCore::replaySmtStackEntry( SmtStackEntry *stackEntry ) +{ + struct timespec start = TimeUtils::sampleMicro(); + + if ( _statistics ) + { + _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); + _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); + } + + // Obtain the current state of the engine + EngineState *stateBeforeSplits = new EngineState; + stateBeforeSplits->_stateId = _stateId; + ++_stateId; + _engine->storeState( *stateBeforeSplits, + TableauStateStorageLevel::STORE_ENTIRE_TABLEAU_STATE ); + stackEntry->_engineState = stateBeforeSplits; + + // Apply all the splits + _engine->applySplit( stackEntry->_activeSplit ); + for ( const auto &impliedSplit : stackEntry->_impliedValidSplits ) + _engine->applySplit( impliedSplit ); + + _stack.append( stackEntry ); + + if ( _statistics ) + { + unsigned level = getStackDepth(); + _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, + level ); + if ( level > _statistics->getUnsignedAttribute + ( Statistics::MAX_DECISION_LEVEL ) ) + _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, + level ); + struct timespec end = TimeUtils::sampleMicro(); + _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); + } +} + +void SmtCore::storeSmtState( SmtState &smtState ) +{ + smtState._impliedValidSplitsAtRoot = _impliedValidSplitsAtRoot; + + for ( auto &stackEntry : _stack ) + smtState._stack.append( stackEntry->duplicateSmtStackEntry() ); + + smtState._stateId = _stateId; +} + +bool SmtCore::pickSplitPLConstraint() +{ + if ( _needToSplit ) + { + _constraintForSplitting = _engine->pickSplitPLConstraint + ( _branchingHeuristic ); + } + return _constraintForSplitting != NULL; +} diff --git a/src/engine/tests/Test_SmtCore.h b/src/engine/tests/Test_SmtCore.h index 51a9f4404e..7a5c1283ff 100644 --- a/src/engine/tests/Test_SmtCore.h +++ b/src/engine/tests/Test_SmtCore.h @@ -22,6 +22,7 @@ #include "PiecewiseLinearConstraint.h" #include "ReluConstraint.h" #include "SmtCore.h" +#include "context/context.h" #include @@ -107,25 +108,35 @@ class SmtCoreTestSuite : public CxxTest::TestSuite } List nextSplits; + void registerCaseSplit( PiecewiseLinearCaseSplit caseSplit ) + { + nextSplits.append( caseSplit ); + allCases.append( (PhaseStatus)(++_numCases) ); + } + List getCaseSplits() const { return nextSplits; } + List allCases; List getAllCases() const { - return List(); + return allCases; } bool phaseFixed() const { - return true; + return false; } - PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus /*caseId*/ ) const + PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus caseId ) const { - PiecewiseLinearCaseSplit dontCare; - return dontCare; + auto it = nextSplits.begin(); + for ( int i = 0; i < (int)caseId - 1; ++i ) + ++it; + + return *it; } PiecewiseLinearCaseSplit getValidCaseSplit() const @@ -169,6 +180,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite { return ""; } + }; void setUp() @@ -188,8 +200,10 @@ class SmtCoreTestSuite : public CxxTest::TestSuite ReluConstraint constraint1( 1, 2 ); ReluConstraint constraint2( 3, 4 ); - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); + TS_ASSERT( !smtCore.needToSplit() ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) - 1; ++i ) { smtCore.reportViolatedConstraint( &constraint1 ); @@ -204,7 +218,8 @@ class SmtCoreTestSuite : public CxxTest::TestSuite void test_perform_split() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -231,9 +246,11 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split3.storeBoundTightening( bound5 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); - constraint.nextSplits.append( split3 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.registerCaseSplit( split3 ); + + constraint.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -242,85 +259,30 @@ class SmtCoreTestSuite : public CxxTest::TestSuite engine->lastRestoredState = NULL; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 0U ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); TS_ASSERT( !constraint.setActiveWasCalled ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( constraint.setActiveWasCalled ); TS_ASSERT( !smtCore.needToSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - // Check that Split1 was performed and tableau state was stored - TS_ASSERT_EQUALS( engine->lastLowerBounds.size(), 1U ); - TS_ASSERT_EQUALS( engine->lastLowerBounds.begin()->_variable, 1U ); - TS_ASSERT_EQUALS( engine->lastLowerBounds.begin()->_bound, 3.0 ); - - TS_ASSERT_EQUALS( engine->lastUpperBounds.size(), 1U ); - TS_ASSERT_EQUALS( engine->lastUpperBounds.begin()->_variable, 1U ); - TS_ASSERT_EQUALS( engine->lastUpperBounds.begin()->_bound, 5.0 ); - - TS_ASSERT( engine->lastStoredState ); - TS_ASSERT( !engine->lastRestoredState ); - - EngineState *originalState = engine->lastStoredState; - engine->lastStoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); - - // Pop Split1, check that the tableau was restored and that - // a Split2 was performed - TS_ASSERT( smtCore.popSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - TS_ASSERT_EQUALS( engine->lastRestoredState, originalState ); - TS_ASSERT( !engine->lastStoredState ); - engine->lastRestoredState = NULL; - - TS_ASSERT( engine->lastLowerBounds.empty() ); - - TS_ASSERT_EQUALS( engine->lastUpperBounds.size(), 2U ); - auto it = engine->lastUpperBounds.begin(); - TS_ASSERT_EQUALS( it->_variable, 2U ); - TS_ASSERT_EQUALS( it->_bound, 13.0 ); - ++it; - TS_ASSERT_EQUALS( it->_variable, 3U ); - TS_ASSERT_EQUALS( it->_bound, 25.0 ); - - engine->lastRestoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); - - // Pop Split2, check that the tableau was restored and that - // a Split3 was performed - TS_ASSERT( smtCore.popSplit() ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 1U ); - - TS_ASSERT_EQUALS( engine->lastRestoredState, originalState ); - TS_ASSERT( !engine->lastStoredState ); - engine->lastRestoredState = NULL; + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 1U ); - TS_ASSERT_EQUALS( engine->lastLowerBounds.size(), 1U ); - it = engine->lastLowerBounds.begin(); - TS_ASSERT_EQUALS( it->_variable, 14U ); - TS_ASSERT_EQUALS( it->_bound, 2.3 ); + // Pop Split1 and check that Split2 was decided + TS_ASSERT( smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 1U ); - TS_ASSERT( engine->lastUpperBounds.empty() ); - - engine->lastRestoredState = NULL; - engine->lastLowerBounds.clear(); - engine->lastUpperBounds.clear(); - engine->lastEquations.clear(); + // Pop Split2, check that Split3 was implied + TS_ASSERT( smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); // Final pop - TS_ASSERT( !smtCore.popSplit() ); - TS_ASSERT( !engine->lastRestoredState ); - TS_ASSERT_EQUALS( smtCore.getStackDepth(), 0U ); + TS_ASSERT( !smtCore.backtrackAndContinueSearch() ); + TS_ASSERT_EQUALS( smtCore.getDecisionLevel(), 0U ); } void test_perform_split__inactive_constraint() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -347,9 +309,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split3.storeBoundTightening( bound5 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); - constraint.nextSplits.append( split3 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.registerCaseSplit( split3 ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -357,7 +319,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint.nextIsActive = false; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Check that no split was performed @@ -370,7 +332,8 @@ class SmtCoreTestSuite : public CxxTest::TestSuite void test_all_splits_so_far() { - SmtCore smtCore( engine ); + CVC4::context::Context context; + SmtCore smtCore( engine, context ); MockConstraint constraint; @@ -391,8 +354,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite split2.storeBoundTightening( bound4 ); // Store the splits - constraint.nextSplits.append( split1 ); - constraint.nextSplits.append( split2 ); + constraint.registerCaseSplit( split1 ); + constraint.registerCaseSplit( split2 ); + constraint.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint ); @@ -400,16 +364,20 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint.nextIsActive = true; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Register a valid split // Split 3 + MockConstraint implication; PiecewiseLinearCaseSplit split3; Tightening bound5( 14, 2.3, Tightening::LB ); + split3.storeBoundTightening( bound5 ); + implication.registerCaseSplit( split3 ); + implication.initializeCDOs( &context ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split3 ) ); + TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication ) ); // Do another real split @@ -424,8 +392,10 @@ class SmtCoreTestSuite : public CxxTest::TestSuite Tightening bound7( 8, 13.0, Tightening::UB ); split5.storeBoundTightening( bound7 ); - constraint2.nextSplits.append( split4 ); - constraint2.nextSplits.append( split5 ); + constraint2.registerCaseSplit( split4 ); + constraint2.registerCaseSplit( split5 ); + + constraint2.initializeCDOs( &context ); for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) smtCore.reportViolatedConstraint( &constraint2 ); @@ -433,7 +403,7 @@ class SmtCoreTestSuite : public CxxTest::TestSuite constraint2.nextIsActive = true; TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); + TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); TS_ASSERT( !smtCore.needToSplit() ); // Check that everything is received in the correct order @@ -452,98 +422,103 @@ class SmtCoreTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( *it, split4 ); } - void test_store_smt_state() - { - // ReLU(x0, x1) - // ReLU(x2, x3) - // ReLU(x4, x5) - - InputQuery inputQuery; - inputQuery.setNumberOfVariables( 6 ); - - ReluConstraint relu1 = ReluConstraint( 0, 1 ); - ReluConstraint relu2 = ReluConstraint( 2, 3 ); - - relu1.transformToUseAuxVariables( inputQuery ); - relu2.transformToUseAuxVariables( inputQuery ); - - SmtCore smtCore( engine ); - - PiecewiseLinearCaseSplit split1; - Tightening bound1( 1, 0.5, Tightening::LB ); - split1.storeBoundTightening( bound1 ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split1 ) ); - - for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) - smtCore.reportViolatedConstraint( &relu1 ); - - TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); - TS_ASSERT( !smtCore.needToSplit() ); - - PiecewiseLinearCaseSplit split2; - Tightening bound2( 3, 2.3, Tightening::UB ); - split2.storeBoundTightening( bound2 ); - TS_ASSERT_THROWS_NOTHING( smtCore.recordImpliedValidSplit( split2 ) ); - - for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) - smtCore.reportViolatedConstraint( &relu2 ); - - TS_ASSERT( smtCore.needToSplit() ); - TS_ASSERT_THROWS_NOTHING( smtCore.performSplit() ); - TS_ASSERT( !smtCore.needToSplit() ); - - SmtState smtState; - smtCore.storeSmtState( smtState ); - TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); - TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); - - TS_ASSERT( smtState._stack.size() == 2 ); - // Examine the first stackEntry - SmtStackEntry *stackEntry = *( smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); - TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); - // Examine the second stackEntry - stackEntry = *( ++smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu2.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu2.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); - - clearSmtState( smtState ); - - TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); - - smtCore.storeSmtState( smtState ); - TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); - TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); - - TS_ASSERT( smtState._stack.size() == 2 ); - // Examine the first stackEntry - stackEntry = *( smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); - TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); - TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); - // Examine the second stackEntry - stackEntry = *( ++smtState._stack.begin() ); - TS_ASSERT( stackEntry->_activeSplit == *( ++relu2.getCaseSplits().begin() ) ); - TS_ASSERT( stackEntry->_alternativeSplits.empty() ); - TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); - - clearSmtState( smtState ); - - TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); - } - - void clearSmtState( SmtState &smtState ) - { - for ( const auto &stackEntry : smtState._stack ) - delete stackEntry; - smtState._stack = List(); - smtState._impliedValidSplitsAtRoot = List(); - } + /* void _test_store_smt_state() */ + /* { */ + /* // ReLU(x0, x1) */ + /* // ReLU(x2, x3) */ + /* // ReLU(x4, x5) */ + + /* InputQuery inputQuery; */ + /* inputQuery.setNumberOfVariables( 6 ); */ + + /* ReluConstraint relu1 = ReluConstraint( 0, 1 ); */ + /* ReluConstraint relu2 = ReluConstraint( 2, 3 ); */ + + /* relu1.transformToUseAuxVariables( inputQuery ); */ + /* relu2.transformToUseAuxVariables( inputQuery ); */ + + /* CVC4::context::Context context; */ + /* SmtCore smtCore( engine, context ); */ + + /* MockConstraint implication; */ + /* PiecewiseLinearCaseSplit split1; */ + /* Tightening bound1( 1, 0.5, Tightening::LB ); */ + /* split1.storeBoundTightening( bound1 ); */ + /* implication.registerCaseSplit( split1 ); */ + /* TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication ) ); */ + + /* for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) */ + /* smtCore.reportViolatedConstraint( &relu1 ); */ + + /* TS_ASSERT( smtCore.needToSplit() ); */ + /* TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); */ + /* TS_ASSERT( !smtCore.needToSplit() ); */ + + /* MockConstraint implication2; */ + /* PiecewiseLinearCaseSplit split2; */ + /* Tightening bound2( 3, 2.3, Tightening::UB ); */ + /* split2.storeBoundTightening( bound2 ); */ + /* implication2.registerCaseSplit( split2 ); */ + /* TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication2 ) ); */ + + /* for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) */ + /* smtCore.reportViolatedConstraint( &relu2 ); */ + + /* TS_ASSERT( smtCore.needToSplit() ); */ + /* TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); */ + /* TS_ASSERT( !smtCore.needToSplit() ); */ + + /* SmtState smtState; */ + /* smtCore.storeSmtState( smtState ); */ + /* TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); */ + /* TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); */ + + /* TS_ASSERT( smtState._stack.size() == 2 ); */ + /* // Examine the first stackEntry */ + /* SmtStackEntry *stackEntry = *( smtState._stack.begin() ); */ + /* TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); */ + /* TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); */ + /* // Examine the second stackEntry */ + /* stackEntry = *( ++smtState._stack.begin() ); */ + /* TS_ASSERT( stackEntry->_activeSplit == *( relu2.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu2.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); */ + + /* clearSmtState( smtState ); */ + + /* TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); */ + + /* smtCore.storeSmtState( smtState ); */ + /* TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); */ + /* TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); */ + + /* TS_ASSERT( smtState._stack.size() == 2 ); */ + /* // Examine the first stackEntry */ + /* stackEntry = *( smtState._stack.begin() ); */ + /* TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); */ + /* TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); */ + /* // Examine the second stackEntry */ + /* stackEntry = *( ++smtState._stack.begin() ); */ + /* TS_ASSERT( stackEntry->_activeSplit == *( ++relu2.getCaseSplits().begin() ) ); */ + /* TS_ASSERT( stackEntry->_alternativeSplits.empty() ); */ + /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); */ + + /* clearSmtState( smtState ); */ + + /* TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); */ + /* } */ + + /* void clearSmtState( SmtState &smtState ) */ + /* { */ + /* for ( const auto &stackEntry : smtState._stack ) */ + /* delete stackEntry; */ + /* smtState._stack = List(); */ + /* smtState._impliedValidSplitsAtRoot = List(); */ + /* } */ void test_todo() { From 5c37f0333b0ed846bdfbe3e91ade03c2c8651cc8 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 15 Jun 2022 15:39:08 -0700 Subject: [PATCH 17/39] Initialize CDOs in PiecewiseLinearConstraints --- src/engine/Engine.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 31834422c2..2f9684d13d 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -163,7 +163,10 @@ bool Engine::solve( unsigned timeoutInSeconds ) // Register the boundManager with all the PL constraints for ( auto &plConstraint : _plConstraints ) + { plConstraint->registerBoundManager( &_boundManager ); + plConstraint->initializeCDOs( &_context ); + } if ( _solveWithMILP ) return solveWithMILPEncoding( timeoutInSeconds ); From 599ce9da64ac46e81136b73f934ad9d9ffd6cfa6 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 15 Jun 2022 15:42:22 -0700 Subject: [PATCH 18/39] Integrate phaseFixed and isImplication semantics --- src/engine/AbsoluteValueConstraint.cpp | 4 ---- src/engine/AbsoluteValueConstraint.h | 1 - src/engine/Engine.cpp | 2 +- src/engine/PiecewiseLinearConstraint.cpp | 12 +++++++++++- src/engine/PiecewiseLinearConstraint.h | 2 +- src/engine/ReluConstraint.cpp | 5 ----- src/engine/ReluConstraint.h | 5 ----- src/engine/SignConstraint.cpp | 4 ---- src/engine/SignConstraint.h | 4 ---- src/engine/SmtCore.cpp | 10 ++++++++-- 10 files changed, 21 insertions(+), 28 deletions(-) diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index 41944d27e9..1f45fbb4c1 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -395,10 +395,6 @@ PiecewiseLinearCaseSplit AbsoluteValueConstraint::getPositiveSplit() const return positivePhase; } -bool AbsoluteValueConstraint::phaseFixed() const -{ - return _phaseStatus != PhaseStatus::PHASE_NOT_FIXED; -} PiecewiseLinearCaseSplit AbsoluteValueConstraint::getImpliedCaseSplit() const { diff --git a/src/engine/AbsoluteValueConstraint.h b/src/engine/AbsoluteValueConstraint.h index 5d01c00d77..ab651ace0e 100644 --- a/src/engine/AbsoluteValueConstraint.h +++ b/src/engine/AbsoluteValueConstraint.h @@ -133,7 +133,6 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint Check whether the constraint's phase has been fixed. */ void fixPhaseIfNeeded(); - bool phaseFixed() const override; /* Preprocessing related functions, to inform that a variable has diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 2f9684d13d..38a07ea04d 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1956,7 +1956,7 @@ bool Engine::applyAllValidConstraintCaseSplits() bool Engine::applyValidConstraintCaseSplit( PiecewiseLinearConstraint *constraint ) { - if ( constraint->isActive() && constraint->phaseFixed() ) + if ( constraint->isActive() && ( constraint->phaseFixed() || constraint->isImplication() ) ) { String constraintString; // This is a performance issue diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 69523612f0..9f60231286 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -170,11 +170,14 @@ void PiecewiseLinearConstraint::markInfeasible( PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() { - ASSERT( getPhaseStatus() == PHASE_NOT_FIXED ); + //ASSERT( getPhaseStatus() == PHASE_NOT_FIXED ); if ( !isFeasible() ) return CONSTRAINT_INFEASIBLE; + if ( phaseFixed() ) + return getPhaseStatus(); + List allCases = getAllCases(); for ( PhaseStatus thisCase : allCases ) { @@ -201,6 +204,13 @@ void PiecewiseLinearConstraint::setStatistics( Statistics *statistics ) _statistics = statistics; } +bool PiecewiseLinearConstraint::phaseFixed() const +{ + if ( _cdPhaseStatus != nullptr ) + return *_cdPhaseStatus != PHASE_NOT_FIXED; + else + return _phaseStatus != PHASE_NOT_FIXED; +}; // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index b7e68fc589..4753b59458 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -197,7 +197,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher /* Check if the constraint's phase has been fixed. */ - virtual bool phaseFixed() const = 0; + virtual bool phaseFixed() const; /* If the constraint's phase has been fixed, get the (valid) case split. diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index ccdd340177..61fe8a9891 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -574,11 +574,6 @@ PiecewiseLinearCaseSplit ReluConstraint::getActiveSplit() const return activePhase; } -bool ReluConstraint::phaseFixed() const -{ - return _phaseStatus != PHASE_NOT_FIXED; -} - PiecewiseLinearCaseSplit ReluConstraint::getImpliedCaseSplit() const { ASSERT( _phaseStatus != PHASE_NOT_FIXED ); diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h index f1dece1ada..3e4679c098 100644 --- a/src/engine/ReluConstraint.h +++ b/src/engine/ReluConstraint.h @@ -137,11 +137,6 @@ class ReluConstraint : public PiecewiseLinearConstraint */ PiecewiseLinearCaseSplit getImpliedCaseSplit() const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; - /* Preprocessing related functions, to inform that a variable has been eliminated completely because it was fixed to some value, diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index bf3d3492f1..a06270b652 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -217,10 +217,6 @@ PiecewiseLinearCaseSplit SignConstraint::getPositiveSplit() const return positivePhase; } -bool SignConstraint::phaseFixed() const -{ - return _phaseStatus != PHASE_NOT_FIXED; -} void SignConstraint::addAuxiliaryEquationsAfterPreprocessing( InputQuery &inputQuery ) diff --git a/src/engine/SignConstraint.h b/src/engine/SignConstraint.h index d2d19121bb..4b655a5ad4 100644 --- a/src/engine/SignConstraint.h +++ b/src/engine/SignConstraint.h @@ -126,10 +126,6 @@ class SignConstraint : public PiecewiseLinearConstraint heuristics should be implemented. */ List getAllCases() const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; /* If the phase is not fixed, add _f <= -2/lb_b * _b + 1 diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index a1f8481152..b98b700351 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -123,9 +123,14 @@ void SmtCore::pushDecision( PiecewiseLinearConstraint *constraint, PhaseStatus void SmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) { - ASSERT( constraint->isImplication() ); + ASSERT( constraint->isImplication() || constraint->phaseFixed() ); SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); - TrailEntry te( constraint, constraint->nextFeasibleCase() ); + PhaseStatus impliedCase = PHASE_NOT_FIXED; + if ( constraint->phaseFixed() ) + impliedCase = constraint->getPhaseStatus(); + else + impliedCase = constraint->nextFeasibleCase(); + TrailEntry te( constraint, impliedCase ); applyTrailEntry( te, false ); SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); } @@ -169,6 +174,7 @@ void SmtCore::decide() void SmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) { + ASSERT( constraint != nullptr ); struct timespec start = TimeUtils::sampleMicro(); if ( _statistics ) From 6ab04581840ce0ad90a1ee22c26758f9f2765a54 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 1 Jul 2022 12:27:26 -0700 Subject: [PATCH 19/39] Remove tests for Store/Clear SmtState --- src/engine/tests/Test_SmtCore.h | 106 -------------------------------- 1 file changed, 106 deletions(-) diff --git a/src/engine/tests/Test_SmtCore.h b/src/engine/tests/Test_SmtCore.h index 7a5c1283ff..66853643f7 100644 --- a/src/engine/tests/Test_SmtCore.h +++ b/src/engine/tests/Test_SmtCore.h @@ -422,115 +422,9 @@ class SmtCoreTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( *it, split4 ); } - /* void _test_store_smt_state() */ - /* { */ - /* // ReLU(x0, x1) */ - /* // ReLU(x2, x3) */ - /* // ReLU(x4, x5) */ - - /* InputQuery inputQuery; */ - /* inputQuery.setNumberOfVariables( 6 ); */ - - /* ReluConstraint relu1 = ReluConstraint( 0, 1 ); */ - /* ReluConstraint relu2 = ReluConstraint( 2, 3 ); */ - - /* relu1.transformToUseAuxVariables( inputQuery ); */ - /* relu2.transformToUseAuxVariables( inputQuery ); */ - - /* CVC4::context::Context context; */ - /* SmtCore smtCore( engine, context ); */ - - /* MockConstraint implication; */ - /* PiecewiseLinearCaseSplit split1; */ - /* Tightening bound1( 1, 0.5, Tightening::LB ); */ - /* split1.storeBoundTightening( bound1 ); */ - /* implication.registerCaseSplit( split1 ); */ - /* TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication ) ); */ - - /* for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) */ - /* smtCore.reportViolatedConstraint( &relu1 ); */ - - /* TS_ASSERT( smtCore.needToSplit() ); */ - /* TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); */ - /* TS_ASSERT( !smtCore.needToSplit() ); */ - - /* MockConstraint implication2; */ - /* PiecewiseLinearCaseSplit split2; */ - /* Tightening bound2( 3, 2.3, Tightening::UB ); */ - /* split2.storeBoundTightening( bound2 ); */ - /* implication2.registerCaseSplit( split2 ); */ - /* TS_ASSERT_THROWS_NOTHING( smtCore.pushImplication( &implication2 ) ); */ - - /* for ( unsigned i = 0; i < ( unsigned ) Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ); ++i ) */ - /* smtCore.reportViolatedConstraint( &relu2 ); */ - - /* TS_ASSERT( smtCore.needToSplit() ); */ - /* TS_ASSERT_THROWS_NOTHING( smtCore.decide() ); */ - /* TS_ASSERT( !smtCore.needToSplit() ); */ - - /* SmtState smtState; */ - /* smtCore.storeSmtState( smtState ); */ - /* TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); */ - /* TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); */ - - /* TS_ASSERT( smtState._stack.size() == 2 ); */ - /* // Examine the first stackEntry */ - /* SmtStackEntry *stackEntry = *( smtState._stack.begin() ); */ - /* TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); */ - /* TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); */ - /* // Examine the second stackEntry */ - /* stackEntry = *( ++smtState._stack.begin() ); */ - /* TS_ASSERT( stackEntry->_activeSplit == *( relu2.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu2.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); */ - - /* clearSmtState( smtState ); */ - - /* TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); */ - - /* smtCore.storeSmtState( smtState ); */ - /* TS_ASSERT( smtState._impliedValidSplitsAtRoot.size() == 1 ); */ - /* TS_ASSERT( *smtState._impliedValidSplitsAtRoot.begin() == split1 ); */ - - /* TS_ASSERT( smtState._stack.size() == 2 ); */ - /* // Examine the first stackEntry */ - /* stackEntry = *( smtState._stack.begin() ); */ - /* TS_ASSERT( stackEntry->_activeSplit == *( relu1.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( *( stackEntry->_alternativeSplits.begin() ) == *( ++relu1.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 1 ); */ - /* TS_ASSERT( *( stackEntry->_impliedValidSplits.begin() ) == split2 ); */ - /* // Examine the second stackEntry */ - /* stackEntry = *( ++smtState._stack.begin() ); */ - /* TS_ASSERT( stackEntry->_activeSplit == *( ++relu2.getCaseSplits().begin() ) ); */ - /* TS_ASSERT( stackEntry->_alternativeSplits.empty() ); */ - /* TS_ASSERT( stackEntry->_impliedValidSplits.size() == 0 ); */ - - /* clearSmtState( smtState ); */ - - /* TS_ASSERT_THROWS_NOTHING( smtCore.popSplit() ); */ - /* } */ - - /* void clearSmtState( SmtState &smtState ) */ - /* { */ - /* for ( const auto &stackEntry : smtState._stack ) */ - /* delete stackEntry; */ - /* smtState._stack = List(); */ - /* smtState._impliedValidSplitsAtRoot = List(); */ - /* } */ - void test_todo() { // Reason: the inefficiency in resizing the tableau mutliple times TS_TRACE( "add support for adding multiple equations at once, not one-by-one" ); } }; - -// -// Local Variables: -// compile-command: "make -C ../../.. " -// tags-file-name: "../../../TAGS" -// c-basic-offset: 4 -// End: -// From 99f6343f4806774bded37a417ef4a18c107d38b8 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 1 Jul 2022 18:13:35 -0700 Subject: [PATCH 20/39] Fix minor issues in SmtCore --- src/engine/SmtCore.cpp | 49 +++++++++++++++++------------------------- 1 file changed, 20 insertions(+), 29 deletions(-) diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index b98b700351..7815db96ae 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -49,6 +49,16 @@ SmtCore::~SmtCore() { } +void SmtCore::reset() +{ + _context.popto( 0 ); + _engine->postContextPopHook(); + _needToSplit = false; + _constraintForSplitting = NULL; + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; +} + void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) { ASSERT( !constraint->phaseFixed() ); @@ -126,10 +136,11 @@ void SmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) ASSERT( constraint->isImplication() || constraint->phaseFixed() ); SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); PhaseStatus impliedCase = PHASE_NOT_FIXED; - if ( constraint->phaseFixed() ) - impliedCase = constraint->getPhaseStatus(); - else + if ( constraint->isImplication() ) impliedCase = constraint->nextFeasibleCase(); + else + impliedCase = constraint->getPhaseStatus(); + ASSERT( impliedCase != PHASE_NOT_FIXED ); TrailEntry te( constraint, impliedCase ); applyTrailEntry( te, false ); SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); @@ -154,10 +165,7 @@ void SmtCore::decide() _numRejectedPhasePatternProposal = 0; // Maybe the constraint has already become inactive - if so, ignore - // TODO: Ideally we will not ever reach this point - // TODO: Maintain a vector of constraints above the threshold - // Iterate until we find an active one - if ( !_constraintForSplitting->isActive() ) + if ( !_constraintForSplitting->isActive() ) { _needToSplit = false; _constraintToViolationCount[_constraintForSplitting] = 0; @@ -170,6 +178,7 @@ void SmtCore::decide() _constraintForSplitting->setActiveConstraint( false ); decideSplit( _constraintForSplitting ); + _constraintForSplitting = nullptr; } void SmtCore::decideSplit( PiecewiseLinearConstraint *constraint ) @@ -242,7 +251,7 @@ void SmtCore::pushContext() bool SmtCore::popSplit() bool SmtCore::popDecisionLevel( TrailEntry &lastDecision ) { - //ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); + ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); if ( _decisions.empty() ) return false; @@ -274,23 +283,15 @@ bool SmtCore::backtrackToFeasibleDecision( TrailEntry &lastDecision ) { SMT_LOG( "Backtracking to a feasible decision..." ); - if ( getDecisionLevel() == 0 ) - return false; - - popDecisionLevel( lastDecision ); - lastDecision.markInfeasible(); - - while ( !lastDecision.isFeasible() ) + do { - interruptIfCompliantWithDebugSolution(); - if ( !popDecisionLevel( lastDecision ) ) return false; lastDecision.markInfeasible(); + interruptIfCompliantWithDebugSolution(); } - - interruptIfCompliantWithDebugSolution(); + while ( !lastDecision.isFeasible() ); return true; } @@ -500,13 +501,3 @@ bool SmtCore::pickSplitPLConstraint() ( _branchingHeuristic ); return _constraintForSplitting != NULL; } - -void SmtCore::reset() -{ - _context.popto( 0 ); - _engine->postContextPopHook(); - _needToSplit = false; - _constraintForSplitting = NULL; - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; -} From 1919c2a138450e4432f245fb4404a328b9366601 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 1 Jul 2022 18:14:13 -0700 Subject: [PATCH 21/39] Fix getPhaseStatus in Disjunction constraint --- src/engine/DisjunctionConstraint.cpp | 8 +++++++- src/engine/DisjunctionConstraint.h | 2 ++ src/engine/PiecewiseLinearConstraint.h | 4 +++- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 0519af3b52..5754f683c1 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -226,7 +226,8 @@ List DisjunctionConstraint::getAllCases() const PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase ) const { - return _disjuncts.get( phaseStatusToInd( phase ) ); + ASSERT ( phase != PHASE_NOT_FIXED ); + return _disjuncts.get( phaseStatusToInd( phase ) ); } bool DisjunctionConstraint::phaseFixed() const @@ -234,6 +235,11 @@ bool DisjunctionConstraint::phaseFixed() const return _feasibleDisjuncts.size() == 1; } +PhaseStatus DisjunctionConstraint::getPhaseStatus() const +{ + return indToPhaseStatus( *_feasibleDisjuncts.begin() ); +} + PiecewiseLinearCaseSplit DisjunctionConstraint::getImpliedCaseSplit() const { return _disjuncts.get( *_feasibleDisjuncts.begin() ); diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index e39448ffa1..feee1fc5fa 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -172,6 +172,8 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint */ String serializeToString() const override; + PhaseStatus getPhaseStatus() const override; + private: /* The disjuncts that form this PL constraint diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 4753b59458..1cf5a9348d 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -349,7 +349,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Method to get PhaseStatus of the constraint. Encapsulates both context dependent and context-less behavior. */ - PhaseStatus getPhaseStatus() const; + virtual PhaseStatus getPhaseStatus() const; /**********************************************************************/ /* Context-dependent Members Initialization and Cleanup */ @@ -397,6 +397,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ unsigned numFeasibleCases() const { + ASSERT( _cdInfeasibleCases != nullptr ); return _numCases - _cdInfeasibleCases->size(); } @@ -405,6 +406,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ bool isFeasible() const { + ASSERT( _cdInfeasibleCases != nullptr ); return numFeasibleCases() > 0u; } From 677584ac0e93682eb62f8a416f2dcbde0902d3b5 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Sun, 17 Jul 2022 20:43:12 -0700 Subject: [PATCH 22/39] Initialize Disjunctions introduced by DeepSoi --- src/engine/Engine.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 38a07ea04d..b6035cc1bd 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -2582,6 +2582,9 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraintBasedOnIntervalWidth() splits.append( s2 ); _disjunctionForSplitting = std::unique_ptr ( new DisjunctionConstraint( splits ) ); + _disjunctionForSplitting->registerBoundManager( &_boundManager ); + _disjunctionForSplitting->initializeCDOs( &_context ); + return _disjunctionForSplitting.get(); } } From 3ff749ef2277b92c2dca6614dc1f7de19f248dd4 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Wed, 27 Jul 2022 17:06:19 -0700 Subject: [PATCH 23/39] Add call to preContextPushHook --- src/engine/SmtCore.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 7815db96ae..4946e4d03d 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -150,6 +150,7 @@ void SmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) { if ( isDecision ) { + _engine->preContextPushHook(); _context.push(); _decisions.push_back( te ); } From f61b0d746b005ae0de564460101ce1d23189d0dd Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 4 Aug 2022 20:12:29 -0700 Subject: [PATCH 24/39] Replace _constraintForSplitting unique_ptr with a vector --- src/engine/Engine.cpp | 16 +++++++++------- src/engine/Engine.h | 2 +- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index b6035cc1bd..7d6af3a2bc 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -91,6 +91,9 @@ Engine::~Engine() delete[] _work; _work = NULL; } + + for ( auto d : _disjunctionForSplitting ) + delete d; } void Engine::setVerbosity( unsigned verbosity ) @@ -2144,7 +2147,7 @@ void Engine::checkBoundCompliancyWithDebugSolution() var.second, _tableau->getLowerBound( var.first ) ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + throw MarabouError( MarabouError::DEBUGGING_ERROR, "Check bound compliance with debug solution" ); } if ( FloatUtils::lt( _tableau->getUpperBound( var.first ), var.second, 1e-5 ) ) @@ -2155,7 +2158,7 @@ void Engine::checkBoundCompliancyWithDebugSolution() var.second, _tableau->getUpperBound( var.first ) ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); + throw MarabouError( MarabouError::DEBUGGING_ERROR, "Check bound compliance with debug solution" ); } } } @@ -2580,12 +2583,11 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraintBasedOnIntervalWidth() List splits; splits.append( s1 ); splits.append( s2 ); - _disjunctionForSplitting = std::unique_ptr - ( new DisjunctionConstraint( splits ) ); - _disjunctionForSplitting->registerBoundManager( &_boundManager ); - _disjunctionForSplitting->initializeCDOs( &_context ); + _disjunctionForSplitting.append( new DisjunctionConstraint( splits ) ); + _disjunctionForSplitting.last()->registerBoundManager( &_boundManager ); + _disjunctionForSplitting.last()->initializeCDOs( &_context ); - return _disjunctionForSplitting.get(); + return _disjunctionForSplitting.last(); } } diff --git a/src/engine/Engine.h b/src/engine/Engine.h index 2c39e71f38..93988c9139 100644 --- a/src/engine/Engine.h +++ b/src/engine/Engine.h @@ -399,7 +399,7 @@ class Engine : public IEngine, public SignalHandler::Signalable /* Disjunction that is used for splitting but doesn't exist in the beginning */ - std::unique_ptr _disjunctionForSplitting; + Vector _disjunctionForSplitting; /* Solve the query with MILP encoding From 398a65741371f91f0e4969f2c3dbe367bb63ffd6 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Mon, 8 Aug 2022 15:45:20 -0700 Subject: [PATCH 25/39] Fix serializedConstructor for PiecewiseLinearConstraints --- src/engine/AbsoluteValueConstraint.cpp | 5 ++++- src/engine/DisjunctionConstraint.cpp | 2 ++ src/engine/MaxConstraint.cpp | 1 + src/engine/PiecewiseLinearConstraint.cpp | 13 +++++++++++++ src/engine/PiecewiseLinearConstraint.h | 2 ++ src/engine/ReluConstraint.cpp | 5 ++++- src/engine/SignConstraint.cpp | 5 ++++- 7 files changed, 30 insertions(+), 3 deletions(-) diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index 1f45fbb4c1..b0ead556f5 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -33,7 +33,8 @@ AbsoluteValueConstraint::AbsoluteValueConstraint( unsigned b, unsigned f ) } AbsoluteValueConstraint::AbsoluteValueConstraint( const String &serializedAbs ) - : _auxVarsInUse( false ) + : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT ) + , _auxVarsInUse( false ) , _haveEliminatedVariables( false ) { String constraintType = serializedAbs.substring( 0, 13 ); @@ -450,6 +451,8 @@ void AbsoluteValueConstraint::dump( String &output ) const existsLowerBound( _negAux ) ? Stringf( "%lf", getLowerBound( _negAux ) ).ascii() : "-inf", existsUpperBound( _negAux ) ? Stringf( "%lf", getUpperBound( _negAux ) ).ascii() : "inf" ); } + + serializeInfeasibleCases( output ); } void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 5754f683c1..33a6b52a8e 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -342,6 +342,8 @@ void DisjunctionConstraint::dump( String &output ) const } output += Stringf( "Active? %s.", _constraintActive ? "Yes" : "No" ); + + serializeInfeasibleCases( output ); } void DisjunctionConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) diff --git a/src/engine/MaxConstraint.cpp b/src/engine/MaxConstraint.cpp index 3ec796e2e4..4dd043a2e3 100644 --- a/src/engine/MaxConstraint.cpp +++ b/src/engine/MaxConstraint.cpp @@ -669,6 +669,7 @@ String MaxConstraint::serializeToString() const // Will be ignored in any case output += Stringf( ",%u", 0 ); + //serializeInfeasibleCases( output ); return output; } diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 9f60231286..a16780b2bc 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -211,6 +211,19 @@ bool PiecewiseLinearConstraint::phaseFixed() const else return _phaseStatus != PHASE_NOT_FIXED; }; + +void PiecewiseLinearConstraint::serializeInfeasibleCases( String &output ) const +{ + output += " CDO info \n ------------------------------"; + output += Stringf(" Num cases: %d", _numCases ); + + if ( _cdInfeasibleCases ) + { + output += Stringf( "Infeasible cases (%d):", _cdInfeasibleCases->size() ); + for ( auto infeasible : *_cdInfeasibleCases ) + output += Stringf("%d", infeasible); + } +} // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 1cf5a9348d..2700df41c1 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -516,6 +516,8 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ bool isCaseInfeasible( PhaseStatus phase ) const; + void serializeInfeasibleCases( String &output ) const; + /**********************************************************************/ /* BOUND WRAPPER METHODS */ /**********************************************************************/ diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index 61fe8a9891..ac0878a0ce 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -42,7 +42,8 @@ ReluConstraint::ReluConstraint( unsigned b, unsigned f ) } ReluConstraint::ReluConstraint( const String &serializedRelu ) - : _haveEliminatedVariables( false ) + : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT ) + , _haveEliminatedVariables( false ) { String constraintType = serializedRelu.substring( 0, 4 ); ASSERT( constraintType == String( "relu" ) ); @@ -612,6 +613,8 @@ void ReluConstraint::dump( String &output ) const existsLowerBound( _aux ) ? Stringf( "%lf", getLowerBound( _aux ) ).ascii() : "-inf", existsUpperBound( _aux ) ? Stringf( "%lf", getUpperBound( _aux ) ).ascii() : "inf" ); } + + serializeInfeasibleCases( output ); } void ReluConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index a06270b652..bab1d0c556 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -39,7 +39,8 @@ SignConstraint::SignConstraint( unsigned b, unsigned f ) } SignConstraint::SignConstraint( const String &serializedSign ) - : _haveEliminatedVariables( false ) + : PiecewiseLinearConstraint( TWO_PHASE_PIECEWISE_LINEAR_CONSTRAINT ) + , _haveEliminatedVariables( false ) { String constraintType = serializedSign.substring( 0, 4 ); ASSERT( constraintType == String( "sign" ) ); @@ -581,6 +582,8 @@ void SignConstraint::dump( String &output ) const output += Stringf( "f in [%s, %s]\n", existsLowerBound( _f ) ? Stringf( "%lf", getLowerBound( _f ) ).ascii() : "-inf", existsUpperBound( _f ) ? Stringf( "%lf", getUpperBound( _f ) ).ascii() : "inf" ); + + serializeInfeasibleCases( output ); } double SignConstraint::computePolarity() const From dac61442c3aba460a6155375ae88c044de3d4d34 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Tue, 23 Aug 2022 15:11:09 -0700 Subject: [PATCH 26/39] Fix Engine::restoreState() --- src/engine/Engine.cpp | 36 ++++++++++++++++++------------------ src/engine/SmtCore.cpp | 7 +++++++ src/engine/SmtCore.h | 5 +++++ 3 files changed, 30 insertions(+), 18 deletions(-) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 7d6af3a2bc..024eb70abf 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1641,16 +1641,16 @@ void Engine::storeState( EngineState &state, TableauStateStorageLevel level ) co state._numPlConstraintsDisabledByValidSplits = _numPlConstraintsDisabledByValidSplits; } -void Engine::restoreState( const EngineState &/*state*/ ) +void Engine::restoreState( const EngineState &state ) { - //ENGINE_LOG( "Restore state starting" ); + ENGINE_LOG( "Restore state starting" ); - // if ( state._tableauStateStorageLevel == TableauStateStorageLevel::STORE_NONE ) - // throw MarabouError( MarabouError::RESTORING_ENGINE_FROM_INVALID_STATE ); + if ( state._tableauStateStorageLevel == TableauStateStorageLevel::STORE_NONE ) + throw MarabouError( MarabouError::RESTORING_ENGINE_FROM_INVALID_STATE ); - // ENGINE_LOG( "\tRestoring tableau state" ); - // _tableau->restoreState( state._tableauState, - // state._tableauStateStorageLevel ); + ENGINE_LOG( "\tRestoring tableau state" ); + _tableau->restoreState( state._tableauState, + state._tableauStateStorageLevel ); // ENGINE_LOG( "\tRestoring constraint states" ); // for ( auto &constraint : _plConstraints ) @@ -1663,17 +1663,17 @@ void Engine::restoreState( const EngineState &/*state*/ ) // _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; - // if ( _lpSolverType == LPSolverType::NATIVE ) - // { - // // Make sure the data structures are initialized to the correct size - // _rowBoundTightener->setDimensions(); - // adjustWorkMemorySize(); - // _activeEntryStrategy->resizeHook( _tableau ); - // _costFunctionManager->initialize(); - //} - - // Reset the violation counts in the SMT core - // _smtCore.resetSplitConditions(); + if ( _lpSolverType == LPSolverType::NATIVE ) + { + // Make sure the data structures are initialized to the correct size + _rowBoundTightener->setDimensions(); + adjustWorkMemorySize(); + _activeEntryStrategy->resizeHook( _tableau ); + _costFunctionManager->initialize(); + } + + //Reset the violation counts in the SMT core + _smtCore.resetSplitConditions(); } void Engine::setNumPlConstraintsDisabledByValidSplits( unsigned numConstraints ) diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 4946e4d03d..4c6684a109 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -502,3 +502,10 @@ bool SmtCore::pickSplitPLConstraint() ( _branchingHeuristic ); return _constraintForSplitting != NULL; } + +void SmtCore::resetSplitConditions() +{ + _constraintToViolationCount.clear(); + _numRejectedPhasePatternProposal = 0; + _needToSplit = false; +} diff --git a/src/engine/SmtCore.h b/src/engine/SmtCore.h index 4e1aac1748..f33ebe1c7c 100644 --- a/src/engine/SmtCore.h +++ b/src/engine/SmtCore.h @@ -243,6 +243,11 @@ class SmtCore */ bool pickSplitPLConstraint(); + /* + Reset violation counts and number of rejected proposal patterns. + */ + void resetSplitConditions(); + /* * For testing purposes */ From 91d5aedbec65765d6d5ec3833312a4f9020edfca Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 26 Aug 2022 15:39:03 -0700 Subject: [PATCH 27/39] Fix SmtCore::reset to account for the context hook sematnics --- src/engine/SmtCore.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 4c6684a109..d514f1bd7c 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -51,8 +51,11 @@ SmtCore::~SmtCore() void SmtCore::reset() { - _context.popto( 0 ); - _engine->postContextPopHook(); + if ( _context.getLevel() > 0 ) + { + _context.popto( 0 ); + _engine->postContextPopHook(); + } _needToSplit = false; _constraintForSplitting = NULL; _constraintToViolationCount.clear(); From b38ed89d8c6aefaa43f2465d7b78954638491697 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 1 Sep 2022 13:59:47 -0700 Subject: [PATCH 28/39] Remove DisjunctionConstraint::phaseFixed and update tests --- src/engine/DisjunctionConstraint.cpp | 5 --- src/engine/DisjunctionConstraint.h | 5 --- src/engine/tests/Test_DisjunctionConstraint.h | 38 +++++++++++-------- 3 files changed, 22 insertions(+), 26 deletions(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 33a6b52a8e..b6edb3a25a 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -230,11 +230,6 @@ PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase return _disjuncts.get( phaseStatusToInd( phase ) ); } -bool DisjunctionConstraint::phaseFixed() const -{ - return _feasibleDisjuncts.size() == 1; -} - PhaseStatus DisjunctionConstraint::getPhaseStatus() const { return indToPhaseStatus( *_feasibleDisjuncts.begin() ); diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index feee1fc5fa..419c922f69 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -118,11 +118,6 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint */ PiecewiseLinearCaseSplit getCaseSplit( PhaseStatus phase ) const override; - /* - Check if the constraint's phase has been fixed. - */ - bool phaseFixed() const override; - /* If the constraint's phase has been fixed, get the implied case split. */ diff --git a/src/engine/tests/Test_DisjunctionConstraint.h b/src/engine/tests/Test_DisjunctionConstraint.h index 6164a0b91e..aabcbc2f89 100644 --- a/src/engine/tests/Test_DisjunctionConstraint.h +++ b/src/engine/tests/Test_DisjunctionConstraint.h @@ -49,6 +49,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite PiecewiseLinearCaseSplit *cs1; PiecewiseLinearCaseSplit *cs2; PiecewiseLinearCaseSplit *cs3; + Context ctx; void setUp() { @@ -195,8 +196,10 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite 5 <= x0 --> x1 = 2x2 + 5 */ + { DisjunctionConstraint dc( caseSplits ); + dc.initializeCDOs( &ctx ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -205,16 +208,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, -1 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 6 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); @@ -222,6 +225,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite { DisjunctionConstraint dc( caseSplits ); + dc.initializeCDOs( &ctx ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -230,16 +234,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 7 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, -2 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs1 ); @@ -261,6 +265,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite BoundManager boundManager( context ); boundManager.initialize( 11 ); dc.registerBoundManager( &boundManager ); + dc.initializeCDOs( &context ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -269,16 +274,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, -1 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyLowerBound( 0, 6 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); @@ -290,6 +295,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite BoundManager boundManager( context ); boundManager.initialize( 11 ); dc.registerBoundManager( &boundManager ); + dc.initializeCDOs( &context ); dc.notifyLowerBound( 0, -10 ); dc.notifyUpperBound( 0, 10 ); @@ -298,16 +304,16 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite dc.notifyLowerBound( 2, -10 ); dc.notifyUpperBound( 2, 10 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 7 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, 2 ); - TS_ASSERT( !dc.phaseFixed() ); + TS_ASSERT( !dc.isImplication() ); dc.notifyUpperBound( 0, -2 ); - TS_ASSERT( dc.phaseFixed() ); + TS_ASSERT( dc.isImplication() ); PiecewiseLinearCaseSplit validSplit = dc.getValidCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs1 ); From d92f6dc3ec674c3b2cbd7c067e7e0787ecef4042 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 1 Sep 2022 14:01:28 -0700 Subject: [PATCH 29/39] Make PiecewiseLinearConstraint::nextFeasibleCase() const --- src/engine/PiecewiseLinearConstraint.cpp | 2 +- src/engine/PiecewiseLinearConstraint.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index a16780b2bc..5165043d50 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -168,7 +168,7 @@ void PiecewiseLinearConstraint::markInfeasible( _cdInfeasibleCases->push_back( infeasibleCase ); } -PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() +PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() const { //ASSERT( getPhaseStatus() == PHASE_NOT_FIXED ); diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 2700df41c1..38c8be96ab 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -390,7 +390,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Worst case complexity O(n^2) This method is overloaded in MAX and DISJUNCTION constraints. */ - virtual PhaseStatus nextFeasibleCase(); + virtual PhaseStatus nextFeasibleCase() const; /* Returns number of cases not yet marked as infeasible. From 5875357b88b207c29298cccdfc864bfb50c9aa0c Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 14:58:30 -0700 Subject: [PATCH 30/39] Fix DisjunctionConstraint::constraintObsolete to always return false. Previous semantics matched an empty/infeasible disjunction. --- src/engine/DisjunctionConstraint.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index b6edb3a25a..426139ab53 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -381,7 +381,7 @@ void DisjunctionConstraint::eliminateVariable( unsigned /* variable */, double / bool DisjunctionConstraint::constraintObsolete() const { - return _feasibleDisjuncts.empty(); + return false; // A Disjunction is obsolete only when a literal is always true. } void DisjunctionConstraint::getEntailedTightenings( List &/* tightenings */ ) const From ff45d2f090dd54b12d4b8b914cf66c4b2d53d0bd Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 15:19:31 -0700 Subject: [PATCH 31/39] Introduce PiecewiseLinearConstraint::getImpliedCase() The method encapsulates both phaseFixed and isImplication semantics, prioritizing isImplication. --- src/engine/PiecewiseLinearConstraint.cpp | 17 +++++++++++++---- src/engine/PiecewiseLinearConstraint.h | 8 +++++++- src/engine/SmtCore.cpp | 8 +------- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 5165043d50..5bfdb211ac 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -212,14 +212,23 @@ bool PiecewiseLinearConstraint::phaseFixed() const return _phaseStatus != PHASE_NOT_FIXED; }; -void PiecewiseLinearConstraint::serializeInfeasibleCases( String &output ) const +PhaseStatus PiecewiseLinearConstraint::getImpliedCase() const { - output += " CDO info \n ------------------------------"; - output += Stringf(" Num cases: %d", _numCases ); + ASSERT( isImplication() || phaseFixed() ); + PhaseStatus impliedCase = PHASE_NOT_FIXED; + if ( isImplication() ) + impliedCase = nextFeasibleCase(); + else + impliedCase = getPhaseStatus(); + ASSERT( impliedCase != PHASE_NOT_FIXED ); + return impliedCase; +} +void PiecewiseLinearConstraint::serializeInfeasibleCases( String &output ) const +{ if ( _cdInfeasibleCases ) { - output += Stringf( "Infeasible cases (%d):", _cdInfeasibleCases->size() ); + output += Stringf( "Infeasible cases ( %d/%d):", _cdInfeasibleCases->size(), _numCases ); for ( auto infeasible : *_cdInfeasibleCases ) output += Stringf("%d", infeasible); } diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 38c8be96ab..70c2a98f2f 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -207,6 +207,11 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher virtual PiecewiseLinearCaseSplit getValidCaseSplit() const = 0; virtual PiecewiseLinearCaseSplit getImpliedCaseSplit() const = 0; + /* + Get implied case split - either based on search (_cdInfeasibleCases) or assignment (_cdPhaseFixed) + */ + PhaseStatus getImpliedCase() const; + /* Returns a list of all cases of this constraint. Used by the nextFeasibleCase to track the state during search. The order of returned @@ -455,6 +460,8 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher return _cdInfeasibleCases; } + void serializeInfeasibleCases( String &output ) const; + protected: unsigned _numCases; // Number of possible cases/phases for this constraint // (e.g. 2 for ReLU, ABS, SIGN; >=2 for Max and Disjunction ) @@ -516,7 +523,6 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher */ bool isCaseInfeasible( PhaseStatus phase ) const; - void serializeInfeasibleCases( String &output ) const; /**********************************************************************/ /* BOUND WRAPPER METHODS */ diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index d514f1bd7c..40b6d9a66f 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -138,13 +138,7 @@ void SmtCore::pushImplication( PiecewiseLinearConstraint *constraint ) { ASSERT( constraint->isImplication() || constraint->phaseFixed() ); SMT_LOG( Stringf( "Implication @ %d ... ", _context.getLevel() ).ascii() ); - PhaseStatus impliedCase = PHASE_NOT_FIXED; - if ( constraint->isImplication() ) - impliedCase = constraint->nextFeasibleCase(); - else - impliedCase = constraint->getPhaseStatus(); - ASSERT( impliedCase != PHASE_NOT_FIXED ); - TrailEntry te( constraint, impliedCase ); + TrailEntry te( constraint, constraint->getImpliedCase() ); applyTrailEntry( te, false ); SMT_LOG( Stringf( "Implication @ %d DONE", _context.getLevel() ).ascii() ); } From d844648f5518300c61aa2bc0adc661bdeb2e25f1 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 15:43:42 -0700 Subject: [PATCH 32/39] Ensure DisjunctionConstraint::getPhaseStatus() meets precondition --- src/engine/DisjunctionConstraint.cpp | 1 + src/engine/PiecewiseLinearConstraint.cpp | 2 +- src/engine/tests/Test_DisjunctionConstraint.h | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 426139ab53..09f9ea299a 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -232,6 +232,7 @@ PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase PhaseStatus DisjunctionConstraint::getPhaseStatus() const { + ASSERT ( phaseFixed() ); return indToPhaseStatus( *_feasibleDisjuncts.begin() ); } diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 5bfdb211ac..1dc43f245a 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -153,7 +153,7 @@ void PiecewiseLinearConstraint::initializeDuplicateCDOs( ASSERT( clone->_cdPhaseStatus != nullptr ); clone->_cdPhaseStatus = nullptr; clone->initializeCDPhaseStatus(); - clone->setPhaseStatus( this->getPhaseStatus() ); + clone->setPhaseStatus( *_cdPhaseStatus ); ASSERT( clone->_cdInfeasibleCases != nullptr ); clone->_cdInfeasibleCases = nullptr; diff --git a/src/engine/tests/Test_DisjunctionConstraint.h b/src/engine/tests/Test_DisjunctionConstraint.h index aabcbc2f89..699cdd6725 100644 --- a/src/engine/tests/Test_DisjunctionConstraint.h +++ b/src/engine/tests/Test_DisjunctionConstraint.h @@ -455,7 +455,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite PiecewiseLinearCaseSplit validSplit = dc.getImpliedCaseSplit(); TS_ASSERT_EQUALS( validSplit, *cs3 ); - dc.markInfeasible( dc.getPhaseStatus() ); + dc.markInfeasible( dc.getImpliedCase() ); TS_ASSERT( !dc.isFeasible() ); TS_ASSERT_EQUALS( dc.nextFeasibleCase(), CONSTRAINT_INFEASIBLE ); } From e9b1b9a3f486a1a27b23657f77fefa06009e002b Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 15:44:26 -0700 Subject: [PATCH 33/39] Simplify getImpliedCaseSplit() --- src/engine/DisjunctionConstraint.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 09f9ea299a..278d437eb4 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -238,7 +238,8 @@ PhaseStatus DisjunctionConstraint::getPhaseStatus() const PiecewiseLinearCaseSplit DisjunctionConstraint::getImpliedCaseSplit() const { - return _disjuncts.get( *_feasibleDisjuncts.begin() ); + ASSERT ( isImplication() ); + return _disjuncts.get( phaseStatusToInd ( getImpliedCase() ) ); } PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const From f4f9ae5e9cf81f33cc5deff72b9eff2610f46c5e Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 16:08:54 -0700 Subject: [PATCH 34/39] Rewrite updateFeasibleDisjuncts --- src/engine/DisjunctionConstraint.cpp | 34 ++++++++++++++++------------ src/engine/DisjunctionConstraint.h | 1 - 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 278d437eb4..c7d669595e 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -155,6 +155,8 @@ void DisjunctionConstraint::notifyLowerBound( unsigned variable, double bound ) setLowerBound( variable, bound ); + //TODO: Maintain a mapping from variables to disjuncts and only check relevant + // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -169,6 +171,8 @@ void DisjunctionConstraint::notifyUpperBound( unsigned variable, double bound ) setUpperBound( variable, bound ); + //TODO: Maintain a mapping from variables to disjuncts and only check relevant + // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -476,23 +480,25 @@ bool DisjunctionConstraint::disjunctSatisfied( const PiecewiseLinearCaseSplit &d void DisjunctionConstraint::updateFeasibleDisjuncts() { - _feasibleDisjuncts.clear(); - - for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + if ( _cdInfeasibleCases ) { - if ( disjunctIsFeasible( ind ) ) - _feasibleDisjuncts.append( ind ); - else if ( _cdInfeasibleCases && !isCaseInfeasible( indToPhaseStatus( ind ) ) ) - markInfeasible( indToPhaseStatus( ind ) ); + for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + { + if ( !isCaseInfeasible( indToPhaseStatus( ind ) ) && + !caseSplitIsFeasible( _disjuncts.get( ind ) ) ) + markInfeasible( indToPhaseStatus( ind ) ); + } } -} - -bool DisjunctionConstraint::disjunctIsFeasible( unsigned ind ) const -{ - if ( _cdInfeasibleCases && isCaseInfeasible( indToPhaseStatus( ind ) ) ) - return false; + else + { + _feasibleDisjuncts.clear(); - return caseSplitIsFeasible( _disjuncts.get( ind ) ); + for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) + { + if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) ) + _feasibleDisjuncts.append( ind ); + } + } } bool DisjunctionConstraint::caseSplitIsFeasible( const PiecewiseLinearCaseSplit &disjunct ) const diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index 419c922f69..68b9588922 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -203,7 +203,6 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint still feasible, given the current variable bounds */ void updateFeasibleDisjuncts(); - bool disjunctIsFeasible( unsigned ind ) const; bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit & caseSplit ) const; inline PhaseStatus indToPhaseStatus( unsigned ind ) const From 4a99bc4a348e872438b5043897e26bea19d43c1f Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 8 Sep 2022 16:25:42 -0700 Subject: [PATCH 35/39] Update class description --- src/engine/DisjunctionConstraint.h | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index 68b9588922..ed112db08c 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -2,7 +2,7 @@ /*! \file DisjunctionConstraint.h ** \verbatim ** Top contributors (to current version): - ** Guy Katz, Duligur Ibeling, Christopher Lazarus, Haoze Wu + ** Guy Katz, Duligur Ibeling, Christopher Lazarus, Haoze Wu, Aleksandar Zeljic ** 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. @@ -13,16 +13,22 @@ ** e1 \/ e2 \/ ... \/ eM, where _elements = { e1, e2, ..., eM } ** ** The constraint introduces identifiers for its PiecewiseLinearCaseSplit - ** elements. + ** elements. The mapping between the cases (PhaseStatus) and local indices is + ** available via indToPhaseStatus and phaseStatusToInd methods. ** ** The constraint is implemented as PiecewiseLinearConstraint ** and operates in two modes: - ** * pre-processing mode, which stores bounds locally, and - ** * context dependent mode, used during the search. + ** * pre-processing mode, which stores _feasibleDisjuncts locally, and + ** * context dependent mode, used during the SMT search. ** ** Invoking initializeCDOs method activates the context dependent mode, and the ** DisjunctionConstraint object synchronizes its state automatically with the central ** Context object. + ** + ** TODOs: + ** - Eliminate updateFeasibleDisjuncts (and its quadratic complexity) by + ** introducing a map between variables and the disjuncts they participate in + ** which enables direct access to disjunct to check feasibility. **/ #ifndef __DisjunctionConstraint_h__ From 619a909d653f0ca4284a0e6262c521735a494c2e Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Mon, 12 Sep 2022 17:35:03 -0700 Subject: [PATCH 36/39] Remove old SmtCore implementation --- src/engine/oldSmtCore | 257 ------------------- src/engine/oldSmtCoreCpp | 533 --------------------------------------- 2 files changed, 790 deletions(-) delete mode 100644 src/engine/oldSmtCore delete mode 100644 src/engine/oldSmtCoreCpp diff --git a/src/engine/oldSmtCore b/src/engine/oldSmtCore deleted file mode 100644 index 416268a11e..0000000000 --- a/src/engine/oldSmtCore +++ /dev/null @@ -1,257 +0,0 @@ -/********************* */ -/*! \file SmtCore.h - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, Parth Shah - ** 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 ]] - -**/ - -#ifndef __SmtCore_h__ -#define __SmtCore_h__ - -#include "DivideStrategy.h" -#include "PiecewiseLinearCaseSplit.h" -#include "PiecewiseLinearConstraint.h" -#include "PLConstraintScoreTracker.h" -#include "SmtState.h" -#include "Stack.h" -#include "SmtStackEntry.h" -#include "Statistics.h" -#include "context/context.h" - -#include - -#define SMT_LOG( x, ... ) LOG( GlobalConfiguration::SMT_CORE_LOGGING, "SmtCore: %s\n", x ) - -class EngineState; -class IEngine; -class String; - -using CVC4::context::Context; - -class SmtCore -{ -public: - SmtCore( IEngine *engine ); - ~SmtCore(); - - /* - Clear the stack. - */ - void freeMemory(); - - /* - Reset the SmtCore - */ - void reset(); - - /* - Initialize the score tracker with the given list of pl constraints. - */ - void initializeScoreTrackerIfNeeded( const List - &plConstraints ); - - /* - Inform the SMT core that a SoI phase pattern proposal is rejected. - */ - void reportRejectedPhasePatternProposal(); - - /* - Update the score of the constraint with the given score in the costTracker. - */ - inline void updatePLConstraintScore( PiecewiseLinearConstraint *constraint, - double score ) - { - ASSERT( _scoreTracker != nullptr ); - _scoreTracker->updateScore( constraint, score ); - } - - /* - Get the constraint in the score tracker with the highest score - */ - inline PiecewiseLinearConstraint *getConstraintsWithHighestScore() const - { - return _scoreTracker->topUnfixed(); - } - - /* - Inform the SMT core that a PL constraint is violated. - */ - void reportViolatedConstraint( PiecewiseLinearConstraint *constraint ); - - /* - Get the number of times a specific PL constraint has been reported as - violated. - */ - unsigned getViolationCounts( PiecewiseLinearConstraint* constraint ) const; - - /* - Reset all reported violation counts and the number of rejected SoI - phase pattern proposal. - */ - void resetSplitConditions(); - - /* - Returns true iff the SMT core wants to perform a case split. - */ - bool needToSplit() const; - - /* - Perform the split according to the constraint marked for - splitting. Update bounds, add equations and update the stack. - */ - void performSplit(); - - /* - Pop an old split from the stack, and perform a new split as - needed. Return true if successful, false if the stack is empty. - */ - bool popSplit(); - - /* - The current stack depth. - */ - unsigned getStackDepth() const; - - /* - Let the smt core know of an implied valid case split that was discovered. - */ - void recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ); - - /* - Return a list of all splits performed so far, both SMT-originating and valid ones, - in the correct order. - */ - void allSplitsSoFar( List &result ) const; - - /* - Have the SMT core start reporting statistics. - */ - void setStatistics( Statistics *statistics ); - - /* - Have the SMT core choose, among a set of violated PL constraints, which - constraint should be repaired (without splitting) - */ - PiecewiseLinearConstraint *chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const; - - inline void setBranchingHeuristics( DivideStrategy strategy ) - { - _branchingHeuristic = strategy; - } - - /* - Replay a stackEntry - */ - void replaySmtStackEntry( SmtStackEntry *stackEntry ); - - /* - Store the current state of the SmtCore into smtState - */ - void storeSmtState( SmtState &smtState ); - - /* - Pick the piecewise linear constraint for splitting, returns true - if a constraint for splitting is successfully picked - */ - bool pickSplitPLConstraint(); - - /* - For debugging purposes only - store a correct possible solution - */ - void storeDebuggingSolution( const Map &debuggingSolution ); - bool checkSkewFromDebuggingSolution(); - bool splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const; - -private: - /* - Valid splits that were implied by level 0 of the stack. - */ - List _impliedValidSplitsAtRoot; - - /* - Collect and print various statistics. - */ - Statistics *_statistics; - - /* - The case-split stack. - */ - List _stack; - - /* - The engine. - */ - IEngine *_engine; - - /* - Context for synchronizing the search. - */ - Context &_context; - /* - Do we need to perform a split and on which constraint. - */ - bool _needToSplit; - PiecewiseLinearConstraint *_constraintForSplitting; - - /* - Count how many times each constraint has been violated. - */ - Map _constraintToViolationCount; - - /* - For debugging purposes only - */ - Map _debuggingSolution; - - /* - A unique ID allocated to every state that is stored, for - debugging purposes. - */ - unsigned _stateId; - - /* - Split when some relu has been violated for this many times during the - Reluplex procedure - */ - unsigned _constraintViolationThreshold; - - /* - Split when there have been this many rejected phase pattern proposal - during the SoI-based local search. - */ - unsigned _deepSoIRejectionThreshold; - - /* - The strategy to pick the piecewise linear constraint to branch on. - */ - DivideStrategy _branchingHeuristic; - - /* - Heap to store the scores of each PLConstraint. - */ - std::unique_ptr _scoreTracker; - - /* - Number of times the phase pattern proposal has been rejected at the - current search state. - */ - unsigned _numRejectedPhasePatternProposal; -}; - -#endif // __SmtCore_h__ - -// -// Local Variables: -// compile-command: "make -C ../.. " -// tags-file-name: "../../TAGS" -// c-basic-offset: 4 -// End: -// diff --git a/src/engine/oldSmtCoreCpp b/src/engine/oldSmtCoreCpp deleted file mode 100644 index 6d14b14e5b..0000000000 --- a/src/engine/oldSmtCoreCpp +++ /dev/null @@ -1,533 +0,0 @@ -/********************* */ -/*! \file SmtCore.cpp - ** \verbatim - ** Top contributors (to current version): - ** Guy Katz, Parth Shah, Duligur Ibeling - ** 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 "Debug.h" -#include "DivideStrategy.h" -#include "EngineState.h" -#include "FloatUtils.h" -#include "GlobalConfiguration.h" -#include "IEngine.h" -#include "MStringf.h" -#include "MarabouError.h" -#include "Options.h" -#include "PseudoImpactTracker.h" -#include "ReluConstraint.h" -#include "SmtCore.h" - -SmtCore::SmtCore( IEngine *engine ) - : _statistics( NULL ) - , _engine( engine ) - , _context( _engine->getContext() ) - , _needToSplit( false ) - , _constraintForSplitting( NULL ) - , _stateId( 0 ) - , _constraintViolationThreshold( Options::get()->getInt( Options::CONSTRAINT_VIOLATION_THRESHOLD ) ) - , _deepSoIRejectionThreshold( Options::get()->getInt( Options::DEEP_SOI_REJECTION_THRESHOLD ) ) - , _branchingHeuristic( Options::get()->getDivideStrategy() ) - , _scoreTracker( nullptr ) - , _numRejectedPhasePatternProposal( 0 ) -{ -} - -SmtCore::~SmtCore() -{ - freeMemory(); -} - -void SmtCore::freeMemory() -{ - for ( const auto &stackEntry : _stack ) - { - delete stackEntry->_engineState; - delete stackEntry; - } - - _stack.clear(); -} - -void SmtCore::reset() -{ - freeMemory(); - _impliedValidSplitsAtRoot.clear(); - _needToSplit = false; - _constraintForSplitting = NULL; - _stateId = 0; - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; -} - -void SmtCore::reportViolatedConstraint( PiecewiseLinearConstraint *constraint ) -{ - if ( !_constraintToViolationCount.exists( constraint ) ) - _constraintToViolationCount[constraint] = 0; - - ++_constraintToViolationCount[constraint]; - - if ( _constraintToViolationCount[constraint] >= - _constraintViolationThreshold ) - { - _needToSplit = true; - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = constraint; - } -} - -unsigned SmtCore::getViolationCounts( PiecewiseLinearConstraint *constraint ) const -{ - if ( !_constraintToViolationCount.exists( constraint ) ) - return 0; - - return _constraintToViolationCount[constraint]; -} - -void SmtCore::initializeScoreTrackerIfNeeded( const - List - &plConstraints ) -{ - if ( GlobalConfiguration::USE_DEEPSOI_LOCAL_SEARCH ) - { - _scoreTracker = std::unique_ptr - ( new PseudoImpactTracker() ); - _scoreTracker->initialize( plConstraints ); - - SMT_LOG( "\tTracking Pseudo Impact..." ); - } -} - -void SmtCore::reportRejectedPhasePatternProposal() -{ - ++_numRejectedPhasePatternProposal; - - if ( _numRejectedPhasePatternProposal >= - _deepSoIRejectionThreshold ) - { - _needToSplit = true; - _engine->applyAllBoundTightenings(); - _engine->applyAllValidConstraintCaseSplits(); - if ( !pickSplitPLConstraint() ) - // If pickSplitConstraint failed to pick one, use the native - // relu-violation based splitting heuristic. - _constraintForSplitting = _scoreTracker->topUnfixed(); - } -} - -bool SmtCore::needToSplit() const -{ - return _needToSplit; -} - -void SmtCore::performSplit() -{ - ASSERT( _needToSplit ); - - _numRejectedPhasePatternProposal = 0; - // Maybe the constraint has already become inactive - if so, ignore - if ( !_constraintForSplitting->isActive() ) - { - _needToSplit = false; - _constraintToViolationCount[_constraintForSplitting] = 0; - _constraintForSplitting = NULL; - return; - } - - struct timespec start = TimeUtils::sampleMicro(); - - ASSERT( _constraintForSplitting->isActive() ); - _needToSplit = false; - - if ( _statistics ) - { - _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - // Before storing the state of the engine, we: - // 1. Obtain the splits. - // 2. Disable the constraint, so that it is marked as disbaled in the EngineState. - List splits = _constraintForSplitting->getCaseSplits(); - ASSERT( !splits.empty() ); - ASSERT( splits.size() >= 2 ); // Not really necessary, can add code to handle this case. - _constraintForSplitting->setActiveConstraint( false ); - - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_BOUNDS_ONLY ); - _engine->preContextPushHook(); - _context.push(); - SmtStackEntry *stackEntry = new SmtStackEntry; - // Perform the first split: add bounds and equations - List::iterator split = splits.begin(); - ASSERT( split->getEquations().size() == 0 ); - _engine->applySplit( *split ); - stackEntry->_activeSplit = *split; - - // Store the remaining splits on the stack, for later - stackEntry->_engineState = stateBeforeSplits; - ++split; - while ( split != splits.end() ) - { - stackEntry->_alternativeSplits.append( *split ); - ++split; - } - - _stack.append( stackEntry ); - - if ( _statistics ) - { - unsigned level = getStackDepth(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - - _constraintForSplitting = NULL; -} - -unsigned SmtCore::getStackDepth() const -{ - ASSERT( _stack.size() == static_cast( _context.getLevel() ) ); - return _stack.size(); -} - -bool SmtCore::popSplit() -{ - SMT_LOG( "Performing a pop" ); - - if ( _stack.empty() ) - return false; - - struct timespec start = TimeUtils::sampleMicro(); - - if ( _statistics ) - { - _statistics->incUnsignedAttribute( Statistics::NUM_POPS ); - // A pop always sends us to a state that we haven't seen before - whether - // from a sibling split, or from a lower level of the tree. - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - bool inconsistent = true; - while ( inconsistent ) - { - // Remove any entries that have no alternatives - String error; - while ( _stack.back()->_alternativeSplits.empty() ) - { - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - - delete _stack.back()->_engineState; - delete _stack.back(); - _stack.popBack(); - _context.pop(); - - if ( _stack.empty() ) - return false; - } - - if ( checkSkewFromDebuggingSolution() ) - { - // Pops should not occur from a compliant stack! - printf( "Error! Popping from a compliant stack\n" ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - - SmtStackEntry *stackEntry = _stack.back(); - - _context.pop(); - _engine->postContextPopHook(); - // Restore the state of the engine - SMT_LOG( "\tRestoring engine state..." ); - _engine->restoreState( *( stackEntry->_engineState ) ); - SMT_LOG( "\tRestoring engine state - DONE" ); - - // Apply the new split and erase it from the list - auto split = stackEntry->_alternativeSplits.begin(); - - // Erase any valid splits that were learned using the split we just - // popped - stackEntry->_impliedValidSplits.clear(); - - SMT_LOG( "\tApplying new split..." ); - ASSERT( split->getEquations().size() == 0 ); - _engine->preContextPushHook(); - _context.push(); - _engine->applySplit( *split ); - SMT_LOG( "\tApplying new split - DONE" ); - - stackEntry->_activeSplit = *split; - stackEntry->_alternativeSplits.erase( split ); - - inconsistent = !_engine->consistentBounds(); - } - - if ( _statistics ) - { - unsigned level = getStackDepth(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } - - checkSkewFromDebuggingSolution(); - - return true; -} - -void SmtCore::resetSplitConditions() -{ - _constraintToViolationCount.clear(); - _numRejectedPhasePatternProposal = 0; - _needToSplit = false; -} - -void SmtCore::recordImpliedValidSplit( PiecewiseLinearCaseSplit &validSplit ) -{ - if ( _stack.empty() ) - _impliedValidSplitsAtRoot.append( validSplit ); - else - _stack.back()->_impliedValidSplits.append( validSplit ); - - checkSkewFromDebuggingSolution(); -} - -void SmtCore::allSplitsSoFar( List &result ) const -{ - result.clear(); - - for ( const auto &it : _impliedValidSplitsAtRoot ) - result.append( it ); - - for ( const auto &it : _stack ) - { - result.append( it->_activeSplit ); - for ( const auto &impliedSplit : it->_impliedValidSplits ) - result.append( impliedSplit ); - } -} - -void SmtCore::setStatistics( Statistics *statistics ) -{ - _statistics = statistics; -} - -void SmtCore::storeDebuggingSolution( const Map &debuggingSolution ) -{ - _debuggingSolution = debuggingSolution; -} - -// Return true if stack is currently compliant, false otherwise -// If there is no stored solution, return false --- incompliant. -bool SmtCore::checkSkewFromDebuggingSolution() -{ - if ( _debuggingSolution.empty() ) - return false; - - String error; - - // First check that the valid splits implied at the root level are okay - for ( const auto &split : _impliedValidSplitsAtRoot ) - { - if ( !splitAllowsStoredSolution( split, error ) ) - { - printf( "Error with one of the splits implied at root level:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - - // Now go over the stack from oldest to newest and check that each level is compliant - for ( const auto &stackEntry : _stack ) - { - // If the active split is non-compliant but there are alternatives, that's fine - if ( !splitAllowsStoredSolution( stackEntry->_activeSplit, error ) ) - { - if ( stackEntry->_alternativeSplits.empty() ) - { - printf( "Error! Have a split that is non-compliant with the stored solution, " - "without alternatives:\n\t%s\n", error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - - // Active split is non-compliant but this is fine, because there are alternatives. We're done. - return false; - } - - // Did we learn any valid splits that are non-compliant? - for ( auto const &split : stackEntry->_impliedValidSplits ) - { - if ( !splitAllowsStoredSolution( split, error ) ) - { - printf( "Error with one of the splits implied at this stack level:\n\t%s\n", - error.ascii() ); - throw MarabouError( MarabouError::DEBUGGING_ERROR ); - } - } - } - - // No problems were detected, the stack is compliant with the stored solution - return true; -} - -bool SmtCore::splitAllowsStoredSolution( const PiecewiseLinearCaseSplit &split, String &error ) const -{ - // False if the split prevents one of the values in the stored solution, true otherwise. - error = ""; - if ( _debuggingSolution.empty() ) - return true; - - for ( const auto &bound : split.getBoundTightenings() ) - { - unsigned variable = bound._variable; - - // If the possible solution doesn't care about this variable, - // ignore it - if ( !_debuggingSolution.exists( variable ) ) - continue; - - // Otherwise, check that the bound is consistent with the solution - double solutionValue = _debuggingSolution[variable]; - double boundValue = bound._value; - - if ( ( bound._type == Tightening::LB ) && FloatUtils::gt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new LB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - else if ( ( bound._type == Tightening::UB ) && FloatUtils::lt( boundValue, solutionValue ) ) - { - error = Stringf( "Variable %u: new UB is %.5lf, which contradicts possible solution %.5lf", - variable, - boundValue, - solutionValue ); - return false; - } - } - - return true; -} - -PiecewiseLinearConstraint *SmtCore::chooseViolatedConstraintForFixing( List &_violatedPlConstraints ) const -{ - ASSERT( !_violatedPlConstraints.empty() ); - - if ( !GlobalConfiguration::USE_LEAST_FIX ) - return *_violatedPlConstraints.begin(); - - PiecewiseLinearConstraint *candidate; - - // Apply the least fix heuristic - auto it = _violatedPlConstraints.begin(); - - candidate = *it; - unsigned minFixes = getViolationCounts( candidate ); - - PiecewiseLinearConstraint *contender; - unsigned contenderFixes; - while ( it != _violatedPlConstraints.end() ) - { - contender = *it; - contenderFixes = getViolationCounts( contender ); - if ( contenderFixes < minFixes ) - { - minFixes = contenderFixes; - candidate = contender; - } - - ++it; - } - - return candidate; -} - -void SmtCore::replaySmtStackEntry( SmtStackEntry *stackEntry ) -{ - struct timespec start = TimeUtils::sampleMicro(); - - if ( _statistics ) - { - _statistics->incUnsignedAttribute( Statistics::NUM_SPLITS ); - _statistics->incUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ); - } - - // Obtain the current state of the engine - EngineState *stateBeforeSplits = new EngineState; - stateBeforeSplits->_stateId = _stateId; - ++_stateId; - _engine->storeState( *stateBeforeSplits, - TableauStateStorageLevel::STORE_ENTIRE_TABLEAU_STATE ); - stackEntry->_engineState = stateBeforeSplits; - - // Apply all the splits - _engine->applySplit( stackEntry->_activeSplit ); - for ( const auto &impliedSplit : stackEntry->_impliedValidSplits ) - _engine->applySplit( impliedSplit ); - - _stack.append( stackEntry ); - - if ( _statistics ) - { - unsigned level = getStackDepth(); - _statistics->setUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL, - level ); - if ( level > _statistics->getUnsignedAttribute - ( Statistics::MAX_DECISION_LEVEL ) ) - _statistics->setUnsignedAttribute( Statistics::MAX_DECISION_LEVEL, - level ); - struct timespec end = TimeUtils::sampleMicro(); - _statistics->incLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO, TimeUtils::timePassed( start, end ) ); - } -} - -void SmtCore::storeSmtState( SmtState &smtState ) -{ - smtState._impliedValidSplitsAtRoot = _impliedValidSplitsAtRoot; - - for ( auto &stackEntry : _stack ) - smtState._stack.append( stackEntry->duplicateSmtStackEntry() ); - - smtState._stateId = _stateId; -} - -bool SmtCore::pickSplitPLConstraint() -{ - if ( _needToSplit ) - { - _constraintForSplitting = _engine->pickSplitPLConstraint - ( _branchingHeuristic ); - } - return _constraintForSplitting != NULL; -} From d9774b788bf17c7b2dc4169fa1f540fd14c03082 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Thu, 15 Sep 2022 15:10:51 -0700 Subject: [PATCH 37/39] Fix formatting in Constraint classes and tests --- src/engine/AbsoluteValueConstraint.cpp | 11 ++- src/engine/AbsoluteValueConstraint.h | 14 ++-- src/engine/DisjunctionConstraint.cpp | 81 +++++++++---------- src/engine/DisjunctionConstraint.h | 10 +-- src/engine/MaxConstraint.cpp | 5 +- src/engine/MaxConstraint.h | 2 +- src/engine/PiecewiseLinearConstraint.cpp | 9 +-- src/engine/PiecewiseLinearConstraint.h | 2 +- src/engine/ReluConstraint.cpp | 16 ++-- src/engine/SignConstraint.cpp | 7 +- src/engine/tests/Test_DisjunctionConstraint.h | 35 ++++---- 11 files changed, 92 insertions(+), 100 deletions(-) diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp index b0ead556f5..158cb3330c 100644 --- a/src/engine/AbsoluteValueConstraint.cpp +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -126,7 +126,7 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound if ( _boundManager == nullptr && existsLowerBound( variable ) && !FloatUtils::gt( bound, getLowerBound( variable ) ) ) - return; + return; setLowerBound( variable, bound ); @@ -180,7 +180,7 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound !FloatUtils::lt( bound, getUpperBound( variable ) ) ) return; - setUpperBound( variable, bound ); + setUpperBound( variable, bound ); // Check whether the phase has become fixed fixPhaseIfNeeded(); @@ -321,7 +321,7 @@ List AbsoluteValueConstraint::getPossibleFixes() return fixes; } -List AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const +List AbsoluteValueConstraint::getSmartFixes( ITableau * /* tableau */ ) const { return getPossibleFixes(); } @@ -601,8 +601,7 @@ void AbsoluteValueConstraint::getEntailedTightenings( List &tighteni } } -void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery - &inputQuery ) +void AbsoluteValueConstraint::transformToUseAuxVariables( InputQuery &inputQuery ) { /* We want to add the two equations @@ -661,7 +660,7 @@ void AbsoluteValueConstraint::getCostFunctionComponent( LinearExpression &cost, PhaseStatus phase ) const { // If the constraint is not active or is fixed, it contributes nothing - if( !isActive() || phaseFixed() ) + if ( !isActive() || phaseFixed() ) return; ASSERT( phase == ABS_PHASE_NEGATIVE || phase == ABS_PHASE_POSITIVE ); diff --git a/src/engine/AbsoluteValueConstraint.h b/src/engine/AbsoluteValueConstraint.h index ab651ace0e..bdd25b6216 100644 --- a/src/engine/AbsoluteValueConstraint.h +++ b/src/engine/AbsoluteValueConstraint.h @@ -23,8 +23,8 @@ ** * context dependent mode, used during the search. ** ** Invoking initializeCDOs method activates the context dependent mode, and the - ** AbsoluteValueConstraint object synchronizes its state automatically with the central - ** Context object. + ** AbsoluteValueConstraint object synchronizes its state automatically with the + ** central Context object. **/ #ifndef __AbsoluteValueConstraint_h__ @@ -34,7 +34,6 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint { - public: /* The f variable is the absolute value of the b variable: @@ -61,8 +60,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint /* Register/unregister the constraint with a talbeau. */ - void registerAsWatcher( ITableau *tableau) override; - void unregisterAsWatcher( ITableau *tableau) override; + void registerAsWatcher( ITableau *tableau ) override; + void unregisterAsWatcher( ITableau *tableau ) override; /* These callbacks are invoked when a watched variable's value @@ -114,8 +113,8 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint /* Returns a list of all cases - { ABS_POSITIVE, ABS_NEGATIVE } - The order of returned cases affects the search, and this method is where related - heuristics should be implemented. + The order of returned cases affects the search, and this method is where + related heuristics should be implemented. */ List getAllCases() const override; @@ -232,4 +231,3 @@ class AbsoluteValueConstraint : public PiecewiseLinearConstraint }; #endif // __AbsoluteValueConstraint_h__ - diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index c7d669595e..fb419fcfa2 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -49,24 +49,24 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio ( 5, serializedDisjunction.length() - 5 ); List values = serializedValues.tokenize( "," ); auto val = values.begin(); - unsigned numDisjuncts = atoi(val->ascii()); + unsigned numDisjuncts = atoi( val->ascii() ); ++val; for ( unsigned i = 0; i < numDisjuncts; ++i ) { PiecewiseLinearCaseSplit split; - unsigned numBounds = atoi(val->ascii()); + unsigned numBounds = atoi( val->ascii() ); ++val; for ( unsigned bi = 0; bi < numBounds; ++bi ) { - Tightening::BoundType type = ( *val == "l") ? Tightening::LB : Tightening::UB; + Tightening::BoundType type = ( *val == "l" ) ? Tightening::LB : Tightening::UB; ++val; - unsigned var = atoi(val->ascii()); + unsigned var = atoi( val->ascii() ); ++val; - double bd = atof(val->ascii()); + double bd = atof( val->ascii() ); ++val; - split.storeBoundTightening( Tightening(var, bd, type) ); + split.storeBoundTightening( Tightening( var, bd, type ) ); } - unsigned numEquations = atoi(val->ascii()); + unsigned numEquations = atoi( val->ascii() ); ++val; for ( unsigned ei = 0; ei < numEquations; ++ei ) @@ -78,29 +78,29 @@ DisjunctionConstraint::DisjunctionConstraint( const String &serializedDisjunctio type = Equation::GE; else { - ASSERT( *val == "e"); + ASSERT( *val == "e" ); } - Equation eq(type); + Equation eq( type ); ++val; - unsigned numAddends = atoi(val->ascii()); + unsigned numAddends = atoi( val->ascii() ); ++val; for ( unsigned ai = 0; ai < numAddends; ++ai ) { - double coef = atof(val->ascii()); + double coef = atof( val->ascii() ); ++val; - unsigned var = atoi(val->ascii()); + unsigned var = atoi( val->ascii() ); ++val; eq.addAddend( coef, var ); } - eq.setScalar(atof(val->ascii())); + eq.setScalar( atof( val->ascii() ) ); ++val; - split.addEquation(eq); + split.addEquation( eq ); } - disjuncts.append(split); + disjuncts.append( split ); } _disjuncts = disjuncts; - for ( unsigned ind = 0; ind < disjuncts.size(); ++ind ) + for ( unsigned ind = 0; ind < disjuncts.size(); ++ind ) _feasibleDisjuncts.append( ind ); extractParticipatingVariables(); @@ -151,11 +151,11 @@ void DisjunctionConstraint::notifyLowerBound( unsigned variable, double bound ) if ( _boundManager == nullptr && existsLowerBound( variable ) && !FloatUtils::gt( bound, getLowerBound( variable ) ) ) - return; + return; setLowerBound( variable, bound ); - //TODO: Maintain a mapping from variables to disjuncts and only check relevant + // TODO: Maintain a mapping from variables to disjuncts and only check relevant // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -167,11 +167,11 @@ void DisjunctionConstraint::notifyUpperBound( unsigned variable, double bound ) if ( _boundManager == nullptr && existsUpperBound( variable ) && !FloatUtils::lt( bound, getUpperBound( variable ) ) ) - return; + return; setUpperBound( variable, bound ); - //TODO: Maintain a mapping from variables to disjuncts and only check relevant + // TODO: Maintain a mapping from variables to disjuncts and only check relevant // disjuncts for feasibility updateFeasibleDisjuncts(); } @@ -207,7 +207,7 @@ List DisjunctionConstraint::getPossibleFixes() c return List(); } -List DisjunctionConstraint::getSmartFixes( ITableau */* tableau */ ) const +List DisjunctionConstraint::getSmartFixes( ITableau * /* tableau */ ) const { // Reluplex does not currently work with Gurobi. ASSERT( _gurobi == NULL ); @@ -230,20 +230,20 @@ List DisjunctionConstraint::getAllCases() const PiecewiseLinearCaseSplit DisjunctionConstraint::getCaseSplit( PhaseStatus phase ) const { - ASSERT ( phase != PHASE_NOT_FIXED ); - return _disjuncts.get( phaseStatusToInd( phase ) ); + ASSERT( phase != PHASE_NOT_FIXED ); + return _disjuncts.get( phaseStatusToInd( phase ) ); } PhaseStatus DisjunctionConstraint::getPhaseStatus() const { - ASSERT ( phaseFixed() ); + ASSERT( phaseFixed() ); return indToPhaseStatus( *_feasibleDisjuncts.begin() ); } PiecewiseLinearCaseSplit DisjunctionConstraint::getImpliedCaseSplit() const { - ASSERT ( isImplication() ); - return _disjuncts.get( phaseStatusToInd ( getImpliedCase() ) ); + ASSERT( isImplication() ); + return _disjuncts.get( phaseStatusToInd( getImpliedCase() ) ); } PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const @@ -251,8 +251,7 @@ PiecewiseLinearCaseSplit DisjunctionConstraint::getValidCaseSplit() const return getImpliedCaseSplit(); } -void DisjunctionConstraint::transformToUseAuxVariables( InputQuery - &inputQuery ) +void DisjunctionConstraint::transformToUseAuxVariables( InputQuery &inputQuery ) { Vector newDisjuncts; for ( const auto &disjunct : _disjuncts ) @@ -390,39 +389,39 @@ bool DisjunctionConstraint::constraintObsolete() const return false; // A Disjunction is obsolete only when a literal is always true. } -void DisjunctionConstraint::getEntailedTightenings( List &/* tightenings */ ) const +void DisjunctionConstraint::getEntailedTightenings( List & /* tightenings */ ) const { } String DisjunctionConstraint::serializeToString() const { String s = "disj,"; - s += Stringf("%u,", _disjuncts.size()); + s += Stringf( "%u,", _disjuncts.size() ); for ( const auto &disjunct : _disjuncts ) { - s += Stringf("%u,", disjunct.getBoundTightenings().size()); + s += Stringf( "%u,", disjunct.getBoundTightenings().size() ); for ( const auto &bound : disjunct.getBoundTightenings() ) { if ( bound._type == Tightening::LB ) - s += Stringf("l,%u,%f,", bound._variable, bound._value); + s += Stringf( "l,%u,%f,", bound._variable, bound._value ); else if ( bound._type == Tightening::UB ) - s += Stringf("u,%u,%f,", bound._variable, bound._value); + s += Stringf( "u,%u,%f,", bound._variable, bound._value ); } - s += Stringf("%u,", disjunct.getEquations().size()); + s += Stringf( "%u,", disjunct.getEquations().size() ); for ( const auto &equation : disjunct.getEquations() ) { if ( equation._type == Equation::LE ) - s += Stringf("l,"); + s += Stringf( "l," ); else if ( equation._type == Equation::GE ) - s += Stringf("g,"); + s += Stringf( "g," ); else - s += Stringf("e,"); - s += Stringf("%u,", equation._addends.size()); + s += Stringf( "e," ); + s += Stringf( "%u,", equation._addends.size() ); for ( const auto &addend : equation._addends ) { - s += Stringf("%f,%u,", addend._coefficient, addend._variable); + s += Stringf( "%f,%u,", addend._coefficient, addend._variable ); } - s += Stringf("%f,", equation._scalar ); + s += Stringf( "%f,", equation._scalar ); } } return s; @@ -495,7 +494,7 @@ void DisjunctionConstraint::updateFeasibleDisjuncts() for ( unsigned ind = 0; ind < _disjuncts.size(); ++ind ) { - if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) ) + if ( caseSplitIsFeasible( _disjuncts.get( ind ) ) ) _feasibleDisjuncts.append( ind ); } } diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index ed112db08c..e6026e901f 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -34,13 +34,13 @@ #ifndef __DisjunctionConstraint_h__ #define __DisjunctionConstraint_h__ -#include "Vector.h" #include "PiecewiseLinearConstraint.h" +#include "Vector.h" class DisjunctionConstraint : public PiecewiseLinearConstraint { public: - ~DisjunctionConstraint() {}; + ~DisjunctionConstraint(){}; DisjunctionConstraint( const List &disjuncts ); DisjunctionConstraint( const Vector &disjuncts ); DisjunctionConstraint( const String &serializedDisjunction ); @@ -154,7 +154,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint virtual bool supportVariableElimination() const override { - return false; + return false; } /* @@ -209,7 +209,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint still feasible, given the current variable bounds */ void updateFeasibleDisjuncts(); - bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit & caseSplit ) const; + bool caseSplitIsFeasible( const PiecewiseLinearCaseSplit &caseSplit ) const; inline PhaseStatus indToPhaseStatus( unsigned ind ) const { @@ -218,7 +218,7 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint inline unsigned phaseStatusToInd( PhaseStatus phase ) const { - //ASSERT( phase != PHASE_NOT_FIXED ); + // ASSERT( phase != PHASE_NOT_FIXED ); return static_cast( phase ) - 1; } }; diff --git a/src/engine/MaxConstraint.cpp b/src/engine/MaxConstraint.cpp index 4dd043a2e3..296d6fbc52 100644 --- a/src/engine/MaxConstraint.cpp +++ b/src/engine/MaxConstraint.cpp @@ -503,7 +503,7 @@ void MaxConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) _auxToElement[auxVar] = newIndex; if ( _phaseStatus == variableToPhase( oldIndex ) ) - _phaseStatus = variableToPhase( newIndex ) ; + _phaseStatus = variableToPhase( newIndex ); } else { @@ -615,7 +615,7 @@ void MaxConstraint::getCostFunctionComponent( LinearExpression &cost, PhaseStatus phase ) const { // If the constraint is not active or is fixed, it contributes nothing - if( !isActive() || phaseFixed() ) + if ( !isActive() || phaseFixed() ) return; if ( phase == MAX_PHASE_ELIMINATED ) @@ -669,7 +669,6 @@ String MaxConstraint::serializeToString() const // Will be ignored in any case output += Stringf( ",%u", 0 ); - //serializeInfeasibleCases( output ); return output; } diff --git a/src/engine/MaxConstraint.h b/src/engine/MaxConstraint.h index fa36337eb0..a80097a03e 100644 --- a/src/engine/MaxConstraint.h +++ b/src/engine/MaxConstraint.h @@ -46,9 +46,9 @@ #ifndef __MaxConstraint_h__ #define __MaxConstraint_h__ -#include "PiecewiseLinearConstraint.h" #include "LinearExpression.h" #include "Map.h" +#include "PiecewiseLinearConstraint.h" #define MAX_VARIABLE_TO_PHASE_OFFSET 1 diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 1dc43f245a..67efe67e17 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -14,6 +14,7 @@ **/ #include "PiecewiseLinearConstraint.h" + #include "Statistics.h" PiecewiseLinearConstraint::PiecewiseLinearConstraint() @@ -170,8 +171,6 @@ void PiecewiseLinearConstraint::markInfeasible( PhaseStatus PiecewiseLinearConstraint::nextFeasibleCase() const { - //ASSERT( getPhaseStatus() == PHASE_NOT_FIXED ); - if ( !isFeasible() ) return CONSTRAINT_INFEASIBLE; @@ -217,9 +216,9 @@ PhaseStatus PiecewiseLinearConstraint::getImpliedCase() const ASSERT( isImplication() || phaseFixed() ); PhaseStatus impliedCase = PHASE_NOT_FIXED; if ( isImplication() ) - impliedCase = nextFeasibleCase(); + impliedCase = nextFeasibleCase(); else - impliedCase = getPhaseStatus(); + impliedCase = getPhaseStatus(); ASSERT( impliedCase != PHASE_NOT_FIXED ); return impliedCase; @@ -230,7 +229,7 @@ void PiecewiseLinearConstraint::serializeInfeasibleCases( String &output ) const { output += Stringf( "Infeasible cases ( %d/%d):", _cdInfeasibleCases->size(), _numCases ); for ( auto infeasible : *_cdInfeasibleCases ) - output += Stringf("%d", infeasible); + output += Stringf( "%d", infeasible ); } } // diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 70c2a98f2f..aa35be7330 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -249,7 +249,7 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher Transform the piecewise linear constraint so that each disjunct contains only bound constraints. */ - virtual void transformToUseAuxVariables( InputQuery & ) {}; + virtual void transformToUseAuxVariables( InputQuery & ){}; void setStatistics( Statistics *statistics ); diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index ac0878a0ce..d0fcadf4d3 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -14,7 +14,6 @@ #include "ReluConstraint.h" -#include "PiecewiseLinearConstraint.h" #include "Debug.h" #include "DivideStrategy.h" #include "FloatUtils.h" @@ -24,6 +23,7 @@ #include "MStringf.h" #include "MarabouError.h" #include "PiecewiseLinearCaseSplit.h" +#include "PiecewiseLinearConstraint.h" #include "Statistics.h" #include "TableauRow.h" @@ -122,12 +122,12 @@ void ReluConstraint::unregisterAsWatcher( ITableau *tableau ) void ReluConstraint::checkIfLowerBoundUpdateFixesPhase( unsigned variable, double bound ) { - if ( variable == _f && FloatUtils::isPositive( bound ) ) - setPhaseStatus( RELU_PHASE_ACTIVE ); - else if ( variable == _b && !FloatUtils::isNegative( bound ) ) - setPhaseStatus( RELU_PHASE_ACTIVE ); - else if ( _auxVarInUse && variable == _aux && FloatUtils::isPositive( bound ) ) - setPhaseStatus( RELU_PHASE_INACTIVE ); + if ( variable == _f && FloatUtils::isPositive( bound ) ) + setPhaseStatus( RELU_PHASE_ACTIVE ); + else if ( variable == _b && !FloatUtils::isNegative( bound ) ) + setPhaseStatus( RELU_PHASE_ACTIVE ); + else if ( _auxVarInUse && variable == _aux && FloatUtils::isPositive( bound ) ) + setPhaseStatus( RELU_PHASE_INACTIVE ); } void ReluConstraint::checkIfUpperBoundUpdateFixesPhase( unsigned variable, double bound ) @@ -849,7 +849,7 @@ void ReluConstraint::getCostFunctionComponent( LinearExpression &cost, PhaseStatus phase ) const { // If the constraint is not active or is fixed, it contributes nothing - if( !isActive() || phaseFixed() ) + if ( !isActive() || phaseFixed() ) return; // This should not be called when the linear constraints have diff --git a/src/engine/SignConstraint.cpp b/src/engine/SignConstraint.cpp index bab1d0c556..f5ed9d1661 100644 --- a/src/engine/SignConstraint.cpp +++ b/src/engine/SignConstraint.cpp @@ -17,8 +17,8 @@ #include "Debug.h" #include "FloatUtils.h" #include "GlobalConfiguration.h" -#include "InputQuery.h" #include "ITableau.h" +#include "InputQuery.h" #include "MStringf.h" #include "MarabouError.h" #include "PiecewiseLinearCaseSplit.h" @@ -298,11 +298,10 @@ String SignConstraint::serializeToString() const return Stringf( "sign,%u,%u", _f, _b ); } -void SignConstraint::getCostFunctionComponent( LinearExpression &cost, - PhaseStatus phase ) const +void SignConstraint::getCostFunctionComponent( LinearExpression &cost, PhaseStatus phase ) const { // If the constraint is not active or is fixed, it contributes nothing - if( !isActive() || phaseFixed() ) + if ( !isActive() || phaseFixed() ) return; ASSERT( phase == SIGN_PHASE_NEGATIVE || phase == SIGN_PHASE_POSITIVE ); diff --git a/src/engine/tests/Test_DisjunctionConstraint.h b/src/engine/tests/Test_DisjunctionConstraint.h index 699cdd6725..1ca8ff8bb6 100644 --- a/src/engine/tests/Test_DisjunctionConstraint.h +++ b/src/engine/tests/Test_DisjunctionConstraint.h @@ -13,16 +13,15 @@ **/ -#include - #include "DisjunctionConstraint.h" +#include "InputQuery.h" #include "MarabouError.h" #include "MockErrno.h" #include "MockTableau.h" -#include "InputQuery.h" -class MockForDisjunctionConstraint - : public MockErrno +#include + +class MockForDisjunctionConstraint : public MockErrno { public: }; @@ -328,15 +327,15 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite DisjunctionConstraint disjunction( caseSplits ); - TS_ASSERT_EQUALS( disjunction.getContext(), static_cast( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getActiveStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getPhaseStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_EQUALS( disjunction.getInfeasibleCasesCDList(), static_cast*>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getContext(), static_cast( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getActiveStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getPhaseStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_EQUALS( disjunction.getInfeasibleCasesCDList(), static_cast *>( nullptr ) ); TS_ASSERT_THROWS_NOTHING( disjunction.initializeCDOs( &context ) ); TS_ASSERT_EQUALS( disjunction.getContext(), &context ); - TS_ASSERT_DIFFERS( disjunction.getActiveStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_DIFFERS( disjunction.getPhaseStatusCDO(), static_cast*>( nullptr ) ); - TS_ASSERT_DIFFERS( disjunction.getInfeasibleCasesCDList(), static_cast*>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getActiveStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getPhaseStatusCDO(), static_cast *>( nullptr ) ); + TS_ASSERT_DIFFERS( disjunction.getInfeasibleCasesCDList(), static_cast *>( nullptr ) ); bool active = false; TS_ASSERT_THROWS_NOTHING( active = disjunction.isActive() ); @@ -520,7 +519,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite Tightening t2( 0, 5, Tightening::UB ); Tightening t3( 3, 0, Tightening::UB ); // First aux introduced here. Tightening t4( 4, 0, Tightening::LB ); // Second aux introduced here. - for ( const auto &t : {t1, t2, t3, t4} ) + for ( const auto &t : { t1, t2, t3, t4 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } ++split; @@ -531,7 +530,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite Tightening t1( 0, 5, Tightening::LB ); Tightening t2( 5, 0, Tightening::UB ); // Third aux introduced here. Tightening t3( 6, 0, Tightening::LB ); // Fourth aux - for ( const auto &t : {t1, t2, t3} ) + for ( const auto &t : { t1, t2, t3 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } ++split; @@ -541,7 +540,7 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite TS_ASSERT( split->getEquations().empty() ); Tightening t1( 7, 0, Tightening::LB ); // 5th aux Tightening t2( 8, 0, Tightening::UB ); // 6th aux - for ( const auto &t : {t1, t2} ) + for ( const auto &t : { t1, t2 } ) TS_ASSERT( split->getBoundTightenings().exists( t ) ); } @@ -623,8 +622,8 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite List recoveredCaseSplits = recoveredDisj.getCaseSplits(); auto split = recoveredCaseSplits.begin(); - TS_ASSERT_EQUALS( *split++, *cs1); - TS_ASSERT_EQUALS( *split++, *cs2); - TS_ASSERT_EQUALS( *split, *cs3); + TS_ASSERT_EQUALS( *split++, *cs1 ); + TS_ASSERT_EQUALS( *split++, *cs2 ); + TS_ASSERT_EQUALS( *split, *cs3 ); } }; From 6dba340583593ee900507d18a1c9aaa4b68fd9bd Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Fri, 16 Sep 2022 17:21:34 -0700 Subject: [PATCH 38/39] Encapsulate context push/pop to track statistics --- src/engine/SmtCore.cpp | 5 ++--- src/engine/SmtCore.h | 6 ++++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/engine/SmtCore.cpp b/src/engine/SmtCore.cpp index 40b6d9a66f..9528c29638 100644 --- a/src/engine/SmtCore.cpp +++ b/src/engine/SmtCore.cpp @@ -148,7 +148,7 @@ void SmtCore::applyTrailEntry( TrailEntry &te, bool isDecision ) if ( isDecision ) { _engine->preContextPushHook(); - _context.push(); + pushContext(); _decisions.push_back( te ); } @@ -246,7 +246,6 @@ void SmtCore::pushContext() } } -bool SmtCore::popSplit() bool SmtCore::popDecisionLevel( TrailEntry &lastDecision ) { ASSERT( static_cast( _context.getLevel() ) == _decisions.size() ); @@ -255,7 +254,7 @@ bool SmtCore::popDecisionLevel( TrailEntry &lastDecision ) SMT_LOG( "Popping trail ..." ); lastDecision = _decisions.back(); - _context.pop(); + popContext(); _engine->postContextPopHook(); SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() ); return true; diff --git a/src/engine/SmtCore.h b/src/engine/SmtCore.h index f33ebe1c7c..ffbb3c364e 100644 --- a/src/engine/SmtCore.h +++ b/src/engine/SmtCore.h @@ -186,6 +186,12 @@ class SmtCore */ bool popSplit(); + /* + Encapsulations of _context.push/pop calls for statistics purposes. + */ + void pushContext(); + void popContext(); + /* Pop a context level - lazily backtracking trail, bounds, etc. Return true if successful, false if the stack is empty. From 6c8759e3b268a65de9dcaa731b9b0aa2ac554241 Mon Sep 17 00:00:00 2001 From: Aleksandar Zeljic Date: Tue, 20 Sep 2022 14:55:08 -0700 Subject: [PATCH 39/39] Update Statistics to reflect changes --- src/common/Statistics.cpp | 14 +++++++------- src/engine/Engine.cpp | 11 +---------- 2 files changed, 8 insertions(+), 17 deletions(-) diff --git a/src/common/Statistics.cpp b/src/common/Statistics.cpp index 2ebb9d54d3..2a69b0e85b 100644 --- a/src/common/Statistics.cpp +++ b/src/common/Statistics.cpp @@ -148,6 +148,12 @@ void Statistics::print() , printPercents( timeSimplexStepsMicro, timeMainLoopMicro ) , timeSimplexStepsMicro / 1000 ); + unsigned long long totalTimePerformingLocalSearch = + getLongAttribute( Statistics::TOTAL_TIME_LOCAL_SEARCH_MICRO ); + printf( "\t\t\t[%.2lf%%] SoI-based local search: %llu milli\n" + , printPercents( totalTimePerformingLocalSearch, timeMainLoopMicro ) + , totalTimePerformingLocalSearch / 1000 + ); unsigned long long totalTimeExplicitBasisBoundTighteningMicro = getLongAttribute(TOTAL_TIME_EXPLICIT_BASIS_BOUND_TIGHTENING_MICRO ); printf( "\t\t[%.2lf%%] Explicit-basis bound tightening: %llu milli\n" @@ -212,12 +218,6 @@ void Statistics::print() , printPercents( totalTimePerformingSymbolicBoundTightening, timeMainLoopMicro ) , totalTimePerformingSymbolicBoundTightening / 1000 ); - unsigned long long totalTimePerformingLocalSearch = - getLongAttribute( Statistics::TOTAL_TIME_LOCAL_SEARCH_MICRO ); - printf( "\t\t[%.2lf%%] SoI-based local search: %llu milli\n" - , printPercents( totalTimePerformingLocalSearch, timeMainLoopMicro ) - , totalTimePerformingLocalSearch / 1000 - ); unsigned long long totalTimeAddingConstraintsToMILPSolver = getLongAttribute( Statistics::TIME_ADDING_CONSTRAINTS_TO_MILP_SOLVER_MICRO ); printf( "\t\t[%.2lf%%] SoI-based local search: %llu milli\n" @@ -326,7 +326,7 @@ void Statistics::print() , getUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL ) , getUnsignedAttribute( Statistics::NUM_VISITED_TREE_STATES ) , getUnsignedAttribute( Statistics::NUM_SPLITS ) - , getUnsignedAttribute( Statistics::NUM_POPS ) ); + , getUnsignedAttribute( Statistics::NUM_CONTEXT_POPS ) ); printf( "\tMax stack depth: %u\n" , getUnsignedAttribute( Statistics::MAX_DECISION_LEVEL ) ); diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 024eb70abf..f344e5b5a7 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1652,16 +1652,7 @@ void Engine::restoreState( const EngineState &state ) _tableau->restoreState( state._tableauState, state._tableauStateStorageLevel ); - // ENGINE_LOG( "\tRestoring constraint states" ); - // for ( auto &constraint : _plConstraints ) - // { - // if ( !state._plConstraintToState.exists( constraint ) ) - // throw MarabouError( MarabouError::MISSING_PL_CONSTRAINT_STATE ); - - // constraint->restoreState( state._plConstraintToState[constraint] ); - // } - - // _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; + _numPlConstraintsDisabledByValidSplits = state._numPlConstraintsDisabledByValidSplits; if ( _lpSolverType == LPSolverType::NATIVE ) {