From 518365bec36601c6ac2dcc09fb25eabc38da8c38 Mon Sep 17 00:00:00 2001 From: Guy Katz Date: Mon, 30 Mar 2020 10:52:46 +0300 Subject: [PATCH 1/4] Improved Relu splits (#232) * test * active split does not require a new var, if aux var is in use * more informative commment --- CMakeLists.txt | 2 +- src/engine/ReluConstraint.cpp | 21 ++++++-- src/engine/tests/Test_ReluConstraint.h | 67 ++++++++++++++++++++++++++ 3 files changed, 84 insertions(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 42bee8126..a58d82bb7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -107,7 +107,7 @@ if (NOT MSVC) set(DEBUG_FLAGS ${COMPILE_FLAGS} ${MEMORY_FLAGS} -g) set(CXXTEST_FLAGS ${DEBUG_FLAGS} -Wno-ignored-qualifiers) else() - set(DEBUG_FLAGS ${COMPILE_FLAGS} ${MEMORY_FLAGS}) + set(DEBUG_FLAGS ${COMPILE_FLAGS} ${MEMORY_FLAGS}) add_definitions(-DNOMINMAX) # remove min max macros endif() diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index f6dd9bc1c..681f88c0a 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -487,11 +487,22 @@ PiecewiseLinearCaseSplit ReluConstraint::getActiveSplit() const // Active phase: b >= 0, b - f = 0 PiecewiseLinearCaseSplit activePhase; activePhase.storeBoundTightening( Tightening( _b, 0.0, Tightening::LB ) ); - Equation activeEquation( Equation::EQ ); - activeEquation.addAddend( 1, _b ); - activeEquation.addAddend( -1, _f ); - activeEquation.setScalar( 0 ); - activePhase.addEquation( activeEquation ); + + if ( _auxVarInUse ) + { + // Special case: aux var in use. + // Because aux = f - b and aux >= 0, we just add that aux <= 0. + activePhase.storeBoundTightening( Tightening( _aux, 0.0, Tightening::UB ) ); + } + else + { + Equation activeEquation( Equation::EQ ); + activeEquation.addAddend( 1, _b ); + activeEquation.addAddend( -1, _f ); + activeEquation.setScalar( 0 ); + activePhase.addEquation( activeEquation ); + } + return activePhase; } diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h index ce995301d..ce597d489 100644 --- a/src/engine/tests/Test_ReluConstraint.h +++ b/src/engine/tests/Test_ReluConstraint.h @@ -264,6 +264,73 @@ class ReluConstraintTestSuite : public CxxTest::TestSuite return true; } + void test_relu_case_splits_with_aux_var() + { + unsigned b = 1; + unsigned f = 4; + + ReluConstraint relu( b, f ); + + relu.notifyLowerBound( b, -10 ); + relu.notifyUpperBound( b, 5 ); + relu.notifyUpperBound( f, 5 ); + + unsigned auxVar = 10; + InputQuery inputQuery; + inputQuery.setNumberOfVariables( auxVar ); + + relu.addAuxiliaryEquations( inputQuery ); + + TS_ASSERT( relu.auxVariableInUse() ); + TS_ASSERT_EQUALS( relu.getAux(), auxVar ); + + List fixes; + List::iterator it; + + List splits = relu.getCaseSplits(); + + Equation activeEquation, inactiveEquation; + + TS_ASSERT_EQUALS( splits.size(), 2U ); + + List::iterator split1 = splits.begin(); + List::iterator split2 = split1; + ++split2; + + TS_ASSERT( isActiveSplitWithAux( b, auxVar, split1 ) || isActiveSplitWithAux( b, auxVar, split2 ) ); + TS_ASSERT( isInactiveSplit( b, f, split1 ) || isInactiveSplit( b, f, split2 ) ); + } + + bool isActiveSplitWithAux( unsigned b, unsigned aux, List::iterator &split ) + { + List bounds = split->getBoundTightenings(); + + TS_ASSERT_EQUALS( bounds.size(), 2U ); + + auto bound = bounds.begin(); + Tightening bound1 = *bound; + + TS_ASSERT_EQUALS( bound1._variable, b ); + TS_ASSERT_EQUALS( bound1._value, 0.0 ); + + if ( bound1._type != Tightening::LB ) + return false; + + ++bound; + + Tightening bound2 = *bound; + + TS_ASSERT_EQUALS( bound2._variable, aux ); + TS_ASSERT_EQUALS( bound2._value, 0.0 ); + + if ( bound2._type != Tightening::UB ) + return false; + + TS_ASSERT( split->getEquations().empty() ); + + return true; + } + void test_register_as_watcher() { unsigned b = 1; From 4ee1ab36949cd435bd8d1f1e0bc3fa2ee78aa824 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 30 Mar 2020 13:43:18 -0700 Subject: [PATCH 2/4] Static flag in cmake (#235) * static build flag * update readme --- CMakeLists.txt | 10 ++++++++-- README.md | 7 +++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a58d82bb7..f8aa636cd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -4,6 +4,7 @@ project(Marabou) set(CMAKE_CXX_STANDARD 11) set(CMAKE_CXX_STANDARD_REQUIRED ON) +option(BUILD_STATIC_MARABOU "Build static Marabou binary" OFF) option(BUILD_PYTHON "Build Python" ON) option(FORCE_PYTHON_BUILD "Build python even if there is only python32" OFF) option(RUN_UNIT_TEST "run unit tests on build" ON) @@ -156,8 +157,13 @@ set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) list(APPEND LIBS Threads::Threads) -# build a static library -target_link_libraries(${MARABOU_LIB} ${LIBS}) +if (BUILD_STATIC_MARABOU) + # build a static library + target_link_libraries(${MARABOU_LIB} ${LIBS} -static) +else() + target_link_libraries(${MARABOU_LIB} ${LIBS}) +endif() + target_include_directories(${MARABOU_LIB} PRIVATE ${LIBS_INCLUDES}) target_compile_options(${MARABOU_LIB} PRIVATE ${RELEASE_FLAGS}) diff --git a/README.md b/README.md index 613558ad9..23391036f 100644 --- a/README.md +++ b/README.md @@ -67,6 +67,13 @@ cd path/to/marabou/repo/folder mkdir build cd build cmake .. +``` +For configuring to build a static Marabou binary, use the following flag +``` +cmake .. -DBUILD_STATIC_MARABOU=ON +``` +To build, run the following: +``` cmake --build . ``` To enable multiprocess build change the last command to: From 6089ab6ea398fdc5b4a308b973d08fa252903b74 Mon Sep 17 00:00:00 2001 From: Guy Katz Date: Tue, 31 Mar 2020 09:46:25 +0300 Subject: [PATCH 3/4] Preprocessing eliminates unused variables (#233) * test * active split does not require a new var, if aux var is in use * support for eliminating unused variables * remove accidental commit * remove print --- src/engine/Equation.cpp | 9 ++++++ src/engine/Equation.h | 7 ++++ src/engine/Preprocessor.cpp | 35 ++++++++++++++++++++ src/engine/Preprocessor.h | 6 ++-- src/engine/tests/Test_Preprocessor.h | 48 +++++++++++++++------------- 5 files changed, 80 insertions(+), 25 deletions(-) diff --git a/src/engine/Equation.cpp b/src/engine/Equation.cpp index e65ce47ea..fb2c4522c 100644 --- a/src/engine/Equation.cpp +++ b/src/engine/Equation.cpp @@ -179,6 +179,15 @@ bool Equation::isVariableMergingEquation( unsigned &x1, unsigned &x2 ) const return false; } +Set Equation::getParticipatingVariables() const +{ + Set result; + for ( const auto &addend : _addends ) + result.insert( addend._variable ); + + return result; +} + // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/Equation.h b/src/engine/Equation.h index af3992f2c..0a17acd0c 100644 --- a/src/engine/Equation.h +++ b/src/engine/Equation.h @@ -18,6 +18,7 @@ #include "List.h" #include "MString.h" +#include "Set.h" /* A class representing a single equation. @@ -69,6 +70,12 @@ class Equation */ bool isVariableMergingEquation( unsigned &x1, unsigned &x2 ) const; + /* + Get the set of indices of all variables that participate in this + equation. + */ + Set getParticipatingVariables() const; + List _addends; double _scalar; EquationType _type; diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp index c30bbea7a..fc087eb05 100644 --- a/src/engine/Preprocessor.cpp +++ b/src/engine/Preprocessor.cpp @@ -494,10 +494,45 @@ bool Preprocessor::processIdenticalVariables() void Preprocessor::collectFixedValues() { + // Compute all used variables: + // 1. Variables that appear in equations + // 2. Variables that participate in PL constraints + // 3. Variables that have been merged (and hence, previously + // appeared in an equation) + Set usedVariables; + for ( const auto &equation : _preprocessed.getEquations() ) + usedVariables += equation.getParticipatingVariables(); + for ( const auto &constraint : _preprocessed.getPiecewiseLinearConstraints() ) + { + for ( const auto &var : constraint->getParticipatingVariables() ) + usedVariables.insert( var ); + } + for ( const auto &merged : _mergedVariables ) + usedVariables.insert( merged.first ); + + // Collect any variables with identical lower and upper bounds, or + // which are unused for ( unsigned i = 0; i < _preprocessed.getNumberOfVariables(); ++i ) { if ( FloatUtils::areEqual( _preprocessed.getLowerBound( i ), _preprocessed.getUpperBound( i ) ) ) + { _fixedVariables[i] = _preprocessed.getLowerBound( i ); + } + else if ( !usedVariables.exists( i ) ) + { + // If possible, choose a value that matches the debugging + // solution. Otherwise, pick the lower bound + if ( _preprocessed._debuggingSolution.exists( i ) && + _preprocessed._debuggingSolution[i] >= _preprocessed.getLowerBound( i ) && + _preprocessed._debuggingSolution[i] <= _preprocessed.getUpperBound( i ) ) + { + _fixedVariables[i] = _preprocessed._debuggingSolution[i]; + } + else + { + _fixedVariables[i] = _preprocessed.getLowerBound( i ); + } + } } } diff --git a/src/engine/Preprocessor.h b/src/engine/Preprocessor.h index 3380982de..b1c828231 100644 --- a/src/engine/Preprocessor.h +++ b/src/engine/Preprocessor.h @@ -77,7 +77,8 @@ class Preprocessor bool processIdenticalVariables(); /* - Collect all variables whose lower and upper bounds are equal + Collect all variables whose lower and upper bounds are equal, or + which do not appear anywhere in the input query. */ void collectFixedValues(); @@ -88,7 +89,8 @@ class Preprocessor void separateMergedAndFixed(); /* - Eliminate any variables that have become fixed or merged with an identical variable + Eliminate any variables that have become fixed or merged with an + identical variable */ void eliminateVariables(); diff --git a/src/engine/tests/Test_Preprocessor.h b/src/engine/tests/Test_Preprocessor.h index 90717e7a1..ae09165e0 100644 --- a/src/engine/tests/Test_Preprocessor.h +++ b/src/engine/tests/Test_Preprocessor.h @@ -353,26 +353,26 @@ class PreprocessorTestSuite : public CxxTest::TestSuite InputQuery inputQuery; inputQuery.setNumberOfVariables( 10 ); - inputQuery.setLowerBound( 0, 1 ); - inputQuery.setUpperBound( 0, 1 ); - inputQuery.setLowerBound( 1, 0 ); + inputQuery.setLowerBound( 0, 1 ); // fixed + inputQuery.setUpperBound( 0, 1 ); + inputQuery.setLowerBound( 1, 0 ); // fixed inputQuery.setUpperBound( 1, 5 ); - inputQuery.setLowerBound( 2, 2 ); + inputQuery.setLowerBound( 2, 2 ); // unused inputQuery.setUpperBound( 2, 3 ); - inputQuery.setLowerBound( 3, 5 ); - inputQuery.setUpperBound( 3, 5 ); - inputQuery.setLowerBound( 4, 0 ); - inputQuery.setUpperBound( 4, 10 ); - inputQuery.setLowerBound( 5, 0 ); - inputQuery.setUpperBound( 5, 10 ); - inputQuery.setLowerBound( 6, 5 ); - inputQuery.setUpperBound( 6, 5 ); - inputQuery.setLowerBound( 7, 0 ); - inputQuery.setUpperBound( 7, 9 ); - inputQuery.setLowerBound( 8, 0 ); - inputQuery.setUpperBound( 8, 9 ); - inputQuery.setLowerBound( 9, 0 ); - inputQuery.setUpperBound( 9, 9 ); + inputQuery.setLowerBound( 3, 5 ); // fixed + inputQuery.setUpperBound( 3, 5 ); + inputQuery.setLowerBound( 4, 0 ); // unused + inputQuery.setUpperBound( 4, 10 ); + inputQuery.setLowerBound( 5, 0 ); // unused + inputQuery.setUpperBound( 5, 10 ); + inputQuery.setLowerBound( 6, 5 ); // fxied + inputQuery.setUpperBound( 6, 5 ); + inputQuery.setLowerBound( 7, 0 ); // normal + inputQuery.setUpperBound( 7, 9 ); + inputQuery.setLowerBound( 8, 0 ); // normal + inputQuery.setUpperBound( 8, 9 ); + inputQuery.setLowerBound( 9, 0 ); // unused + inputQuery.setUpperBound( 9, 9 ); // x0 + x1 + x3 = 10 Equation equation1; @@ -382,7 +382,7 @@ class PreprocessorTestSuite : public CxxTest::TestSuite equation1.setScalar( 10 ); inputQuery.addEquation( equation1 ); - // x2 + x3 = 6 + // x7 + x8 = 12 Equation equation2; equation2.addAddend( 1, 7 ); equation2.addAddend( 1, 8 ); @@ -391,9 +391,11 @@ class PreprocessorTestSuite : public CxxTest::TestSuite InputQuery processed = Preprocessor().preprocess( inputQuery, true ); - // Variables x0, x3 and x6 were fixed and should be eliminated. + // Variables 2, 4, 5 and 9 are unused and should be eliminated. + // Variables 0, 3 and 6 were fixed and should be eliminated. // Because of equation1 variable 1 should become fixed at 4 and be eliminated too. - TS_ASSERT_EQUALS( processed.getNumberOfVariables(), 6U ); + // This only leaves variables 7 and 8. + TS_ASSERT_EQUALS( processed.getNumberOfVariables(), 2U ); // Equation 1 should have been eliminated TS_ASSERT_EQUALS( processed.getEquations().size(), 1U ); @@ -402,10 +404,10 @@ class PreprocessorTestSuite : public CxxTest::TestSuite Equation preprocessedEquation = *processed.getEquations().begin(); List::iterator addend = preprocessedEquation._addends.begin(); TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); - TS_ASSERT_EQUALS( addend->_variable, 3U ); + TS_ASSERT_EQUALS( addend->_variable, 0U ); ++addend; TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); - TS_ASSERT_EQUALS( addend->_variable, 4U ); + TS_ASSERT_EQUALS( addend->_variable, 1U ); TS_ASSERT_EQUALS( preprocessedEquation._scalar, 12.0 ); } From 38d97ab7c2beb51e5ab0a7e65318cee0d54f22dc Mon Sep 17 00:00:00 2001 From: Guy Katz Date: Tue, 31 Mar 2020 10:01:38 +0300 Subject: [PATCH 4/4] Absolute value PL constraint (#228) * initial abs cinstraint, three files - h, cpp and error * variable name * removing run3 files * wip * Sources.mk - add AbsConstraint.cpp; AbsConstraint.cpp - Add some signatures, fix satisfied(), implement getPossibleFixes() * add constant ABS_CONSTRAINT_COMPARISON_TOLERANCE * add ifndef to AbsConstraint.h * add some signatures to AbsConstraint.h and fix some signatures at AbsConstraint.cpp * fixing errors * fix errors * split and more * add some signatures * notify functions * finsh write functions. next step - testing * test file * notifyLowerBound and notifyUpperBound * test with sumathi * add check at notify lower/upper bound if new bound is better then old bound. add some documentation * getEntailedTightenings * fix at notifyUpperBound * Test to entailed_tighteningst * duplicate and restore * register_and_unregister * test for notifyVariableValue, satisfied and updateVariableIndex * more tests * edit comments * more tests * some fixes * some fixes * fix * add getter to _lowerBounds * test_abs_entailed_tighteningst * fix * upper\lower bpound f <0 , get_upper_bound * more testing and print func * fix x_f<0 * fix x_f<0 * some changes * some changes * without test_abs_entailed_tighteningst2 * some changes if upper/ lower bound <0 * fix tighteningst2 * some fixes * more tests for getEntailedTightenings * add cases to getEntailedTightnings * finish testing getEntailedTighteningsgit add Test_AbsConstraint.h! * change non overlap at getEntailedTightenings * change ovelap tests * CMakeLists * test fixes and case split * fix * finish tests * abs_feasible_2 like relu_feasible_2 * add regress for abs constraint * add some print at getEntailedTightening befor ASSERT * notifynotifyLowerBound if var == _f && bound <0. i delete & bound ==0 * same as befor change not is posetive * change the part when the bounds of _f need to be zero * notifyLowerBound and upper, when update the prtner, if var is f, i add && bound>0 * test_abs_entailed_tighteningst0 if lower bound of f is <0 * check that _constraintBoundTightener exists before using it * add test for _f bound<0 * more test lower bounf f<0 * 1 is UNSAT- not working, 2 is SAT * getE fix overlap * get lower bound, change to double * more tests * add feasible2 * non * better printing of bounds * without no overlap * fix * unsat * more regress * getEntailedTightenings without max positive * fix a bug regarding bound extraction of fixed variables * Entailed_Tightenings without max and min * more regress * match to tha changes at absconstraint * without max/min at getEntailedTightenings * match to changes at ans * more regress * add new files acas regress fixed input and with constraint. inputQuery fix typo * check correctness * fix the new network, but there is steal problem * fix the new network, but there is yet problem * change fix point * configuration * fix acas abs constraint * add for at the main, add documentaion * coding style * changes * minor * the old regression test moved to be a system test * moving some files around * typo * compilation issues * cleanup * cleanup * refactoring * finished pass on main class * remove AbsError class * compilation * thorough phass over the unit tests * more polishing of bound tighting and phase-fixing-detection * system test cleanup * dont override variable elimination * additional tests * some more cleanup * remove a few comments * Merge from master (#231) * Use ndebug (#229) Used NDEBUG flag to indicate of not debug mode (CMake adds this flag be default in release mode) Default compilation is release mode * Cmake: Minor (#230) * fix a couple of warnings * minor Co-authored-by: yuvaljacoby Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> * bug fix * remove "unused"s * minor * Aleks' comments * space * test no longer needed Co-authored-by: shirana Co-authored-by: Christopher Lazarus Co-authored-by: Guy Katz Co-authored-by: yuvaljacoby Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> --- src/configuration/GlobalConfiguration.cpp | 1 + src/configuration/GlobalConfiguration.h | 5 +- src/engine/AbsoluteValueConstraint.cpp | 440 +++++++ src/engine/AbsoluteValueConstraint.h | 172 +++ src/engine/CMakeLists.txt | 1 + src/engine/Engine.cpp | 6 + src/engine/InputQuery.cpp | 25 +- src/engine/InputQuery.h | 3 +- src/engine/PiecewiseLinearConstraint.h | 13 + src/engine/Preprocessor.cpp | 1 - src/engine/ReluConstraint.cpp | 2 +- src/engine/ReluConstraint.h | 9 +- .../tests/Test_AbsoluteValueConstraint.h | 1059 +++++++++++++++++ src/engine/tests/Test_ReluConstraint.h | 1 - src/system_tests/CMakeLists.txt | 2 + src/system_tests/Test_AbsoluteValue.h | 246 ++++ 16 files changed, 1976 insertions(+), 10 deletions(-) create mode 100644 src/engine/AbsoluteValueConstraint.cpp create mode 100644 src/engine/AbsoluteValueConstraint.h create mode 100644 src/engine/tests/Test_AbsoluteValueConstraint.h create mode 100644 src/system_tests/Test_AbsoluteValue.h diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp index c6986cd98..d5e4013dd 100644 --- a/src/configuration/GlobalConfiguration.cpp +++ b/src/configuration/GlobalConfiguration.cpp @@ -69,6 +69,7 @@ const double GlobalConfiguration::PSE_GAMMA_ERROR_THRESHOLD = 0.001; const double GlobalConfiguration::PSE_GAMMA_UPDATE_TOLERANCE = 0.000000001; const double GlobalConfiguration::RELU_CONSTRAINT_COMPARISON_TOLERANCE = 0.001; +const double GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE = 0.001; const bool GlobalConfiguration::ONLY_AUX_INITIAL_BASIS = false; diff --git a/src/configuration/GlobalConfiguration.h b/src/configuration/GlobalConfiguration.h index d8e217947..6786c50e4 100644 --- a/src/configuration/GlobalConfiguration.h +++ b/src/configuration/GlobalConfiguration.h @@ -131,9 +131,12 @@ class GlobalConfiguration // PSE's Gamma function's update tolerance static const double PSE_GAMMA_UPDATE_TOLERANCE; - // The tolerance for checking whether f = Relu( b ), to determine a ReLU's statisfaction + // The tolerance for checking whether f = Relu( b ) static const double RELU_CONSTRAINT_COMPARISON_TOLERANCE; + // The tolerance for checking whether f = Abs( b ) + static const double ABS_CONSTRAINT_COMPARISON_TOLERANCE; + // Should the initial basis be comprised only of auxiliary (row) variables? static const bool ONLY_AUX_INITIAL_BASIS; diff --git a/src/engine/AbsoluteValueConstraint.cpp b/src/engine/AbsoluteValueConstraint.cpp new file mode 100644 index 000000000..e5d9d540c --- /dev/null +++ b/src/engine/AbsoluteValueConstraint.cpp @@ -0,0 +1,440 @@ +/********************* */ +/*! \file ReluConstraint.cpp + ** \verbatim + ** Top contributors (to current version): + ** Shiran Aziz, Guy Katz + ** This file is part of the Marabou project. + ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + **/ + +#include "AbsoluteValueConstraint.h" +#include "ConstraintBoundTightener.h" +#include "Debug.h" +#include "FloatUtils.h" +#include "ITableau.h" +#include "MStringf.h" +#include "MarabouError.h" +#include "PiecewiseLinearCaseSplit.h" +#include "Statistics.h" + +AbsoluteValueConstraint::AbsoluteValueConstraint( unsigned b, unsigned f ) + : _b( b ) + , _f( f ) + , _haveEliminatedVariables( false ) +{ + setPhaseStatus( PhaseStatus::PHASE_NOT_FIXED ); +} + +PiecewiseLinearConstraint *AbsoluteValueConstraint::duplicateConstraint() const +{ + AbsoluteValueConstraint *clone = new AbsoluteValueConstraint( _b, _f ); + *clone = *this; + return clone; +} + +void AbsoluteValueConstraint::restoreState( const PiecewiseLinearConstraint *state ) +{ + const AbsoluteValueConstraint *abs = dynamic_cast( state ); + *this = *abs; +} + +void AbsoluteValueConstraint::registerAsWatcher( ITableau *tableau ) +{ + tableau->registerToWatchVariable( this, _b ); + tableau->registerToWatchVariable( this, _f ); +} + +void AbsoluteValueConstraint::unregisterAsWatcher( ITableau *tableau ) +{ + tableau->unregisterToWatchVariable( this, _b ); + tableau->unregisterToWatchVariable( this, _f ); +} + +void AbsoluteValueConstraint::notifyVariableValue( unsigned variable, double value ) +{ + _assignment[variable] = value; +} + +void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound ) +{ + if ( _statistics ) + _statistics->incNumBoundNotificationsPlConstraints(); + + if ( _lowerBounds.exists( variable ) && + !FloatUtils::gt( bound, _lowerBounds[variable] ) ) + return; + + _lowerBounds[variable] = bound; + + // Check whether the phase has become fixed + fixPhaseIfNeeded(); + + // Update partner's bound + if ( isActive() && _constraintBoundTightener ) + { + if ( variable == _b ) + { + if ( bound < 0 ) + { + double fUpperBound = FloatUtils::max( -bound, _upperBounds[_b] ); + _constraintBoundTightener->registerTighterUpperBound( _f, fUpperBound ); + } + else + { + // Phase is fixed, don't care about this case + } + } + else + { + // F's lower bound can only cause bound propagations if it + // fixes the phase of the constraint, so no need to + // bother. The only exception is if the lower bound is, + // for some reason, negative + if ( bound < 0 ) + _constraintBoundTightener->registerTighterLowerBound( _f, 0 ); + } + } +} + +void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound ) +{ + if ( _statistics ) + _statistics->incNumBoundNotificationsPlConstraints(); + + if ( _upperBounds.exists( variable ) && !FloatUtils::lt( bound, _upperBounds[variable] ) ) + return; + + _upperBounds[variable] = bound; + + // Check whether the phase has become fixed + fixPhaseIfNeeded(); + + // Update partner's bound + if ( isActive() && _constraintBoundTightener ) + { + if ( variable == _b ) + { + if ( bound > 0 ) + { + double fUpperBound = FloatUtils::max( bound, -_lowerBounds[_b] ); + _constraintBoundTightener->registerTighterUpperBound( _f, fUpperBound ); + } + else + { + // Phase is fixed, don't care about this case + } + } + else + { + // F's upper bound can restrict both bounds of B + if ( bound < _upperBounds[_b] ) + _constraintBoundTightener->registerTighterUpperBound( _b, bound ); + + if ( -bound > _lowerBounds[_b] ) + _constraintBoundTightener->registerTighterLowerBound( _b, -bound ); + } + } +} + +bool AbsoluteValueConstraint::participatingVariable(unsigned variable ) const +{ + return ( variable == _b ) || ( variable == _f ); +} + +List AbsoluteValueConstraint::getParticipatingVariables() const +{ + return List( { _b, _f } ); +} + +bool AbsoluteValueConstraint::satisfied() const +{ + if ( !( _assignment.exists( _b ) && _assignment.exists( _f ) ) ) + throw MarabouError( MarabouError::PARTICIPATING_VARIABLES_ABSENT ); + + double bValue = _assignment.get( _b ); + double fValue = _assignment.get( _f ); + + // Possible violations: + // 1. f is negative + // 2. f is positive, abs(b) and f are not equal + + if ( fValue < 0 ) + return false; + + return FloatUtils::areEqual( FloatUtils::abs( bValue ), + fValue, + GlobalConfiguration::ABS_CONSTRAINT_COMPARISON_TOLERANCE ); +} + +List AbsoluteValueConstraint::getPossibleFixes() const +{ + ASSERT( !satisfied() ); + ASSERT( _assignment.exists( _b ) ); + ASSERT( _assignment.exists( _f ) ); + + double bValue = _assignment.get( _b ); + double fValue = _assignment.get( _f ); + + ASSERT( !FloatUtils::isNegative( fValue ) ); + + List fixes; + + // Possible violations: + // 1. f is positive, b is positive, b and f are unequal + // 2. f is positive, b is negative, -b and f are unequal + + fixes.append( PiecewiseLinearConstraint::Fix( _b, fValue ) ); + fixes.append( PiecewiseLinearConstraint::Fix( _b, -fValue ) ); + fixes.append( PiecewiseLinearConstraint::Fix( _f, FloatUtils::abs( bValue ) ) ); + + return fixes; +} + +List AbsoluteValueConstraint::getSmartFixes( ITableau */* tableau */ ) const +{ + return getPossibleFixes(); +} + +List AbsoluteValueConstraint::getCaseSplits() const +{ + ASSERT( _phaseStatus == PhaseStatus::PHASE_NOT_FIXED ); + + List splits; + splits.append( getNegativeSplit() ); + splits.append( getPositiveSplit() ); + + return splits; +} + +PiecewiseLinearCaseSplit AbsoluteValueConstraint::getNegativeSplit() const +{ + PiecewiseLinearCaseSplit negativePhase; + + // Negative phase: b <= 0, b + f = 0 + negativePhase.storeBoundTightening( Tightening( _b, 0.0, Tightening::UB ) ); + + Equation negativeEquation( Equation::EQ ); + negativeEquation.addAddend( 1, _b ); + negativeEquation.addAddend( 1, _f ); + negativeEquation.setScalar( 0 ); + negativePhase.addEquation( negativeEquation ); + + return negativePhase; +} + +PiecewiseLinearCaseSplit AbsoluteValueConstraint::getPositiveSplit() const +{ + PiecewiseLinearCaseSplit positivePhase; + + // Positive phase: b >= 0, b - f = 0 + positivePhase.storeBoundTightening( Tightening( _b, 0.0, Tightening::LB ) ); + + //b - f = 0 + Equation positiveEquation( Equation::EQ ); + positiveEquation.addAddend( 1, _b ); + positiveEquation.addAddend( -1, _f ); + positiveEquation.setScalar( 0 ); + positivePhase.addEquation( positiveEquation ); + + return positivePhase; +} + +bool AbsoluteValueConstraint::phaseFixed() const +{ + return _phaseStatus != PhaseStatus::PHASE_NOT_FIXED; +} + +PiecewiseLinearCaseSplit AbsoluteValueConstraint::getValidCaseSplit() const +{ + ASSERT( _phaseStatus != PhaseStatus::PHASE_NOT_FIXED ); + + if ( _phaseStatus == PhaseStatus::PHASE_POSITIVE ) + return getPositiveSplit(); + + return getNegativeSplit(); +} + +void AbsoluteValueConstraint::eliminateVariable( unsigned /* variable */, double /* fixedValue */ ) +{ + // In an absolute value constraint, if a variable is removed the + // entire constraint can be discarded + _haveEliminatedVariables = true; +} + +void AbsoluteValueConstraint::updateVariableIndex( unsigned oldIndex, unsigned newIndex ) +{ + ASSERT( oldIndex == _b || oldIndex == _f ); + ASSERT( !_assignment.exists( newIndex ) && + !_lowerBounds.exists( newIndex ) && + !_upperBounds.exists( newIndex ) && + newIndex != _b && newIndex != _f ); + + if ( _assignment.exists( oldIndex ) ) + { + _assignment[newIndex] = _assignment.get( oldIndex ); + _assignment.erase( oldIndex ); + } + + if ( _lowerBounds.exists( oldIndex ) ) + { + _lowerBounds[newIndex] = _lowerBounds.get( oldIndex ); + _lowerBounds.erase( oldIndex ); + } + + if ( _upperBounds.exists( oldIndex ) ) + { + _upperBounds[newIndex] = _upperBounds.get( oldIndex ); + _upperBounds.erase( oldIndex ); + } + + if ( oldIndex == _b ) + _b = newIndex; + else + _f = newIndex; +} + +bool AbsoluteValueConstraint::constraintObsolete() const +{ + return _haveEliminatedVariables; +} + +void AbsoluteValueConstraint::getEntailedTightenings( List &tightenings ) const +{ + ASSERT( _lowerBounds.exists( _b ) && _lowerBounds.exists( _f ) && + _upperBounds.exists( _b ) && _upperBounds.exists( _f ) ); + + // Upper bounds + double bUpperBound = _upperBounds[_b]; + double fUpperBound = _upperBounds[_f]; + // Lower bounds + double bLowerBound = _lowerBounds[_b]; + double fLowerBound = _lowerBounds[_f]; + + // F's lower bound should always be non-negative + if ( fLowerBound < 0 ) + { + tightenings.append( Tightening( _f, 0.0, Tightening::LB ) ); + fLowerBound = 0; + } + + if ( bLowerBound >= 0 ) + { + // Positive phase, all bounds much match + tightenings.append( Tightening( _f, bLowerBound, Tightening::LB ) ); + tightenings.append( Tightening( _b, fLowerBound, Tightening::LB ) ); + + tightenings.append( Tightening( _f, bUpperBound, Tightening::UB ) ); + tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) ); + } + + else if ( bUpperBound <= 0 ) + { + // Negative phase, all bounds must match + + tightenings.append( Tightening( _f, -bUpperBound, Tightening::LB ) ); + tightenings.append( Tightening( _b, -fUpperBound, Tightening::LB ) ); + + tightenings.append( Tightening( _f, -bLowerBound, Tightening::UB ) ); + tightenings.append( Tightening( _b, -fLowerBound, Tightening::UB ) ); + } + + else if ( bLowerBound < 0 && bUpperBound >= 0 && FloatUtils::isZero( fLowerBound ) ) + { + // Phase undetermined, b can be either positive or negative, f can be 0 + tightenings.append( Tightening( _b, -fUpperBound , Tightening::LB ) ); + tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) ); + tightenings.append( Tightening( _f, FloatUtils::max( -bLowerBound , bUpperBound ), Tightening::UB ) ); + } + + else if ( bLowerBound < 0 && bUpperBound >= 0 && fLowerBound > 0 ) + { + // Phase undetermined, b can be either positive or negative, f strictly positive + tightenings.append( Tightening( _b, -fUpperBound, Tightening::LB ) ); + tightenings.append( Tightening( _b, fUpperBound, Tightening::UB ) ); + tightenings.append( Tightening( _f, FloatUtils::max( -bLowerBound, bUpperBound ), Tightening::UB ) ); + + // Below we test if the phase has actually become fixed + if ( fLowerBound > -bLowerBound ) + { + // Positive phase + tightenings.append( Tightening( _b, fLowerBound, Tightening::LB ) ); + } + + if ( fLowerBound > bUpperBound ) + { + // Negative phase + tightenings.append( Tightening( _b, -fLowerBound, Tightening::UB ) ); + } + + } +} + +void AbsoluteValueConstraint::getAuxiliaryEquations( List &/* newEquations */ ) const +{ + // Currently unsupported +} + +String AbsoluteValueConstraint::serializeToString() const +{ + // Output format is: Abs,f,b + return Stringf( "absoluteValue,%u,%u", _f, _b ); +} + +void AbsoluteValueConstraint::fixPhaseIfNeeded() +{ + // Option 1: b's range is strictly positive + if ( _lowerBounds.exists( _b ) && _lowerBounds[_b] >= 0 ) + { + setPhaseStatus( PHASE_POSITIVE ); + return; + } + + // Option 2: b's range is strictly negative: + if ( _upperBounds.exists( _b ) && _upperBounds[_b] <= 0 ) + { + setPhaseStatus( PHASE_NEGATIVE ); + return; + } + + if ( !_lowerBounds.exists( _f ) ) + return; + + // Option 3: f's range is strictly disjoint from b's positive + // range + if ( _upperBounds.exists( _b ) && _lowerBounds[_f] > _upperBounds[_b] ) + { + setPhaseStatus( PHASE_NEGATIVE ); + return; + } + + // Option 4: f's range is strictly disjoint from b's negative + // range, in absolute value + if ( _lowerBounds.exists( _b ) && _lowerBounds[_f] > -_lowerBounds[_b] ) + { + setPhaseStatus( PHASE_POSITIVE ); + return; + } +} + +void AbsoluteValueConstraint::setPhaseStatus( PhaseStatus phaseStatus ) +{ + _phaseStatus = phaseStatus; +} + +bool AbsoluteValueConstraint::supportsSymbolicBoundTightening() const +{ + return false; +} + +// +// Local Variables: +// compile-command: "make -C ../.. " +// tags-file-name: "../../TAGS" +// c-basic-offset: 4 +// End: +// diff --git a/src/engine/AbsoluteValueConstraint.h b/src/engine/AbsoluteValueConstraint.h new file mode 100644 index 000000000..a652c0b1d --- /dev/null +++ b/src/engine/AbsoluteValueConstraint.h @@ -0,0 +1,172 @@ +/********************* */ +/*! \file ReluConstraint.h + ** \verbatim + ** Top contributors (to current version): + ** Shiran Aziz, Guy Katz + ** This file is part of the Marabou project. + ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + + **/ + +#ifndef __AbsoluteValueConstraint_h__ +#define __AbsoluteValueConstraint_h__ + +#include "PiecewiseLinearConstraint.h" + +class AbsoluteValueConstraint : public PiecewiseLinearConstraint +{ + +public: + enum PhaseStatus { + PHASE_NOT_FIXED = 0, + PHASE_POSITIVE = 1, + PHASE_NEGATIVE = 2, + }; + + AbsoluteValueConstraint( unsigned b, unsigned f ); + + /* + Return a clone of the constraint. + */ + PiecewiseLinearConstraint *duplicateConstraint() const; + + /* + Restore the state of this constraint from the given one. + */ + void restoreState( const PiecewiseLinearConstraint *state ); + + /* + Register/unregister the constraint with a talbeau. + */ + void registerAsWatcher( ITableau *tableau); + void unregisterAsWatcher( ITableau *tableau); + + /* + These callbacks are invoked when a watched variable's value + changes, or when its bounds change. + */ + void notifyVariableValue( unsigned variable, double value ); + void notifyLowerBound( unsigned variable, double bound ); + void notifyUpperBound( unsigned variable, double bound ); + + /* + Returns true iff the variable participates in this piecewise + linear constraint. + */ + bool participatingVariable( unsigned variable ) const; + + /* + Get the list of variables participating in this constraint. + */ + List getParticipatingVariables() const; + + /* + Returns true iff the assignment satisfies the constraint + */ + bool satisfied() const; + + /* + Returns a list of possible fixes for the violated constraint. + */ + List getPossibleFixes() const; + + /* + Return a list of smart fixes for violated constraint. + Currently not implemented, just calls getPossibleFixes(). + */ + List getSmartFixes( ITableau *tableau ) const; + + /* + Returns the list of case splits that this piecewise linear + constraint breaks into: + + y = |x| <--> + ( x <= 0 /\ y = -x ) \/ ( x >= 0 /\ y = x ) + */ + List getCaseSplits() const; + + /* + Check whether the constraint's phase has been fixed. + */ + void fixPhaseIfNeeded(); + bool phaseFixed() const; + + /* + * If the constraint's phase has been fixed, get the (valid) case split. + */ + PiecewiseLinearCaseSplit getValidCaseSplit() const; + + /* + Preprocessing related functions, to inform that a variable has + been eliminated completely because it was fixed to some value, + or that a variable's index has changed (e.g., x4 is now called + x2). constraintObsolete() returns true iff and the constraint + has become obsolote as a result of variable eliminations. + */ + void eliminateVariable( unsigned variable, double fixedValue ); + void updateVariableIndex( unsigned oldIndex, unsigned newIndex ); + bool constraintObsolete() const; + + /* + Get the tightenings entailed by the constraint. + */ + void getEntailedTightenings( List &tightenings ) const; + + /* + For preprocessing: get any auxiliary equations that this + constraint would like to add to the equation pool. In the ReLU + case, this is an equation of the form aux = f - b, where aux is + non-negative. + */ + void getAuxiliaryEquations( List &newEquations ) const; + + /* + Returns string with shape: absoluteValue,_f,_b + */ + String serializeToString() const; + + /* + Return true if and only if this piecewise linear constraint supports + symbolic bound tightening. + */ + bool supportsSymbolicBoundTightening() const; + +private: + /* + The variables that make up this constraint; _f = | _b |. + */ + unsigned _b, _f; + + /* + True iff _b or _f have been eliminated. + */ + bool _haveEliminatedVariables; + + /* + The phase status of this constraint: positive, negative, or not + yet fixed. + */ + PhaseStatus _phaseStatus; + void setPhaseStatus( PhaseStatus phaseStatus ); + + /* + The two case splits. + */ + PiecewiseLinearCaseSplit getPositiveSplit() const; + PiecewiseLinearCaseSplit getNegativeSplit() const; +}; + +#endif // __AbsoluteValueConstraint_h__ + +// +// Local Variables: +// compile-command: "make -C ../.. " +// tags-file-name: "../../TAGS" +// c-basic-offset: 4 +// End: +// diff --git a/src/engine/CMakeLists.txt b/src/engine/CMakeLists.txt index e2e4229eb..46122d992 100644 --- a/src/engine/CMakeLists.txt +++ b/src/engine/CMakeLists.txt @@ -16,6 +16,7 @@ macro(engine_add_unit_test name) USE_MOCK_ENGINE "unit") endmacro() +engine_add_unit_test(AbsoluteValueConstraint) engine_add_unit_test(BlandsRule) engine_add_unit_test(ConstraintBoundTightener) engine_add_unit_test(ConstraintMatrixAnalyzer) diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 0f539d96b..fc48b43e8 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -1125,6 +1125,8 @@ void Engine::extractSolution( InputQuery &inputQuery ) if ( _preprocessor.variableIsFixed( variable ) ) { inputQuery.setSolutionValue( i, _preprocessor.getFixedValue( variable ) ); + inputQuery.setLowerBound( i, _preprocessor.getFixedValue( variable ) ); + inputQuery.setUpperBound( i, _preprocessor.getFixedValue( variable ) ); continue; } @@ -1134,10 +1136,14 @@ void Engine::extractSolution( InputQuery &inputQuery ) // Finally, set the assigned value inputQuery.setSolutionValue( i, _tableau->getValue( variable ) ); + inputQuery.setLowerBound( i, _tableau->getLowerBound( variable ) ); + inputQuery.setUpperBound( i, _tableau->getUpperBound( variable ) ); } else { inputQuery.setSolutionValue( i, _tableau->getValue( i ) ); + inputQuery.setLowerBound( i, _tableau->getLowerBound( i ) ); + inputQuery.setUpperBound( i, _tableau->getUpperBound( i ) ); } } } diff --git a/src/engine/InputQuery.cpp b/src/engine/InputQuery.cpp index 3bdbf9553..70ad73951 100644 --- a/src/engine/InputQuery.cpp +++ b/src/engine/InputQuery.cpp @@ -343,7 +343,7 @@ void InputQuery::saveQuery( const String &fileName ) // Lower Bounds for ( const auto &lb : _lowerBounds ) queryFile->write( Stringf( "\n%d,%f", lb.first, lb.second ) ); - + // Upper Bounds for ( const auto &ub : _upperBounds ) queryFile->write( Stringf( "\n%d,%f", ub.first, ub.second ) ); @@ -431,6 +431,29 @@ List InputQuery::getOutputVariables() const return result; } +void InputQuery::printAllBounds() const +{ + printf( "InputQuery: Dumping all bounds\n" ); + + for ( unsigned i = 0; i < _numberOfVariables; ++i ) + { + printf( "\tx%u: [", i ); + if ( _lowerBounds.exists( i ) ) + printf( "%lf, ", _lowerBounds[i] ); + else + printf( "-INF, " ); + + if ( _upperBounds.exists( i ) ) + printf( "%lf]", _upperBounds[i] ); + else + printf( "+INF]" ); + printf( "\n" ); + + } + + printf( "\n\n" ); +} + void InputQuery::printInputOutputBounds() const { printf( "Dumping bounds of the input and output variables:\n" ); diff --git a/src/engine/InputQuery.h b/src/engine/InputQuery.h index 9a5530767..a2603b980 100644 --- a/src/engine/InputQuery.h +++ b/src/engine/InputQuery.h @@ -57,7 +57,7 @@ class InputQuery Methods for handling input and output variables */ void markInputVariable( unsigned variable, unsigned inputIndex ); - void markOutputVariable( unsigned variable, unsigned inputIndex ); + void markOutputVariable( unsigned variable, unsigned outputIndex ); unsigned inputVariableByIndex( unsigned index ) const; unsigned outputVariableByIndex( unsigned index ) const; unsigned getNumInputVariables() const; @@ -118,6 +118,7 @@ class InputQuery */ void printInputOutputBounds() const; void dump() const; + void printAllBounds() const; /* Adjsut the input/output variable mappings because variables have been merged diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 4988d273b..844263d83 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -236,6 +236,19 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher _score = score; } + /* + Retrieve the current lower and upper bounds + */ + double getLowerBound( unsigned i ) const + { + return _lowerBounds[i]; + } + + double getUpperBound( unsigned i ) const + { + return _upperBounds[i]; + } + protected: bool _constraintActive; Map _assignment; diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp index fc087eb05..b7896822c 100644 --- a/src/engine/Preprocessor.cpp +++ b/src/engine/Preprocessor.cpp @@ -69,7 +69,6 @@ InputQuery Preprocessor::preprocess( const InputQuery &query, bool attemptVariab { continueTightening = processEquations(); continueTightening = processConstraints() || continueTightening; - if ( attemptVariableElimination ) continueTightening = processIdenticalVariables() || continueTightening; diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index 681f88c0a..a8008ee3b 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -46,7 +46,7 @@ ReluConstraint::ReluConstraint( const String &serializedRelu ) String constraintType = serializedRelu.substring( 0, 4 ); ASSERT( constraintType == String( "relu" ) ); - // remove the constraint type in serialized form + // Remove the constraint type in serialized form String serializedValues = serializedRelu.substring( 5, serializedRelu.length() - 5 ); List values = serializedValues.tokenize( "," ); diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h index f8ac26798..b6c7bc861 100644 --- a/src/engine/ReluConstraint.h +++ b/src/engine/ReluConstraint.h @@ -100,10 +100,11 @@ class ReluConstraint : public PiecewiseLinearConstraint PiecewiseLinearCaseSplit getValidCaseSplit() const; /* - Preprocessing related functions, to inform that a variable has been eliminated completely - because it was fixed to some value, or that a variable's index has changed (e.g., x4 is now - called x2). constraintObsolete() returns true iff and the constraint has become obsolote - as a result of variable eliminations. + Preprocessing related functions, to inform that a variable has + been eliminated completely because it was fixed to some value, + or that a variable's index has changed (e.g., x4 is now called + x2). constraintObsolete() returns true iff and the constraint + has become obsolote as a result of variable eliminations. */ void eliminateVariable( unsigned variable, double fixedValue ); void updateVariableIndex( unsigned oldIndex, unsigned newIndex ); diff --git a/src/engine/tests/Test_AbsoluteValueConstraint.h b/src/engine/tests/Test_AbsoluteValueConstraint.h new file mode 100644 index 000000000..a33defee0 --- /dev/null +++ b/src/engine/tests/Test_AbsoluteValueConstraint.h @@ -0,0 +1,1059 @@ +/********************* */ +/*! \file Test_ReluConstraint.h + ** \verbatim + ** Top contributors (to current version): + ** Shiran Aziz + ** 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 + +#include "AbsoluteValueConstraint.h" +#include "MarabouError.h" +#include "MockErrno.h" +#include "MockTableau.h" +#include "PiecewiseLinearCaseSplit.h" +#include +#include + +class MockForAbsoluteValueConstraint : public MockErrno +{ +public: +}; + +class AbsoluteValueConstraintTestSuite : public CxxTest::TestSuite +{ +public: + MockForAbsoluteValueConstraint *mock; + + void setUp() + { + TS_ASSERT( mock = new MockForAbsoluteValueConstraint ); + } + + void tearDown() + { + TS_ASSERT_THROWS_NOTHING( delete mock ); + } + + void test_abs_duplicate_and_restore() + { + AbsoluteValueConstraint abs1( 4, 6 ); + abs1.setActiveConstraint( false ); + abs1.notifyVariableValue( 4, 1.0 ); + abs1.notifyVariableValue( 6, 1.0 ); + + abs1.notifyLowerBound( 4, -8.0 ); + abs1.notifyUpperBound( 4, 8.0 ); + + abs1.notifyLowerBound( 6, 0.0 ); + abs1.notifyUpperBound( 6, 8.0 ); + + PiecewiseLinearConstraint *abs2 = abs1.duplicateConstraint(); + + abs1.notifyVariableValue( 4, -2 ); + + TS_ASSERT( !abs1.satisfied() ); + + TS_ASSERT( !abs2->isActive() ); + TS_ASSERT( abs2->satisfied() ); + + abs2->restoreState( &abs1 ); + TS_ASSERT( !abs2->satisfied() ); + + TS_ASSERT_THROWS_NOTHING( delete abs2 ); + } + + void test_register_and_unregister_as_watcher() + { + unsigned b = 1; + unsigned f = 4; + + MockTableau tableau; + + AbsoluteValueConstraint abs( b, f ); + + TS_ASSERT_THROWS_NOTHING( abs.registerAsWatcher( &tableau ) ); + + TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher.size(), 2U ); + TS_ASSERT( tableau.lastUnregisteredVariableToWatcher.empty() ); + TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher[b].size(), 1U ); + TS_ASSERT( tableau.lastRegisteredVariableToWatcher[b].exists( &abs ) ); + TS_ASSERT_EQUALS( tableau.lastRegisteredVariableToWatcher[f].size(), 1U ); + TS_ASSERT( tableau.lastRegisteredVariableToWatcher[f].exists( &abs ) ); + + tableau.lastRegisteredVariableToWatcher.clear(); + + TS_ASSERT_THROWS_NOTHING( abs.unregisterAsWatcher( &tableau ) ); + + TS_ASSERT( tableau.lastRegisteredVariableToWatcher.empty() ); + TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher.size(), 2U ); + TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher[b].size(), 1U ); + TS_ASSERT( tableau.lastUnregisteredVariableToWatcher[b].exists( &abs ) ); + TS_ASSERT_EQUALS( tableau.lastUnregisteredVariableToWatcher[f].size(), 1U ); + TS_ASSERT( tableau.lastUnregisteredVariableToWatcher[f].exists( &abs ) ); + } + + void test_participating_variables() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + List participatingVariables; + + TS_ASSERT_THROWS_NOTHING( participatingVariables = abs.getParticipatingVariables() ); + TS_ASSERT_EQUALS( participatingVariables.size(), 2U ); + auto it = participatingVariables.begin(); + TS_ASSERT_EQUALS( *it, b ); + ++it; + TS_ASSERT_EQUALS( *it, f ); + + TS_ASSERT_EQUALS( abs.getParticipatingVariables(), List( {1,4} ) ); + + TS_ASSERT( abs.participatingVariable( b ) ); + TS_ASSERT( abs.participatingVariable( f ) ); + TS_ASSERT( !abs.participatingVariable( 2 ) ); + TS_ASSERT( !abs.participatingVariable( 0 ) ); + TS_ASSERT( !abs.participatingVariable( 5 ) ); + } + + void test_abs_notify_variable_value_and_satisfied() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + abs.notifyVariableValue( b, 5 ); + abs.notifyVariableValue( f, 5 ); + TS_ASSERT( abs.satisfied() ); + + abs.notifyVariableValue( b, -5 ); + abs.notifyVariableValue( f, 5 ); + TS_ASSERT( abs.satisfied() ); + + abs.notifyVariableValue( b, 5 ); + abs.notifyVariableValue( f, -5 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( f, -1 ); + abs.notifyVariableValue( b, -5 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( b, 1 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( b, 5 ); + abs.notifyVariableValue( f, 4 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( b, -4 ); + abs.notifyVariableValue( f, -5 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( f, 1 ); + abs.notifyVariableValue( b, -2 ); + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( f, -1 ); + abs.notifyVariableValue( b, -2 ); + TS_ASSERT( !abs.satisfied() ); + } + + void test_abs_update_variable_index() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + // Changing variable indices + abs.notifyVariableValue( b, 1 ); + abs.notifyVariableValue( f, 1 ); + TS_ASSERT( abs.satisfied() ); + + unsigned newB = 12; + unsigned newF = 14; + + TS_ASSERT_THROWS_NOTHING( abs.updateVariableIndex( b, newB ) ); + TS_ASSERT_THROWS_NOTHING( abs.updateVariableIndex( f, newF ) ); + + TS_ASSERT( abs.satisfied() ); + + abs.notifyVariableValue( newF, 2 ); + + TS_ASSERT( !abs.satisfied() ); + + abs.notifyVariableValue( newB, 2 ); + + TS_ASSERT( abs.satisfied() ); + } + + void test_abs_getPossibleFixes() + { + // Possible violations: + // 1. f is positive, b is positive, b and f are unequal + // 2. f is positive, b is negative, -b and f are unequal + + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + List fixes; + List::iterator it; + + // 1. f is positive, b is positive, b and f are unequal + + abs.notifyVariableValue( b, 2 ); + abs.notifyVariableValue( f, 1 ); + + fixes = abs.getPossibleFixes(); + TS_ASSERT_EQUALS( fixes.size(), 3U ); + it = fixes.begin(); + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, 1 ); + ++it; + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, -1 ); + ++it; + TS_ASSERT_EQUALS( it->_variable, f ); + TS_ASSERT_EQUALS( it->_value, 2 ); + + // 2. f is positive, b is negative, -b and f are unequal + abs.notifyVariableValue( b, -2 ); + abs.notifyVariableValue( f, 1 ); + + fixes = abs.getPossibleFixes(); + TS_ASSERT_EQUALS( fixes.size(), 3U ); + it = fixes.begin(); + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, 1 ); + ++it; + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, -1 ); + ++it; + TS_ASSERT_EQUALS( it->_variable, f ); + TS_ASSERT_EQUALS( it->_value, 2 ); + } + + void test_eliminate_variable_b() + { + unsigned b = 1; + unsigned f = 4; + + MockTableau tableau; + + AbsoluteValueConstraint abs( b, f ); + + abs.registerAsWatcher( &tableau ); + + TS_ASSERT( !abs.constraintObsolete() ); + TS_ASSERT_THROWS_NOTHING( abs.eliminateVariable( b, 5 ) ); + TS_ASSERT( abs.constraintObsolete() ); + } + + void test_eliminate_variable_f() + { + unsigned b = 1; + unsigned f = 4; + + MockTableau tableau; + + AbsoluteValueConstraint abs( b, f ); + + abs.registerAsWatcher( &tableau ); + + TS_ASSERT( !abs.constraintObsolete() ); + TS_ASSERT_THROWS_NOTHING( abs.eliminateVariable( f, 5 ) ); + TS_ASSERT( abs.constraintObsolete() ); + } + + void test_abs_entailed_tightenings_positive_phase_1() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + + abs.notifyLowerBound( b, 1 ); + abs.notifyLowerBound( f, 2 ); + abs.notifyUpperBound( b, 7 ); + abs.notifyUpperBound( f, 7 ); + + // 1 < x_b < 7 , 2 < x_f < 7 -> 2 < x_b + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 1, 2, 7, 7, entailedTightenings ); + + abs.notifyLowerBound( b, 3 ); + // 3 < x_b < 7 , 2 < x_f < 7 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 3, 2, 7, 7, entailedTightenings ); + + abs.notifyLowerBound( f, 3 ); + abs.notifyUpperBound( b, 6 ); + // 3 < x_b < 6 , 3 < x_f < 7 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 3, 3, 6, 7, entailedTightenings ); + + abs.notifyUpperBound( f, 6 ); + abs.notifyUpperBound( b, 7 ); + // 3 < x_b < 6 , 3 < x_f < 6 + // --> x_b < 6 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 3, 3, 6, 6, entailedTightenings ); + + abs.notifyLowerBound( f, -3 ); + // 3 < x_b < 6 , 3 < x_f < 6 + // --> 3 < x_f + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 3, 3, 6, 6, entailedTightenings ); + + abs.notifyLowerBound( b, 5 ); + abs.notifyUpperBound( f, 5 ); + // 5 < x_b < 6 , 3 < x_f < 5 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 5, 3, 6, 5, entailedTightenings ); + } + + void test_abs_entailed_tightenings_positive_phase_2() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + + // 8 < b < 18, 48 < f < 64 + abs.notifyUpperBound( b, 18 ); + abs.notifyUpperBound( f, 64 ); + abs.notifyLowerBound( b, 8 ); + abs.notifyLowerBound( f, 48 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 8, 48, 18, 64, entailedTightenings ); + } + + void test_abs_entailed_tightenings_positive_phase_3() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + + // 3 < b < 4, 1 < f < 2 + abs.notifyUpperBound( b, 4 ); + abs.notifyUpperBound( f, 2 ); + abs.notifyLowerBound( b, 3 ); + abs.notifyLowerBound( f, 1 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 3, 1, 4, 2, entailedTightenings ); + } + + void test_abs_entailed_tightenings_positive_phase_4() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyUpperBound( b, 7 ); + abs.notifyUpperBound( f, 6 ); + abs.notifyLowerBound( b, 0 ); + abs.notifyLowerBound( f, 0 ); + + // 0 < x_b < 7 ,0 < x_f < 6 + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 0, 0, 7, 6, entailedTightenings ); + + abs.notifyUpperBound( b, 5 ); + // 0 < x_b < 5 ,0 < x_f < 6 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 0, 0, 5, 6, entailedTightenings ); + + abs.notifyLowerBound( b, 1 ); + // 1 < x_b < 5 ,0 < x_f < 6 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 1, 0, 5, 6, entailedTightenings ); + + abs.notifyUpperBound( f, 4 ); + // 1 < x_b < 5 ,0 < x_f < 4 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 1, 0, 5, 4, entailedTightenings ); + + // Non overlap + abs.notifyUpperBound( f, 2 ); + abs.notifyLowerBound( b, 3 ); + + // 3 < x_b < 5 ,0 < x_f < 2 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + TS_ASSERT_EQUALS( entailedTightenings.size(), 4U ); + assert_lower_upper_bound( f, b, 3, 0, 5, 2, entailedTightenings ); + } + + void test_abs_entailed_tightenings_positive_phase_5() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + + abs.notifyUpperBound( b, 6 ); + abs.notifyUpperBound( f, 5 ); + abs.notifyLowerBound( b, 4 ); + abs.notifyLowerBound( f, 3 ); + + // 4 < x_b < 6 ,3 < x_f < 5 + entailedTightenings.clear(); + abs.getEntailedTightenings( entailedTightenings ); + assert_lower_upper_bound( f, b, 4, 3, 6, 5, entailedTightenings ); + } + + void test_abs_entailed_tightenings_positive_phase_6() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, 5 ); + abs.notifyUpperBound( b, 10 ); + abs.notifyLowerBound( f, -1 ); + abs.notifyUpperBound( f, 10 ); + + TS_ASSERT( abs.phaseFixed() ); + abs.getEntailedTightenings( entailedTightenings ); + + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( f, 0, Tightening::LB ), + + Tightening( b, 0, Tightening::LB ), + Tightening( b, 10, Tightening::UB ), + Tightening( f, 5, Tightening::LB ), + Tightening( f, 10, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -6 ); + abs.notifyUpperBound( b, 3 ); + abs.notifyLowerBound( f, 2 ); + abs.notifyUpperBound( f, 4 ); + + // -6 < x_b < 3 ,2 < x_f < 4 + abs.getEntailedTightenings( entailedTightenings ); + + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -4, Tightening::LB ), + Tightening( b, 4, Tightening::UB ), + Tightening( f, 6, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + + // -6 < x_b < 2 ,2 < x_f < 4 + abs.notifyUpperBound( b, 2 ); + abs.getEntailedTightenings( entailedTightenings ); + + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -4, Tightening::LB ), + Tightening( b, 4, Tightening::UB ), + Tightening( f, 6, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + + // -6 < x_b < 1 ,2 < x_f < 4, now stuck in negative phase + abs.notifyUpperBound( b, 1 ); + abs.getEntailedTightenings( entailedTightenings ); + + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -4, Tightening::LB ), + Tightening( b, 4, Tightening::UB ), + Tightening( f, 6, Tightening::UB ), + Tightening( b, -2, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive_2() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -5 ); + abs.notifyUpperBound( b, 10 ); + abs.notifyLowerBound( f, 3 ); + abs.notifyUpperBound( f, 7 ); + + // -5 < x_b < 10 ,3 < x_f < 7 + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -7, Tightening::LB ), + Tightening( b, 7, Tightening::UB ), + Tightening( f, 10, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + + // -5 < x_b < 10 ,6 < x_f < 7, positive phase + abs.notifyLowerBound( f, 6 ); + + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -7, Tightening::LB ), + Tightening( b, 7, Tightening::UB ), + Tightening( f, 10, Tightening::UB ), + Tightening( b, 6, Tightening::LB ), + }) ); + + entailedTightenings.clear(); + + // -5 < x_b < 3 ,6 < x_f < 7 + + // Extreme case, disjoint ranges + + abs.notifyUpperBound( b, 3 ); + + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -7, Tightening::LB ), + Tightening( b, 7, Tightening::UB ), + Tightening( f, 5, Tightening::UB ), + Tightening( b, 6, Tightening::LB ), + Tightening( b, -6, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_phase_not_fixed_f_strictly_positive_3() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs(b, f); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -1 ); + abs.notifyUpperBound( b, 1 ); + abs.notifyLowerBound( f, 2 ); + abs.notifyUpperBound( f, 4 ); + + // -1 < x_b < 1 ,2 < x_f < 4 + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -4, Tightening::LB ), + Tightening( b, 4, Tightening::UB ), + Tightening( f, 1, Tightening::UB ), + Tightening( b, 2, Tightening::LB ), + Tightening( b, -2, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_phase_not_fixed_f_non_negative() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -7 ); + abs.notifyUpperBound( b, 7 ); + abs.notifyLowerBound( f, 0 ); + abs.notifyUpperBound( f, 6 ); + + // -7 < x_b < 7 ,0 < x_f < 6 + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -6, Tightening::LB ), + Tightening( b, 6, Tightening::UB ), + Tightening( f, 7, Tightening::UB ), + }) ); + + + entailedTightenings.clear(); + + // -7 < x_b < 5 ,0 < x_f < 6 + abs.notifyUpperBound( b, 5 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -6, Tightening::LB ), + Tightening( b, 6, Tightening::UB ), + Tightening( f, 7, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + // 0 < x_b < 5 ,0 < x_f < 6 + abs.notifyLowerBound( b, 0 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, 0, Tightening::LB ), + Tightening( b, 6, Tightening::UB ), + Tightening( f, 0, Tightening::LB ), + Tightening( f, 5, Tightening::UB ), + }) ); + + + entailedTightenings.clear(); + + // 3 < x_b < 5 ,0 < x_f < 6 + abs.notifyLowerBound( b, 3 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, 0, Tightening::LB ), + Tightening( b, 6, Tightening::UB ), + Tightening( f, 3, Tightening::LB ), + Tightening( f, 5, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_negative_phase() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -20 ); + abs.notifyUpperBound( b, -2 ); + abs.notifyLowerBound( f, 0 ); + abs.notifyUpperBound( f, 15 ); + + // -20 < x_b < -2 ,0 < x_f < 15 + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -15, Tightening::LB ), + Tightening( b, 0, Tightening::UB ), + Tightening( f, 2, Tightening::LB ), + Tightening( f, 20, Tightening::UB ), + }) ); + + + entailedTightenings.clear(); + + // -20 < x_b < -2 ,7 < x_f < 15 + abs.notifyLowerBound( f, 7 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -15, Tightening::LB ), + Tightening( b, -7, Tightening::UB ), + Tightening( f, 2, Tightening::LB ), + Tightening( f, 20, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + + // -12 < x_b < -2 ,7 < x_f < 15 + abs.notifyLowerBound( b, -12 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -15, Tightening::LB ), + Tightening( b, -7, Tightening::UB ), + Tightening( f, 2, Tightening::LB ), + Tightening( f, 12, Tightening::UB ), + }) ); + + entailedTightenings.clear(); + + // -12 < x_b < -8 ,7 < x_f < 15 + abs.notifyUpperBound( b, -8 ); + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -15, Tightening::LB ), + Tightening( b, -7, Tightening::UB ), + Tightening( f, 8, Tightening::LB ), + Tightening( f, 12, Tightening::UB ), + }) ); + } + + void test_abs_entailed_tightenings_negative_phase_2() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + List entailedTightenings; + List::iterator it; + + abs.notifyLowerBound( b, -20 ); + abs.notifyUpperBound( b, -2 ); + abs.notifyLowerBound( f, 25 ); + abs.notifyUpperBound( f, 30 ); + + // -20 < x_b < -2 ,25 < x_f < 30 + abs.getEntailedTightenings( entailedTightenings ); + assert_tightenings_match( entailedTightenings, + List + ({ + Tightening( b, -30, Tightening::LB ), + Tightening( b, -25, Tightening::UB ), + Tightening( f, 2, Tightening::LB ), + Tightening( f, 20, Tightening::UB ), + }) ); + } + + void test_abs_case_splits() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + List fixes; + List::iterator it; + + List splits = abs.getCaseSplits(); + + Equation positiveEquation, negativeEquation; + + TS_ASSERT_EQUALS( splits.size(), 2U ); + + List::iterator split1 = splits.begin(); + List::iterator split2 = split1; + ++split2; + + TS_ASSERT( isPositiveSplit( b, f, split1 ) || isPositiveSplit( b, f, split2 ) ); + TS_ASSERT( isNegativeSplit( b, f, split1 ) || isNegativeSplit( b, f, split2 ) ); + } + + bool isPositiveSplit( unsigned b, unsigned f, List::iterator &split ) + { + List bounds = split->getBoundTightenings(); + + auto bound = bounds.begin(); + Tightening bound1 = *bound; + + TS_ASSERT_EQUALS( bound1._variable, b ); + TS_ASSERT_EQUALS( bound1._value, 0.0 ); + + if ( bound1._type != Tightening::LB ) + return false; + + TS_ASSERT_EQUALS( bounds.size(), 1U ); + + Equation positiveEquation; + auto equations = split->getEquations(); + TS_ASSERT_EQUALS( equations.size(), 1U ); + positiveEquation = split->getEquations().front(); + TS_ASSERT_EQUALS( positiveEquation._addends.size(), 2U ); + TS_ASSERT_EQUALS( positiveEquation._scalar, 0.0 ); + + auto addend = positiveEquation._addends.begin(); + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, b ); + + ++addend; + TS_ASSERT_EQUALS( addend->_coefficient, -1.0 ); + TS_ASSERT_EQUALS( addend->_variable, f ); + + TS_ASSERT_EQUALS( positiveEquation._type, Equation::EQ ); + + return true; + } + + bool isNegativeSplit( unsigned b, unsigned f, List::iterator &split ) + { + List bounds = split->getBoundTightenings(); + + auto bound = bounds.begin(); + Tightening bound1 = *bound; + + TS_ASSERT_EQUALS( bound1._variable, b ); + TS_ASSERT_EQUALS( bound1._value, 0.0 ); + + if ( bound1._type != Tightening::UB ) + return false; + + Equation negativeEquation; + auto equations = split->getEquations(); + TS_ASSERT_EQUALS( equations.size(), 1U ); + negativeEquation = split->getEquations().front(); + TS_ASSERT_EQUALS( negativeEquation._addends.size(), 2U ); + TS_ASSERT_EQUALS( negativeEquation._scalar, 0.0 ); + + auto addend = negativeEquation._addends.begin(); + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, b ); + + ++addend; + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, f ); + + TS_ASSERT_EQUALS( negativeEquation._type, Equation::EQ ); + return true; + } + + void test_constraint_phase_gets_fixed() + { + unsigned b = 1; + unsigned f = 4; + + MockTableau tableau; + + // Upper bounds + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyUpperBound( b, -1.0 ); + TS_ASSERT( abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyUpperBound( b, 0.0 ); + TS_ASSERT( abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyUpperBound( f, 5 ); + TS_ASSERT( !abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyUpperBound( b, 3.0 ); + TS_ASSERT( !abs.phaseFixed() ); + } + + // Lower bounds + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyLowerBound( b, 3.0 ); + TS_ASSERT( abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyLowerBound( b, 0.0 ); + TS_ASSERT( abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyLowerBound( f, 6.0 ); + TS_ASSERT( !abs.phaseFixed() ); + } + + { + AbsoluteValueConstraint abs( b, f ); + TS_ASSERT( !abs.phaseFixed() ); + abs.notifyLowerBound( b, -2.5 ); + TS_ASSERT( !abs.phaseFixed() ); + } + } + + void test_valid_split_abs_phase_fixed_to_active() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + List fixes; + List::iterator it; + + TS_ASSERT( !abs.phaseFixed() ); + TS_ASSERT_THROWS_NOTHING( abs.notifyLowerBound( b, 5 ) ); + TS_ASSERT( abs.phaseFixed() ); + + PiecewiseLinearCaseSplit split; + TS_ASSERT_THROWS_NOTHING( split = abs.getValidCaseSplit() ); + + Equation activeEquation; + + List bounds = split.getBoundTightenings(); + + TS_ASSERT_EQUALS( bounds.size(), 1U ); + auto bound = bounds.begin(); + Tightening bound1 = *bound; + + TS_ASSERT_EQUALS( bound1._variable, b ); + TS_ASSERT_EQUALS( bound1._type, Tightening::LB ); + TS_ASSERT_EQUALS( bound1._value, 0.0 ); + + auto equations = split.getEquations(); + TS_ASSERT_EQUALS( equations.size(), 1U ); + activeEquation = split.getEquations().front(); + TS_ASSERT_EQUALS( activeEquation._addends.size(), 2U ); + TS_ASSERT_EQUALS( activeEquation._scalar, 0.0 ); + + auto addend = activeEquation._addends.begin(); + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, b ); + + ++addend; + TS_ASSERT_EQUALS( addend->_coefficient, -1.0 ); + TS_ASSERT_EQUALS( addend->_variable, f ); + + TS_ASSERT_EQUALS( activeEquation._type, Equation::EQ ); + } + + void test_valid_split_abs_phase_fixed_to_inactive() + { + unsigned b = 1; + unsigned f = 4; + + AbsoluteValueConstraint abs( b, f ); + + List fixes; + List::iterator it; + + TS_ASSERT( !abs.phaseFixed() ); + TS_ASSERT_THROWS_NOTHING( abs.notifyUpperBound( b, -2 ) ); + TS_ASSERT( abs.phaseFixed() ); + + PiecewiseLinearCaseSplit split; + TS_ASSERT_THROWS_NOTHING( split = abs.getValidCaseSplit() ); + + Equation activeEquation; + + List bounds = split.getBoundTightenings(); + + TS_ASSERT_EQUALS( bounds.size(), 1U ); + auto bound = bounds.begin(); + Tightening bound1 = *bound; + + TS_ASSERT_EQUALS( bound1._variable, b ); + TS_ASSERT_EQUALS( bound1._type, Tightening::UB ); + TS_ASSERT_EQUALS( bound1._value, 0.0 ); + + auto equations = split.getEquations(); + TS_ASSERT_EQUALS( equations.size(), 1U ); + activeEquation = split.getEquations().front(); + TS_ASSERT_EQUALS( activeEquation._addends.size(), 2U ); + TS_ASSERT_EQUALS( activeEquation._scalar, 0.0 ); + + auto addend = activeEquation._addends.begin(); + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, b ); + + ++addend; + TS_ASSERT_EQUALS( addend->_coefficient, 1.0 ); + TS_ASSERT_EQUALS( addend->_variable, f ); + + TS_ASSERT_EQUALS( activeEquation._type, Equation::EQ ); + } + + void assert_lower_upper_bound( unsigned f, + unsigned b, + double fLower, + double bLower, + double fUpper, + double bUpper, + List entailedTightenings ) + { + List::iterator it; + it = entailedTightenings.begin(); + + TS_ASSERT_EQUALS( entailedTightenings.size(),4U ); + TS_ASSERT_EQUALS( it->_variable, f ); + TS_ASSERT_EQUALS( it->_value, fLower ); + TS_ASSERT_EQUALS( it->_type, Tightening::LB ); + it++; + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, bLower ); + TS_ASSERT_EQUALS( it->_type, Tightening::LB ); + it++; + TS_ASSERT_EQUALS( it->_variable, f ); + TS_ASSERT_EQUALS( it->_value, fUpper ); + TS_ASSERT_EQUALS( it->_type, Tightening::UB ); + it++; + TS_ASSERT_EQUALS( it->_variable, b ); + TS_ASSERT_EQUALS( it->_value, bUpper); + TS_ASSERT_EQUALS( it->_type, Tightening::UB ); + } + + void assert_tightenings_match( List a, List b ) + { + TS_ASSERT_EQUALS( a.size(), b.size() ); + + for ( const auto &it : a ) + TS_ASSERT( b.exists( it ) ); + } +}; + +// +// Local Variables: +// compile-command: "make -C ../../.. " +// tags-file-name: "../../../TAGS" +// c-basic-offset: 4 +// End: +// diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h index ce597d489..061b361b9 100644 --- a/src/engine/tests/Test_ReluConstraint.h +++ b/src/engine/tests/Test_ReluConstraint.h @@ -1225,7 +1225,6 @@ class ReluConstraintTestSuite : public CxxTest::TestSuite } }; - // // Local Variables: // compile-command: "make -C ../../.. " diff --git a/src/system_tests/CMakeLists.txt b/src/system_tests/CMakeLists.txt index d801097b1..317dfc8e3 100644 --- a/src/system_tests/CMakeLists.txt +++ b/src/system_tests/CMakeLists.txt @@ -12,6 +12,8 @@ add_system_test(max) add_system_test(mps) add_system_test(relu) add_system_test(Disjunction) +add_system_test(AbsoluteValue) + file(COPY "${RESOURCES_DIR}/mps/lp_feasible_1.mps" DESTINATION ${CMAKE_BINARY_DIR}) file(COPY "${RESOURCES_DIR}/mps/lp_infeasible_1.mps" DESTINATION ${CMAKE_BINARY_DIR}) file(COPY ${ACAS_REGRESS_NET} DESTINATION ${CMAKE_BINARY_DIR}) diff --git a/src/system_tests/Test_AbsoluteValue.h b/src/system_tests/Test_AbsoluteValue.h new file mode 100644 index 000000000..e3ed45212 --- /dev/null +++ b/src/system_tests/Test_AbsoluteValue.h @@ -0,0 +1,246 @@ +/********************* */ +/*! \file Test_Bsolutevalue.h + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the Marabou project. + ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + +**/ + +#include + +#include "AbsoluteValueConstraint.h" +#include "AcasParser.h" +#include "Engine.h" +#include "FloatUtils.h" +#include "InputQuery.h" + +class AbsoluteValueTestSuite : public CxxTest::TestSuite +{ +public: + void setUp() + { + } + + void tearDown() + { + } + + void test_absoluate_value_unsat() + { + InputQuery inputQuery; + inputQuery.setNumberOfVariables( 6 ); + + inputQuery.setLowerBound( 0, -1 ); + inputQuery.setUpperBound( 0, 1 ); + + inputQuery.setLowerBound( 5, 5 ); + inputQuery.setUpperBound( 5, 6 ); + + Equation equation1; + equation1.addAddend( 1, 0 ); + equation1.addAddend( -1, 1 ); + equation1.setScalar( 0 ); + inputQuery.addEquation( equation1 ); + + Equation equation2; + equation2.addAddend( 1, 0 ); + equation2.addAddend( 1, 3 ); + equation2.setScalar( 0 ); + inputQuery.addEquation( equation2 ); + + Equation equation3; + equation3.addAddend( 1, 2 ); + equation3.addAddend( 1, 4 ); + equation3.addAddend( -1, 5 ); + equation3.setScalar( 0 ); + inputQuery.addEquation( equation3 ); + + AbsoluteValueConstraint *abs1 = new AbsoluteValueConstraint( 1, 2 ); + AbsoluteValueConstraint *abs2 = new AbsoluteValueConstraint( 3, 4 ); + + inputQuery.addPiecewiseLinearConstraint( abs1 ); + inputQuery.addPiecewiseLinearConstraint( abs2 ); + + Engine engine; + if ( !engine.processInputQuery( inputQuery ) ) + { + // Expected result + return; + } + + TS_ASSERT( !engine.solve() ); + } + + void test_absoluate_value_sat() + { + InputQuery inputQuery; + inputQuery.setNumberOfVariables( 6 ); + + inputQuery.setLowerBound( 0, -1 ); + inputQuery.setUpperBound( 0, 1 ); + + inputQuery.setLowerBound( 5, 0.5 ); + inputQuery.setUpperBound( 5, 6 ); + + Equation equation1; + equation1.addAddend( 1, 0 ); + equation1.addAddend( -1, 1 ); + equation1.setScalar( 0 ); + inputQuery.addEquation( equation1 ); + + Equation equation2; + equation2.addAddend( 1, 0 ); + equation2.addAddend( 1, 3 ); + equation2.setScalar( 0 ); + inputQuery.addEquation( equation2 ); + + Equation equation3; + equation3.addAddend( 1, 2 ); + equation3.addAddend( 1, 4 ); + equation3.addAddend( -1, 5 ); + equation3.setScalar( 0 ); + inputQuery.addEquation( equation3 ); + + AbsoluteValueConstraint *abs1 = new AbsoluteValueConstraint( 1, 2 ); + AbsoluteValueConstraint *abs2 = new AbsoluteValueConstraint( 3, 4 ); + + inputQuery.addPiecewiseLinearConstraint( abs1 ); + inputQuery.addPiecewiseLinearConstraint( abs2 ); + + Engine engine; + TS_ASSERT( engine.processInputQuery( inputQuery ) ); + TS_ASSERT( engine.solve() ); + + engine.extractSolution( inputQuery ); + + double value_x0 = inputQuery.getSolutionValue( 0 ); + double value_x1b = inputQuery.getSolutionValue( 1 ); + double value_x1f = inputQuery.getSolutionValue( 2 ); + double value_x2b = inputQuery.getSolutionValue( 3 ); + double value_x2f = inputQuery.getSolutionValue( 4 ); + double value_x3 = inputQuery.getSolutionValue( 5 ); + + TS_ASSERT( FloatUtils::areEqual( value_x0, value_x1b ) ); + TS_ASSERT( FloatUtils::areEqual( value_x0, -value_x2b ) ); + TS_ASSERT( FloatUtils::areEqual( value_x3, value_x1f + value_x2f ) ); + + TS_ASSERT( FloatUtils::gte( value_x0, -1 ) && FloatUtils::lte( value_x0, 1 ) ); + TS_ASSERT( FloatUtils::gte( value_x1f, 0 ) && FloatUtils::lte( value_x1f, 1 ) ); + TS_ASSERT( FloatUtils::gte( value_x3, 0.5 ) && FloatUtils::lte( value_x1f, 6 ) ); + + TS_ASSERT( FloatUtils::areEqual( FloatUtils::abs( value_x1b ), value_x1f ) ); + TS_ASSERT( FloatUtils::areEqual( FloatUtils::abs( value_x2b ), value_x2f ) ); + } + + void test_absoluate_value_on_acas() + { + InputQuery inputQuery; + AcasParser acasParser( RESOURCES_DIR "/nnet/acasxu/ACASXU_experimental_v2a_1_1.nnet" ); + acasParser.generateQuery( inputQuery ); + + // We run an adversarial-robustness-like query around 0, by + // bounding the expression + // + // \sum_{i=1}^5 | x_i | + // + // where x_i are the input nodes. This requires adding 6 new + // variables to the query: + // + // 5 variables for x'_i = abs( x_i ) + // 1 variable for sum( x'i ) + + unsigned numVariables = inputQuery.getNumberOfVariables(); + inputQuery.setNumberOfVariables( numVariables + 6 ); + + // Individual absolute values + for ( unsigned i = 0; i < 5; ++i ) + { + unsigned inputVariable = acasParser.getInputVariable( i ); + AbsoluteValueConstraint *abs = new AbsoluteValueConstraint + ( inputVariable, numVariables + i ); + inputQuery.addPiecewiseLinearConstraint( abs ); + } + + // Sum of absolute values + Equation equation; + equation.addAddend( -1, numVariables + 5 ); + for ( unsigned i = 0; i < 5; ++i ) + { + equation.addAddend( 1, numVariables + i ); + } + inputQuery.addEquation( equation ); + + // Bound the maximal L1 change (delta) + const double delta = 0.01; + inputQuery.setUpperBound( numVariables + 5, delta ); + + // Output constraint: we seek a point in which output 0 gets + // a lower score than output 1 + unsigned minimalOutputVar = acasParser.getOutputVariable( 0 ); + unsigned largerOutputVar = acasParser.getOutputVariable( 1 ); + + Equation equationOut; + equationOut.setType( Equation::LE ); + + // minimal - larger <= 0 --> larger >= minimal + equationOut.addAddend( 1 , minimalOutputVar ); + equationOut.addAddend( -1, largerOutputVar ); + equationOut.setScalar( 0 ); + inputQuery.addEquation( equationOut ); + + // Run the query + Engine engine; + if( !engine.processInputQuery( inputQuery ) ) + { + // No counter example found, this is acceptable + return; + } + + bool result = engine.solve(); + if ( !result ) + { + // No counter example found, this is acceptable + return; + } + + engine.extractSolution( inputQuery ); + + // Run through the original network to check correctness + Vector inputs; + for ( unsigned i = 0; i < 5; ++i ) + { + inputs.append( inputQuery.getSolutionValue( i ) ); + } + + Vector outputs; + acasParser.evaluate( inputs, outputs ); + + double minimalOutputValue = outputs[0]; + double largerOutputValue = outputs[1]; + + // Check whether minVar >= runnerUp, as we asked + TS_ASSERT( FloatUtils::gte( largerOutputValue, minimalOutputValue ) ); + + // Check whether the sum of inptus <= delta + double sum = 0.0; + for ( unsigned i = 0; i < 5; ++i ) + sum += FloatUtils::abs( inputs[i] ); + + TS_ASSERT( FloatUtils::gte( delta, sum, 0.001 ) ); + } +}; + +// +// Local Variables: +// compile-command: "make -C ../../.. " +// tags-file-name: "../../../TAGS" +// c-basic-offset: 4 +// End: +//