Skip to content

Commit 5d0edb0

Browse files
committed
made egjes between states and pc
1 parent c5482cb commit 5d0edb0

File tree

3 files changed

+14
-15
lines changed

3 files changed

+14
-15
lines changed

VSharp.Explorer/AISearcher.fs

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -361,8 +361,12 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
361361
let parentOf = Array.zeroCreate (2 * numOfParentOfEdges)
362362
let shapeOfHistory = [| 2L; numOfHistoryEdges |]
363363
let historyIndex_vertexToState = Array.zeroCreate (2 * numOfHistoryEdges)
364-
let shapeOfPcToState = [| 2L; gameState.States.Length |]
365-
let index_pcToState = Array.zeroCreate (2 * gameState.States.Length)
364+
365+
let pathConditionNum =
366+
gameState.States
367+
|> Array.sumBy(fun s -> s.PathCondition.Length)
368+
let shapeOfPcToState = [| 2L; pathConditionNum |]
369+
let index_pcToState = Array.zeroCreate (2 * pathConditionNum)
366370

367371
let shapeOfHistoryAttributes =
368372
[| int64 numOfHistoryEdges; int64 numOfHistoryEdgeAttributes |]
@@ -381,15 +385,11 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
381385
parentOf[j] <- int64 stateIds[state.Id]
382386
parentOf[numOfParentOfEdges + j] <- int64 stateIds[children])
383387

384-
firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length
385-
386-
index_pcToState.[firstFreePositionInPcToState] <-
387-
int64 pathConditionVerticesIds[state.PathCondition.[firstFreePositionInPcToState]]
388-
389-
index_pcToState.[firstFreePositionInPcToState + gameState.States.Length] <-
390-
int64 stateIds[state.Id]
391-
392-
firstFreePositionInPcToState <- firstFreePositionInPcToState + 1
388+
state.PathCondition
389+
|> Array.iteri (fun i pcId ->
390+
let j = firstFreePositionInPcToState + i
391+
index_pcToState[j] <- int64 pathConditionVerticesIds[pcId]
392+
index_pcToState[numOfParentOfEdges + j] <- int64 stateIds[state.Id])
393393

394394
state.History
395395
|> Array.iteri (fun i historyElem ->

VSharp.IL/Serializer.fs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -495,13 +495,13 @@ let collectGameState (basicBlocks: ResizeArray<BasicBlock>) filterStates process
495495
for term in pathCondition do
496496
pathConditionDelta.AddRange(collectPathCondition term termsWithId processedPathConditionVertices)
497497

498-
let children = [| for p in pathCondition -> termsWithId.[p] |]
498+
let pathConditionId = [| for p in pathCondition -> termsWithId.[p] |]
499499

500500
State(
501501
s.Id,
502502
(uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1<byte_offset>)
503503
* 1u<byte_offset>,
504-
children,
504+
pathConditionId,
505505
s.VisitedAgainVertices,
506506
s.VisitedNotCoveredVerticesInZone,
507507
s.VisitedNotCoveredVerticesOutOfZone,

VSharp.ML.GameServer/Messages.fs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,6 @@ type pathConditionVertexType =
7272
| StandardFunctionApplication = 45
7373
| Cast = 46
7474
| Combine = 47
75-
| PathConditionRoot = 48
7675

7776

7877
[<Struct>]
@@ -153,7 +152,7 @@ type StateHistoryElem =
153152
type State =
154153
val Id: uint<stateId>
155154
val Position: uint<byte_offset> // to basic block id
156-
val PathCondition: uint<pathConditionVertexId> array
155+
val PathCondition: array<uint<pathConditionVertexId>>
157156
val VisitedAgainVertices: uint
158157
val VisitedNotCoveredVerticesInZone: uint
159158
val VisitedNotCoveredVerticesOutOfZone: uint

0 commit comments

Comments
 (0)