|
1 | 1 | use std::ops::Index; |
2 | 2 |
|
3 | 3 | use super::solver::{ |
4 | | - count_true, traits::BoolArrayLike, traits::Operand, BoolExprArray1D, BoolVar, BoolVarArray1D, |
5 | | - BoolVarArray2D, FromModel, FromOwnedPartialModel, GraphDivisionOptions, Model, |
| 4 | + count_true, traits::BoolArrayLike, traits::Operand, BoolExprArray1D, BoolExprArray2D, BoolVar, |
| 5 | + BoolVarArray1D, BoolVarArray2D, FromModel, FromOwnedPartialModel, GraphDivisionOptions, Model, |
6 | 6 | OwnedPartialModel, Solver, |
7 | 7 | }; |
8 | 8 | use cspuz_core::csp::BoolExpr as CSPBoolExpr; |
@@ -953,6 +953,134 @@ pub fn crossable_single_cycle_grid_edges( |
953 | 953 | (is_passed, is_cross) |
954 | 954 | } |
955 | 955 |
|
| 956 | +pub struct DirectedEdges { |
| 957 | + pub up: BoolExprArray2D, |
| 958 | + pub down: BoolExprArray2D, |
| 959 | + pub left: BoolExprArray2D, |
| 960 | + pub right: BoolExprArray2D, |
| 961 | +} |
| 962 | + |
| 963 | +impl DirectedEdges { |
| 964 | + pub fn new(is_active_edge: &BoolGridEdges, direction: &BoolGridEdges) -> DirectedEdges { |
| 965 | + let up = &is_active_edge.vertical & &direction.vertical; |
| 966 | + let down = &is_active_edge.vertical & !&direction.vertical; |
| 967 | + let left = &is_active_edge.horizontal & &direction.horizontal; |
| 968 | + let right = &is_active_edge.horizontal & !&direction.horizontal; |
| 969 | + DirectedEdges { |
| 970 | + up, |
| 971 | + down, |
| 972 | + left, |
| 973 | + right, |
| 974 | + } |
| 975 | + } |
| 976 | + |
| 977 | + pub fn inbound(&self, pos: (usize, usize)) -> BoolExprArray1D { |
| 978 | + let (y, x) = pos; |
| 979 | + let mut ret = vec![]; |
| 980 | + if y > 0 { |
| 981 | + ret.push(self.down.at((y - 1, x))); |
| 982 | + } |
| 983 | + if y < self.up.shape().0 { |
| 984 | + ret.push(self.up.at((y, x))); |
| 985 | + } |
| 986 | + if x > 0 { |
| 987 | + ret.push(self.right.at((y, x - 1))); |
| 988 | + } |
| 989 | + if x < self.left.shape().1 { |
| 990 | + ret.push(self.left.at((y, x))); |
| 991 | + } |
| 992 | + BoolExprArray1D::new(ret) |
| 993 | + } |
| 994 | + |
| 995 | + pub fn outbound(&self, pos: (usize, usize)) -> BoolExprArray1D { |
| 996 | + let (y, x) = pos; |
| 997 | + let mut ret = vec![]; |
| 998 | + if y > 0 { |
| 999 | + ret.push(self.up.at((y - 1, x))); |
| 1000 | + } |
| 1001 | + if y < self.down.shape().0 { |
| 1002 | + ret.push(self.down.at((y, x))); |
| 1003 | + } |
| 1004 | + if x > 0 { |
| 1005 | + ret.push(self.left.at((y, x - 1))); |
| 1006 | + } |
| 1007 | + if x < self.right.shape().1 { |
| 1008 | + ret.push(self.right.at((y, x))); |
| 1009 | + } |
| 1010 | + BoolExprArray1D::new(ret) |
| 1011 | + } |
| 1012 | +} |
| 1013 | + |
| 1014 | +pub fn active_edges_directed_cycle_path( |
| 1015 | + solver: &mut Solver, |
| 1016 | + is_active_edge: &BoolGridEdges, |
| 1017 | + allow_self_cross: bool, |
| 1018 | + allow_path: bool, |
| 1019 | +) -> DirectedEdges { |
| 1020 | + let (h, w) = is_active_edge.base_shape(); |
| 1021 | + |
| 1022 | + let direction = &BoolGridEdges::new(solver, (h, w)); |
| 1023 | + let directed_loop = DirectedEdges::new(is_active_edge, direction); |
| 1024 | + |
| 1025 | + for y in 0..=h { |
| 1026 | + for x in 0..=w { |
| 1027 | + let inbound = directed_loop.inbound((y, x)); |
| 1028 | + let outbound = directed_loop.outbound((y, x)); |
| 1029 | + |
| 1030 | + match (allow_self_cross, allow_path) { |
| 1031 | + (false, false) => { |
| 1032 | + let deg = &solver.int_var(0, 1); |
| 1033 | + solver.add_expr(inbound.count_true().eq(deg)); |
| 1034 | + solver.add_expr(outbound.count_true().eq(deg)); |
| 1035 | + } |
| 1036 | + (false, true) => { |
| 1037 | + solver.add_expr(inbound.count_true().le(1)); |
| 1038 | + solver.add_expr(outbound.count_true().le(1)); |
| 1039 | + } |
| 1040 | + (true, false) => { |
| 1041 | + solver.add_expr(inbound.count_true().eq(outbound.count_true())); |
| 1042 | + } |
| 1043 | + (true, true) => { |
| 1044 | + let in_deg = &solver.int_var(0, 2); |
| 1045 | + let out_deg = &solver.int_var(0, 2); |
| 1046 | + solver.add_expr(inbound.count_true().eq(in_deg)); |
| 1047 | + solver.add_expr(outbound.count_true().eq(out_deg)); |
| 1048 | + solver |
| 1049 | + .add_expr((in_deg.le(1) & out_deg.le(1)) | (in_deg.eq(2) & out_deg.eq(2))); |
| 1050 | + } |
| 1051 | + } |
| 1052 | + } |
| 1053 | + } |
| 1054 | + |
| 1055 | + if allow_self_cross { |
| 1056 | + for y in 1..h { |
| 1057 | + for x in 1..w { |
| 1058 | + solver.add_expr( |
| 1059 | + is_active_edge.vertex_neighbors((y, x)).all().imp( |
| 1060 | + directed_loop |
| 1061 | + .up |
| 1062 | + .at((y - 1, x)) |
| 1063 | + .iff(directed_loop.up.at((y, x))) |
| 1064 | + & directed_loop |
| 1065 | + .down |
| 1066 | + .at((y - 1, x)) |
| 1067 | + .iff(directed_loop.down.at((y, x))) |
| 1068 | + & directed_loop |
| 1069 | + .left |
| 1070 | + .at((y, x - 1)) |
| 1071 | + .iff(directed_loop.left.at((y, x))) |
| 1072 | + & directed_loop |
| 1073 | + .right |
| 1074 | + .at((y, x - 1)) |
| 1075 | + .iff(directed_loop.right.at((y, x))), |
| 1076 | + ), |
| 1077 | + ); |
| 1078 | + } |
| 1079 | + } |
| 1080 | + } |
| 1081 | + directed_loop |
| 1082 | +} |
| 1083 | + |
956 | 1084 | #[cfg(test)] |
957 | 1085 | mod tests { |
958 | 1086 | use super::*; |
@@ -998,4 +1126,148 @@ mod tests { |
998 | 1126 | ] |
999 | 1127 | ); |
1000 | 1128 | } |
| 1129 | + |
| 1130 | + #[test] |
| 1131 | + fn test_active_edges_directed_cycle_path() { |
| 1132 | + // no cross, cycle only |
| 1133 | + { |
| 1134 | + let mut solver = Solver::new(); |
| 1135 | + let edges = crate::graph::BoolGridEdges::new(&mut solver, (3, 4)); |
| 1136 | + |
| 1137 | + single_cycle_grid_edges(&mut solver, &edges); |
| 1138 | + let directed_edges = |
| 1139 | + active_edges_directed_cycle_path(&mut solver, &edges, false, false); |
| 1140 | + solver.add_expr(directed_edges.right.at((0, 0))); |
| 1141 | + solver.add_expr(directed_edges.left.at((1, 1))); |
| 1142 | + solver.add_expr(directed_edges.up.at((0, 3))); |
| 1143 | + |
| 1144 | + let answer = solver.solve(); |
| 1145 | + assert!(answer.is_some()); |
| 1146 | + let answer = answer.unwrap(); |
| 1147 | + assert_eq!( |
| 1148 | + answer.get(&edges.horizontal), |
| 1149 | + vec![ |
| 1150 | + vec![true, true, false, true], |
| 1151 | + vec![false, true, false, false], |
| 1152 | + vec![false, true, true, false], |
| 1153 | + vec![true, true, true, true], |
| 1154 | + ] |
| 1155 | + ); |
| 1156 | + assert_eq!( |
| 1157 | + answer.get(&edges.vertical), |
| 1158 | + vec![ |
| 1159 | + vec![true, false, true, true, true], |
| 1160 | + vec![true, true, false, true, true], |
| 1161 | + vec![true, false, false, false, true], |
| 1162 | + ] |
| 1163 | + ); |
| 1164 | + } |
| 1165 | + |
| 1166 | + // no cross, allow paths |
| 1167 | + { |
| 1168 | + let mut solver = Solver::new(); |
| 1169 | + let edges = crate::graph::BoolGridEdges::new(&mut solver, (3, 4)); |
| 1170 | + solver.add_answer_key_bool(&edges.horizontal); |
| 1171 | + solver.add_answer_key_bool(&edges.vertical); |
| 1172 | + |
| 1173 | + let directed_edges = active_edges_directed_cycle_path(&mut solver, &edges, false, true); |
| 1174 | + solver.add_expr(directed_edges.right.at((1, 1))); |
| 1175 | + solver.add_expr(directed_edges.left.at((1, 3))); |
| 1176 | + solver.add_expr(directed_edges.up.at((2, 2))); |
| 1177 | + |
| 1178 | + let irrefutable_facts = solver.irrefutable_facts(); |
| 1179 | + assert!(irrefutable_facts.is_some()); |
| 1180 | + let irrefutable_facts = irrefutable_facts.unwrap(); |
| 1181 | + assert_eq!( |
| 1182 | + irrefutable_facts.get(&edges.horizontal), |
| 1183 | + vec![ |
| 1184 | + vec![None, None, None, None], |
| 1185 | + vec![None, Some(true), Some(false), Some(true)], |
| 1186 | + vec![None, None, None, None], |
| 1187 | + vec![None, None, None, None], |
| 1188 | + ] |
| 1189 | + ); |
| 1190 | + assert_eq!( |
| 1191 | + irrefutable_facts.get(&edges.vertical), |
| 1192 | + vec![ |
| 1193 | + vec![None, None, None, None, None], |
| 1194 | + vec![None, None, Some(false), None, None], |
| 1195 | + vec![None, None, Some(true), None, None], |
| 1196 | + ] |
| 1197 | + ); |
| 1198 | + } |
| 1199 | + |
| 1200 | + // allow cross, cycle only |
| 1201 | + { |
| 1202 | + let mut solver = Solver::new(); |
| 1203 | + let edges = crate::graph::BoolGridEdges::new(&mut solver, (3, 4)); |
| 1204 | + solver.add_answer_key_bool(&edges.horizontal); |
| 1205 | + solver.add_answer_key_bool(&edges.vertical); |
| 1206 | + |
| 1207 | + crossable_single_cycle_grid_edges(&mut solver, &edges); |
| 1208 | + let directed_edges = active_edges_directed_cycle_path(&mut solver, &edges, true, false); |
| 1209 | + solver.add_expr(directed_edges.right.at((0, 0))); |
| 1210 | + solver.add_expr(directed_edges.left.at((0, 2))); |
| 1211 | + solver.add_expr(directed_edges.down.at((2, 0))); |
| 1212 | + |
| 1213 | + let irrefutable_facts = solver.irrefutable_facts(); |
| 1214 | + assert!(irrefutable_facts.is_some()); |
| 1215 | + let irrefutable_facts = irrefutable_facts.unwrap(); |
| 1216 | + assert_eq!( |
| 1217 | + irrefutable_facts.get(&edges.horizontal), |
| 1218 | + vec![ |
| 1219 | + vec![Some(true), Some(false), Some(true), None], |
| 1220 | + vec![Some(true), Some(true), None, None], |
| 1221 | + vec![Some(true), Some(false), None, None], |
| 1222 | + vec![Some(true), Some(true), None, None], |
| 1223 | + ] |
| 1224 | + ); |
| 1225 | + assert_eq!( |
| 1226 | + irrefutable_facts.get(&edges.vertical), |
| 1227 | + vec![ |
| 1228 | + vec![Some(true), Some(true), Some(true), None, None], |
| 1229 | + vec![Some(false), Some(true), None, None, None], |
| 1230 | + vec![Some(true), Some(false), None, None, None], |
| 1231 | + ] |
| 1232 | + ); |
| 1233 | + } |
| 1234 | + |
| 1235 | + // no cross, allow paths |
| 1236 | + { |
| 1237 | + let mut solver = Solver::new(); |
| 1238 | + let edges = crate::graph::BoolGridEdges::new(&mut solver, (3, 4)); |
| 1239 | + solver.add_answer_key_bool(&edges.horizontal); |
| 1240 | + solver.add_answer_key_bool(&edges.vertical); |
| 1241 | + |
| 1242 | + let directed_edges = active_edges_directed_cycle_path(&mut solver, &edges, true, true); |
| 1243 | + solver.add_expr(directed_edges.up.at((0, 1))); |
| 1244 | + solver.add_expr(directed_edges.left.at((3, 2))); |
| 1245 | + solver.add_expr(edges.horizontal.at((0, 1))); |
| 1246 | + solver.add_expr(edges.horizontal.at((1, 1))); |
| 1247 | + solver.add_expr(edges.horizontal.at((1, 2))); |
| 1248 | + solver.add_expr(edges.vertical.at((0, 2))); |
| 1249 | + solver.add_expr(edges.vertical.at((1, 2))); |
| 1250 | + |
| 1251 | + let irrefutable_facts = solver.irrefutable_facts(); |
| 1252 | + assert!(irrefutable_facts.is_some()); |
| 1253 | + let irrefutable_facts = irrefutable_facts.unwrap(); |
| 1254 | + assert_eq!( |
| 1255 | + irrefutable_facts.get(&edges.horizontal), |
| 1256 | + vec![ |
| 1257 | + vec![Some(false), Some(true), Some(false), None], |
| 1258 | + vec![None, Some(true), Some(true), None], |
| 1259 | + vec![None, None, None, None], |
| 1260 | + vec![None, None, Some(true), None], |
| 1261 | + ] |
| 1262 | + ); |
| 1263 | + assert_eq!( |
| 1264 | + irrefutable_facts.get(&edges.vertical), |
| 1265 | + vec![ |
| 1266 | + vec![None, Some(true), Some(true), None, None], |
| 1267 | + vec![None, None, Some(true), None, None], |
| 1268 | + vec![None, None, Some(false), None, None], |
| 1269 | + ] |
| 1270 | + ); |
| 1271 | + } |
| 1272 | + } |
1001 | 1273 | } |
0 commit comments