Open alberdingk-thijm opened 2 years ago
Given the network below, NV currently appears to get stuck during the second round of inlining, following map unrolling.
(* Benchmark testing fault tolerance reachability to the destination. *) type attribute = bool symbolic failed : set[tedge] let cardinality s = foldEdges (fun e b x -> if b then x + 1 else x) s 0 require ((cardinality failed) <= 2) let dest = 10n let nodes = 20 let edges = { 3-16; (*core-0,Serial0 --> aggregation-8,Serial0*) 13-12; (*aggregation-5,Serial3 --> edge-7,Serial1*) 8-1; (*aggregation-16,Serial1 --> core-1,Serial3*) 6-7; (*aggregation-17,Serial3 --> core-2,Serial1*) 19-16; (*edge-10,Serial0 --> aggregation-8,Serial2*) 14-3; (*aggregation-4,Serial0 --> core-0,Serial2*) 6-4; (*aggregation-17,Serial0 --> core-3,Serial1*) 4-13; (*core-3,Serial2 --> aggregation-5,Serial1*) 9-18; (*edge-14,Serial0 --> aggregation-12,Serial2*) 17-0; (*aggregation-13,Serial3 --> edge-15,Serial1*) 8-2; (*aggregation-16,Serial2 --> edge-18,Serial0*) 3-14; (*core-0,Serial2 --> aggregation-4,Serial0*) 18-3; (*aggregation-12,Serial0 --> core-0,Serial1*) 1-8; (*core-1,Serial3 --> aggregation-16,Serial1*) 7-15; (*core-2,Serial0 --> aggregation-9,Serial3*) 15-5; (*aggregation-9,Serial2 --> edge-11,Serial1*) 18-0; (*aggregation-12,Serial3 --> edge-15,Serial0*) 10-8; (*edge-19,Serial0 --> aggregation-16,Serial3*) 5-16; (*edge-11,Serial0 --> aggregation-8,Serial3*) 6-2; (*aggregation-17,Serial1 --> edge-18,Serial1*) 7-17; (*core-2,Serial3 --> aggregation-13,Serial0*) 15-4; (*aggregation-9,Serial0 --> core-3,Serial0*) 0-18; (*edge-15,Serial0 --> aggregation-12,Serial3*) 7-6; (*core-2,Serial1 --> aggregation-17,Serial3*) 16-5; (*aggregation-8,Serial3 --> edge-11,Serial0*) 13-7; (*aggregation-5,Serial0 --> core-2,Serial2*) 16-19; (*aggregation-8,Serial2 --> edge-10,Serial0*) 14-11; (*aggregation-4,Serial2 --> edge-6,Serial0*) 11-13; (*edge-6,Serial1 --> aggregation-5,Serial2*) 3-18; (*core-0,Serial1 --> aggregation-12,Serial0*) 9-17; (*edge-14,Serial1 --> aggregation-13,Serial2*) 6-10; (*aggregation-17,Serial2 --> edge-19,Serial1*) 13-4; (*aggregation-5,Serial1 --> core-3,Serial2*) 2-6; (*edge-18,Serial1 --> aggregation-17,Serial1*) 18-1; (*aggregation-12,Serial1 --> core-1,Serial1*) 15-19; (*aggregation-9,Serial1 --> edge-10,Serial1*) 1-14; (*core-1,Serial2 --> aggregation-4,Serial1*) 2-8; (*edge-18,Serial0 --> aggregation-16,Serial2*) 8-3; (*aggregation-16,Serial0 --> core-0,Serial3*) 17-4; (*aggregation-13,Serial1 --> core-3,Serial3*) 18-9; (*aggregation-12,Serial2 --> edge-14,Serial0*) 0-17; (*edge-15,Serial1 --> aggregation-13,Serial3*) 7-13; (*core-2,Serial2 --> aggregation-5,Serial0*) 4-17; (*core-3,Serial3 --> aggregation-13,Serial1*) 14-1; (*aggregation-4,Serial1 --> core-1,Serial2*) 8-10; (*aggregation-16,Serial3 --> edge-19,Serial0*) 10-6; (*edge-19,Serial1 --> aggregation-17,Serial2*) 1-18; (*core-1,Serial1 --> aggregation-12,Serial1*) 15-7; (*aggregation-9,Serial3 --> core-2,Serial0*) 11-14; (*edge-6,Serial0 --> aggregation-4,Serial2*) 12-13; (*edge-7,Serial1 --> aggregation-5,Serial3*) 17-7; (*aggregation-13,Serial0 --> core-2,Serial3*) 3-8; (*core-0,Serial3 --> aggregation-16,Serial0*) 17-9; (*aggregation-13,Serial2 --> edge-14,Serial1*) 13-11; (*aggregation-5,Serial2 --> edge-6,Serial1*) 16-1; (*aggregation-8,Serial1 --> core-1,Serial0*) 16-3; (*aggregation-8,Serial0 --> core-0,Serial0*) 4-15; (*core-3,Serial0 --> aggregation-9,Serial0*) 19-15; (*edge-10,Serial1 --> aggregation-9,Serial1*) 12-14; (*edge-7,Serial0 --> aggregation-4,Serial3*) 14-12; (*aggregation-4,Serial3 --> edge-7,Serial0*) 1-16; (*core-1,Serial0 --> aggregation-8,Serial1*) 4-6; (*core-3,Serial1 --> aggregation-17,Serial0*) 5-15; (*edge-11,Serial1 --> aggregation-9,Serial2*) } let init n = if n = dest then true else false let trans e x = if failed[e] then false else x let merge n x y = x || y let assert_node node x = x (* {edge-15=0, core-1=1, edge-18=2, core-0=3, core-3=4, edge-11=5, aggregation-17=6, core-2=7, aggregation-16=8, edge-14=9, edge-19=10, edge-6=11, edge-7=12, aggregation-5=13, aggregation-4=14, aggregation-9=15, aggregation-8=16, aggregation-13=17, aggregation-12=18, edge-10=19}*) let sol = solution {init = init; trans = trans; merge = merge} assert foldNodes (fun k v acc -> acc && assert_node k v) sol true
Inlining starts on the following expression:
require ((match failed~161 with | (UnrollingFoldVar~198,UnrollingFoldVar~199,UnrollingFoldVar~200,UnrollingFoldVar~201,UnrollingFoldVar~202,UnrollingFoldVar~203,UnrollingFoldVar~204,UnrollingFoldVar~205,UnrollingFoldVar~206,UnrollingFoldVar~207,UnrollingFoldVar~208,UnrollingFoldVar~209,UnrollingFoldVar~210,UnrollingFoldVar~211,UnrollingFoldVar~212,UnrollingFoldVar~213,UnrollingFoldVar~214,UnrollingFoldVar~215,UnrollingFoldVar~216,UnrollingFoldVar~217,UnrollingFoldVar~218,UnrollingFoldVar~219,UnrollingFoldVar~220,UnrollingFoldVar~221,UnrollingFoldVar~222,UnrollingFoldVar~223,UnrollingFoldVar~224,UnrollingFoldVar~225,UnrollingFoldVar~226,UnrollingFoldVar~227,UnrollingFoldVar~228,UnrollingFoldVar~229,UnrollingFoldVar~230,UnrollingFoldVar~231,UnrollingFoldVar~232,UnrollingFoldVar~233,UnrollingFoldVar~234,UnrollingFoldVar~235,UnrollingFoldVar~236,UnrollingFoldVar~237,UnrollingFoldVar~238,UnrollingFoldVar~239,UnrollingFoldVar~240,UnrollingFoldVar~241,UnrollingFoldVar~242,UnrollingFoldVar~243,UnrollingFoldVar~244,UnrollingFoldVar~245,UnrollingFoldVar~246,UnrollingFoldVar~247,UnrollingFoldVar~248,UnrollingFoldVar~249,UnrollingFoldVar~250,UnrollingFoldVar~251,UnrollingFoldVar~252,UnrollingFoldVar~253,UnrollingFoldVar~254,UnrollingFoldVar~255,UnrollingFoldVar~256,UnrollingFoldVar~257,UnrollingFoldVar~258,UnrollingFoldVar~259,UnrollingFoldVar~260,UnrollingFoldVar~261) -> (((((fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) )) 19~16 ) UnrollingFoldVar~261 ) (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 19~15 UnrollingFoldVar~260 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 18~9 UnrollingFoldVar~259 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 18~3 UnrollingFoldVar~258 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 18~1 UnrollingFoldVar~257 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 18~0 UnrollingFoldVar~256 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 17~9 UnrollingFoldVar~255 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 17~7 UnrollingFoldVar~254 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 17~4 UnrollingFoldVar~253 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 17~0 UnrollingFoldVar~252 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 16~19 UnrollingFoldVar~251 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 16~5 UnrollingFoldVar~250 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 16~3 UnrollingFoldVar~249 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 16~1 UnrollingFoldVar~248 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 15~19 UnrollingFoldVar~247 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 15~7 UnrollingFoldVar~246 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 15~5 UnrollingFoldVar~245 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 15~4 UnrollingFoldVar~244 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 14~12 UnrollingFoldVar~243 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 14~11 UnrollingFoldVar~242 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 14~3 UnrollingFoldVar~241 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 14~1 UnrollingFoldVar~240 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 13~12 UnrollingFoldVar~239 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 13~11 UnrollingFoldVar~238 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 13~7 UnrollingFoldVar~237 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 13~4 UnrollingFoldVar~236 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 12~14 UnrollingFoldVar~235 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 12~13 UnrollingFoldVar~234 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 11~14 UnrollingFoldVar~233 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 11~13 UnrollingFoldVar~232 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 10~8 UnrollingFoldVar~231 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 10~6 UnrollingFoldVar~230 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 9~18 UnrollingFoldVar~229 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 9~17 UnrollingFoldVar~228 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 8~10 UnrollingFoldVar~227 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 8~3 UnrollingFoldVar~226 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 8~2 UnrollingFoldVar~225 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 8~1 UnrollingFoldVar~224 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 7~17 UnrollingFoldVar~223 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 7~15 UnrollingFoldVar~222 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 7~13 UnrollingFoldVar~221 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 7~6 UnrollingFoldVar~220 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 6~10 UnrollingFoldVar~219 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 6~7 UnrollingFoldVar~218 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 6~4 UnrollingFoldVar~217 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 6~2 UnrollingFoldVar~216 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 5~16 UnrollingFoldVar~215 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 5~15 UnrollingFoldVar~214 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 4~17 UnrollingFoldVar~213 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 4~15 UnrollingFoldVar~212 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 4~13 UnrollingFoldVar~211 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 4~6 UnrollingFoldVar~210 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 3~18 UnrollingFoldVar~209 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 3~16 UnrollingFoldVar~208 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 3~14 UnrollingFoldVar~207 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 3~8 UnrollingFoldVar~206 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 2~8 UnrollingFoldVar~205 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 2~6 UnrollingFoldVar~204 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 1~18 UnrollingFoldVar~203 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 1~16 UnrollingFoldVar~202 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 1~14 UnrollingFoldVar~201 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 1~8 UnrollingFoldVar~200 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 0~18 UnrollingFoldVar~199 (fun e~173 -> (fun b~174 -> (fun x~175 -> if b~174 then x~175 +u32 1u32 else x~175 ) ) ) 0~17 UnrollingFoldVar~198 0u32 ) )) <=u32 2u32
but then does not appear to ever finish.
Given the network below, NV currently appears to get stuck during the second round of inlining, following map unrolling.
Inlining starts on the following expression:
but then does not appear to ever finish.