MCPcopy Create free account
hub / github.com/NeuralNetworkVerification/Marabou / verifyInvariants

Method verifyInvariants

src/engine/Tableau.cpp:2229–2326  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

2227}
2228
2229void Tableau::verifyInvariants()
2230{
2231 if ( _lpSolverType != LPSolverType::NATIVE )
2232 return;
2233
2234 // All merged variables are non-basic
2235 for ( const auto &merged : _mergedVariables )
2236 {
2237 if ( _basicVariables.exists( merged.first ) )
2238 {
2239 printf( "Error! Merged variable x%u is basic!\n", merged.first );
2240 exit( 1 );
2241 }
2242 }
2243
2244 // All assignments are well formed
2245 for ( unsigned i = 0; i < _m; ++i )
2246 {
2247 if ( !FloatUtils::wellFormed( _basicAssignment[i] ) )
2248 {
2249 printf( "Assignment for basic variable %u (index %u) is not well formed: %.15lf. "
2250 "Range: [%.15lf, %.15lf]\n",
2251 _basicIndexToVariable[i],
2252 i,
2253 _basicAssignment[i],
2254 getLowerBound( _basicIndexToVariable[i] ),
2255 getUpperBound( _basicIndexToVariable[i] ) );
2256 exit( 1 );
2257 }
2258 }
2259
2260 for ( unsigned i = 0; i < _n - _m; ++i )
2261 {
2262 if ( !FloatUtils::wellFormed( _nonBasicAssignment[i] ) )
2263 {
2264 printf( "Assignment for non-basic variable is not well formed: %.15lf\n",
2265 _nonBasicAssignment[i] );
2266 exit( 1 );
2267 }
2268 }
2269
2270 for ( unsigned i = 0; i < _n - _m; ++i )
2271 {
2272 unsigned variable = _nonBasicIndexToVariable[i];
2273 double value = _nonBasicAssignment[i];
2274
2275 double lb = getLowerBound( variable );
2276 double relaxedLb = lb - ( GlobalConfiguration::BOUND_COMPARISON_ADDITIVE_TOLERANCE +
2277 GlobalConfiguration::BOUND_COMPARISON_MULTIPLICATIVE_TOLERANCE *
2278 FloatUtils::abs( lb ) );
2279
2280 double ub = getUpperBound( variable );
2281 double relaxedUb = ub + ( GlobalConfiguration::BOUND_COMPARISON_ADDITIVE_TOLERANCE +
2282 GlobalConfiguration::BOUND_COMPARISON_MULTIPLICATIVE_TOLERANCE *
2283 FloatUtils::abs( ub ) );
2284
2285 if ( !( ( relaxedLb <= value ) && ( value <= relaxedUb ) ) )
2286 {

Callers 5

solveMethod · 0.45
applySplitMethod · 0.45
minimizeHeuristicCostMethod · 0.45
restorePrecisionMethod · 0.45

Calls 3

absFunction · 0.85
asciiMethod · 0.80
existsMethod · 0.45

Tested by

no test coverage detected