Fixed bug where step was not being incremented after deciding on a new literal. Updated test scripts based on new output format

Author: mrushyendra

.gitignore

@@ -1,2 +1,4 @@
 *.swp
 *.o
+solver
+test

benchmarks/__MACOSX/benchmarks/groups/group/._bench1.sh

@@ -9,7 +9,7 @@ w=0
 
 for i in `cat name1`; do
 		python dpll.py ../../bench1/sat/$i > results 2>&1
-		if (grep -q "[^N]SATISFIABLE" results) || (grep -q "^SATISFIABLE" results); then
+		if (grep -q "[^n]sat" results) || (grep -q "^sat" results); then
 		  echo "$i Pass!"
 			let "c+=1"
 			let "s+=1"
@@ -24,7 +24,7 @@ done
 
 for i in `cat name2`; do
 		python dpll.py ../../bench1/unsat/$i > results 2>&1
-		if grep -q "UNSATISFIABLE" results; then
+		if grep -q "unsat" results; then
 		  echo "$i Pass!"
 			let "c+=1"
 			let "s+=1"

benchmarks/__MACOSX/benchmarks/groups/group/._bench2.sh

@@ -9,7 +9,7 @@ w=0
 
 for i in `cat name3`; do
 		python dpll.py ../../bench2/sat/$i > results 2>&1
-		if (grep -q "[^N]SATISFIABLE" results) || (grep -q "^SATISFIABLE" results); then
+		if (grep -q "[^n]sat" results) || (grep -q "^sat" results); then
 		  echo "$i Pass!"
 			let "c+=1"
 			let "s+=1"
@@ -24,7 +24,7 @@ done
 
 for i in `cat name4`; do
 		python dpll.py ../../bench2/unsat/$i > results 2>&1
-		if grep -q "UNSATISFIABLE" results; then
+		if grep -q "unsat" results; then
 		  echo "$i Pass!"
 			let "c+=1"
 			let "s+=1"

benchmarks/__MACOSX/benchmarks/groups/group/._bench3.sh

@@ -9,7 +9,7 @@ w=0
 
 for i in `cat name5`; do
 		python dpll.py ../../bench3/$i > results 2>&1
-		if grep -q "UNSATISFIABLE" results; then
+		if grep -q "unsat" results; then
 		  echo "$i Pass!"
 			let "c+=1"
 			let "s+=1"

benchmarks/__MACOSX/benchmarks/groups/group/._bench3.sh.zip

@@ -8,7 +8,7 @@ VarAssignment::VarAssignment() : truthVal(false), level(-1), step(0), antecedent
 
 VarAssignment::~VarAssignment(){}
 
-void VarAssignment::setAssignment(bool tVal, int lvl, int stp, int ant){
+void VarAssignment::setAssignment(bool tVal, int lvl, int stp, unsigned int ant){
     this->truthVal = tVal;
     this->level = lvl;
     this->step = stp;
@@ -151,7 +151,8 @@ vector<int> CDCL(vector<Clause>& f, const unsigned int numVars, int& sat){
         int step = 0;
         int guessedLit = vsids.decide(assignment);
         bool truthVal = guessedLit > 0 ? true : false;
-        setAssignment(assignment, abs(guessedLit), truthVal, level, step, -1, numAssigned);
+        setAssignment(assignment, abs(guessedLit), truthVal, level, step, 0, numAssigned);
+        ++step;
 
         queue<int> q(deque<int>{guessedLit});
         tuple<int, unsigned int, int> conflict; //(isConflict, clause number, conflicting variable) tuple
@@ -270,7 +271,7 @@ tuple<int, unsigned int, int> bcp(vector<Clause>& f, vector<VarAssignment>& a, q
     return make_tuple(0,0,0);
 }
 
-void setAssignment(vector<VarAssignment>& a, int var, bool truthVal, int level, int step, int antecedent, unsigned int& numAssigned){
+void setAssignment(vector<VarAssignment>& a, int var, bool truthVal, int level, int step, unsigned int antecedent, unsigned int& numAssigned){
     a[var].setAssignment(truthVal, level, step, antecedent);
     numAssigned++;
 }
@@ -300,7 +301,6 @@ pair<int, Clause> analyzeConflict(vector<Clause>& f, vector<VarAssignment>& a, u
                 maxStep = a[abs(newLits[i])].step;
             }
         }
-
         unsigned int antecedent = a[lastAssignedVar].antecedent;
         resolve(newLits, f[antecedent].getLits(), conflictVar);
     }

benchmarks/benchmarks/groups/group/bench1.sh

@@ -16,7 +16,7 @@ class VarAssignment {
     public:
         VarAssignment();
         ~VarAssignment();
-        void setAssignment(bool tVal, int lvl, int stp, int ant);
+        void setAssignment(bool tVal, int lvl, int stp, unsigned int ant);
         void unsetAssignment();
         bool truthVal;
         int level; //-1 if not assigned truthVal
@@ -67,7 +67,7 @@ map<int, unordered_set<unsigned int>> initWatchLists(vector<Clause>& f);
 int initialCheck(vector<Clause>& f, vector<VarAssignment>& a, map<int, unordered_set<unsigned int>> watchLists, int level, unsigned int& numAssigned);
 tuple<int, unsigned int, int> bcp(vector<Clause>& f, vector<VarAssignment>& a, queue<int> q, map<int, unordered_set<unsigned int>> watchLists,
         int& level, int& step, unsigned int& numAssigned);
-void setAssignment(vector<VarAssignment>& a, int var, bool truthVal, int level, int step, int antecedent, unsigned int& numAssigned);
+void setAssignment(vector<VarAssignment>& a, int var, bool truthVal, int level, int step, unsigned int antecedent, unsigned int& numAssigned);
 void unsetAssignment(vector<VarAssignment>& a, int var, unsigned int& numAssigned);
 pair<int, Clause> analyzeConflict(vector<Clause>& f, vector<VarAssignment>& a, unsigned int clauseNum, int conflictVar);
 unsigned int numLitsAtLvl(vector<int>& lits, int level, const vector<VarAssignment>& a);