@@ -369,26 +369,26 @@ let collectPathCondition
369369 let termsToVisit = Stack< Core.term> [| term |]
370370 let pathConditionDelta = ResizeArray< PathConditionVertex>()
371371
372+ let getIdForTerm term =
373+ if termsWithId.ContainsKey term then
374+ termsWithId.[ term]
375+ else
376+ let newId = getFirstFreePathConditionVertexId ()
377+ termsWithId.Add( term, newId)
378+ newId
379+
380+ let handleChild term ( children : ResizeArray < _ >) =
381+ children.Add( getIdForTerm term)
382+ termsToVisit.Push term
383+
372384 while termsToVisit.Count > 0 do
373385 let currentTerm = termsToVisit.Pop()
374386
375- let getIdForTerm term =
376- if termsWithId.ContainsKey term then
377- termsWithId.[ term]
378- else
379- let newId = getFirstFreePathConditionVertexId ()
380- termsWithId.Add( term, newId)
381- newId
382-
383387 let markAsVisited ( vertexType : pathConditionVertexType ) children =
384388 let newVertex = PathConditionVertex( getIdForTerm currentTerm, vertexType, children)
385389 processedPathConditionVertices.Add currentTerm |> ignore
386390 pathConditionDelta.Add newVertex
387391
388- let handleTerm term ( children : ResizeArray < _ >) =
389- children.Add( getIdForTerm term)
390- termsToVisit.Push term
391-
392392 if not <| processedPathConditionVertices.Contains currentTerm then
393393 match currentTerm.term with
394394 | Nop -> markAsVisited pathConditionVertexType.Nop [||]
@@ -398,7 +398,7 @@ let collectPathCondition
398398 let children = ResizeArray< uint< pathConditionVertexId>>()
399399
400400 for t in termList do
401- handleTerm t children
401+ handleChild t children
402402
403403 let children = children.ToArray()
404404
@@ -450,23 +450,23 @@ let collectPathCondition
450450 let children = ResizeArray< uint< pathConditionVertexId>>()
451451
452452 for _, t in PersistentDict.toSeq fields do
453- handleTerm t children
453+ handleChild t children
454454
455455 markAsVisited pathConditionVertexType.Struct ( children.ToArray())
456456 | HeapRef(_, _) -> markAsVisited pathConditionVertexType.HeapRef [||]
457457 | Ref(_) -> markAsVisited pathConditionVertexType.Ref [||]
458458 | Ptr(_, _, t) ->
459459 let children = ResizeArray< uint< pathConditionVertexId>> [||]
460- handleTerm t children
460+ handleChild t children
461461 markAsVisited pathConditionVertexType.Ptr ( children.ToArray())
462462 | Slice( t, listOfTuples) ->
463463 let children = ResizeArray< uint< pathConditionVertexId>> [||]
464- handleTerm t children
464+ handleChild t children
465465
466466 for t1, t2, t3, _ in listOfTuples do
467- handleTerm t1 children
468- handleTerm t2 children
469- handleTerm t3 children
467+ handleChild t1 children
468+ handleChild t2 children
469+ handleChild t3 children
470470
471471 markAsVisited pathConditionVertexType.Slice ( children.ToArray())
472472 | Ite(_) -> markAsVisited pathConditionVertexType.Ite [||]
@@ -574,11 +574,7 @@ let dumpGameState fileForResultWithoutExtension (movedStateId: uint<stateId>) =
574574 basicBlocks.Add( basicBlock)
575575
576576 let gameState =
577- collectGameState
578- basicBlocks
579- true
580- ( HashSet< Core.term>())
581- ( Dictionary< Core.term, uint< pathConditionVertexId>>())
577+ collectGameState basicBlocks true ( HashSet< Core.term>()) ( Dictionary< Core.term, uint< pathConditionVertexId>>())
582578
583579 let statesInfoToDump = collectStatesInfoToDump basicBlocks
584580 let gameStateJson = JsonSerializer.Serialize gameState
0 commit comments