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

Method encodeRoundConstraint

src/engine/MILPEncoder.cpp:731–756  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

729}
730
731void MILPEncoder::encodeRoundConstraint( GurobiWrapper &gurobi, RoundConstraint *round, bool relax )
732{
733 /*
734 We have already introduced during preprocessing
735 f - b <= 0.5
736 b - f <= 0.5
737
738 Therefore, nothing needs to be done if we are encoding the relaxation.
739 Otherwise, we introduce a new integer variable i and assert that f is
740 equal to i.
741 */
742 if ( !relax )
743 {
744 unsigned targetVariable = round->getF();
745 String varName = Stringf( "i%u", _intVarIndex );
746 gurobi.addVariable( varName,
747 _tableau.getLowerBound( targetVariable ),
748 _tableau.getUpperBound( targetVariable ),
749 GurobiWrapper::INTEGER );
750 List<GurobiWrapper::Term> terms;
751 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
752 terms.append( GurobiWrapper::Term( -1, Stringf( "i%u", _intVarIndex ) ) );
753 gurobi.addEqConstraint( terms, 0 );
754 ++_intVarIndex;
755 }
756}
757
758void MILPEncoder::encodeCostFunction( GurobiWrapper &gurobi, const LinearExpression &cost )
759{

Callers

nothing calls this directly

Calls 8

StringfClass · 0.85
TermClass · 0.50
getFMethod · 0.45
addVariableMethod · 0.45
getLowerBoundMethod · 0.45
getUpperBoundMethod · 0.45
appendMethod · 0.45
addEqConstraintMethod · 0.45

Tested by

no test coverage detected