Fixes

pcasso-src/LevelPool.cc

@@ -29,6 +29,9 @@ bool LevelPool::add_shared(vec<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& 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];

pcasso-src/LookaheadSplitting.cc

@@ -337,6 +337,8 @@ lbool LookaheadSplitting::produceSplitting(vec<vec<vec<Lit>* >* > **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<vec<vec<Lit>* >* > **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<vec<Lit>* > **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<vec<Lit>* > **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<vec<Lit>* > **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<vec<Lit>* > **valid)
         }
     }
 
-    Lit next;
+    Lit next = lit_Undef;
 
     if (bestVarIndex != var_Undef) {
         bool pol = false;
@@ -1579,7 +1587,7 @@ Lit LookaheadSplitting::pickBranchLiteral(vec<vec<Lit>* > **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;
     }
 

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<vector<Lit>*>);
-        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]);
         }

pcasso-src/SolverPT.cc

@@ -1435,7 +1435,9 @@ void SolverPT::push_learnts()
     bool sharedSuccess = false;
     bool fullPool = false;
 
+    vec<Lit> 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<Lit> 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()<learnts_indeces.size());

scripts/pcasso.sh

@@ -42,7 +42,7 @@ simplifier="$DIR/coprocessor"
 #
 file=$1				# first argument is CNF instance to be solved
 shift 1
-tmpDir=$2			# directory to write the temporary files to
+tmpDir=$1			# directory to write the temporary files to
 shift 1											# reduce the parameters, removed the very first one. remaining $@ parameters are arguments
 
 # in case no tmpDir has been specified, create one and trap for deletion on exit