diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..84c048a --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/build/ diff --git a/CHANGELOG b/CHANGELOG index d7cc2e7..c7704ea 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -3,6 +3,8 @@ Features: ----------- - checking of each derivation with empty assumptionlist while processing the DER section, terminating early if RTP is proven +- error messages more descriptive +- a warning is issued if the numbers in the labels are not consistent with the internal VIPR counter. Build system ------------ diff --git a/code/CMakeLists.txt b/code/CMakeLists.txt index b56de64..e51eea3 100644 --- a/code/CMakeLists.txt +++ b/code/CMakeLists.txt @@ -88,13 +88,13 @@ if(VIPRCOMP) set(libs ${libs} ${SOPLEX_LIBRARIES}) # add viprcomp target and link - add_executable(viprcomp viprcomp.cpp) + add_executable(viprcompseq viprcompseq.cpp) add_executable(viprincomp incompletify.cpp) add_definitions(-DSOPLEX_WITH_GMP) - target_link_libraries(viprcomp ${libs}) + target_link_libraries(viprcompseq ${libs}) target_link_libraries(viprincomp ${libs}) - target_link_libraries(viprcomp ${libs}) - target_link_libraries(viprcomp TBB::tbb) + target_link_libraries(viprcompseq ${libs}) +# target_link_libraries(viprcompseq TBB::tbb) message(STATUS "Soplex found.") else() message(STATUS "viprcomp not installed, because SoPlex could not be found.") diff --git a/code/viprchk.cpp b/code/viprchk.cpp index d9ae691..9c1e887 100644 --- a/code/viprchk.cpp +++ b/code/viprchk.cpp @@ -142,12 +142,12 @@ class Constraint _coefsEqualObj = false; } - void canonicalize() { _coefficients->canonicalize(); } - void compactify() { _coefficients->compactify(); } + void canonicalize() const { _coefficients->canonicalize(); } + void compactify() const { _coefficients->compactify(); } bool round(); mpq_class getRhs() const { return _rhs; } - mpq_class getCoef(const int index) { if( _coefficients->find(index) != _coefficients->end() ) + mpq_class getCoef(const int index) const { if( _coefficients->find(index) != _coefficients->end() ) return (*_coefficients)[index]; else return mpq_class(0); } @@ -155,12 +155,12 @@ class Constraint int getSense() const { return _sense; } - bool isAssumption() { return _isAssumption; } + bool isAssumption() const { return _isAssumption; } bool isFalsehood() const { return _falsehood; } // true iff the constraint is a contradiction like 0 >= 1 - bool isTautology(); + bool isTautology() const; // true iff the constraint is a tautology like 0 <= 1 bool hasAsm(const int index) { @@ -176,8 +176,8 @@ class Constraint void setassumptionList(const SVectorBool assumptionList) { _assumptionList = assumptionList; } SVectorBool getassumptionList() const { return _assumptionList; } - bool dominates(Constraint &other) const; - void print(); + bool dominates(const Constraint &other) const; + void print() const; void trash() { _trashed = true; _falsehood = false; _coefficients = nullptr; _rhs = 0; _assumptionList.clear(); } @@ -186,15 +186,13 @@ class Constraint string label() const { return _label; } void setMaxRefIdx(int refIdx) { _refIdx = refIdx; } - int getMaxRefIdx() { return _refIdx; } + int getMaxRefIdx() const { return _refIdx; } Constraint operator-(const Constraint& other) { Constraint returncons(*this); - for(auto it = other._coefficients->begin(); it != other._coefficients->end(); ++it) - { - (*returncons._coefficients)[it->first] -= it->second; - } + for(auto & it : *other._coefficients) + (*returncons._coefficients)[it.first] -= it.second; returncons._rhs -= other._rhs; return returncons; @@ -211,7 +209,7 @@ class Constraint bool _falsehood; bool _coefsEqualObj; - bool _isFalsehood(); + bool _isFalsehood() const; bool _trashed; }; @@ -254,10 +252,10 @@ bool processRTP(); bool processSOL(); bool processDER(); -bool readMultipliers(int &sense, SVectorGMP &mult); -bool readConstraintCoefficients(shared_ptr &v, bool& coefEqualsObj); +bool readMultipliers(int &sense, SVectorGMP &mult, std::string& label); +bool readConstraintCoefficients(shared_ptr &coefficients, bool& coefEqualsObj); bool readConstraint( string &label, int &sense, mpq_class &rhs, - shared_ptr &coef, bool& coefEqualsObj); + shared_ptr &coefficients, bool& coefEqualsObj); inline mpq_class floor(const mpq_class &q); // rounding down inline mpq_class ceil(const mpq_class &q); // rounding up @@ -265,11 +263,13 @@ bool isInteger(const mpq_class &q); // check if variable is integer mpq_class scalarProduct(shared_ptr u, shared_ptr v); -bool canUnsplit( Constraint &toDer, const int con1, const int a1, const int con2, - const int a2, SVectorBool &assumptionList); +bool canUnsplit( Constraint &toDer, int con1, int a1, int con2, int a2, SVectorBool &assumptionList); -bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coef, - int currConIdx, SVectorBool &amsList); +bool readLinComb( int &sense, mpq_class &rhs, + const std::shared_ptr &coefficients, + int currentConstraintIndex, + SVectorBool &assumptionList, + std::string &label ); // Main function int main(int argc, char *argv[]) @@ -277,7 +277,7 @@ int main(int argc, char *argv[]) if( argc != 2 ) { cerr << "Usage: " << argv[0] << " \n"; - return ViprStatus::ERROR; + return ERROR; } certificateFile.open(argv[1]); @@ -285,7 +285,7 @@ int main(int argc, char *argv[]) if( certificateFile.fail() ) { cerr << "Failed to open file " << argv[1] << endl; - return ViprStatus::ERROR; + return ERROR; } double start_cpu_tm = clock(); @@ -297,16 +297,16 @@ int main(int argc, char *argv[]) if( processRTP() ) if( processSOL() ) if( processDER() ) { - double cpu_dur = (clock() - start_cpu_tm) - / (double)CLOCKS_PER_SEC; + const double cpu_dur = (clock() - start_cpu_tm) + / static_cast(CLOCKS_PER_SEC); cout << endl << "Completed in " << cpu_dur << " seconds (CPU)" << endl; - return ViprStatus::OKAY; + return OKAY; } cout << endl << "Verification failed." << endl; - return ViprStatus::ERROR; + return ERROR; } @@ -356,17 +356,15 @@ bool processVER() { certificateFile >> tmpStr; returnStatement = checkVersion(tmpStr); -break; + break; } - else if( tmpStr == "%" ) - { + if( tmpStr == "%" ) getline(certificateFile, tmpStr); - } else { cerr << endl << "Comment or VER expected. Read instead " - << tmpStr << endl; -break; + << tmpStr << endl; + break; } } @@ -403,8 +401,6 @@ bool processVAR() cerr << "Invalid number after VAR" << endl; returnStatement = false; } - - // Store variables else { @@ -440,7 +436,6 @@ bool processINT() certificateFile >> section; - // Check section if( section != "INT" ) { @@ -456,17 +451,13 @@ bool processINT() { cerr << "Invalid number after INT" << endl; } - - // Store integer variables else { isInt.resize(variable.size()); - for( auto it = isInt.begin(); it != isInt.end(); ++it ) - { - *it = false; - } + for(auto && it : isInt) + it = false; if( numberOfIntegers > 0 ) { @@ -536,16 +527,12 @@ bool processOBJ() assert(!dummy); objectiveIntegral = true; - for( auto it = objectiveCoefficients->begin(); it != objectiveCoefficients->end(); ++it ) - { - if ( !isInteger(it->second) || !isInt[it->first] ) + for(auto & it : *objectiveCoefficients) + if ( !isInteger(it.second) || !isInt[it.first] ) objectiveIntegral = false; - } if( !returnStatement ) - { cerr << "Failed to read objective coefficients" << endl; - } } TERMINATE: @@ -569,9 +556,7 @@ bool processCON() // Check section if( section != "CON" ) - { cerr << "CON expected. Read instead " << section << endl; - } else { certificateFile >> numberOfConstraints >> numberOfBounds; @@ -789,15 +774,15 @@ bool processSOL() } // Check integrality constraints - for( auto it = solutionSpecified->begin(); it != solutionSpecified->end(); ++it ) + for(auto & it : *solutionSpecified) { - if( isInt[it->first] && !isInteger(it->second) ) + if( isInt[it.first] && !isInteger(it.second) ) { cerr << "Noninteger value for integer variable " - << it->first << endl; + << it.first << endl; goto TERMINATE; } - sol[it->first] = it->second; + sol[it.first] = it.second; } for( int j = 0; j < numberOfConstraints; ++j ) @@ -866,6 +851,18 @@ bool processSOL() return returnStatement; } + +int parseNumber(const std::string& s) { + // find first digit + std::size_t pos = 0; + while (pos < s.size() && !std::isdigit(static_cast(s[pos]))) + ++pos; + + if (pos == s.size()) throw std::invalid_argument("no digits in string"); + + return std::stoi(s.substr(pos)); +} + // Processes derived constraints // Checks derivation types and derived constraints // Finally confirms or rejects Solution and/or relation to prove @@ -875,8 +872,6 @@ bool processDER() cout << endl << "Processing DER section..." << endl; - bool returnStatement = false; - string section; certificateFile >> section; @@ -905,6 +900,7 @@ bool processDER() string label; int sense; mpq_class rhs; + bool warning_issued = false; for( int i = 0; i < numberOfDerivations; ++i ) { @@ -914,6 +910,7 @@ bool processDER() if( !readConstraint(label, sense, rhs, coef, coefEqualsObj) ) return false; + if( label[0] == '%' ) { i--; @@ -929,27 +926,29 @@ bool processDER() certificateFile >> bracket >> kind; + + if( bracket != "{" ) { cerr << "Expecting { but read instead " << bracket << endl; return false; } - DerivationType derivationType = DerivationType::UNKNOWN; + DerivationType derivationType = UNKNOWN; if( kind == "asm" ) - derivationType = DerivationType::ASM; + derivationType = ASM; else if( kind == "sol" ) - derivationType = DerivationType::SOL; + derivationType = SOL; else if( kind == "lin" ) - derivationType = DerivationType::LIN; + derivationType = LIN; else if( kind == "rnd" ) - derivationType = DerivationType::RND; + derivationType = RND; else if( kind == "uns" ) - derivationType = DerivationType::UNS; + derivationType = UNS; // The constraint to be derived - Constraint toDer(label, sense, rhs, coef, (derivationType == DerivationType::ASM), emptyList); + Constraint toDer(label, sense, rhs, coef, (derivationType == ASM), emptyList); if( coefEqualsObj ) toDer.markObjectiveCoefficients(); @@ -961,11 +960,18 @@ bool processDER() int newConIdx = constraint.size(); + if ( !warning_issued && parseNumber(label) != newConIdx) { + cerr << "Warning: indices are not ascending for " << label << ". This can indicate an error!" << endl; + warning_issued = true; + } + + + switch( derivationType ) { // Assumption, i.e. set of assumptions only contains index of constraint - case DerivationType::ASM: + case ASM: assumptionList[ newConIdx ] = true; certificateFile >> bracket; @@ -976,14 +982,14 @@ bool processDER() } break; // Linear combination or rounding - case DerivationType::LIN: - case DerivationType::RND: + case LIN: + case RND: { shared_ptr coefDer(make_shared()); mpq_class rhsDer; int senseDer; - if( !readLinComb(senseDer, rhsDer, coefDer, newConIdx, assumptionList) ) + if( !readLinComb(senseDer, rhsDer, coefDer, newConIdx, assumptionList, label) ) return false; certificateFile >> bracket; @@ -1029,7 +1035,7 @@ bool processDER() break; // Unsplit - case DerivationType::UNS: + case UNS: { int con1, asm1, con2, asm2; @@ -1067,7 +1073,7 @@ bool processDER() } } break; - case DerivationType::SOL: + case SOL: { mpq_class cutoffbound = bestObjectiveValue; if (objectiveIntegral) @@ -1080,17 +1086,17 @@ bool processDER() cerr << "Cutoff bound can only be applied to objective value " << endl; return false; } - else if (sense != -1) + if (sense != -1) { cerr << "Cutoff bound should have sense 'L'" << endl; return false; } - else if (rhs < cutoffbound ) + if (rhs < cutoffbound ) { cerr << "No solution known with objective at most " << rhs << ", best solution is " << bestObjectiveValue << endl; return false; } - else if( bracket != "}" ) + if( bracket != "}" ) { cerr << "Expecting } but read instead " << bracket << endl; return false; @@ -1100,7 +1106,6 @@ bool processDER() default: cout << label << ": unknown derivation type " << kind << endl; return false; - break; } // Set the list of assumptions @@ -1114,12 +1119,12 @@ bool processDER() // Check whether we have globally proven the dual side of RTP if( assumptionList == emptyList ) { - if( relationToProveType == RelationToProveType::INFEAS && constraint.back().isFalsehood() ) + if( relationToProveType == INFEAS && constraint.back().isFalsehood() ) { cout << "Successfully verified infeasibility." << endl; return true; } - else if( relationToProveType == RelationToProveType::RANGE && constraint.back().hasObjectiveCoefficients() && constraint.back().dominates(relationToProve) ) + if( relationToProveType == RANGE && constraint.back().hasObjectiveCoefficients() && constraint.back().dominates(relationToProve) ) { cout << endl << "Terminated after " << i << " derivations." << endl; @@ -1128,10 +1133,10 @@ bool processDER() } cout << "Successfully verified optimal value range " - << (lowerStr == "-inf" ? "(" : "[") - << lowerStr << ", " << upperStr - << (upperStr == "inf" ? ")" : "]") - << "." << endl; + << (lowerStr == "-inf" ? "(" : "[") + << lowerStr << ", " << upperStr + << (upperStr == "inf" ? ")" : "]") + << "." << endl; return true; } @@ -1141,7 +1146,7 @@ bool processDER() certificateFile.ignore(std::numeric_limits::max(), '\n'); if( i < numberOfDerivations - 1 ) // Never trash last constraint - if( (refIdx >= 0) && (refIdx < int(constraint.size())) ) + if( refIdx >= 0 && refIdx < int(constraint.size()) ) { constraint.back().trash(); } @@ -1164,7 +1169,7 @@ bool processDER() } else { - if( relationToProveType == RelationToProveType::INFEAS ) + if( relationToProveType == INFEAS ) cout << "Failed to verify infeasibility." << endl; else if( isMin && checkLower ) cout << "Failed to derive lower bound." << endl; @@ -1185,10 +1190,9 @@ bool processDER() inline mpq_class floor(const mpq_class &q) { mpz_t z; - mpq_class result; - mpz_init (z); + mpz_init(z); mpz_fdiv_q(z, q.get_num_mpz_t(), q.get_den_mpz_t()); // Divide numerator by denominator and floor the result - result = mpz_class(z); + mpq_class result = mpz_class(z); mpz_clear (z); return result; } @@ -1197,10 +1201,9 @@ inline mpq_class floor(const mpq_class &q) inline mpq_class ceil(const mpq_class &q) { mpz_t z; - mpq_class result; - mpz_init (z); + mpz_init(z); mpz_cdiv_q(z, q.get_num_mpz_t(), q.get_den_mpz_t()); // Divide numerator by denominator and ceil the result - result = mpz_class(z); + mpq_class result = mpz_class(z); mpz_clear (z); return result; } @@ -1211,8 +1214,8 @@ bool isInteger(const mpq_class &q) } -bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coefficients, - int currentConstraintIndex,SVectorBool &assumptionList) +bool readLinComb(int &sense, mpq_class &rhs, const shared_ptr &coefficients, + const int currentConstraintIndex, SVectorBool &assumptionList, std::string &label) { bool returnStatement = true; @@ -1222,7 +1225,7 @@ bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coefficient std::cout << "reading linear combination" << std::endl; #endif - if( !readMultipliers(sense, mult) ) + if( !readMultipliers(sense, mult, label) ) { returnStatement = false; } @@ -1233,9 +1236,9 @@ bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coefficient assumptionList.clear(); mpq_class t; - for(auto & it : mult) + for(const auto & it : mult) { - auto index = it.first; + const auto index = it.first; auto a = it.second; auto myassumptionList = constraint[index].getassumptionList(); @@ -1259,8 +1262,8 @@ bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coefficient rhs += a * constraint[index].getRhs(); - if( (constraint[index].getMaxRefIdx() <= currentConstraintIndex) && - (constraint[index].getMaxRefIdx() >= 0) ) + if( constraint[index].getMaxRefIdx() <= currentConstraintIndex && + constraint[index].getMaxRefIdx() >= 0 ) constraint[index].trash(); } } @@ -1270,7 +1273,7 @@ bool readLinComb( int &sense, mpq_class &rhs, shared_ptr coefficient } -bool readMultipliers(int &sense, SVectorGMP &mult) +bool readMultipliers(int &sense, SVectorGMP &mult, std::string& label) { int k; @@ -1290,7 +1293,7 @@ bool readMultipliers(int &sense, SVectorGMP &mult) if( index < 0 ) { - cerr << "Index is out of bounds " << index << endl; + cerr << "In "<< label << ": Index is out of bounds " << index << endl; returnStatement = false; goto TERMINATE; } @@ -1302,7 +1305,7 @@ bool readMultipliers(int &sense, SVectorGMP &mult) #ifndef NDEBUG if( index < 0 || index >= constraint.size( ) ) { - cerr << "Index out of range " << index << " (0," << constraint.size() << ")" << endl; + cerr << "In " << label << ": Index out of range " << index << " (0," << constraint.size() << ")" << endl; returnStatement = false; goto TERMINATE; } @@ -1317,10 +1320,10 @@ bool readMultipliers(int &sense, SVectorGMP &mult) } else { - int tmp = constraint[index].getSense() * sgn(a); + const int tmp = constraint[index].getSense() * sgn(a); if( tmp != 0 && sense != tmp ) { - cerr << "Coefficient has wrong sign for index " << index << endl; + cerr << "In " << label << ": Coefficient has wrong sign for index " << index << endl; returnStatement = false; goto TERMINATE; } @@ -1357,28 +1360,22 @@ bool readConstraintCoefficients(shared_ptr &coefficients, bool& coef cerr << "Error reading number of elements " << endl; goto TERMINATE; } - else - { - for( int j = 0; j < k; j++ ) - { - int index; - mpq_class a; + for (int j = 0; j < k; j++) { + int index; + mpq_class a; - certificateFile >> index >> a; - if( certificateFile.fail() ) - { - cerr << "Error reading integer-rational pair " << endl; - goto TERMINATE; - } - else if( index < 0 || index >= numberOfVariables ) - { - cerr << "Index out of bounds: " << index << endl; - goto TERMINATE; - } - (*coefficients)[index] = a; + certificateFile >> index >> a; + if (certificateFile.fail()) { + cerr << "Error reading integer-rational pair " << endl; + goto TERMINATE; } - returnStatement = true; + if (index < 0 || index >= numberOfVariables) { + cerr << "Index out of bounds: " << index << endl; + goto TERMINATE; + } + (*coefficients)[index] = a; } + returnStatement = true; } coefficients->compactify(); @@ -1448,7 +1445,7 @@ bool canUnsplit( Constraint &toDer, const int con1, const int a1, cerr << "unsplitting trashed constraint: " << c1.label() << endl; goto TERMINATE; } - else if( c2.isTrashed() ) + if( c2.isTrashed() ) { cerr << "unsplitting trashed constraint: " << c2.label() << endl; goto TERMINATE; @@ -1499,7 +1496,7 @@ bool canUnsplit( Constraint &toDer, const int con1, const int a1, cerr << "accessing trashed constraint: " << branchAsm1.label() << endl; goto TERMINATE; } - else if( c2.isTrashed() ) + if( c2.isTrashed() ) { cerr << "accessing trashed constraint: " << c2.label() << endl; goto TERMINATE; @@ -1519,7 +1516,7 @@ bool canUnsplit( Constraint &toDer, const int con1, const int a1, // check if disjunction gives a tautology with respect to the variable // integrality requirements - bool stat = true; + bool stat; if( branchAsm1.getSense() < 0 ) stat = ((branchAsm1.getRhs() + 1) == branchAsm2.getRhs()); else // must be > 0 @@ -1533,7 +1530,7 @@ bool canUnsplit( Constraint &toDer, const int con1, const int a1, shared_ptr c1ptr = branchAsm1.coefSVec(); shared_ptr c2ptr = branchAsm2.coefSVec(); - if( (c1ptr == c2ptr) || (*c1ptr == *c2ptr) ) // coefSVec can both point to objectiveCoefficients + if( c1ptr == c2ptr || *c1ptr == *c2ptr ) // coefSVec can both point to objectiveCoefficients { for(auto & it : *c1ptr) @@ -1544,7 +1541,7 @@ bool canUnsplit( Constraint &toDer, const int con1, const int a1, << endl; goto TERMINATE; } - else if( !isInteger(it.second) ) + if( !isInteger(it.second) ) { cerr << "canUnsplit: noninteger coefficient for index " << it.first << endl; @@ -1663,8 +1660,7 @@ bool Constraint::round() } -bool Constraint::_isFalsehood() -{ +bool Constraint::_isFalsehood() const { bool returnStatement = false; if( _coefficients->empty() ) @@ -1677,7 +1673,7 @@ bool Constraint::_isFalsehood() } -bool Constraint::dominates(Constraint &other) const +bool Constraint::dominates(const Constraint &other) const { bool returnStatement = false; @@ -1702,7 +1698,7 @@ bool Constraint::dominates(Constraint &other) const } -bool Constraint::isTautology() { +bool Constraint::isTautology() const { bool returnStatement = false; if( _coefficients->empty() ) @@ -1718,9 +1714,8 @@ bool Constraint::isTautology() { } -void Constraint::print() { +void Constraint::print() const { bool first = true; - mpq_class myCoefficient; cout.precision(std::numeric_limits::max_digits10); int count = 0; @@ -1728,12 +1723,12 @@ void Constraint::print() { if( _isAssumption ) cout << "Is assumption: "; - for(auto & it : *_coefficients) + for(const auto & it : *_coefficients) { - auto index = it.first; + const auto index = it.first; auto a = it.second; - myCoefficient = abs(a); + mpq_class myCoefficient = abs(a); if( a > 0 ) { @@ -1775,11 +1770,8 @@ void Constraint::print() { if( !_isAssumption && !_assumptionList.empty() ) { cout << " -- assumptions: " << endl; - for( auto it = _assumptionList.begin(); it != _assumptionList.end(); ++it ) - { - auto index = it->first; - cout << " "<< it->first << ": " << constraint[index].label() << endl; - } + for(const auto & it : _assumptionList) + cout << " " << it.first << ": " << constraint[it.first].label() << endl; cout << endl; } #endif diff --git a/code/viprchk_parallel.cpp b/code/viprchk_parallel.cpp index 02de402..79e6c47 100644 --- a/code/viprchk_parallel.cpp +++ b/code/viprchk_parallel.cpp @@ -152,7 +152,7 @@ class Constraint void setassumptionList(const SVectorBool assumptionList) { _assumptionList = assumptionList; } SVectorBool getassumptionList() const { return _assumptionList; } - bool dominates(Constraint &other) const; + bool dominates(const Constraint &other) const; void print(); void trash() { _trashed = true; _falsehood = false; _coefficients = nullptr; @@ -1724,7 +1724,7 @@ bool Constraint::_isFalsehood() } -bool Constraint::dominates(Constraint &other) const +bool Constraint::dominates(const Constraint &other) const { bool returnStatement = false; diff --git a/code/viprcomp.cpp b/code/viprcompseq.cpp similarity index 81% rename from code/viprcomp.cpp rename to code/viprcompseq.cpp index 31bf9c2..bc1da98 100644 --- a/code/viprcomp.cpp +++ b/code/viprcompseq.cpp @@ -38,9 +38,6 @@ // Timing #include -// Parallelization -#include - // Namespaces using namespace std; using namespace soplex; @@ -84,9 +81,7 @@ vector variableNames; // variable names DSVectorPointer ObjCoeff(make_shared()); // sparse vector of objective coefficients size_t numberOfVariables; -unsigned int nthreads = thread::hardware_concurrency(); - -struct Constraint {DSVectorPointer vec; Rational side; int sense; string line;}; // @todo: take care of deep copies here! +struct Constraint {DSVectorPointer vec; Rational side; int sense; }; // @todo: take care of deep copies here! vector constraints; typedef boost::bimap bimap; // maps rows of the LP to corresponding indices in the certificate used for updating the local LPs @@ -97,73 +92,6 @@ vector> upperBounds; // rational boundval, multipl struct passData { SoPlex passLp; bimap LProwCertificateMap;}; -struct parallelData { passData* bufData; stringstream linestream; bool needscompletion; std::vector conidx; string line;}; - -// circular buffer (also known as ring buffer, circular queue, cyclic queue), references: -// https://oneapi-src.github.io/oneTBB/main/tbb_userguide/Using_Circular_Buffers.html -// https://stackoverflow.com/a/15167828/15777342 -class circBuf -{ - int tail, head, size; - std::vector arr; - public: - circBuf( int maxtokens ) - { - head = tail = -1; - size = maxtokens; - arr.resize(maxtokens); - } - /// assignment operator - void resize( int maxtokens ) - { - head = tail = -1; - size = maxtokens; - arr.resize(maxtokens); - } - void enqueue(passData* warmStartData); - passData* dequeue(); - bool isEmpty() { return head == -1; } -}; - -void circBuf::enqueue( passData* warmStartData ) -{ - if( head == -1 ) - { - head = tail = 0; - arr[tail] = warmStartData; - } - else if( (tail == size-1) && (head != 0) ) - { - tail = 0; - arr[tail] = warmStartData; - } - else - { - tail++; - arr[tail] = warmStartData; - } -} - -passData* circBuf::dequeue() -{ - passData* data = arr[head]; - if( head == tail ) - { - head = -1; - tail = -1; - } - else if( head == size-1 ) - { - head = 0; - } - else - { - head++; - } - return data; -} - - // Forward declaration void modifyFileName( string &path, const string &newExtension ); @@ -177,7 +105,6 @@ bool processRTP(); bool processSOL(); bool processDER( SoPlex workinglp ); bool getConstraints( SoPlex &workinglp, string &consense, Rational &rhs, int &activeConstraint, size_t currentDerivation); -std::string completelin( SoPlex &workinglp, bimap& LProwCertificateMap, Constraint &constraint); static bool completeWeakDomination(DSVectorRational &row, int consense, Rational &rhs, stringstream& completedLine, stringstream &initialLine, string& constraintname); @@ -232,7 +159,6 @@ static void printUsage(const char* const argv[], int idx) \n turn off to boost performance if only weak derivations are present.\n" " --debugmode=on/off enable extra debug output from viprcomp\n" " --verbosity= set verbosity level inside SoPlex\n" - " --threads= maximal number of threads to use \n" "\n"; if(idx <= 0) cerr << "missing input file\n\n"; @@ -345,23 +271,6 @@ int main(int argc, char *argv[]) cout << "Continue with default setings (SoPlex on)" << endl; } } - // set maximal number of threads that should be used - else if(strncmp(option, "threads=", 8) == 0) - { - char* str = &option[8]; - if( isdigit(option[8])) - { - int maxthreads = atoi(str); - if( maxthreads < 0 || maxthreads > thread::hardware_concurrency() ) - { - cerr << "threads outside of valid range: specified " << maxthreads << " but maximal number is " << thread::hardware_concurrency() << endl; - printUsage(argv, optidx); - return 1; - } - else - nthreads = maxthreads; - } - } else if(strncmp(option, "outfile=", 8) == 0) { path = string(&option[8]); @@ -887,86 +796,10 @@ static size_t pushLineToConstraints(string& line, size_t conidx) cerr << "wrong sense for constraints " << consense << endl; break; } - constraints[conidx] = {row, rhs, sense, line}; + constraints[conidx] = {row, rhs, sense}; return constraints.size() - 1; } -// read data from certificateFile and buffer it correctly in the stringstream of returnData -static void processSequentialInputFilter(parallelData& returnData, size_t& lineindex, tbb::flow_control& fc) -{ - string line; - bool stop = false; - int nbufferedlines = 0; - - stringstream passstream; - bool lineneedscompletion = false; - size_t filepos = certificateFile.tellg(); - - while( !stop && getline(certificateFile, line) ) - { - lineneedscompletion = (line.find("weak") != string::npos) || (line.find("incomplete") != string::npos); - // line needs to be completed -> only one line at a time - if( lineneedscompletion ) - { - if( nbufferedlines == 0 ) - { - returnData.conidx.push_back(lineindex); - pushLineToConstraints(line, lineindex); - lineindex++; - nbufferedlines++; - passstream << line; - stop = true; - } - else - { - // reset to beginning of line - certificateFile.seekg(filepos); - stop = true; - lineneedscompletion = false; - } - } - else - { - returnData.conidx.push_back(lineindex); - pushLineToConstraints(line, lineindex); - lineindex++; - passstream << line << std::endl; - nbufferedlines++; - if( nbufferedlines >= 10 ) - stop = true; - } - filepos = certificateFile.tellg(); - } - - returnData.needscompletion = lineneedscompletion; - - if( nbufferedlines > 0 ) - returnData.linestream << passstream.rdbuf(); - else - fc.stop(); -} - -// read data from certificateFile and buffer it correctly in the stringstream of returnData -static void readFileIntoMemory(size_t initialLine, std::vector& toCompleteLines) -{ - string line; - size_t lineindex = initialLine; - bool lineneedscompletion = false; - - while( getline(certificateFile, line) ) - { - if( line.length() == 0 || line[0] == '%' ) - continue; - - lineneedscompletion = (line.find("weak") != string::npos) || (line.find("incomplete") != string::npos); - // line needs to be completed -> only one line at a time - if( lineneedscompletion ) - toCompleteLines.push_back(lineindex); - - pushLineToConstraints(line, lineindex); - lineindex++; - } -} bool processDER(SoPlex workinglp) { @@ -1007,112 +840,49 @@ bool processDER(SoPlex workinglp) // skip to next line certificateFile.ignore(std::numeric_limits::max(), '\n'); - cout << "Available threads: " << nthreads << endl; - lineindex = numberOfConstraints; - readFileIntoMemory(lineindex, toCompleteLines); - - circBuf circQueue(0); + string line; + bool lineneedscompletion = false; + completedFile << endl; - // generate and queue the LPs that are needed in parallel - if( usesoplex ) + while( getline(certificateFile, line) ) { - circQueue.resize(2 * nthreads); - for(int i = 0; i < 2 * nthreads; ++i) - { - passData* queueData = new passData[1]; - //queueData->passLp(); - queueData->passLp.setIntParam(SoPlex::READMODE, SoPlex::READMODE_RATIONAL); - queueData->passLp.setIntParam(SoPlex::SOLVEMODE, SoPlex::SOLVEMODE_RATIONAL); - queueData->passLp.setIntParam(SoPlex::CHECKMODE, SoPlex::CHECKMODE_RATIONAL); - queueData->passLp.setIntParam(SoPlex::SYNCMODE, SoPlex::SYNCMODE_AUTO); - queueData->passLp.setRealParam(SoPlex::FEASTOL, 0.0); - queueData->passLp.setRealParam(SoPlex::OPTTOL, 0.0); - queueData->passLp = workinglp; - circQueue.enqueue(queueData); - } - } - - // reset the line index - lineindex = 0; - - gettimeofday( &end, 0 ); - cout << endl << "processing file into memory took " << getTimeSecs(start, end) - << " seconds (Wall Clock)" << endl; - - gettimeofday( &start, 0 ); - - - // pipeline to complete the derivations - tbb::parallel_pipeline(nthreads, - // sequential filter to manage the circular buffer and to ensure output is in correct order - tbb::make_filter( tbb::filter_mode::serial_in_order, - [&]( tbb::flow_control& fc) { - parallelData returnData; - while(lineindex != toCompleteLines.size()) - { - if( usesoplex ) - returnData.bufData = circQueue.dequeue(); - returnData.conidx.push_back(toCompleteLines[lineindex]); - lineindex++; - return returnData; - } - fc.stop(); - return returnData; - } - ) & - // parallel processing and completion of derivations -> passes completed line to last filter - tbb::make_filter( tbb::filter_mode::parallel, - [&]( parallelData returnData ) { - returnData.line = completelin(returnData.bufData->passLp, returnData.bufData->LProwCertificateMap, constraints[returnData.conidx[0]]); - return returnData; - } - ) & - // manages the queueing of the circular buffer and pushes the completed lines to a vector in the correct order - tbb::make_filter( tbb::filter_mode::serial_in_order, - [&]( parallelData returnData ) { - - completedlines.push_back(returnData.line); - if( usesoplex ) - circQueue.enqueue(returnData.bufData); - } - ) - ); + if( line.empty() || line[0] == '%' ) + continue; - if( usesoplex ) - { - while(!circQueue.isEmpty()) + // line needs to be completed -> only one line at a time + if( line.find("weak") != string::npos ) { - passData* data = circQueue.dequeue(); - delete[] data; + toCompleteLines.push_back(lineindex); + pushLineToConstraints(line, lineindex); + auto constraint = constraints[lineindex]; + basic_string constraintname = line.substr(0, line.find(' ')); + + int consense = constraint.sense; + Rational& rhs = constraint.side; + DSVectorPointer row = constraint.vec; + + auto derivationstart = line.find("lin"); + stringstream linestream(line.substr(derivationstart + 3)); + string numberOfCoefficients; + linestream >> numberOfCoefficients; + stringstream completedDerivation; + vector activeDerivations; + auto retval = completeWeakDomination(*row, consense, rhs, completedDerivation, linestream, constraintname); + completedDerivation << " -1 "; + completedFile << line.substr(0,derivationstart + 3) + completedDerivation.str() << endl; } - } - - - gettimeofday( &end, 0 ); - cout << endl << "processing completion pipeline took " << getTimeSecs(start, end) - << " seconds (Wall Clock)" << endl; - - gettimeofday(&start, 0 ); - - // output the lines to the certificate - int c = 0; - completedFile << endl; - for( auto i = numberOfConstraints; i < constraints.size(); ++i ) - { - if( toCompleteLines.size() == 0 || c >= toCompleteLines.size() || i != toCompleteLines[c] ) - completedFile << constraints[i].line << endl; else { - completedFile << completedlines[c] << endl; - c++; + pushLineToConstraints(line, lineindex); + completedFile << line << endl; } + lineindex++; } gettimeofday( &end, 0 ); - cout << endl << "writing to file took " << getTimeSecs(start, end) - << " seconds (Wall Clock)" << endl << endl; + cout << endl << "completing took " << getTimeSecs(start, end) << " seconds (Wall Clock)" << endl; std::cout << "Completed " << toCompleteLines.size() << " out of " << numberOfDerivations << endl; return true; @@ -1234,79 +1004,11 @@ bool getConstraints(SoPlex &workinglp, string &consense, Rational &rhs, int &act returnStatement = false; } - constraints.push_back({row, Rational(rhs), sense, ""}); + constraints.push_back({row, Rational(rhs), sense }); return returnStatement; } -string completelin( SoPlex &workinglp, bimap& LProwCertificateMap, Constraint& constraint) -{ - string& line = constraint.line; - int consense = constraint.sense; - Rational& rhs = constraint.side; - DSVectorPointer row = constraint.vec; - - auto derivationstart = line.find("lin"); - stringstream linestream(line.substr(derivationstart + 3)); - stringstream completedDerivation; - string numberOfCoefficients; - vector activeDerivations; - - bool retval = true; - - linestream >> numberOfCoefficients; - - if( numberOfCoefficients == "incomplete" ) - { - string tmp; - - assert(usesoplex); - if( !usesoplex ) - { - cerr << "Soplex support must be enabled to process incomplete constraint type. Rerun with parameter soplex=ON." << endl; - return ""; - } - VectorRational newObjective(0); - newObjective.reSize(workinglp.numColsRational()); - newObjective.reDim(workinglp.numColsRational()); - newObjective = *row; - workinglp.changeObjRational(newObjective); - - // workinglp.setRealParam(SoPlex::TIMELIMIT, 10.0); - - assert( consense == 0 || consense == -1 || consense == 1); - - if( consense >= 0 ) - workinglp.setIntParam(SoPlex::OBJSENSE, SoPlex::OBJSENSE_MINIMIZE); - else - workinglp.setIntParam(SoPlex::OBJSENSE, SoPlex::OBJSENSE_MAXIMIZE); - - linestream >> tmp; - while( tmp != "}" ) - { - activeDerivations.push_back(stol(tmp)); - linestream >> tmp; - } - linestream.seekg(0); - retval = completeIncomplete( workinglp, LProwCertificateMap, activeDerivations, "", completedDerivation, linestream ); -#ifndef NDEBUG - cout << "Completed derivation: " << line.substr(0,10) << endl; -#endif - } - else if( numberOfCoefficients == "weak" ) - { - basic_string constraintname = line.substr(0, line.find(' ')); - retval = completeWeakDomination(*row, consense, rhs, completedDerivation, linestream, constraintname); - } - else - cerr << "Wrong type of derivation: " << numberOfCoefficients << endl; - - completedDerivation << " -1 "; - - string completedstring = line.substr(0,derivationstart + 3) + completedDerivation.str(); - return completedstring; - -} // Reads multipliers for completing weak domination static bool readMultipliers( int &sense, SVectorRat &mult, stringstream &baseLine )