Skip to content

Commit b457812

Browse files
committed
✨ Report reference number instructions
1 parent bebb49f commit b457812

File tree

2 files changed

+8
-2
lines changed

2 files changed

+8
-2
lines changed

src/Grisette/Lib/Synth/Reasoning/Parallel/Scheduler/Config.hs

+2-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,8 @@ data
7474
doDeadCodeElimination :: Bool,
7575
schedulerRandomSeed :: Int,
7676
pollIntervalSeconds :: Double,
77-
biasedDrawProbability :: Double
77+
biasedDrawProbability :: Double,
78+
referenceNumInsts :: Maybe Int
7879
} ->
7980
SchedulerConfig
8081
sketchSpec

src/Grisette/Lib/Synth/Reasoning/Parallel/Scheduler/Result.hs

+6-1
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ import Grisette.Lib.Synth.Reasoning.Parallel.Scheduler.Config
5757
logger,
5858
parallelism,
5959
pollIntervalSeconds,
60+
referenceNumInsts,
6061
restartRunningTimeThresholdSeconds,
6162
schedulerRandomSeed,
6263
schedulerTimeoutSeconds,
@@ -387,7 +388,8 @@ printResults Scheduler {config = SchedulerConfig {..}, ..} result = do
387388
"Num of root programs: " <> pformat numOfRootPrograms,
388389
"Num of components: " <> pformat numOfComponents,
389390
"Undetermined ratio: " <> pformat undeterminedRatio,
390-
"Avg component choices: " <> pformat avgCompChoices
391+
"Avg component choices: " <> pformat avgCompChoices,
392+
"Number of instructions in reference: " <> maybe "inf" pformat referenceNumInsts
391393
]
392394
SolutionFound ParallelSynthesisSolutionFoundResult {..} -> do
393395
let elapsedTime =
@@ -405,6 +407,7 @@ printResults Scheduler {config = SchedulerConfig {..}, ..} result = do
405407
"Undetermined ratio: " <> pformat undeterminedRatio,
406408
"Avg component choices: " <> pformat avgCompChoices,
407409
"Min number of instructions: " <> pformat minNumInsts,
410+
"Number of instructions in reference: " <> maybe "inf" pformat referenceNumInsts,
408411
"Best solution found with cost "
409412
<> pformat bestCost
410413
<> " in "
@@ -463,6 +466,7 @@ writeResultsCSV path result scheduler = do
463466
"time_to_best_since_scheduler_start",
464467
"time_to_best",
465468
"min_num_instructions",
469+
"num_ref_instructions",
466470
"initial_cost",
467471
"cost",
468472
"num_lattice_nodes",
@@ -514,6 +518,7 @@ writeResultsCSV path result scheduler = do
514518
maybe "inf" show timeToBestSinceSchedulerStart,
515519
maybe "inf" show timeToBest,
516520
minNumInstructions,
521+
maybe "inf" show (referenceNumInsts (config scheduler)),
517522
show initialCost,
518523
show cost,
519524
show numOfNodesInLattice,

0 commit comments

Comments
 (0)