Skip to content

Commit 95c09ec

Browse files
committed
removing pc-root from the states
1 parent 47a76a3 commit 95c09ec

File tree

3 files changed

+12
-10
lines changed

3 files changed

+12
-10
lines changed

VSharp.Explorer/AISearcher.fs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -384,7 +384,7 @@ type internal AISearcher(oracle: Oracle, aiAgentTrainingMode: Option<AIAgentTrai
384384
firstFreePositionInParentsOf <- firstFreePositionInParentsOf + state.Children.Length
385385

386386
index_pcToState.[firstFreePositionInPcToState] <-
387-
int64 pathConditionVerticesIds[state.PathCondition.Id]
387+
int64 pathConditionVerticesIds[state.PathCondition.[firstFreePositionInPcToState]]
388388

389389
index_pcToState.[firstFreePositionInPcToState + gameState.States.Length] <-
390390
int64 stateIds[state.Id]

VSharp.IL/Serializer.fs

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

498-
let pathConditionRoot =
499-
PathConditionVertex(
500-
id = getFirstFreePathConditionVertexId (),
501-
pathConditionVertexType = pathConditionVertexType.PathConditionRoot,
502-
children = [| for p in pathCondition -> termsWithId.[p] |]
503-
)
498+
// let pathConditionRoot =
499+
// PathConditionVertex(
500+
// id = getFirstFreePathConditionVertexId (),
501+
// pathConditionVertexType = pathConditionVertexType.PathConditionRoot,
502+
// children = [| for p in pathCondition -> termsWithId.[p] |]
503+
// )
504504

505-
pathConditionDelta.Add pathConditionRoot
505+
// pathConditionDelta.Add pathConditionRoot
506+
507+
let children = [| for p in pathCondition -> termsWithId.[p] |]
506508

507509
State(
508510
s.Id,
509511
(uint <| s.CodeLocation.offset - currentBasicBlock.StartOffset + 1<byte_offset>)
510512
* 1u<byte_offset>,
511-
pathConditionRoot,
513+
children,
512514
s.VisitedAgainVertices,
513515
s.VisitedNotCoveredVerticesInZone,
514516
s.VisitedNotCoveredVerticesOutOfZone,

VSharp.ML.GameServer/Messages.fs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ type StateHistoryElem =
153153
type State =
154154
val Id: uint<stateId>
155155
val Position: uint<byte_offset> // to basic block id
156-
val PathCondition: PathConditionVertex
156+
val PathCondition: uint<pathConditionVertexId> array
157157
val VisitedAgainVertices: uint
158158
val VisitedNotCoveredVerticesInZone: uint
159159
val VisitedNotCoveredVerticesOutOfZone: uint

0 commit comments

Comments
 (0)