From b078e058be63692b2c6af03e73f3390f5c6d5b38 Mon Sep 17 00:00:00 2001 From: idan0610 Date: Tue, 6 Feb 2024 11:31:15 +0200 Subject: [PATCH] Fix for disjunction bug with input variables + update tests (#709) * Fix for disjunction with input variables + update tests * Moving functionality into classes DisjunctionConstraint and Preprocessor * small fix * small coding style fix * Fix coding style * Adding tests for DisjunctionConstraint and Preprocessor to test new functionality * fix coding style for tests --- resources/onnx/vnnlib/test_sub_const.vnnlib | 2 +- src/engine/DisjunctionConstraint.cpp | 62 ++ src/engine/DisjunctionConstraint.h | 8 + src/engine/Engine.cpp | 2 +- src/engine/MarabouError.h | 1 + src/engine/PiecewiseLinearConstraint.cpp | 20 + src/engine/PiecewiseLinearConstraint.h | 6 + src/engine/Preprocessor.cpp | 43 ++ src/engine/Preprocessor.h | 6 + src/engine/tests/Test_DisjunctionConstraint.h | 42 ++ src/engine/tests/Test_Preprocessor.h | 27 + src/input_parsers/VnnLibParser.cpp | 62 +- src/input_parsers/tests/Test_VnnLibParser.h | 584 +++++------------- 13 files changed, 429 insertions(+), 436 deletions(-) diff --git a/resources/onnx/vnnlib/test_sub_const.vnnlib b/resources/onnx/vnnlib/test_sub_const.vnnlib index 0dafe6f3ea..3efee41f69 100644 --- a/resources/onnx/vnnlib/test_sub_const.vnnlib +++ b/resources/onnx/vnnlib/test_sub_const.vnnlib @@ -2,6 +2,6 @@ (declare-const Y_0 Real) (assert (>= (- X_0 1) 1)) -(assert (<= X_0 1)) +(assert (<= X_0 3)) (assert (>= Y_0 0)) \ No newline at end of file diff --git a/src/engine/DisjunctionConstraint.cpp b/src/engine/DisjunctionConstraint.cpp index 8899761c24..9e0e353102 100644 --- a/src/engine/DisjunctionConstraint.cpp +++ b/src/engine/DisjunctionConstraint.cpp @@ -552,3 +552,65 @@ bool DisjunctionConstraint::addFeasibleDisjunct( const PiecewiseLinearCaseSplit void DisjunctionConstraint::addTableauAuxVar( unsigned /* tableauAuxVar */, unsigned /* constraintAuxVar */ ) { } + +double DisjunctionConstraint::getMinLowerBound( unsigned int var ) const +{ + if ( !participatingVariable( var ) ) + { + return FloatUtils::negativeInfinity(); + } + + double minLowerBound = FloatUtils::infinity(); + for ( const auto &disjunct : _disjuncts ) + { + bool foundLowerBound = false; + for ( const auto &bound : disjunct.getBoundTightenings() ) + { + if ( bound._variable == var && bound._type == Tightening::LB ) + { + foundLowerBound = true; + minLowerBound = FloatUtils::min( minLowerBound, bound._value ); + } + } + + if ( !foundLowerBound ) + { + throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_BOUND, + Stringf( "Variable %d missing lower bound in given disjunction constraint %s", var, + serializeToString().ascii() ).ascii() ); + } + } + + return minLowerBound; +} + +double DisjunctionConstraint::getMaxUpperBound( unsigned int var ) const +{ + if ( !participatingVariable( var ) ) + { + return FloatUtils::infinity(); + } + + double maxUpperBound = FloatUtils::negativeInfinity(); + for ( const auto &disjunct : _disjuncts ) + { + bool foundUpperBound = false; + for ( const auto &bound : disjunct.getBoundTightenings() ) + { + if ( bound._variable == var && bound._type == Tightening::UB ) + { + foundUpperBound = true; + maxUpperBound = FloatUtils::max( maxUpperBound, bound._value ); + } + } + + if ( !foundUpperBound ) + { + throw MarabouError( MarabouError::PARTICIPATING_VARIABLE_MISSING_BOUND, + Stringf( "Variable %d missing upper bound in given disjunction constraint %s", var, + serializeToString().ascii() ).ascii() ); + } + } + + return maxUpperBound; +} \ No newline at end of file diff --git a/src/engine/DisjunctionConstraint.h b/src/engine/DisjunctionConstraint.h index 060d041a57..30fd69faa4 100644 --- a/src/engine/DisjunctionConstraint.h +++ b/src/engine/DisjunctionConstraint.h @@ -189,6 +189,14 @@ class DisjunctionConstraint : public PiecewiseLinearConstraint */ bool addFeasibleDisjunct( const PiecewiseLinearCaseSplit &disjunct ); + /* + Get the minimal lower bound and maximal upper bound for the given variable, + across all disjuncts. If some disjunct does not contain a bound, an exception + will be thrown. + */ + double getMinLowerBound( unsigned int var ) const override; + double getMaxUpperBound( unsigned int var ) const override; + private: /* The disjuncts that form this PL constraint diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index 0db1a8256f..66c175af68 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -3719,4 +3719,4 @@ void Engine::extractBounds( InputQuery &inputQuery ) inputQuery.setUpperBound( i, _preprocessedQuery->getUpperBound( i ) ); } } -} +} \ No newline at end of file diff --git a/src/engine/MarabouError.h b/src/engine/MarabouError.h index 5ae9dfd0d5..ad49194e06 100644 --- a/src/engine/MarabouError.h +++ b/src/engine/MarabouError.h @@ -51,6 +51,7 @@ class MarabouError : public Error REQUESTED_NONEXISTENT_CASE_SPLIT = 25, UNABLE_TO_INITIALIZATION_PHASE_PATTERN = 26, BOUNDS_NOT_UP_TO_DATE_IN_LP_SOLVER = 27, + PARTICIPATING_VARIABLE_MISSING_BOUND = 28, // Error codes for Query Loader FILE_DOES_NOT_EXIST = 100, diff --git a/src/engine/PiecewiseLinearConstraint.cpp b/src/engine/PiecewiseLinearConstraint.cpp index 7ee5132043..9db62fcb5f 100644 --- a/src/engine/PiecewiseLinearConstraint.cpp +++ b/src/engine/PiecewiseLinearConstraint.cpp @@ -203,6 +203,26 @@ void PiecewiseLinearConstraint::setStatistics( Statistics *statistics ) _statistics = statistics; } +double PiecewiseLinearConstraint::getMinLowerBound( unsigned int var ) const +{ + if ( existsLowerBound( var ) ) + { + return getLowerBound( var ); + } + + return FloatUtils::infinity(); +} + +double PiecewiseLinearConstraint::getMaxUpperBound( unsigned int var ) const +{ + if ( existsUpperBound( var ) ) + { + return getUpperBound( var ); + } + + return FloatUtils::negativeInfinity(); +} + // // Local Variables: // compile-command: "make -C ../.. " diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 0f7f1181ef..a8c7893648 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -255,6 +255,12 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher virtual void addAuxiliaryEquationsAfterPreprocessing( InputQuery &/* inputQuery */ ) {} + /* + Get the minimal lower bound and maximal upper bound for the given variable. + */ + virtual double getMinLowerBound( unsigned int var ) const; + virtual double getMaxUpperBound( unsigned int var ) const; + /* Whether the constraint can contribute the SoI cost function. */ diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp index eef739af32..7b6a5c989e 100644 --- a/src/engine/Preprocessor.cpp +++ b/src/engine/Preprocessor.cpp @@ -78,6 +78,12 @@ std::unique_ptr Preprocessor::preprocess( const InputQuery &query, b */ transformConstraintsIfNeeded(); + /* + Try to find missing lower and upper bounds for input variables from + piecewise linear constraints. + */ + getMissingInputBoundsFromConstraints(); + /* Merge consecutive WS layers */ @@ -210,6 +216,43 @@ void Preprocessor::transformConstraintsIfNeeded() plConstraint->transformToUseAuxVariables( *_preprocessed ); } +void Preprocessor::getMissingInputBoundsFromConstraints() +{ + const auto &lowerBounds = _preprocessed->getLowerBounds(); + const auto &upperBounds = _preprocessed->getUpperBounds(); + + for ( unsigned int var : _preprocessed->getInputVariables() ) + { + if ( !lowerBounds.exists( var ) ) + { + double minLowerBound = FloatUtils::infinity(); + for ( const auto &plConstraint : _preprocessed->getPiecewiseLinearConstraints() ) + { + minLowerBound = FloatUtils::min( minLowerBound, plConstraint->getMinLowerBound( var ) ); + } + + if ( !FloatUtils::areEqual( minLowerBound, FloatUtils::infinity() ) ) + { + _preprocessed->setLowerBound( var, minLowerBound ); + } + } + + if ( !upperBounds.exists( var ) ) + { + double maxUpperBound = FloatUtils::negativeInfinity(); + for ( const auto &plConstraint : _preprocessed->getPiecewiseLinearConstraints() ) + { + maxUpperBound = FloatUtils::max( maxUpperBound, plConstraint->getMaxUpperBound( var ) ); + } + + if ( !FloatUtils::areEqual( maxUpperBound, FloatUtils::negativeInfinity() ) ) + { + _preprocessed->setUpperBound( var, maxUpperBound ); + } + } + } +} + void Preprocessor::makeAllEquationsEqualities() { for ( auto &equation : _preprocessed->getEquations() ) diff --git a/src/engine/Preprocessor.h b/src/engine/Preprocessor.h index 5665e164af..fdfa5b244c 100644 --- a/src/engine/Preprocessor.h +++ b/src/engine/Preprocessor.h @@ -88,6 +88,12 @@ class Preprocessor */ void transformConstraintsIfNeeded(); + /** + * Try to find missing lower and upper bounds of input variables from + * piecewise linear constraints. + */ + void getMissingInputBoundsFromConstraints(); + /* Transform all equations of type GE or LE to type EQ. */ diff --git a/src/engine/tests/Test_DisjunctionConstraint.h b/src/engine/tests/Test_DisjunctionConstraint.h index 6164a0b91e..4cf7ef89f4 100644 --- a/src/engine/tests/Test_DisjunctionConstraint.h +++ b/src/engine/tests/Test_DisjunctionConstraint.h @@ -621,4 +621,46 @@ class DisjunctionConstraintTestSuite : public CxxTest::TestSuite TS_ASSERT_EQUALS( *split++, *cs2); TS_ASSERT_EQUALS( *split, *cs3); } + + void test_min_lower_bound() + { + // Disjuncts are: + // -1 <= x0 <= 1, x1 = 2 + // 1 <= x0 <= 5, x1 = x0 + // 5 <= x0 , x1 = 2x2 + 5 + + List caseSplits = { *cs1, *cs2, *cs3 }; + + // Add lower bound for x0 in first disjunct (otherwise MarabouError will be thrown) + caseSplits.front().storeBoundTightening( Tightening( 0, -1, Tightening::LB ) ); + + DisjunctionConstraint disj = DisjunctionConstraint( caseSplits ); + + double minX0LowerBound = 0; + TS_ASSERT_THROWS_NOTHING( minX0LowerBound = disj.getMinLowerBound( 0 ) ) + TS_ASSERT_EQUALS( minX0LowerBound, -1 ) + + TS_ASSERT_THROWS( disj.getMinLowerBound( 1 ), MarabouError ) + } + + void test_max_upper_bound() + { + // Disjuncts are: + // x0 <= 1, x1 = 2 + // 1 <= x0 <= 5, x1 = x0 + // 5 <= x0 <= 3 , x1 = 2x2 + 5 + + List caseSplits = { *cs1, *cs2, *cs3 }; + + // Add upper bound for x0 in last disjunct (otherwise MarabouError will be thrown) + caseSplits.back().storeBoundTightening( Tightening( 0, 3, Tightening::UB ) ); + + DisjunctionConstraint disj = DisjunctionConstraint( caseSplits ); + + double maxX0UpperBound = 0; + TS_ASSERT_THROWS_NOTHING( maxX0UpperBound = disj.getMaxUpperBound( 0 ) ) + TS_ASSERT_EQUALS( maxX0UpperBound, 5 ) + + TS_ASSERT_THROWS( disj.getMaxUpperBound( 1 ), MarabouError ) + } }; diff --git a/src/engine/tests/Test_Preprocessor.h b/src/engine/tests/Test_Preprocessor.h index 1ed31d17e9..2b7ef3e618 100644 --- a/src/engine/tests/Test_Preprocessor.h +++ b/src/engine/tests/Test_Preprocessor.h @@ -16,6 +16,7 @@ #include +#include "DisjunctionConstraint.h" #include "Engine.h" #include "FloatUtils.h" #include "InfeasibleQueryException.h" @@ -935,6 +936,32 @@ class PreprocessorTestSuite : public CxxTest::TestSuite } } + void test_preprocessor_with_input_bounds_in_disjunction() + { + InputQuery ipq; + ipq.setNumberOfVariables( 1 ); + ipq.markInputVariable( 0, 0 ); + + PiecewiseLinearCaseSplit cs1; + cs1.storeBoundTightening( Tightening( 0, -1, Tightening::LB ) ); + cs1.storeBoundTightening( Tightening( 0, 3, Tightening::UB ) ); + + PiecewiseLinearCaseSplit cs2; + cs2.storeBoundTightening( Tightening( 0, -4, Tightening::LB ) ); + cs2.storeBoundTightening( Tightening( 0, 2, Tightening::UB ) ); + + List caseSplits = {cs1, cs2}; + DisjunctionConstraint *disj = new DisjunctionConstraint( caseSplits ); + ipq.addPiecewiseLinearConstraint( disj ); + + InputQuery processed; + TS_ASSERT_THROWS_NOTHING( processed = *( Preprocessor(). + preprocess( ipq ) ) ); + + TS_ASSERT_EQUALS( processed.getLowerBound( 0 ), -4 ) + TS_ASSERT_EQUALS( processed.getUpperBound( 0 ), 3 ) + } + void test_todo() { TS_TRACE( "In test_variable_elimination, test something about updated bounds and updated PL constraints" ); diff --git a/src/input_parsers/VnnLibParser.cpp b/src/input_parsers/VnnLibParser.cpp index d93c3834c1..52b3f0a733 100644 --- a/src/input_parsers/VnnLibParser.cpp +++ b/src/input_parsers/VnnLibParser.cpp @@ -14,6 +14,7 @@ **/ #include +#include "Equation.h" #include "File.h" #include "InputParserError.h" #include "VnnLibParser.h" @@ -199,9 +200,33 @@ int VnnLibParser::parseAssert( int index, const Vector &tokens, InputQue { List equations; index = parseCondition( index, tokens, equations ); - for ( const auto &it: equations ) + for ( const auto &eq : equations ) { - inputQuery.addEquation( it ); + if ( eq._addends.size() == 1 ) + { + const Equation::Addend &addend = eq._addends.front(); + if ( addend._coefficient < 0 ) + { + inputQuery.setLowerBound( addend._variable, eq._scalar / addend._coefficient ); + } + else if ( addend._coefficient > 0 ) + { + inputQuery.setUpperBound( addend._variable, eq._scalar / addend._coefficient ); + } + else if ( eq._scalar < 0 ) + { + throw InputParserError( InputParserError::UNEXPECTED_INPUT, + Stringf( "Illegal vnnlib constraint: 0 < %f", eq._scalar ).ascii() ); + } + else + { + continue; + } + } + else + { + inputQuery.addEquation( eq ); + } } } else if ( op == "or" ) @@ -214,9 +239,34 @@ int VnnLibParser::parseAssert( int index, const Vector &tokens, InputQue index = parseCondition( index + 1, tokens, equations ); PiecewiseLinearCaseSplit split; - for ( const auto &it: equations ) + for ( const auto &eq : equations ) { - split.addEquation( it ); + if ( eq._addends.size() == 1 ) + { + // Add bounds as tightenings + unsigned var = eq._addends.front()._variable; + double coeff = eq._addends.front()._coefficient; + if ( coeff == 0 ) + throw CommonError( CommonError::DIVISION_BY_ZERO, + "Zero coefficient encountered in vnnlib constraint" ); + double scalar = eq._scalar / coeff; + Equation::EquationType type = eq._type; + + if ( type == Equation::EQ ) + { + split.storeBoundTightening( Tightening( var, scalar, Tightening::LB ) ); + split.storeBoundTightening( Tightening( var, scalar, Tightening::UB ) ); + } + else if ( ( type == Equation::GE && coeff > 0 ) || + ( type == Equation::LE && coeff < 0 ) ) + split.storeBoundTightening( Tightening( var, scalar, Tightening::LB ) ); + else + split.storeBoundTightening( Tightening( var, scalar, Tightening::UB ) ); + } + else + { + split.addEquation( eq ); + } } disjunctList.append( split ); } @@ -323,7 +373,7 @@ double VnnLibParser::processAddConstraint( const VnnLibParser::Term &term, Equat double scalar = 0; double coefficient = isRhs ? -1 : 1; - for ( const auto &arg: term._args ) + for ( const auto &arg : term._args ) { if ( arg._type == Term::TermType::CONST ) { @@ -420,7 +470,7 @@ double VnnLibParser::processMulConstraint( const VnnLibParser::Term &term, Equat bool varExists = false; unsigned int var; - for ( const Term &arg: term._args ) + for ( const Term &arg : term._args ) { if ( arg._type == Term::TermType::CONST ) { diff --git a/src/input_parsers/tests/Test_VnnLibParser.h b/src/input_parsers/tests/Test_VnnLibParser.h index b2e48a5a76..24b749f93c 100644 --- a/src/input_parsers/tests/Test_VnnLibParser.h +++ b/src/input_parsers/tests/Test_VnnLibParser.h @@ -29,33 +29,21 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite String onnxFilename = Stringf( "%s/%s", RESOURCES_DIR "/onnx/vnnlib/", "test_nano_vnncomp.onnx" ); InputQuery inputQuery; - Equation testEq = Equation( Equation::EquationType::LE ); OnnxParser onnxParser( onnxFilename ); onnxParser.generateQuery( inputQuery ); TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); - - Equation &eq = *eqIter; - testEq.addAddend( 1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( -1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( inputVar ) && lowerBounds.get( inputVar ) == -1 ) + TS_ASSERT( upperBounds.exists( inputVar ) && upperBounds.get( inputVar ) == 1 ) + TS_ASSERT( upperBounds.exists( outputVar ) && upperBounds.get( outputVar ) == -1 ) } void test_tiny_vnncomp() @@ -64,36 +52,30 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite String onnxFilename = Stringf( "%s/%s", RESOURCES_DIR "/onnx/vnnlib/", "test_tiny_vnncomp.onnx" ); InputQuery inputQuery; - Equation testEq = Equation( Equation::EquationType::LE ); OnnxParser onnxParser( onnxFilename ); onnxParser.generateQuery( inputQuery ); TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); + auto *disjunction = ( DisjunctionConstraint * ) ( inputQuery.getPiecewiseLinearConstraints().back() ); const auto &caseSplits = disjunction->getCaseSplits(); const auto &caseSplitsIter = caseSplits.begin(); - auto eqIter = ( *caseSplitsIter ).getEquations().rbegin(); + auto boundsIter = ( *caseSplitsIter ).getBoundTightenings().begin(); - Equation eq = *eqIter; - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( -100 ); - TS_ASSERT( eq.equivalent( testEq ) ) + Tightening t = *boundsIter; + TS_ASSERT( t == Tightening( inputVar, -1, Tightening::LB ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + boundsIter++; + t = *boundsIter; + TS_ASSERT( t == Tightening( inputVar, 1, Tightening::UB ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + boundsIter++; + t = *boundsIter; + TS_ASSERT( t == Tightening( outputVar, 100, Tightening::LB ) ) } void test_small_vnncomp() @@ -109,29 +91,24 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); + auto *disjunction = ( DisjunctionConstraint * ) ( inputQuery.getPiecewiseLinearConstraints().back() ); const auto &caseSplits = disjunction->getCaseSplits(); const auto &caseSplitsIter = caseSplits.begin(); - auto eqIter = ( *caseSplitsIter ).getEquations().rbegin(); + auto boundsIter = ( *caseSplitsIter ).getBoundTightenings().begin(); - Equation eq = *eqIter; - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( -100 ); - TS_ASSERT( eq.equivalent( testEq ) ) + Tightening t = *boundsIter; + TS_ASSERT( t == Tightening( inputVar, -1, Tightening::LB ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + boundsIter++; + t = *boundsIter; + TS_ASSERT( t == Tightening( inputVar, 1, Tightening::UB ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + boundsIter++; + t = *boundsIter; + TS_ASSERT( t == Tightening( outputVar, 100, Tightening::LB ) ) } void test_sat_vnncomp() @@ -147,6 +124,30 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); + + unsigned int input0 = inputQuery.inputVariableByIndex( 0 ); + unsigned int input1 = inputQuery.inputVariableByIndex( 1 ); + unsigned int input2 = inputQuery.inputVariableByIndex( 2 ); + unsigned int input3 = inputQuery.inputVariableByIndex( 3 ); + unsigned int input4 = inputQuery.inputVariableByIndex( 4 ); + + TS_ASSERT( lowerBounds.exists( input0 ) && lowerBounds.get( input0 ) == -0.30353115613746867 ) + TS_ASSERT( upperBounds.exists( input0 ) && upperBounds.get( input0 ) == -0.29855281193475053 ) + + TS_ASSERT( lowerBounds.exists( input1 ) && lowerBounds.get( input1 ) == -0.009549296585513092 ) + TS_ASSERT( upperBounds.exists( input1 ) && upperBounds.get( input1 ) == 0.009549296585513092 ) + + TS_ASSERT( lowerBounds.exists( input2 ) && lowerBounds.get( input2 ) == 0.4933803235848431 ) + TS_ASSERT( upperBounds.exists( input2 ) && upperBounds.get( input2 ) == 0.49999999998567607 ) + + TS_ASSERT( lowerBounds.exists( input3 ) && lowerBounds.get( input3 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input3 ) && upperBounds.get( input3 ) == 0.5 ) + + TS_ASSERT( lowerBounds.exists( input4 ) && lowerBounds.get( input4 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input4 ) && upperBounds.get( input4 ) == 0.5 ) + auto eqIter = inputQuery.getEquations().rbegin(); Equation &eq = *eqIter; @@ -179,76 +180,6 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite testEq.setScalar( 0 ); TS_ASSERT( eq.equivalent( testEq ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( -0.4933803235848431 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( 0.49999999998567607 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0.30353115613746867 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( -0.29855281193475053 ); - TS_ASSERT( eq.equivalent( testEq ) ) - Engine engine; engine.setVerbosity( 0 ); TS_ASSERT_THROWS_NOTHING( engine.processInputQuery( inputQuery ) ); @@ -269,6 +200,30 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); + + unsigned int input0 = inputQuery.inputVariableByIndex( 0 ); + unsigned int input1 = inputQuery.inputVariableByIndex( 1 ); + unsigned int input2 = inputQuery.inputVariableByIndex( 2 ); + unsigned int input3 = inputQuery.inputVariableByIndex( 3 ); + unsigned int input4 = inputQuery.inputVariableByIndex( 4 ); + + TS_ASSERT( lowerBounds.exists( input0 ) && lowerBounds.get( input0 ) == -0.30353115613746867 ) + TS_ASSERT( upperBounds.exists( input0 ) && upperBounds.get( input0 ) == -0.29855281193475053 ) + + TS_ASSERT( lowerBounds.exists( input1 ) && lowerBounds.get( input1 ) == -0.009549296585513092 ) + TS_ASSERT( upperBounds.exists( input1 ) && upperBounds.get( input1 ) == 0.009549296585513092 ) + + TS_ASSERT( lowerBounds.exists( input2 ) && lowerBounds.get( input2 ) == 0.4933803235848431 ) + TS_ASSERT( upperBounds.exists( input2 ) && upperBounds.get( input2 ) == 0.49999999998567607 ) + + TS_ASSERT( lowerBounds.exists( input3 ) && lowerBounds.get( input3 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input3 ) && upperBounds.get( input3 ) == 0.5 ) + + TS_ASSERT( lowerBounds.exists( input4 ) && lowerBounds.get( input4 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input4 ) && upperBounds.get( input4 ) == 0.5 ) + auto eqIter = inputQuery.getEquations().rbegin(); Equation &eq = *eqIter; @@ -301,76 +256,6 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite testEq.setScalar( 0 ); TS_ASSERT( eq.equivalent( testEq ) ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( -0.4933803235848431 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( 0.49999999998567607 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0.30353115613746867 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( -0.29855281193475053 ); - TS_ASSERT( eq.equivalent( testEq ) ) - Engine engine; engine.setVerbosity( 0 ); TS_ASSERT_THROWS_NOTHING( engine.processInputQuery( inputQuery ) ); @@ -391,26 +276,16 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); - Equation &eq = *eqIter; - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( inputVar ) && lowerBounds.get( inputVar ) == 0 ) + TS_ASSERT( upperBounds.exists( inputVar ) && upperBounds.get( inputVar ) == 1 ) + TS_ASSERT( lowerBounds.exists( outputVar ) && lowerBounds.get( outputVar ) == 0 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) } void test_add_var() @@ -426,103 +301,44 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - Equation &eq = *eqIter; - testEq.addAddend( 1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.addAddend( 1, inputQuery.outputVariableByIndex( 1 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) + unsigned int input0 = inputQuery.inputVariableByIndex( 0 ); + unsigned int input1 = inputQuery.inputVariableByIndex( 1 ); + unsigned int input2 = inputQuery.inputVariableByIndex( 2 ); + unsigned int input3 = inputQuery.inputVariableByIndex( 3 ); + unsigned int input4 = inputQuery.inputVariableByIndex( 4 ); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 2 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input0 ) && lowerBounds.get( input0 ) == -0.30353115613746867 ) + TS_ASSERT( upperBounds.exists( input0 ) && upperBounds.get( input0 ) == -0.29855281193475053 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 1 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input1 ) && lowerBounds.get( input1 ) == -0.009549296585513092 ) + TS_ASSERT( upperBounds.exists( input1 ) && upperBounds.get( input1 ) == 0.009549296585513092 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input2 ) && lowerBounds.get( input2 ) == 0.4933803235848431 ) + TS_ASSERT( upperBounds.exists( input2 ) && upperBounds.get( input2 ) == 0.49999999998567607 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input3 ) && lowerBounds.get( input3 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input3 ) && upperBounds.get( input3 ) == 0.5 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input4 ) && lowerBounds.get( input4 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input4 ) && upperBounds.get( input4 ) == 0.5 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) + unsigned int output0 = inputQuery.outputVariableByIndex( 0 ); + unsigned int output1 = inputQuery.outputVariableByIndex( 1 ); + unsigned int output2 = inputQuery.outputVariableByIndex( 2 ); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( -0.4933803235848431 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( output0 ) && lowerBounds.get( output0 ) == 0 ) + TS_ASSERT( lowerBounds.exists( output1 ) && lowerBounds.get( output1 ) == 0 ) + TS_ASSERT( lowerBounds.exists( output2 ) && lowerBounds.get( output2 ) == 0 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( 0.49999999998567607 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0.30353115613746867 ); - TS_ASSERT( eq.equivalent( testEq ) ) + auto eqIter = inputQuery.getEquations().rbegin(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( -0.29855281193475053 ); + Equation &eq = *eqIter; + testEq.addAddend( 1, output0 ); + testEq.addAddend( 1, output1 ); + testEq.setScalar( 1 ); TS_ASSERT( eq.equivalent( testEq ) ) } @@ -539,26 +355,15 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); - Equation &eq = *eqIter; - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( -2 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( inputVar ) && lowerBounds.get( inputVar ) == 2 ) + TS_ASSERT( upperBounds.exists( inputVar ) && upperBounds.get( inputVar ) == 3 ) + TS_ASSERT( lowerBounds.exists( outputVar ) && lowerBounds.get( outputVar ) == 0 ) } void test_sub_var() @@ -574,103 +379,44 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); - - Equation &eq = *eqIter; - testEq.addAddend( 1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 1 ) ); - testEq.setScalar( 1 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 2 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 1 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + unsigned int input0 = inputQuery.inputVariableByIndex( 0 ); + unsigned int input1 = inputQuery.inputVariableByIndex( 1 ); + unsigned int input2 = inputQuery.inputVariableByIndex( 2 ); + unsigned int input3 = inputQuery.inputVariableByIndex( 3 ); + unsigned int input4 = inputQuery.inputVariableByIndex( 4 ); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input0 ) && lowerBounds.get( input0 ) == -0.30353115613746867 ) + TS_ASSERT( upperBounds.exists( input0 ) && upperBounds.get( input0 ) == -0.29855281193475053 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input1 ) && lowerBounds.get( input1 ) == -0.009549296585513092 ) + TS_ASSERT( upperBounds.exists( input1 ) && upperBounds.get( input1 ) == 0.009549296585513092 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 4 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input2 ) && lowerBounds.get( input2 ) == 0.4933803235848431 ) + TS_ASSERT( upperBounds.exists( input2 ) && upperBounds.get( input2 ) == 0.49999999998567607 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( -0.3 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input3 ) && lowerBounds.get( input3 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input3 ) && upperBounds.get( input3 ) == 0.5 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 3 ) ); - testEq.setScalar( 0.5 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( input4 ) && lowerBounds.get( input4 ) == 0.3 ) + TS_ASSERT( upperBounds.exists( input4 ) && upperBounds.get( input4 ) == 0.5 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( -0.4933803235848431 ); - TS_ASSERT( eq.equivalent( testEq ) ) + unsigned int output0 = inputQuery.outputVariableByIndex( 0 ); + unsigned int output1 = inputQuery.outputVariableByIndex( 1 ); + unsigned int output2 = inputQuery.outputVariableByIndex( 2 ); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 2 ) ); - testEq.setScalar( 0.49999999998567607 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 1 ) ); - testEq.setScalar( 0.009549296585513092 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( output0 ) && lowerBounds.get( output0 ) == 0 ) + TS_ASSERT( lowerBounds.exists( output1 ) && lowerBounds.get( output1 ) == 0 ) + TS_ASSERT( lowerBounds.exists( output2 ) && lowerBounds.get( output2 ) == 0 ) - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0.30353115613746867 ); - TS_ASSERT( eq.equivalent( testEq ) ) + auto eqIter = inputQuery.getEquations().rbegin(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 1, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( -0.29855281193475053 ); + Equation &eq = *eqIter; + testEq.addAddend( 1, inputQuery.outputVariableByIndex( 0 ) ); + testEq.addAddend( -1, inputQuery.outputVariableByIndex( 1 ) ); + testEq.setScalar( 1 ); TS_ASSERT( eq.equivalent( testEq ) ) } @@ -687,32 +433,14 @@ class VnnLibParserTestSuite : public CxxTest::TestSuite TS_ASSERT_THROWS_NOTHING( VnnLibParser().parse( filename, inputQuery ) ); - auto eqIter = inputQuery.getEquations().rbegin(); + unsigned int inputVar = inputQuery.inputVariableByIndex( 0 ); + unsigned int outputVar = inputQuery.outputVariableByIndex( 0 ); - Equation &eq = *eqIter; - testEq.addAddend( -1, inputQuery.outputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 0, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 1000 ); - TS_ASSERT( eq.equivalent( testEq ) ) + const auto &lowerBounds = inputQuery.getLowerBounds(); + const auto &upperBounds = inputQuery.getUpperBounds(); - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( 2, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 2 ); - TS_ASSERT( eq.equivalent( testEq ) ) - - eqIter++; - eq = *eqIter; - testEq = Equation( Equation::EquationType::LE ); - testEq.addAddend( -2, inputQuery.inputVariableByIndex( 0 ) ); - testEq.setScalar( 0 ); - TS_ASSERT( eq.equivalent( testEq ) ) + TS_ASSERT( lowerBounds.exists( inputVar ) && lowerBounds.get( inputVar ) == 0 ) + TS_ASSERT( upperBounds.exists( inputVar ) && upperBounds.get( inputVar ) == 1 ) + TS_ASSERT( lowerBounds.exists( outputVar ) && lowerBounds.get( outputVar ) == 0 ) } }; \ No newline at end of file