76 lines
2.4 KiB
TypeScript
76 lines
2.4 KiB
TypeScript
|
// packages/strategies/nondeterministic/src/strategy.ts
|
||
|
|
// RunStrategy adapter for the nondeterministic runner.
|
||
|
|
|
||
|
|
import type {
|
||
|
|
RunStrategy,
|
||
|
|
RunResult,
|
||
|
|
RunOptions,
|
||
|
|
StepFn,
|
||
|
|
StrategyOptions,
|
||
|
|
} from "../../../../src/core/eval/strategy/contract";
|
||
|
|
import {
|
||
|
|
failResult,
|
||
|
|
resolveStrategyOptions,
|
||
|
|
runStatsFromSteps,
|
||
|
|
valueResult,
|
||
|
|
} from "../../../../src/core/eval/strategy/contract";
|
||
|
|
import type { Runtime } from "../../../../src/core/eval/runtime";
|
||
|
|
import type { State } from "../../../../src/core/eval/machine";
|
||
|
|
import { VFalse, type Val } from "../../../../src/core/eval/values";
|
||
|
|
import { runNondet, type NondetOptions, type NondetResult } from "./runner";
|
||
|
|
|
||
|
|
/**
|
||
|
|
* NondeterministicStrategy: fork at amb choice points,
|
||
|
|
* explore with BFS/DFS frontier management.
|
||
|
|
*/
|
||
|
|
export class NondeterministicStrategy implements RunStrategy {
|
||
|
|
readonly name = "nondeterministic";
|
||
|
|
readonly description = "Forking strategy for amb-based nondeterministic evaluation";
|
||
|
|
readonly interceptedOps: readonly string[] = ["amb.op", "amb.fail"];
|
||
|
|
|
||
|
|
async run(
|
||
|
|
runtime: Runtime,
|
||
|
|
initial: State,
|
||
|
|
stepFnOrOptions?: StepFn | StrategyOptions,
|
||
|
|
maybeOptions?: RunOptions,
|
||
|
|
): Promise<RunResult> {
|
||
|
|
const options = resolveStrategyOptions(stepFnOrOptions, maybeOptions);
|
||
|
|
|
||
|
|
// Extract nondet-specific config from options
|
||
|
|
const cfg = (options.strategyConfig ?? {}) as Partial<NondetOptions>;
|
||
|
|
|
||
|
|
const nondetOpts: NondetOptions = {
|
||
|
|
mode: cfg.mode ?? "first",
|
||
|
|
frontier: cfg.frontier ?? "bfs",
|
||
|
|
quantumSteps: cfg.quantumSteps ?? 1000,
|
||
|
|
maxTotalSteps: options.maxSteps ?? cfg.maxTotalSteps ?? 100_000,
|
||
|
|
maxJobs: cfg.maxJobs ?? 10_000,
|
||
|
|
};
|
||
|
|
|
||
|
|
const result = await runNondet(runtime, initial, nondetOpts);
|
||
|
|
|
||
|
|
return nondetResultToRunResult(result, initial, options.maxSteps ?? 0);
|
||
|
|
}
|
||
|
|
}
|
||
|
|
|
||
|
|
function nondetResultToRunResult(nr: NondetResult, state: State, steps: number): RunResult {
|
||
|
|
switch (nr.tag) {
|
||
|
|
case "None":
|
||
|
|
return failResult("nondeterministic search produced no solutions", state, runStatsFromSteps(steps));
|
||
|
|
case "One":
|
||
|
|
return valueResult(
|
||
|
|
nr.value,
|
||
|
|
state,
|
||
|
|
runStatsFromSteps(steps, { solutions: 1 }),
|
||
|
|
{ meta: { nondet: "one", solutions: 1 } },
|
||
|
|
);
|
||
|
|
case "Many":
|
||
|
|
return valueResult(
|
||
|
|
{ tag: "Vector", items: nr.values } as Val,
|
||
|
|
state,
|
||
|
|
runStatsFromSteps(steps, { solutions: nr.values.length }),
|
||
|
|
{ meta: { nondet: "many", solutions: nr.values.length } },
|
||
|
|
);
|
||
|
|
}
|
||
|
|
}
|