Commits

Alexandru Moșoi committed a187df8

bcp: deletes satisfied clauses by unit clauses.

Comments (0)

Files changed (1)

 }
 
 // Adds a new clause to BCP
+// Returns true if a conflict is identified.
 func (bcp *BCP) addClause(clause *Clause) bool {
 	if len(clause.Literals) == 0 {
 		panic("empty clause")
 			return true
 		}
 
+		// Deletes satisfied clauses.
+		for _, watch := range bcp.watches[unit] {
+			watch.clause.Deleted = true
+		}
+		bcp.watches[unit] = nil
+
+		// And enqueues the unit for propagation.
 		bcp.queueUnit(unit, nil)
 		return false
 	}
 	return false
 }
 
-func (bcp *BCP) checkConflict(ignore Literal, clause *Clause) {
-	if ignore != 0 && !bcp.reasons[ignore].alive {
-		panic("literal not assigned")
-	}
-
-	if clause != nil {
-		return
-	}
-
-	for _, lit := range clause.Literals {
-		if lit != ignore.Neg() {
-			bcp.checkConflict(lit, bcp.reasons[lit].clause)
-		}
-	}
-}
-
 // Analyzes a conflict clause.
 // For now stores the clause in bcp.Learned
 func (bcp *BCP) analyze(conflict *Clause) {
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.