Skip to content

Commit cdd9411

Browse files
authored
fix: post process new domain (#129)
When creating a new domain, it could be that the lb/ub is a hole, or that there are holes outside of the bounds. This is currently not post processed before creating the domain, so this happens after minimisation for the first time. This can cause the number of literals after minimisation to be higher than before, causing an overflow: https://github.com/ConSol-Lab/Pumpkin/blob/d66ecb6e541b9d15562dc7db223b8a86b3bade13/pumpkin-solver/src/engine/conflict_analysis/minimisers/recursive_minimiser.rs#L65 Post-processing the new domain fixes this problem.
1 parent d66ecb6 commit cdd9411

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

pumpkin-solver/src/engine/conflict_analysis/minimisers/semantic_minimiser.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,12 +118,18 @@ impl SemanticMinimiser {
118118
}
119119

120120
fn grow(&mut self, lower_bound: i32, upper_bound: i32, holes: Vec<i32>) {
121-
let initial_domain = SimpleIntegerDomain {
121+
let mut initial_domain = SimpleIntegerDomain {
122122
lower_bound,
123123
upper_bound,
124124
holes: HashSet::from_iter(holes.iter().cloned()),
125125
inconsistent: false,
126126
};
127+
128+
initial_domain.propagate_holes_on_lower_bound();
129+
initial_domain.propagate_holes_on_upper_bound();
130+
initial_domain.remove_redundant_holes();
131+
initial_domain.update_consistency();
132+
127133
let _ = self.original_domains.push(initial_domain.clone());
128134
let _ = self.domains.push(initial_domain);
129135
}

0 commit comments

Comments
 (0)