diff --git a/pcasso-src/LevelPool.cc b/pcasso-src/LevelPool.cc index 94a5ed2..5bcc8af 100644 --- a/pcasso-src/LevelPool.cc +++ b/pcasso-src/LevelPool.cc @@ -29,6 +29,9 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup temp[0] = toLit(nodeID); + assert(toInt(temp[0]) >= 0 && "the number to identify the node should be positive"); + assert(writeP == 0 || shared_clauses[writeP-1] == lit_Undef); // the pointer should point at the end of a clause + assert(temp.size() < shared_clauses.size()); if (writeP + temp.size() < shared_clauses.size() - 2) { // Space for the ending lit_Undef @@ -38,7 +41,7 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup writeP += temp.size(); int k = writeP; ++writeP; - while (shared_clauses[k] != lit_Undef) { + while (shared_clauses[k] != lit_Undef && k < endP) { // clean the whole vector, or until the next end of a clause shared_clauses[k++] = lit_Undef; } if (writeP > endP) { endP = writeP; } @@ -54,7 +57,7 @@ bool LevelPool::add_shared(vec& lits, unsigned int nodeID, bool disable_dup } int k = writeP; ++writeP; - while (shared_clauses[k] != lit_Undef) { + while (shared_clauses[k] != lit_Undef && k < endP) { shared_clauses[k++] = lit_Undef; } assert(endP > writeP); @@ -68,10 +71,11 @@ LevelPool::getChunk(int readP, vec& chunk) if (readP >= endP) { return; } - if (((readP != 0 && shared_clauses[readP - 1] == lit_Undef) || readP == 0)) { + if (( (readP != 0 && shared_clauses[readP - 1] == lit_Undef) || readP == 0)) { if (readP <= writeP) { chunk.growTo(writeP - readP); int j = 0; + assert(readP == 0 || toInt(shared_clauses[readP]) >= 0); // the first literal indicates the ID of the node that shared the clause for (int i = readP; i < writeP; ++i) { assert(writeP - readP == chunk.size()); assert(j < chunk.size()); @@ -82,6 +86,7 @@ LevelPool::getChunk(int readP, vec& chunk) } else { chunk.growTo((endP - readP) + writeP); int j = 0; + assert(readP == 0 || toInt(shared_clauses[readP]) >= 0); // the first literal indicates the ID of the node that shared the clause for (int i = readP; i < endP; ++i) { assert(j < chunk.size()); chunk[j++] = shared_clauses[i]; @@ -96,6 +101,7 @@ LevelPool::getChunk(int readP, vec& chunk) } else { chunk.growTo(writeP); int j = 0; + assert(writeP == 0 || toInt(shared_clauses[0]) > 0); // the first literal indicates the ID of the node that shared the clause for (int i = 0; i < writeP; ++i) { assert(j < chunk.size()); chunk[j++] = shared_clauses[i]; diff --git a/pcasso-src/LookaheadSplitting.cc b/pcasso-src/LookaheadSplitting.cc index fcf2455..c946b48 100644 --- a/pcasso-src/LookaheadSplitting.cc +++ b/pcasso-src/LookaheadSplitting.cc @@ -337,6 +337,8 @@ lbool LookaheadSplitting::produceSplitting(vec* >* > **splits, vec< } else if (next == lit_Undef) { if (checkSolution()) { return l_True; + } else { + assert(false && "this case should be handled, a split is required"); } } @@ -509,6 +511,8 @@ lbool LookaheadSplitting::produceSplitting(vec* >* > **splits, vec< if (next == lit_Undef) { if (checkSolution()) { return l_True; + } else { + assert(false && "this case should be handled, a split is required"); } } if (decisionLevel() == 0 && splitting->size() == 0) { @@ -1192,8 +1196,9 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) sizePositiveLookahead = trail.size() - initTrailSize; for (int j = initTrailSize; j < trail.size(); j++) { //fprintf(stderr, "Watcher size = %d\n", watches[trail[j]].size()); - sizeWatcherPositiveLookahead += sign(trail[j]) ? watcherNegLitSize[bestKList[i]] : watcherPosLitSize[bestKList[i]]; - binClausePositiveLookahead += sign(trail[j]) ? numPosLitTerClause[var(trail[j])] : numNegLitTerClause[var(trail[j])]; + const Var v = var(trail[j]); + sizeWatcherPositiveLookahead += sign(trail[j]) ? watcherNegLitSize[v] : watcherPosLitSize[v]; + binClausePositiveLookahead += sign(trail[j]) ? numPosLitTerClause[v] : numNegLitTerClause[v]; } //check if solution found if (checkSolution()) { @@ -1267,8 +1272,9 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) } sizeNegativeLookahead = trail.size() - initTrailSize; for (int j = initTrailSize; j < trail.size(); j++) { - sizeWatcherNegativeLookahead += sign(trail[j]) ? watcherNegLitSize[bestKList[i]] : watcherPosLitSize[bestKList[i]]; - binClauseNegativeLookahead += sign(trail[j]) ? numPosLitTerClause[var(trail[j])] : numNegLitTerClause[var(trail[j])]; + const Var v = var(trail[j]); + sizeWatcherNegativeLookahead += sign(trail[j]) ? watcherNegLitSize[v] : watcherPosLitSize[v]; + binClauseNegativeLookahead += sign(trail[j]) ? numPosLitTerClause[v] : numNegLitTerClause[v]; } //check if to perform double lookahead if (opt_double_lookahead) { @@ -1425,10 +1431,12 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) jump: cancelUntil(decLev); - for (int i = 0; i < score.size(); i++) { - if (score[i] > 0 && score[i] > bestVarScore && value(bestKList[i]) == l_Undef) { - bestVarScore = score[i]; - bestVarIndex = i; + if (bestKList.size() > 0) { + for (int i = 0; i < score.size(); i++) { + if (score[i] > 0 && score[i] > bestVarScore && value(bestKList[i]) == l_Undef) { + bestVarScore = score[i]; + bestVarIndex = i; + } } } @@ -1445,7 +1453,7 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) } } - Lit next; + Lit next = lit_Undef; if (bestVarIndex != var_Undef) { bool pol = false; @@ -1579,7 +1587,7 @@ Lit LookaheadSplitting::pickBranchLiteral(vec* > **valid) *///if(opt_var_eq>0) //fprintf(stderr, "splitter: Var Equivalence \t\t\t = %d \n", varEq.size()/2); //fprintf(stderr, "splitter: Best Var Index = %d\n",bestVarIndex); - if (opt_tabu) { + if (opt_tabu && next != lit_Undef) { tabuList[var(next)] = true; } diff --git a/pcasso-src/Master.cc b/pcasso-src/Master.cc index 1008f5e..1648520 100644 --- a/pcasso-src/Master.cc +++ b/pcasso-src/Master.cc @@ -196,6 +196,7 @@ int Master::run() // check the state of the tree // solve the next node in the tree if (MSverbosity > 0) { fprintf(stderr, "M: start main loop\n"); } + int stuck = 0; while (!done) { int idles = 0; // important, because this indicates that there can be done more in the next round! @@ -208,12 +209,15 @@ int Master::run() if (threadData[i].s == unclean) { // Davide> Free memory - if (threadData[i].result == 20 && stopUnsatChilds) { + if (threadData[i].result == 20) { // The children are NOT running, so I can delete every pool lock(); threadData[i].nodeToSolve->setState(TreeNode::unsat, true); + // fprintf(stderr, "c root node state: %d\n", root.getState()); unlock(); - killUnsatChildren(i); + if (stopUnsatChilds) { + killUnsatChildren(i); + } } uncleans++; @@ -371,7 +375,13 @@ int Master::run() for (; i < threads; ++i) { if (threadData[i].s == splitting) { break; } // TODO SHOULDN'T BE IDLE ?? DAVIDE> if (threadData[i].s == working) { break; } // do not stop if some worker is doing something + if (threadData[i].s == unclean) { break; } // do not stop if some worker is not cleaned up yet } + + // allow the solver 16 times reaching this before we actually stop working + stuck ++; + if (stuck < 16) { continue; } + // if there is a thread that is still doing something, we did not run out of work! if (i == threads) { fprintf(stderr, "\n***\n*** RUN OUT OF WORK - return unknown?\n***\n\n"); @@ -384,7 +394,9 @@ int Master::run() else if (threadData[i].s == unclean) { uncleans++; } } - fprintf(stderr, "c idle: %d working: %d splitting: %d unclean: %d\n", idles, workers, splitters, uncleans); + fprintf(stderr, "c (after %d iterations): idle: %d working: %d splitting: %d unclean: %d\n", stuck, idles, workers, splitters, uncleans); + // for debugging purposes, stop here. we assume, there is a solution but nobody told us, so let's check + assert(false && "this should not be reached"); exit(0); } @@ -871,7 +883,7 @@ Master::solveInstance(void* data) } else { // result of solver is "unknown" if (master.plainpart) { tData.nodeToSolve->setState(TreeNode::retry); } - else { tData.nodeToSolve->setState(TreeNode::unknown); } + else { if (tData.nodeToSolve->getState() == TreeNode::retry) tData.nodeToSolve->setState(TreeNode::unknown); } if (keepToplevelUnits > 0) { int toplevelVariables = 0; @@ -933,7 +945,7 @@ Master::splitInstance(void* data) if (Portfolio && tData.nodeToSolve->getLevel() < PortfolioLevel) { // perform portfolio only until this level! master.lock(); // ********************* START CRITICAL *********************** childConstraints.push_back(new vector*>); - tData.nodeToSolve->setState(TreeNode::unknown); + if (tData.nodeToSolve->getState() == TreeNode::retry) { tData.nodeToSolve->setState(TreeNode::unknown); } // only modify, if it's retry tData.nodeToSolve->expand(childConstraints); master.addNode(tData.nodeToSolve->getChild(0)); tData.result = ret; @@ -1140,7 +1152,7 @@ Master::splitInstance(void* data) // shut down all threads that are running below that node (necessary?) } else { // simply set the node to the unknown state - tData.nodeToSolve->setState(TreeNode::unknown); + if (tData.nodeToSolve->getState() == TreeNode::retry) { tData.nodeToSolve->setState(TreeNode::unknown); } for (unsigned int i = 0; i < validConstraints.size(); i++) { tData.nodeToSolve->addNodeConstraint(validConstraints[i]); } diff --git a/pcasso-src/SolverPT.cc b/pcasso-src/SolverPT.cc index 59001c4..6a1b5f1 100644 --- a/pcasso-src/SolverPT.cc +++ b/pcasso-src/SolverPT.cc @@ -1435,7 +1435,9 @@ void SolverPT::push_learnts() bool sharedSuccess = false; bool fullPool = false; + vec c_lits; for (unsigned int i = 0; i < learnts_indeces.size(); i++) { + if(learnts_indeces[i].size() == 0) continue; // nothing to share for this level, skip it! davide::LevelPool* pool = previous_pools[i]; if (pool == 0) { continue; } @@ -1450,15 +1452,21 @@ void SolverPT::push_learnts() pool->levelPoolLock.wLock(); } for (unsigned int j = 0; j < learnts_indeces[i].size(); j++) { - Clause& c = ca[learnts[learnts_indeces[i][j]]]; + int lc_index = learnts_indeces[i][j]; + if (lc_index >= learnts.size()) { + assert(lc_index < learnts.size() && "indexes to learned clauses to share have to be in bounds"); + continue; + } + Clause& c = ca[learnts[lc_index]]; c.setShared(); - vec c_lits; + c_lits.clear(); // memory consumption optimization for (unsigned j = 0; j < c.size(); j++) { //creating vector of literals present in the clause c_lits.push(c[j]); } + assert(c.getPTLevel() >= i && "cannot share clause more upwards than its PT level allows"); sharedSuccess = pool->add_shared(c_lits, tnode->id(), disable_dupl_removal, disable_dupl_check); fullPool = pool->isFull(); @@ -1545,7 +1553,7 @@ void SolverPT::pull_learnts(int curr_restarts) } pool->levelPoolLock.rLock(); // Davide> START CRITICAL } - int readP = shared_indeces[i]; + volatile int readP = shared_indeces[i]; pool->getChunk(readP, chunk); @@ -1773,6 +1781,10 @@ void SolverPT::reduceDB() int limit = learnts.size() / 2; + for (int i = 0; i < learnts_indeces.size(); ++i) { + learnts_indeces[i].clear(); + } + for (i = j = 0; i < learnts.size(); i++) { Clause& c = ca[learnts[i]]; //assert(c.getPTLevel()