Merge pull request #1 from conp-solutions/fixes

Fixes

Author: conp-solutions

.travis.yml

@@ -0,0 +1,18 @@
+language: cpp
+dist: trusty
+compiler: g++
+sudo: required
+
+before_install:
+  - sudo add-apt-repository ppa:ubuntu-toolchain-r/test -y
+  - sudo apt-get update -q
+  - sudo apt-get remove gcc g++
+  - sudo apt-get install g++-7 gcc-7 -y
+  - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60 --slave /usr/bin/g++ g++ /usr/bin/g++-7
+  - sudo update-alternatives --install /usr/bin/gcc-ar gcc-ar /usr/bin/gcc-ar-7 60
+  - sudo update-alternatives --install /usr/bin/gcc-ranlib gcc-ranlib /usr/bin/gcc-ranlib-7 60
+  - sudo update-alternatives --install /usr/bin/x86_64-linux-gnu-gcc x86_64-linux-gnu-gcc /usr/bin/x86_64-linux-gnu-gcc-7 60 --slave /usr/bin/x86_64-linux-gnu-g++ x86_64-linux-gnu-g++ /usr/bin/x86_64-linux-gnu-g++-7
+
+# run the typical ci checks, for now, compile
+script:
+  - make pcassod pcassoRS -j $(nproc)

VERSION

@@ -1 +1 @@
-const float solverVersion = 4.27;
+const float solverVersion = 7.9;

core/Dimacs.h

@@ -66,6 +66,7 @@ static void parse_DIMACS_main(B& in, Solver& S)
                 // if (clauses > 4000000)
                 //     S.eliminate(true);
             } else {
+                assert(false && "This should not happen");
                 printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
             }
         } else if (*in == 'c' || *in == 'p') {

license.txt

@@ -2,7 +2,7 @@ MiniSat     -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
                Copyright (c) 2007-2010  Niklas Sorensson
 Glucose     -- Copyright (c) 2009-2012, Gilles Audemard, Laurent Simon
 Riss3g      -- Copyright (c) 2012-2014, Norbert Manthey
-Pcasso      -- Copyright (c) 2014, Ahmed Irfan, Davide Lanti, Norbert Manthey
+Pcasso      -- Copyright (c) 2014-2018, Ahmed Irfan, Davide Lanti, Norbert Manthey
 
 Permission is hereby granted, free of charge, to use this software for
 evaluation and research purposes.

mtl/template.mk

@@ -21,7 +21,7 @@ LINKSCOBJS = $(filter-out */Main.os, $(LIBSCOBJS))
 
 
 CXX       ?= g++ -std=c++11
-CFLAGS    ?= -Wall -Wno-parentheses
+CFLAGS    ?= -Wall -Wextra -Wno-parentheses -Wno-reorder
 LFLAGS    ?= -Wall
 
 COPTIMIZE ?= -O3

pcasso-src/Master.cc

@@ -1267,6 +1267,7 @@ Master::parseFormula(string filename)
                     // if (clauses > 4000000)
                     //     S.eliminate(true);
                 } else {
+                    assert(false && "This should not happen");
                     fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *stream), exit(3);
                 }
             } else if (*stream == 'c' || *stream == 'p') {

pcasso-src/Master.h

@@ -105,7 +105,7 @@ class Master
         Master* master;     // handle to the master class, for backward communication (e.g. wakeup)
         Master::state s;        // state of the thread
         SplitterSolver* solver;         // The most recent solver
-        ThreadData() : id(-1), result(0), timeout(-1), conflicts(-1), handle((pthread_t)0), s(idle), solver(NULL) {}
+        ThreadData() : nodeToSolve(0), id(-1), result(0), timeout(-1), conflicts(-1), handle((pthread_t)0), master(0), s(idle), solver(NULL) {}
     };
 
     // to maintain the original formula

pcasso-src/SolverPT.cc

@@ -199,7 +199,7 @@ Var SolverPT::newVar(bool sign, bool dvar, char type)
 {
     assert(varPT.size() == nVars());
     varPT.push(0);//adding PT level of the new variable
-    int v = nVars();
+    Var v = nVars();
     watches  .init(mkLit(v, false));
     watches  .init(mkLit(v, true));
 
@@ -222,6 +222,8 @@ Var SolverPT::newVar(bool sign, bool dvar, char type)
     permDiff  .resize(v + 1); // add space for the next variable
     trail    .capacity(v + 1);
     setDecisionVar(v, dvar);
+
+    return v;
 }
 
 void SolverPT::setLiteralPTLevel(const Lit& l, unsigned pt)
@@ -1128,7 +1130,7 @@ lbool SolverPT::search(int nof_conflicts)
                 pull_learnts(starts);
                 if (!ok) { return l_False; }
                 if (!simplify()) {
-                    printf("c last restart ## conflicts  :  %d %d \n", conflictC, decisionLevel());
+                    // fprintf(stderr, "c last restart ## conflicts  :  %d %d \n", conflictC, decisionLevel());
                     return l_False;
                 }
             }
@@ -1165,7 +1167,7 @@ lbool SolverPT::search(int nof_conflicts)
 
                 if (next == lit_Undef) {
 
-                    printf("c last restart ## conflicts  :  %d %d \n", conflictC, decisionLevel());
+                    // fprintf("c last restart ## conflicts  :  %d %d \n", conflictC, decisionLevel());
                     // Model found:
                     return l_True;
                 }

scripts/pcasso.sh

@@ -55,6 +55,7 @@ fi
 
 
 # some temporary files 
+mkdir -p $tmpDir
 undo=$tmpDir/undo_$$						# path to temporary file that stores cp3 undo information
 tmpCNF=$tmpDir/tmpCNF_$$				# path to temporary file that stores cp3 simplified formula
 model=$tmpDir/model_$$					# path to temporary file that model of the preprocessor (stdout)

utils/ParseUtils.h

@@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef Minisat_ParseUtils_h
 #define Minisat_ParseUtils_h
 
+#include <assert.h>
 #include <stdlib.h>
 #include <stdio.h>
 #include <math.h>
@@ -102,17 +103,17 @@ static double parseDouble(B& in)   // only in the form X.XXXXXe-XX
     if (*in == EOF) { return 0; }
     if (*in == '-') { neg = true, ++in; }
     else if (*in == '+') { ++in; }
-    if (*in < '1' || *in > '9') { printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
+    if (*in < '1' || *in > '9') { assert(false && "This should not happen"); printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
     accu = (double)(*in - '0');
     ++in;
-    if (*in != '.') { printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
+    if (*in != '.') { assert(false && "This should not happen"); printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
     ++in; // skip dot
     currentExponent = 0.1;
     while (*in >= '0' && *in <= '9')
         accu = accu + currentExponent * ((double)(*in - '0')),
         currentExponent /= 10,
                            ++in;
-    if (*in != 'e') { printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
+    if (*in != 'e') { assert(false && "This should not happen"); printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
     ++in; // skip dot
     exponent = parseInt(in); // read exponent
     accu *= pow(10, exponent);
@@ -128,7 +129,7 @@ static int64_t parseInt(B& in)
     skipWhitespace(in);
     if (*in == '-') { neg = true, ++in; }
     else if (*in == '+') { ++in; }
-    if (*in < '0' || *in > '9') { fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
+    if (*in < '0' || *in > '9') { assert(false && "This should not happen"); fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3); }
     while (*in >= '0' && *in <= '9')
         val = val * 10 + (*in - '0'),
         ++in;