Skip to content

Inlining a foldEdges expression appears to blow up #76

Open
Open
Inlining a foldEdges expression appears to blow up#76
Labels
bugSomething isn't working

Description

@alberdingk-thijm
alberdingk-thijm
opened on Oct 11, 2021

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions