Skip to content

Commit

Permalink
Revert "minor fix"
Browse files Browse the repository at this point in the history
This reverts commit 0426ba3.
  • Loading branch information
prsabahrami committed Jan 24, 2025
1 parent 0426ba3 commit b95b789
Show file tree
Hide file tree
Showing 4 changed files with 84 additions and 360 deletions.
8 changes: 3 additions & 5 deletions src/solver/clause.rs
Original file line number Diff line number Diff line change
Expand Up @@ -265,12 +265,10 @@ impl Clause {
false,
)
} else {
// No valid requirement candidate and condition is true
// This is an immediate conflict - we can't satisfy the requirement
// We need to watch the condition candidate to detect when it becomes true
// No valid requirement candidate, use first condition candidate and mark conflict
(
Clause::Conditional(parent_id, condition, requirement),
Some([parent_id.negative(), condition_first_candidate.negative()]),
Some([parent_id.negative(), condition_first_candidate.positive()]),
true,
)
}
Expand All @@ -286,7 +284,7 @@ impl Clause {
false,
)
} else {
// All conditions false, no conflict
// All conditions false
(
Clause::Conditional(parent_id, condition, requirement),
None,
Expand Down
34 changes: 0 additions & 34 deletions src/solver/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1155,40 +1155,6 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
self.decide_assertions(level)?;
self.decide_learned(level)?;

// Check for conflicts in conditional clauses
for ((solvable_id, condition), clauses) in &self.conditional_clauses {
// Only check clauses where the parent is true
if self.decision_tracker.assigned_value(*solvable_id) != Some(true) {
continue;
}

// Check if the condition is true
let condition_requirement: Requirement = (*condition).into();
let conditional_candidates = &self.requirement_to_sorted_candidates[&condition_requirement];
let condition_is_true = conditional_candidates.iter().any(|candidates| {
candidates.iter().any(|&candidate| {
self.decision_tracker.assigned_value(candidate) == Some(true)
})
});

if condition_is_true {
// For each clause, check if all requirement candidates are false
for (requirement, clause_id) in clauses {
let requirement_candidates = &self.requirement_to_sorted_candidates[requirement];
let all_candidates_false = requirement_candidates.iter().all(|candidates| {
candidates.iter().all(|&candidate| {
self.decision_tracker.assigned_value(candidate) == Some(false)
})
});

if all_candidates_false {
// This is a conflict - we have a true condition but can't satisfy the requirement
return Err(PropagationError::Conflict(*solvable_id, true, *clause_id));
}
}
}
}

// For each decision that has not been propagated yet, we propagate the
// decision.
//
Expand Down
10 changes: 10 additions & 0 deletions tests/.solver.rs.pending-snap
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
{"run_id":"1737574135-658533000","line":1475,"new":{"module_name":"solver","snapshot_name":"conditional_requirements-2","metadata":{"source":"tests/solver.rs","assertion_line":1475,"expression":"result"},"snapshot":""},"old":{"module_name":"solver","metadata":{},"snapshot":"b=1\nc=1"}}
{"run_id":"1737574174-973942000","line":1211,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":1428,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":923,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":1254,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":1306,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":885,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":906,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":943,"new":null,"old":null}
{"run_id":"1737574174-973942000","line":1376,"new":null,"old":null}
Loading

0 comments on commit b95b789

Please sign in to comment.