09/11/cc+h

shmily93 · shmily93 · commit 30259b3ecae9 · 2015-09-12T01:53:12.000+08:00
diff --git a/core/Solver.cc b/core/Solver.cc
@@ -286,7 +286,7 @@ void Solver::dpl()
                                 NextClause: ;
                         }
                 }
-                ws.shrink(i-j);
+                ws.shrink(i-j);
                 return TRUE;
         }//according to watches,simplify the clauses
 
@@ -302,7 +302,7 @@ void Solver::dpl()
 	        }
 
         }//push the conflictclause set of learntClause into passiveClause
-
+
     int  Solver::lookAhead(){
                 assert(false);
         }//yu gu

Original file line number	Diff line number	Diff line change
`@@ -286,7 +286,7 @@ void Solver::dpl()`
`286`	`286`	`NextClause: ;`
`287`	`287`	`}`
`288`	`288`	`}`
`289`		`- ws.shrink(i-j);`
	`289`	`+ ws.shrink(i-j);`
`290`	`290`	`return TRUE;`
`291`	`291`	`}//according to watches,simplify the clauses`
`292`	`292`
`@@ -302,7 +302,7 @@ void Solver::dpl()`
`302`	`302`	`}`
`303`	`303`
`304`	`304`	`}//push the conflictclause set of learntClause into passiveClause`
`305`		`-`
	`305`	`+`
`306`	`306`	`int Solver::lookAhead(){`
`307`	`307`	`assert(false);`
`308`	`308`	`}//yu gu`