Commits

Alexandru Moșoi committed 75c26a1

bce: removes blocked clauses from occur.

Comments (0)

Files changed (1)

 			continue
 		}
 
+		tail := 0
 		for _, clause := range occur[lit] {
 			if clause == nil || clause.Deleted {
 				continue
 			}
 
 			if !blockedClauseElimination(paint, colors, occur[lit.Neg()]) {
+				occur[lit][tail] = clause
+				tail++
 				continue
 			}
 
 			// Clause is blocked, removes it from formula.
-			// TODO: update occur
 			clause.Deleted = true
 			blocked := new(blockedClause)
 			blocked.literal = lit
 				queue.Add(lit1.Neg())
 			}
 		}
+		occur[lit] = occur[lit][:tail]
 	}
 
 	log.Printf("Removed %d blocked clauses", len(bce.blocked))