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

Method encodeAbsoluteValueConstraint

src/engine/MILPEncoder.cpp:321–370  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

319}
320
321void MILPEncoder::encodeAbsoluteValueConstraint( GurobiWrapper &gurobi,
322 AbsoluteValueConstraint *abs,
323 bool relax )
324{
325 ASSERT( abs->auxVariablesInUse() );
326
327 if ( !abs->isActive() || abs->phaseFixed() )
328 {
329 ASSERT( ( FloatUtils::gte( _tableau.getLowerBound( abs->getB() ), 0 ) &&
330 FloatUtils::lte( _tableau.getUpperBound( abs->getPosAux() ), 0 ) ) ||
331 ( FloatUtils::lte( _tableau.getUpperBound( abs->getB() ), 0 ) &&
332 FloatUtils::lte( _tableau.getUpperBound( abs->getNegAux() ), 0 ) ) );
333 return;
334 }
335
336 unsigned sourceVariable = abs->getB();
337 unsigned targetVariable = abs->getF();
338 double sourceLb = _tableau.getLowerBound( sourceVariable );
339 double sourceUb = _tableau.getUpperBound( sourceVariable );
340 double targetUb = _tableau.getUpperBound( targetVariable );
341
342 ASSERT( FloatUtils::isPositive( sourceUb ) && FloatUtils::isNegative( sourceLb ) );
343
344 /*
345 We have added f - b >= 0 and f + b >= 0. We add
346 f - b <= (1 - a) * (ub_f - lb_b) and f + b <= a * (ub_f + ub_b)
347
348 When a = 1, the constraints become:
349 f - b <= 0, f + b <= ub_f + ub_b.
350 When a = 0, the constriants become:
351 f - b <= ub_f - lb_b, f + b <= 0
352 */
353 gurobi.addVariable( Stringf( "a%u", _binVarIndex ),
354 0,
355 1,
356 relax ? GurobiWrapper::CONTINUOUS : GurobiWrapper::BINARY );
357
358 List<GurobiWrapper::Term> terms;
359 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
360 terms.append( GurobiWrapper::Term( -1, Stringf( "x%u", sourceVariable ) ) );
361 terms.append( GurobiWrapper::Term( targetUb - sourceLb, Stringf( "a%u", _binVarIndex ) ) );
362 gurobi.addLeqConstraint( terms, targetUb - sourceLb );
363
364 terms.clear();
365 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
366 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", sourceVariable ) ) );
367 terms.append( GurobiWrapper::Term( -( targetUb + sourceUb ), Stringf( "a%u", _binVarIndex ) ) );
368 gurobi.addLeqConstraint( terms, 0 );
369 ++_binVarIndex;
370}
371
372void MILPEncoder::encodeDisjunctionConstraint( GurobiWrapper &gurobi,
373 DisjunctionConstraint *disj,

Callers

nothing calls this directly

Calls 15

StringfClass · 0.85
getPosAuxMethod · 0.80
getNegAuxMethod · 0.80
TermClass · 0.50
auxVariablesInUseMethod · 0.45
isActiveMethod · 0.45
phaseFixedMethod · 0.45
getLowerBoundMethod · 0.45
getBMethod · 0.45
getUpperBoundMethod · 0.45
getFMethod · 0.45
addVariableMethod · 0.45

Tested by

no test coverage detected