problemreductions/rules/
registersufficiency_ilp.rs1use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
4use crate::models::misc::RegisterSufficiency;
5use crate::reduction;
6use crate::rules::traits::{ReduceTo, ReductionResult};
7
8#[derive(Debug, Clone)]
9pub struct ReductionRegisterSufficiencyToILP {
10 target: ILP<bool>,
11 num_vertices: usize,
12}
13
14impl ReductionResult for ReductionRegisterSufficiencyToILP {
15 type Source = RegisterSufficiency;
16 type Target = ILP<bool>;
17
18 fn target_problem(&self) -> &ILP<bool> {
19 &self.target
20 }
21
22 fn extract_solution(
23 &self,
24 target_solution: &<Self::Target as crate::traits::Problem>::Solution,
25 ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
26 crate::rules::traits::validate_target_witness(
27 self.target_problem(),
28 target_solution,
29 |value| value.value.is_some(),
30 "target ILP assignment is infeasible",
31 )?;
32
33 let n = self.num_vertices;
34 (0..n)
35 .map(|v| {
36 target_solution[v * n..(v + 1) * n]
37 .iter()
38 .position(|&computed| computed != 0)
39 .ok_or_else(|| {
40 crate::rules::ExtractionError::invalid("vertex is never computed")
41 })
42 })
43 .collect()
44 }
45}
46
47#[crate::aggregate_reduction(ilp_feasibility)]
48impl crate::rules::AggregateReductionResult for ReductionRegisterSufficiencyToILP {}
49
50#[reduction(transform = {
51 exact {
52 num_vars = "2 * num_vertices^2 - num_vertices * num_sinks",
53 num_constraints = "num_vertices^2 + 2 * num_vertices * num_arcs + num_vertices",
54 num_nonzeros = "4 * num_vertices^2 - 2 * num_vertices + 5 * num_vertices * num_arcs - num_arcs",
55 },
56 upper_bound {
57 max_constraint_magnitude_bits = "num_vertices + 1",
58 },
59})]
60impl ReduceTo<ILP<bool>> for RegisterSufficiency {
61 type Result = ReductionRegisterSufficiencyToILP;
62
63 fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
64 let n = self.num_vertices();
65 let overflow = || {
66 crate::rules::ReductionError::integer_overflow::<Self, ILP<bool>>(
67 "counting cumulative scheduling variables",
68 )
69 };
70 let square = n.checked_mul(n).ok_or_else(overflow)?;
71 let mut has_dependent = vec![false; n];
72 for &(_, u) in self.arcs() {
73 has_dependent[u] = true;
74 }
75 let non_sinks = has_dependent.iter().filter(|&&value| value).count();
76 let num_vars = n
77 .checked_mul(non_sinks)
78 .and_then(|count| square.checked_add(count))
79 .ok_or_else(overflow)?;
80 let horizon = Self::exact_i64(n, "bounding schedule row sums")?;
81 let bound = Self::exact_i64(self.bound(), "representing the register bound")?.min(horizon);
82 let computed = |v: usize, t: usize| v * n + t;
83 let mut live_offset: Vec<_> = (0..n).map(|v| v * n).collect();
84 let mut next = square;
85 for (v, &needed) in has_dependent.iter().enumerate() {
86 if needed {
87 live_offset[v] = next;
88 next += n;
89 }
90 }
91 let mut constraints = Vec::new();
92 for v in 0..n {
93 for t in 0..n.saturating_sub(1) {
94 constraints.push(LinearConstraint::le(
95 vec![(computed(v, t), 1), (computed(v, t + 1), -1)],
96 0,
97 ));
98 }
99 }
100 for t in 0..n {
101 constraints.push(LinearConstraint::eq(
102 (0..n).map(|v| (computed(v, t), 1)).collect(),
103 Self::exact_i64(t + 1, "counting completed vertices")?,
104 ));
105 }
106 for &(w, u) in self.arcs() {
107 for t in 0..n {
108 let mut precedence = vec![(computed(w, t), 1)];
109 if t > 0 {
110 precedence.push((computed(u, t - 1), -1));
111 }
112 constraints.push(LinearConstraint::le(precedence, 0));
113 constraints.push(LinearConstraint::ge(
114 vec![
115 (live_offset[u] + t, 1),
116 (computed(u, t), -1),
117 (computed(w, t), 1),
118 ],
119 0,
120 ));
121 }
122 }
123 for t in 0..n {
124 constraints.push(LinearConstraint::le(
126 live_offset.iter().map(|&offset| (offset + t, 1)).collect(),
127 bound,
128 ));
129 }
130
131 Ok(ReductionRegisterSufficiencyToILP {
132 target: ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
133 .map_err(Self::target_construction)?,
134 num_vertices: n,
135 })
136 }
137}
138
139#[cfg(feature = "example-db")]
140pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
141 vec![crate::example_db::specs::RuleExampleSpec {
142 id: "registersufficiency_to_ilp",
143 build: || {
144 let source = RegisterSufficiency::new(
145 7,
146 vec![
147 (2, 0),
148 (2, 1),
149 (3, 1),
150 (4, 2),
151 (4, 3),
152 (5, 0),
153 (6, 4),
154 (6, 5),
155 ],
156 3,
157 );
158 crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
159 },
160 }]
161}
162
163#[cfg(test)]
164#[path = "../unit_tests/rules/registersufficiency_ilp.rs"]
165mod tests;