removed pathConditionRoot from the states in V#

removing pathConditionRoot from the states

Author: Gitubrr

VSharp.Explorer/AISearcher.fs

@@ -295,16 +295,18 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
 
                         OrtValue.CreateTensorValueFromMemory(attributes, shape)
 
-                    let states, numOfParentOfEdges, numOfHistoryEdges =
+                    let states, numOfParentOfEdges, numOfPathConditionEdges, numOfHistoryEdges =
                         let mutable numOfParentOfEdges = 0
+                        let mutable numOfPathConditionEdges = 0
                         let mutable numOfHistoryEdges = 0
                         let shape = [| int64 gameState.States.Length; numOfStateAttributes |]
                         let attributes = Array.zeroCreate (gameState.States.Length * numOfStateAttributes)
 
                         for i in 0 .. gameState.States.Length - 1 do
                             let v = gameState.States.[i]
-                            numOfHistoryEdges <- numOfHistoryEdges + v.History.Length
                             numOfParentOfEdges <- numOfParentOfEdges + v.Children.Length
+                            numOfPathConditionEdges <- numOfPathConditionEdges + v.PathCondition.Length 
+                            numOfHistoryEdges <- numOfHistoryEdges + v.History.Length
                             stateIds.Add(v.Id, i)
                             let j = i * numOfStateAttributes
                             attributes.[j] <- float32 v.Position
@@ -314,7 +316,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
                             attributes.[j + 4] <- float32 v.StepWhenMovedLastTime
                             attributes.[j + 5] <- float32 v.InstructionsVisitedInCurrentBlock
 
-                        OrtValue.CreateTensorValueFromMemory(attributes, shape), numOfParentOfEdges, numOfHistoryEdges
+                        OrtValue.CreateTensorValueFromMemory(attributes, shape), numOfParentOfEdges, numOfPathConditionEdges, numOfHistoryEdges
 
                     let pcToPcEdgeIndex =
                         let shapeOfIndex = [| 2L; numOfPcToPcEdges |]
@@ -361,8 +363,8 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
                         let parentOf = Array.zeroCreate (2 * numOfParentOfEdges)
                         let shapeOfHistory = [| 2L; numOfHistoryEdges |]
                         let historyIndex_vertexToState = Array.zeroCreate (2 * numOfHistoryEdges)
-                        let shapeOfPcToState = [| 2L; gameState.States.Length |]
-                        let index_pcToState = Array.zeroCreate (2 * gameState.States.Length)
+                        let shapeOfPcToState = [| 2L; numOfPathConditionEdges |]
+                        let index_pcToState = Array.zeroCreate (2 * numOfPathConditionEdges)
 
                         let shapeOfHistoryAttributes =
                             [| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |]
@@ -383,13 +385,13 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
 
                             firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length
 
-                            index_pcToState.[firstFreePositionInPcToState] <-
-                                int64 pathConditionVerticesIds[state.PathCondition.Id]
-
-                            index_pcToState.[firstFreePositionInPcToState + gameState.States.Length] <-
-                                int64 stateIds[state.Id]
-
-                            firstFreePositionInPcToState <- firstFreePositionInPcToState + 1
+                            state.PathCondition
+                            |> Array.iteri (fun i pcId ->
+                                let j = firstFreePositionInPcToState + i
+                                index_pcToState[j] <- int64 pathConditionVerticesIds[pcId]
+                                index_pcToState[numOfPathConditionEdges + j] <- int64 stateIds[state.Id])
+                                
+                            firstFreePositionInPcToState <- firstFreePositionInPcToState + state.PathCondition.Length
 
                             state.History
                             |> Array.iteri (fun i historyElem ->

VSharp.IL/Serializer.fs

@@ -495,20 +495,13 @@ let collectGameState (basicBlocks: ResizeArray<BasicBlock>) filterStates process
                 for term in pathCondition do
                     pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices)
 
-                let pathConditionRoot =
-                    PathConditionVertex(
-                        id = getFirstFreePathConditionVertexId (),
-                        pathConditionVertexType = pathConditionVertexType.PathConditionRoot,
-                        children = [| for p in pathCondition -> termsWithId.[p] |]
-                    )
-
-                pathConditionDelta.Add pathConditionRoot
+                let pathCondition = [| for p in pathCondition -> termsWithId.[p] |]
 
                 State(
                     s.Id,
                     (uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1<byte_offset>)
                     * 1u<byte_offset>,
-                    pathConditionRoot,
+                    pathCondition,
                     s.VisitedAgainVertices,
                     s.VisitedNotCoveredVerticesInZone,
                     s.VisitedNotCoveredVerticesOutOfZone,

VSharp.ML.GameServer/Messages.fs

@@ -72,7 +72,6 @@ type pathConditionVertexType =
     | StandardFunctionApplication = 45
     | Cast = 46
     | Combine = 47
-    | PathConditionRoot = 48
 
 
 [<Struct>]
@@ -153,7 +152,7 @@ type StateHistoryElem =
 type State =
     val Id: uint<stateId>
     val Position: uint<byte_offset> // to basic block id
-    val PathCondition: PathConditionVertex
+    val PathCondition: array<uint<pathConditionVertexId>> 
     val VisitedAgainVertices: uint
     val VisitedNotCoveredVerticesInZone: uint
     val VisitedNotCoveredVerticesOutOfZone: uint