Struct Engine 

pub struct Engine<'p> {
    pub unresolved: Weight,
    pub observed: bool,
    pub densities: bool,
    pub last_ruling_out: Option<Span>,
    pub sinks: Vec<Sink>,
    pub stats: Stats,
    pub failures: Failures,
    /* private fields */
}

Fields

unresolved: Weight

Weight left unaccounted for (loops cut short, truncated tails).

observed: bool

Whether the current inference scope has run observe.

densities: bool

Whether it has observed a value with a density, which makes the evidence a density too (docs/semantics.md, section 14).

last_ruling_out: Option<Span>

The last observation that ruled out a world, for impossible evidence.

sinks: Vec<Sink>

stats: Stats

failures: Failures

In partial mode: the worlds that failed, in the current call.

Implementations

impl<'p> Engine<'p>

pub fn new( prog: &'p Program, live: &'p Liveness, conj: &'p Conjugacy, config: Config, inputs: &'p [Value], print: &'p mut (dyn FnMut(&str) + Send), ) -> Engine<'p>

pub fn run_main(&mut self) -> Result<Weight>

Run the top level. Returns the total weight of the worlds that finish.

pub fn run_batch( &mut self, rng: Rng, first: u64, n: u64, printed: usize, ) -> (Result<Batch>, Printed)

Sample the runs first..first + n with the random numbers rng (docs/semantics.md, section 14), after earlier batches printed printed bytes. A batch starts afresh: its reports and counters are its own, so batches can run on any thread; only caches carry over. What it prints comes back with its result, even when it fails.